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 import 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
|
1 |
esSatisfacible :: FNC -> Bool |
tal que (esSatisfacible f) se verifica si la FNC f es satistacible. Por ejemplo,
|
1 2 3 4 |
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.
Soluciones
|
1 2 3 4 5 6 7 |
module Problema_SAT_para_FNC where import Modelos_de_FNC import Evaluacion_de_FNC esSatisfacible :: FNC -> Bool esSatisfacible = not . null . modelos |
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
«Un gran descubrimiento resuelve un gran problema, pero hay un grano de descubrimiento en cualquier problema.»
Estas serían tres definiciones equivalentes de la función