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