Ver el código de «Reducción de SAT a Clique en Haskell»

<source lang="haskell">
-- SAT_Clique.hs
-- Reducción de SAT a Clique.
-- José A. Alonso Jiménez
-- Sevilla, 6 de febrero de 2020
-- ---------------------------------------------------------------------

module SAT_Clique where

import SAT
import Cliques
import Data.List
import Test.QuickCheck

-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    nodosFNC :: FNC -> [(Int,Literal)]
-- tal que (nodosFNC f) es la lista de los literales de las cláuslas de
-- f junto con el número de la cláusula. Por ejemplo,
--    λ> nodosFNC [[1,-2,3],[-1,2],[-2,3]]
--    [(0,1),(0,-2),(0,3),(1,-1),(1,2),(2,-2),(2,3)]
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Ejercicio. El grafo correspondiente a una fórmula f en FNC tiene como
-- nodos (nodosFNC f). Hay un arco entre los nodos correspondientes a
-- cláusulas distintas cuyos literales no son complementarios. Por
-- ejemplo, 
-- 
-- Definir la función
--    grafoFNC :: FNC -> Grafo (Int,Literal)
-- tal que (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))]
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    cliquesFNC :: FNC -> [[(Int,Literal)]]
-- tal 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)]]
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    cliquesCompletos :: FNC -> [[(Int,Literal)]]
-- tal que (cliquesCompletos f) es la lista de los cliques del grafo de
-- f que tiene elmismo número de elementos que el número de cláusulas de
-- 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]]
--    []
-- ---------------------------------------------------------------------

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

-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    esSatisfaciblePorClique :: FNC -> Bool
-- tal que (esSatisfaciblePorClique f) se verifica si f no contiene la
-- cláusula vacía, tiene má 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
-- ---------------------------------------------------------------------

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

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

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.

-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    modelosCliqueFNC :: FNC -> [Interpretacion]
-- tales que (modelosCliqueFNC f) es la lista de los modelos de f
-- calculados mediante los cliques completos del grafo de f. Por ejemplo,
--    λ> modelosCliqueFNC [[1,-2,3],[-1,2],[-2,3]]
--    [[],[1,2,3],[2,3],[3]]
--    λ> modelosCliqueFNC [[1,-2,3],[3,2],[-2,3]]
--    [[1,2,3],[1,3],[2,3],[3]]
-- ---------------------------------------------------------------------

modelosCliqueFNC :: FNC -> [Interpretacion]
modelosCliqueFNC f 
  | [] `elem` f'   = []
  | length f' == 1 = [[a | c <- f', a <- c, a > 0]]
  |otherwise       = sort (nub (map nub [ modeloClique xs
                                        | xs <- cliquesCompletos f]))
  where f' = nub (map (nub . sort) f) 
        modeloClique xs = [x | (_,x) <- xs, x > 0]

-- ---------------------------------------------------------------------
-- Ejercicio. Comprobar con QuickCheck que, para toda fórmula f en FNC,
-- todos los elementos de (modelosCliqueFNC f) son modelos de f.
-- ---------------------------------------------------------------------

prop_modelosPorClique :: FNC -> Bool
prop_modelosPorClique f =
  and [esModelo i f | i <- modelosCliqueFNC f]

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