Ir al contenido principal

Reducción de SAT a Clique

Nota: En este ejercicio se usa la misma notación que en los anteriores importando los módulos

  • Evaluacion_de_FNC
  • Modelos_de_FNC
  • Problema_SAT_para_FNC
  • Cliques
  • KCliques
  • Grafo_FNC

Definir las funciones

cliquesFNC :: FNC -> [[(Int,Literal)]]
cliquesCompletos :: FNC -> [[(Int,Literal)]]
esSatisfaciblePorClique :: FNC -> Bool

tales 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)]]
  • (cliquesCompletos f) es la lista de los cliques del grafo de f que tiene tantos elementos como cláusulas tiene 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]]
[]
  • (esSatisfaciblePorClique f) se verifica si f no contiene la cláusula vacía, tiene más 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

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


Leer más…

Grafo de una FNC (fórmula en forma normal conjuntiva)

Para reducir el problema del clique a SAT se comienza asociando a cada fórmula F en FNC un grafo G de forma que F es saisfacible si, y sólo si, G tiene un clique con tantos nodos como cláusulas tiene F.

Los nodos del grafo de F son los literales de las cláusulas de F junto con el número de la cláusula. Por ejemplo, la lista de nodos de la FNC [[1,-2,3],[-1,2],[-2,3]] es

[(0,1),(0,-2),(0,3),
 (1,-1),(1,2),
 (2,-2),(2,3)]

En el grafo de F, hay un arco entre dos nodos si, y solo si, corresponden a cláusulas distintas y sus literales no son complementarios. Por ejemplo,

  • hay un arco entre (0,1) y (1,2) [porque son de cláusulas distintas (0 y 1) y sus literales (1 y 2) no son complementarios.
  • no hay un arco entre (0,1) y (1,-1) [porque sus literales (1 y -1) no son complementarios.
  • no hay un arco entre (0,1) y (0,3) [porque son de la misma cláusula (la 0)].

Nota: En este ejercicio se usará los conceptos de los anteriores importando los módulos Evaluacion_de_FNC y Grafo.

Definir las funciones

nodosFNC :: FNC -> [(Int,Literal)]
grafoFNC :: FNC -> Grafo (Int,Literal)

tales que

  • (nodosFNC f) es la lista de los nodos del grafo de f. Por ejemplo,
λ> nodosFNC [[1,-2,3],[-1,2],[-2,3]]
[(0,1),(0,-2),(0,3),(1,-1),(1,2),(2,-2),(2,3)]
  • (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))]

Leer más…

Cliques de orden k

Nota: En este ejercicio usaremos las mismas notaciones que en el anterior importando el módulo Cliques.

Definir la función

kCliques :: Eq a => Grafo a -> Int -> [[a]]

tal que (kCliques 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]]
λ> kCliques [(n,n+1) | n <- [1..100]] 3
[]

Nota: Escribir la solución en el módulo KCliques para poderlo usar en los siguientes ejercicios.


Leer más…

Cliques de un grafo

Nota: En este ejercicio usaremos las mismas notaciones que en el anterior importando el módulo Grafo.

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 las funciones

esClique :: Eq a => Grafo a -> [a] -> Bool
cliques  :: Eq a => Grafo a -> [[a]]

tales 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
  • (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]]

Nota: Escribir la solución en el módulo Cliques para poderlo usar en los siguientes ejercicios.


Leer más…

Parejas de un conjunto

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)]
length (parejas [sin,cos,tan,log])  ==  6

Leer más…

Nodos y conexiones de un grafo

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

Se define el tipo de grafo por

type Grafo a = [(a,a)]

Definir las funciones

nodos      :: Eq a => Grafo a -> [a]
conectados :: Eq a => Grafo a -> a -> a -> Bool

tales 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]
  • (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

Nota: Escribir la solución en el módulo Grafo para poderlo usar en los siguientes ejercicios.


Leer más…

Problema SAT para FNC (fórmulas en forma normal conjuntiva)

Nota: En este ejercicio usaremos las mismas notaciones que en los anteriores importando los módulos Modelos_de_FNC y Evaluacion_de_FNC.

Una FNC (fórmula en forma normal conjuntiva) es satisfacible, si tiene algún modelo. Por ejemplo,

Definir la función

esSatisfacible :: FNC -> Bool

tal que (esSatisfacible f) se verifica si la FNC f es satistacible. Por ejemplo,

esSatisfacible [[-1,2],[-2,1]]    ==  True
esSatisfacible [[-1,2],[-2],[1]]  ==  False
esSatisfacible [[1,2],[]]         ==  False
esSatisfacible []                 ==  True

Nota: Escribir la solución en el módulo Problema_de_SAT_para_FNC para poderlo usar en los siguientes ejercicios.


Leer más…

Modelos de FNC (fórmulas en forma normal conjuntiva)

Nota: En este ejercicio usaremos las mismas notaciones que en anterior importando los módulos Interpretaciones_de_FNC y Evaluacion_de_FNC.

Una interpretación I es un modelo de un literal L si el valor de L en I es verdadero. Por ejemplo, la interpretación [2,5]

  • es modelo del literal x(2) (porque 2 ∈ [2,5])
  • no es modelo del literal x(3) (porque 3 ∉ [2,5])
  • es modelo del literal -x(4) (porque 4 ∉ [2,5])

Una interpretación I es un modelo de una cláusula C si el valor de C en I es verdadero. Por ejemplo, la interpretación [2,5]

  • es modelo de la cláusula (x(2) v x(3)) (porque x(2) es verdadero)
  • no es modelo de la cláusula (x(3) v x(4)) (porque x(3) y x(4) son falsos)

Una interpretación I es un modelo de una FNC F si el valor de F en I es verdadero. Por ejemplo, la interpretación [2,5]

  • es modelo de la FNC ((x(2) v x(5)) & (-x(4) v x(3)) porque lo es de sus dos cláusulas.

Definir las siguientes funciones

esModeloLiteral  :: Interpretacion -> Literal -> Bool
esModeloClausula :: Interpretacion -> Clausula -> Bool
esModelo         :: Interpretacion -> FNC -> Bool
modelosClausula  :: Clausula -> [Interpretacion]
modelos          :: FNC -> [Interpretacion]

tales que

  • (esModeloLiteral i l) se verifica si i es modelo del literal l. Por ejemplo,
esModeloLiteral [3,5] 3     ==  True
esModeloLiteral [3,5] 4     ==  False
esModeloLiteral [3,5] (-3)  ==  False
esModeloLiteral [3,5] (-4)  ==  True
  • (esModeloClausula i c) se verifica si i es modelo de la cláusula c. Por ejemplo,
esModeloClausula [3,5] [2,3,-5]  ==  True
esModeloClausula [3,5] [2,4,-1]  ==  True
esModeloClausula [3,5] [2,4,1]   ==  False
  • (esModelo i f) se verifica si i es modelo de la fórmula f. Por ejemplo,
esModelo [1,3] [[1,-2],[3]]  ==  True
esModelo [1]   [[1,-2],[3]]  ==  False
esModelo [1]   []            ==  True
  • (modelosClausula c) es la lista de los modelos de la cláusula c. Por ejemplo,
modelosClausula [-1,2]  ==  [[],[2],[1,2]]
modelosClausula [-1,1]  ==  [[],[1]]
modelosClausula []      ==  []
  • (modelos f) es la lista de los modelos de la fórmula f. Por ejemplo,
modelos [[-1,2],[-2,1]]    ==  [[],[1,2]]
modelos [[-1,2],[-2],[1]]  ==  []
modelos [[1,-1,2]]         ==  [[],[1],[2],[1,2]]

Nota: Escribir la solución en el módulo Modelos_de_FNC para poderlo usar en los siguientes ejercicios.


Leer más…

Interpretaciones de FNC (fórmulas en forma normal conjuntiva)

Nota: En este ejercicio usaremos las mismas notaciones que en los anteriores importando los módulos Evaluacion_de_FNC y Atomos_de_FNC.

Definir las siguientes funciones

interpretacionesClausula :: Clausula -> [Interpretacion]
interpretaciones         :: FNC -> [Interpretacion]

tales que

  • (interpretacionesClausula c) es el conjunto de interpretaciones de la cláusula c. Por ejemplo,
interpretacionesClausula [1,2,-1]  ==  [[],[1],[2],[1,2]]
interpretacionesClausula []        ==  [[]]
  • (interpretaciones f) es el conjunto de interpretaciones de la fórmula f. Por ejemplo,
interpretaciones [[1,-2],[-1,2]] == [[],[1],[2],[1,2]]
interpretaciones []              == [[]]

Nota: Escribir la solución en el módulo Interpretaciones_de_FNC para poderlo usar en los siguientes ejercicios.


Leer más…