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
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 |
-- 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
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 |
-- 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. |