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.

Soluciones

module Problema_SAT_para_FNC where

import Modelos_de_FNC
import Evaluacion_de_FNC

esSatisfacible :: FNC -> Bool
esSatisfacible = not . null . modelos