Menu Close

RA2019: Reducción de SAT a Clique en Haskell

En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado una implementación de la reducción del problema SAT al problema Clique.

En primer lugar se ha estudiado una implementación del problema del Clique en la que se ha definido los grafos no ordenados (como pares de nodos), los cliques y cómo calcular los clique de un tamaño dado.

A continuación se ha estudiado cómo asociar a una fórmula en forma normal conjuntiva un grafo tal que la fórmula es satisfacible si, y sólo si, el grafo tiene un clique cuyo tamaño sea el número de cláusulas de la fórmula

Los códigos usados en la presentación son los siguientes:

Código del prolblema del Clique

-- Cliques.hs
-- El problema del clique.
-- José A. Alonso Jiménez
-- Sevilla, 6 de febrero de 2020
-- ---------------------------------------------------------------------
 
module Cliques where
 
import Data.List
 
-- ---------------------------------------------------------------------
-- Un grafo no dirigido se representa por la lista de sus arcos. Por
-- ejemplo, el grafo
--              1  -- 2 -- 4
--                    | \  |
--                    |  \ |
--                    3 -- 5
-- se representa por [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)].
 
--
-- Definir el tipo Grafo.
-- ---------------------------------------------------------------------
 
type Grafo a = [(a,a)]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    nodos :: Eq a => Grafo a -> [a]
-- tal que (nodos g) es la lista de los nodos del grafo g. Por ejemplo,
--    nodos [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)]  ==  [1,2,3,4,5]
-- ---------------------------------------------------------------------
 
nodos :: Eq a => Grafo a -> [a]
nodos g = nub (concat [[x,y] | (x,y) <- g])
 
-- ---------------------------------------------------------------------
-- Ejercicio: Definir la función
--    conectados :: Eq a => Grafo a -> a -> a -> Bool
-- tal que (conectados g x y) se verifica si el grafo no dirigido g
-- posee un arco con extremos x e y. Por ejemplo,
--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3 2  ==  True
--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 2 3  ==  True
--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3 4  ==  False
-- ---------------------------------------------------------------------
 
conectados :: Eq a => Grafo a -> a -> a -> Bool
conectados g x y =
  (x,y) `elem` g || (y,x) `elem` g 
 
-- ---------------------------------------------------------------------
-- Ejercicio: Definir la función
--    parejas :: [a] -> [(a,a)]
-- tal que (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]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Un clique (en español, pandilla) de un grafo g es un
-- conjunto de nodos de g tal que todos sus elementos están conectados
-- en g.
--
-- Definir la función
--    esClique :: Eq a => Grafo a -> [a] -> Bool
-- tal que (esClique g xs) se verifica si el conjunto de nodos xs del
-- grafo g es un clique de g.Por ejemplo,
--    esClique [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] [2,3,5]  ==  True
--    esClique [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] [2,3,4]  ==  False
-- ---------------------------------------------------------------------
 
esClique :: Eq a => Grafo a -> [a] -> Bool
esClique g xs =
  and [conectados g x y | (x,y) <- parejas xs]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    cliques :: Eq a => Grafo a -> [[a]]
-- tal que (cliques g) es la lista de los cliques del grafo g. Por
-- ejemplo, 
--    λ> cliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)]
--    [[],[1],[2],[1,2],[3],[2,3],[4],[2,4],
--     [5],[2,5],[3,5],[2,3,5],[4,5],[2,4,5]]
-- ---------------------------------------------------------------------
 
cliques :: Eq a => Grafo a -> [[a]]
cliques g =
  [xs | xs <- subsequences (nodos g)
      , esClique g xs]
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función 
--    kSubconjuntos :: [a] -> Int -> [[a]]
-- tal que (kSubconjuntos xs k) es la lista de los subconjuntos de xs
-- con k elementos. Por ejemplo,
--    ghci> kSubconjuntos "bcde" 2
--    ["bc","bd","be","cd","ce","de"]
--    ghci> kSubconjuntos "bcde" 3
--    ["bcd","bce","bde","cde"]
--    ghci> kSubconjuntos "abcde" 3
--    ["abc","abd","abe","acd","ace","ade","bcd","bce","bde","cde"]
-- ---------------------------------------------------------------------
 
kSubconjuntos :: [a] -> Int -> [[a]]
kSubconjuntos _ 0      = [[]]
kSubconjuntos [] _     = []
kSubconjuntos (x:xs) k = 
  [x:ys | ys <- kSubconjuntos xs (k-1)] ++ kSubconjuntos xs k  
 
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
--    kCliques :: Eq a => Grafo a -> Int -> [[a]]
-- tal que (cliques g k) es la lista de los cliques del grafo g de
-- tamaño k. Por ejemplo, 
--    λ> kCliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3
--    [[2,3,5],[2,4,5]]
--    λ> kCliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 2
--    [[1,2],[2,3],[2,4],[2,5],[3,5],[4,5]]
-- ---------------------------------------------------------------------
 
-- 1ª definición
kCliques1 :: Eq a => Grafo a -> Int -> [[a]]
kCliques1 g k =
  [xs | xs <- cliques g
      , length xs == k]
 
-- 2ª definición
kCliques :: Eq a => Grafo a -> Int -> [[a]]
kCliques g k =
  [xs | xs <- kSubconjuntos (nodos g) k
      , esClique g xs]
 
-- Comparación de eficiencia
-- =========================
 
--    λ> kCliques1 [(n,n+1) | n <- [1..20]] 3
--    []
--    (4.28 secs, 3,204,548,608 bytes)
--    λ> kCliques [(n,n+1) | n <- [1..20]] 3
--    []
--    (0.01 secs, 3,075,768 bytes)

Código de la reducción de SAT a Clique

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