Ir al contenido principal

Reducción de SAT a Clique

Nota: En este ejercicio se usa la misma notación que en los anteriores importando los módulos

  • Evaluacion_de_FNC
  • Modelos_de_FNC
  • Problema_SAT_para_FNC
  • Cliques
  • KCliques
  • Grafo_FNC

Definir las funciones

cliquesFNC :: FNC -> [[(Int,Literal)]]
cliquesCompletos :: FNC -> [[(Int,Literal)]]
esSatisfaciblePorClique :: FNC -> Bool

tales que

  • (cliquesFNCf) es la lista de los cliques del grafo de f. Por ejemplo,
λ> cliquesFNC [[1,-2,3],[-1,2],[-2,3]]
[[], [(0,1)], [(1,2)], [(0,1),(1,2)], [(2,-2)],
 [(0,1),(2,-2)], [(2,3)], [(0,1),(2,3)], [(1,2),(2,3)],
 [(0,1),(1,2),(2,3)], [(0,-2)], [(2,-2),(0,-2)], [(2,3),(0,-2)],
 [(1,-1)], [(2,-2),(1,-1)], [(2,3),(1,-1)], [(0,-2),(1,-1)],
 [(2,-2),(0,-2),(1,-1)], [(2,3),(0,-2),(1,-1)], [(0,3)],
 [(1,2),(0,3)], [(2,-2),(0,3)], [(2,3),(0,3)],
 [(1,2),(2,3),(0,3)], [(1,-1),(0,3)],
 [(2,-2),(1,-1),(0,3)], [(2,3),(1,-1),(0,3)]]
  • (cliquesCompletos f) es la lista de los cliques del grafo de f que tiene tantos elementos como cláusulas tiene f. Por ejemplo,
λ> cliquesCompletos [[1,-2,3],[-1,2],[-2,3]]
[[(0,1),(1,2),(2,3)],   [(2,-2),(0,-2),(1,-1)],
 [(2,3),(0,-2),(1,-1)], [(1,2),(2,3),(0,3)],
 [(2,-2),(1,-1),(0,3)], [(2,3),(1,-1),(0,3)]]
λ> cliquesCompletos [[1,2],[1,-2],[-1,2],[-1,-2]]
[]
  • (esSatisfaciblePorClique f) se verifica si f no contiene la cláusula vacía, tiene más de una cláusula y posee algún clique completo. Por ejemplo,
λ> esSatisfaciblePorClique [[1,-2,3],[-1,2],[-2,3]]
True
λ> esSatisfaciblePorClique [[1,2],[1,-2],[-1,2],[-1,-2]]
False

Comprobar con QuickCheck que toda fórmula en FNC es satisfacible si, y solo si, es satisfacible por Clique.

Soluciones

module Reduccion_de_SAT_a_Clique where

import Evaluacion_de_FNC
import Modelos_de_FNC
import Problema_SAT_para_FNC
import Cliques
import KCliques
import Grafo_FNC
import Data.List (nub, sort)
import Test.QuickCheck

cliquesFNC :: FNC -> [[(Int,Literal)]]
cliquesFNC f = cliques (grafoFNC f)

cliquesCompletos :: FNC -> [[(Int,Literal)]]
cliquesCompletos cs = kCliques (grafoFNC cs) (length cs)

esSatisfaciblePorClique :: FNC -> Bool
esSatisfaciblePorClique f =
     [] `notElem` f'
  && (length f' <= 1 || not (null (cliquesCompletos f')))
  where f' = nub (map (nub . sort) f)

-- La propiedad es
prop_esSatisfaciblePorClique :: FNC -> Bool
prop_esSatisfaciblePorClique f =
  esSatisfacible f == esSatisfaciblePorClique f

-- La comprobación es
--    λ> quickCheckWith (stdArgs {maxSize=7}) prop_esSatisfaciblePorClique
--    +++ OK, passed 100 tests.