Grafo de una FNC (fórmula en forma normal conjuntiva)
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
|
1 2 3 |
[(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
|
1 2 |
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,
|
1 2 |
λ> 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,
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
λ> 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
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 |
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] |
Otras soluciones
- Se pueden escribir otras soluciones en los comentarios.
- El código se debe escribir entre una línea con <pre lang=»haskell»> y otra con </pre>
Pensamiento
«Las matemáticas tienen dos caras: son la ciencia rigurosa de Euclides, pero también son algo más. La matemática presentada a la manera euclidiana aparece como una ciencia sistemática y deductiva; pero la matemática en ciernes aparece como una ciencia experimental e inductiva. Ambos aspectos son tan antiguos como la propia ciencia de las matemáticas.»