-- SAT.hs
-- El problema SAT para fóemulas en FNC.
-- José A. Alonso Jiménez <jalonso@us,es>
-- Sevilla, 4 de febrero de 2020
-- ---------------------------------------------------------------------
module SAT where
import Data.List
-- ---------------------------------------------------------------------
-- § Átomos, literales, cláusulas y FNC
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Usareremos las siguientes representaciones:
-- + Los átomos se representan por enteros positivos. Por ejemplo, 3
-- representa x(3).
-- + Los literales se representa por enteros. Por ejemplo, 3 reprsenta
-- el literal positivo x(3) y -5 el literal negativo -x(3).
-- + Una cláusula es una lista de literales que representa su
-- disyunción. Por ejemplo, [3,2,-4] representa a x(3) v x(2) v -x(4).
-- + Una fórmula en forma normal conjuntiva (FNC) es una lista de
-- cláusulas que representa su conjunción. Por ejemplo, [[3,2],[-1,2,5]]
-- representa a (x(3) v x(2)) & (-x(1) v x(2) v x(5)).
--
-- Definir los tipo de datos Atomo, Literal, Clausula y FNC.
-- ---------------------------------------------------------------------
type Atomo = Int
type Literal = Int
type Clausula = [Literal]
type FNC = [Clausula]
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- complementario :: Literal -> Literal
-- tal que (complementario l) es el complementario de l. Por ejemplo,
-- complementario 3 == -3
-- complementario (-3) == 3
-- ---------------------------------------------------------------------
complementario :: Literal -> Literal
complementario l = (-1) * l
-- ---------------------------------------------------------------------
-- § Átomos de cláusulas y de FNC
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- atomosClausula :: Clausula -> [Prop]
-- tal que (atomosClausula c) es el conjunto de los átomos de c. Por
-- ejemplo,
-- atomosClausula [1,3,-1] == [1,3]
-- ---------------------------------------------------------------------
atomosClausula :: Clausula -> [Atomo]
atomosClausula c = nub (map abs c)
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- unionGeneral :: Eq a => [[a]] -> [a]
-- tal que (unionGeneral x) es la unión de los conjuntos de la lista de
-- conjuntos x. Por ejemplo,
-- unionGeneral [] == []
-- unionGeneral [[1]] == [1]
-- unionGeneral [[1],[1,2],[2,3]] == [1,2,3]
-- ---------------------------------------------------------------------
unionGeneral :: Eq a => [[a]] -> [a]
unionGeneral [] = []
unionGeneral (x:xs) = x `union` unionGeneral xs
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- atomosFNC :: FNC -> [Prop]
-- tal que (atomosFNC f) es el conjunto de los átomos de f. Por ejemplo,
-- atomosFNC [[1,2],[4,-2]] == [1,2,4]
-- ---------------------------------------------------------------------
atomosFNC :: FNC -> [Atomo]
atomosFNC f = unionGeneral [atomosClausula c | c <- f]
-- ---------------------------------------------------------------------
-- § Interpretaciones
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Una interpretación I es un conjunto de átomos. Se supone
-- que los átomos de I son verdaderos y los restantes son falsos.
--
-- Definir el tipo de dato Interpretacion.
-- ---------------------------------------------------------------------
type Interpretacion = [Atomo]
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- interpretacionesClausula :: Clausula -> [Interpretacion]
-- tal que (interpretacionesClausula c) es el conjunto de
-- interpretaciones de c. Por ejemplo,
-- interpretacionesClausula [1,2,-1] == [[],[1],[2],[1,2]]
-- interpretacionesClausula [] == [[]]
-- ---------------------------------------------------------------------
interpretacionesClausula :: Clausula -> [Interpretacion]
interpretacionesClausula c = subsequences (atomosClausula c)
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- interpretaciones :: FNC -> [Interpretacion]
-- tal que (interpretaciones f) es el conjunto de interpretaciones de
-- f. Por ejemplo,
-- interpretaciones [[1,-2],[-1,2]] == [[],[1],[2],[1,2]]
-- interpretaciones [] == [[]]
-- ---------------------------------------------------------------------
interpretaciones :: FNC -> [Interpretacion]
interpretaciones f = subsequences (atomosFNC f)
-- ---------------------------------------------------------------------
-- § Modelos de literales, cláusulas y FNC
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esModeloLiteral :: Interpretacion -> Literal -> Bool
-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por
-- ejemplo,
-- esModeloLiteral [3,5] 3 == True
-- esModeloLiteral [3,5] 4 == False
-- esModeloLiteral [3,5] (-3) == False
-- esModeloLiteral [3,5] (-4) == True
-- ---------------------------------------------------------------------
esModeloLiteral :: Interpretacion -> Literal -> Bool
esModeloLiteral i l
| l > 0 = l `elem` i
| otherwise = complementario l `notElem` i
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esModeloClausula :: Interpretacion -> Clausula -> Bool
-- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloClausula [3,5] [2,3,-5] == True
-- esModeloClausula [3,5] [2,4,-1] == True
-- esModeloClausula [3,5] [2,4,1] == False
-- ---------------------------------------------------------------------
esModeloClausula :: Interpretacion -> Clausula -> Bool
esModeloClausula i c = or [esModeloLiteral i l | l <- c]
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- modelosClausula :: Clausula -> [Interpretacion]
-- tal que (modelosClausula c) es la lista de los modelos de c. Por
-- ejemplo,
-- modelosClausula [-1,2] == [[],[2],[1,2]]
-- modelosClausula [-1,1] == [[],[1]]
-- modelosClausula [] == []
-- ---------------------------------------------------------------------
modelosClausula :: Clausula -> [Interpretacion]
modelosClausula c =
[i | i <- interpretacionesClausula c,
esModeloClausula i c]
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esModelo :: Interpretacion -> FNC -> Bool
-- tal que (esModelo i f) se verifica si i es modelo de f. Por ejemplo,
-- esModelo [1,3] [[1,-2],[3]] == True
-- esModelo [1] [[1,-2],[3]] == False
-- esModelo [1] [] == True
-- ---------------------------------------------------------------------
esModelo :: Interpretacion -> FNC -> Bool
esModelo i s =
and [esModeloClausula i c | c <- s]
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- modelos :: FNC -> [Interpretacion]
-- tal que (modelos f) es la lista de los modelos de f. Por ejemplo,
-- modelos [[-1,2],[-2,1]] == [[],[1,2]]
-- modelos [[-1,2],[-2],[1]] == []
-- modelos [[1,-1,2]] == [[],[1],[2],[1,2]]
-- ---------------------------------------------------------------------
modelos :: FNC -> [Interpretacion]
modelos s =
[i | i <- interpretaciones s,
esModelo i s]
-- ---------------------------------------------------------------------
-- § Cláusulas válidas, satisfacibles e insatisfacibles
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esSatisfacibleClausula :: Clausula -> Bool
-- tal que (esSatisfacibleClausula c) se verifica si la cláusula c es
-- satisfacible. Por ejemplo,
-- esSatisfacibleClausula [1,2,-1] == True
-- esSatisfacibleClausula [1,2,-3] == True
-- esSatisfacibleClausula [] == False
-- ---------------------------------------------------------------------
-- 1ª definición
esSatisfacibleClausula1 :: Clausula -> Bool
esSatisfacibleClausula1 c =
or [esModeloClausula i c | i <- interpretacionesClausula c]
-- 2ª definición
esSatisfacibleClausula :: Clausula -> Bool
esSatisfacibleClausula = not . null
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esInsatisfacibleClausula :: Clausula -> Bool
-- tal que (esInsatisfacibleClausula c) se verifica si la cláusula c es
-- insatisfacible. Por ejemplo,
-- esInsatisfacibleClausula [1,2,-1] == False
-- esInsatisfacibleClausula [1,2,-3] == False
-- esInsatisfacibleClausula [] == True
-- ---------------------------------------------------------------------
-- 1ª definición
esInsatisfacibleClausula1 :: Clausula -> Bool
esInsatisfacibleClausula1 c =
and [not (esModeloClausula i c) | i <- interpretacionesClausula c]
-- 2ª definición
esInsatisfacibleClausula :: Clausula -> Bool
esInsatisfacibleClausula = null
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esValidaClausula :: Clausula -> Bool
-- tal que (esValidaClausula c) se verifica si la cláusula c es
-- válida. Por ejemplo,
-- esValidaClausula [1,2,-1] == True
-- esValidaClausula [1,2,-3] == False
-- esValidaClausula [] == False
-- ---------------------------------------------------------------------
-- 1ª definición
esValidaClausula1 :: Clausula -> Bool
esValidaClausula1 c =
and [esModeloClausula i c | i <- interpretacionesClausula c]
-- 2ª definición
esValidaClausula :: Clausula -> Bool
esValidaClausula c =
not (null [l | l <- c, complementario l `elem` c])
-- ---------------------------------------------------------------------
-- § FNC válidas, satisfacible e insatisfacibles
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. 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,2]] == True
-- esSatisfacible [[-1,1],[-2,2]] == True
-- esSatisfacible [] == True
-- ---------------------------------------------------------------------
esSatisfacible :: FNC -> Bool
esSatisfacible s =
not (null (modelos s))
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esInsatisfacible :: FNC -> Bool
-- tal que (esInsatisfacible f) se verifica si la FNC f es
-- insatisfacible. Por ejemplo,
-- esInsatisfacible [[-1,2],[-2,1]] == False
-- esInsatisfacible [[-1],[1]] == True
-- ---------------------------------------------------------------------
esInsatisfacible :: FNC -> Bool
esInsatisfacible f =
null (modelos f)
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esValida :: FNC -> Bool
-- tal que (esValida f) se verifica si f es válida. Por ejemplo,
-- esValida [[-1,2],[-2,1]] == False
-- esValida [[-1,1],[-2,2]] == True
-- esValida [] == True
-- ---------------------------------------------------------------------
-- 1ª definición
esValida1 :: FNC -> Bool
esValida1 f =
modelos f == interpretaciones f
-- 2ª definición
esValida :: FNC -> Bool
esValida f =
and [esValidaClausula c | c <- f]
