Reducción de SAT a Clique
Nota: En este ejercicio se usa la misma notación que en los anteriores importando los módulos
|
1 2 3 4 5 6 |
+ Evaluacion_de_FNC + Modelos_de_FNC + Problema_SAT_para_FNC + Cliques + KCliques + Grafo_FNC |
Definir las funciones
|
1 2 3 |
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,
|
1 2 3 4 5 6 7 8 9 |
λ> 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,
|
1 2 3 4 5 6 |
λ> 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,
|
1 2 3 4 |
λ> 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.
Soluciones
|
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 |
module Reduccion_de_SAT_a_Clique where import Evaluacion_de_FNC import Modelos_de_FNC import Problema_SAT_para_FNC import Cliques import KCliques import Grafo_FNC import Data.List (nub, sort) import Test.QuickCheck cliquesFNC :: FNC -> [[(Int,Literal)]] cliquesFNC f = cliques (grafoFNC f) cliquesCompletos :: FNC -> [[(Int,Literal)]] cliquesCompletos cs = kCliques (grafoFNC cs) (length cs) esSatisfaciblePorClique :: FNC -> Bool esSatisfaciblePorClique f = [] `notElem` f' && (length f' <= 1 || not (null (cliquesCompletos f'))) where f' = nub (map (nub . sort) f) -- La propiedad es 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. |
Otras soluciones
- Se pueden escribir otras soluciones en los comentarios.
- El código se debe escribir entre una línea con <pre lang=»haskell»> y otra con </pre>
Pensamiento
«La resolución de problemas es una habilidad práctica como, digamos, la natación. Adquirimos cualquier habilidad práctica por imitación y práctica. Tratando de nadar, imitas lo que otras personas hacen con sus manos y pies para mantener sus cabezas sobre el agua, y, finalmente, aprendes a nadar practicando la natación. Al intentar resolver problemas, hay que observar e imitar lo que hacen otras personas al resolver problemas y, finalmente, se aprende a resolver problemas haciéndolos.»