Grafo de una FNC (fórmula en forma normal conjuntiva)

José A. Alonso

26-02-2020

Para reducir el problema del clique a SAT se comienza asociando a cada fórmula F en FNC un grafo G de forma que F es saisfacible si, y sólo si, G tiene un clique con tantos nodos como cláusulas tiene F.

Los nodos del grafo de F son los literales de las cláusulas de F junto con el número de la cláusula. Por ejemplo, la lista de nodos de la FNC [[1,-2,3],[-1,2],[-2,3]] es

[(0,1),(0,-2),(0,3),
 (1,-1),(1,2),
 (2,-2),(2,3)]

En el grafo de F, hay un arco entre dos nodos si, y solo si, corresponden a cláusulas distintas y sus literales no son complementarios. Por ejemplo,

hay un arco entre (0,1) y (1,2) [porque son de cláusulas distintas (0 y 1) y sus literales (1 y 2) no son complementarios.
no hay un arco entre (0,1) y (1,-1) [porque sus literales (1 y -1) no son complementarios.
no hay un arco entre (0,1) y (0,3) [porque son de la misma cláusula (la 0)].

Nota: En este ejercicio se usará los conceptos de los anteriores importando los módulos Evaluacion_de_FNC y Grafo.

Definir las funciones

nodosFNC :: FNC -> [(Int,Literal)]
grafoFNC :: FNC -> Grafo (Int,Literal)

tales que

(nodosFNC f) es la lista de los nodos del grafo de f. Por ejemplo,

λ> nodosFNC [[1,-2,3],[-1,2],[-2,3]]
[(0,1),(0,-2),(0,3),(1,-1),(1,2),(2,-2),(2,3)]

(grafo FNC f) es el grafo de f. Por ejemplo,

λ> grafoFNC [[1,-2,3],[-1,2],[-2,3]]
[ ((0,1),(1,2)),  ((0,1),(2,-2)), ((0,1),(2,3)),
  ((0,-2),(1,-1)),((0,-2),(2,-2)),((0,-2),(2,3)),
  ((0,3),(1,-1)), ((0,3),(1,2)),  ((0,3),(2,-2)),((0,3),(2,3)),
  ((1,-1),(2,-2)),((1,-1),(2,3)),
  ((1,2),(2,3))]
λ> grafoFNC [[1,2],[1,-2],[-1,2],[-1,-2]]
[((0,1),(1,1)),((0,1),(1,-2)),((0,1),(2,2)),((0,1),(3,-2)),
 ((0,2),(1,1)),((0,2),(2,-1)),((0,2),(2,2)),((0,2),(3,-1)),
 ((1,1),(2,2)),((1,1),(3,-2)),
 ((1,-2),(2,-1)),((1,-2),(3,-1)),((1,-2),(3,-2)),
 ((2,-1),(3,-1)),((2,-1),(3,-2)),
 ((2,2),(3,-1))]

Soluciones

module Grafo_FNC where

import Evaluacion_de_FNC
import Grafo
import Data.List (tails)

nodosFNC :: FNC -> [(Int,Literal)]
nodosFNC f =
  [(i,x) | (i,xs) <- zip [0..] f
         , x <- xs]

grafoFNC :: FNC -> Grafo (Int,Literal)
grafoFNC f =
  [ ((i,x),(i',x'))
  | ((i,x),(i',x')) <- parejas (nodosFNC f)
  , i' /= i
  , x' /= negate x]

-- (parejas xs) es la lista de las parejas formados por los elementos de
-- xs y sus siguientes en xs. Por ejemplo,
--    parejas [1..4] == [(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)]
parejas :: [a] -> [(a,a)]
parejas xs =
  [(x,y) | (x:ys) <- tails xs
         , y <- ys]