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)

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

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

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.

Código del prolblema del Clique

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

Se puede imprimir o compartir con