Menu Close

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

   [(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]

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.”

George Pólya.

Medio

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

  1. fercarnav
     
    import Evaluacion_de_FNC 
    import Grafo
     
    nodosFNC :: FNC -> [(Int,Literal)]
    nodosFNC xss = nodosFNCaux xss 0
     
    nodosFNCaux :: FNC -> Int -> [(Int,Literal)]
    nodosFNCaux [] _ = []
    nodosFNCaux (xs:xss) n  =  map (formaPareja n) xs ++ nodosFNCaux xss (n+1)
     
    formaPareja :: a -> a -> (a,a)
    formaPareja a b = (a,b)
     
    grafoFNC :: FNC -> Grafo (Int,Literal)
    grafoFNC xss = grafoFNCaux (nodosFNC xss)
     
    grafoFNCaux ::  [(Int,Literal)] -> Grafo (Int,Literal)
    grafoFNCaux [] = []
    grafoFNCaux (y:ys) = [formaPareja y z | z<- ys , fst z /= fst y, snd z /= -snd y ]++grafoFNCaux ys
  2. anthormol
    import Evaluacion_de_FNC
    import Grafo
     
    nodosFNC :: FNC -> [(Int,Literal)]
    nodosFNC f = concat [zip (repeat x) ys | (x, ys) <- zip [0..] f]
     
    grafoFNC :: FNC -> Grafo (Int,Literal)
    grafoFNC f = concat [aux n (dropWhile (/=n) (x:y:xs)) | n <- nodosFNC f]
          where x:y:xs = nodosFNC f
                aux n [] = []
                aux n (y:xs) | fst n == fst y = aux n xs
                             | snd n == - snd y = aux n xs
                             | otherwise = (n,y) : aux n xs
  3. juabaerui
    import Evaluacion_de_FNC
    import Grafo
     
    nodosFNC :: FNC -> [(Int,Literal)]
    nodosFNC f = concat [[(r,x) | x <- k]| (r,k) <- zip [0..] f]
     
    grafoFNC :: FNC -> Grafo (Int,Literal)
    grafoFNC f = grafoFNC' (nodosFNC f)
     
    grafoFNC' :: [(Int,Literal)] -> Grafo (Int,Literal)
    grafoFNC' [] = []
    grafoFNC' (x:xs) = [(x,y) | y <- xs, fst x /= fst y, snd x /= (- snd y)] ++ grafoFNC' xs

Escribe tu solución

Este sitio usa Akismet para reducir el spam. Aprende cómo se procesan los datos de tus comentarios.