-- DavisPutnam.hs
-- El procedimiento de Davis y Putnam para SAT
-- José A. Alonso Jiménez <jalonso@us,es>
-- Sevilla, 4 de febrero de 2020
-- ---------------------------------------------------------------------
module SAT_DavisPutnam where
import SAT
import Data.List
import Test.QuickCheck
-- ---------------------------------------------------------------------
-- § Eliminación de tautologías
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esTautologia :: Clausula -> Bool
-- tal que (esTautologia c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautologia [1,2,-1] == True
-- esTautologia [1,2,-3] == False
-- esTautologia [] == False
-- ---------------------------------------------------------------------
esTautologia :: Clausula -> Bool
esTautologia = esValidaClausula
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- eliminaTautologias :: FNC -> FNC
-- tal que (eliminaTautologias s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
-- eliminaTautologias [[1,2],[1,3,-1]] == [[1,2]]
-- ---------------------------------------------------------------------
eliminaTautologias :: FNC -> FNC
eliminaTautologias s =
[c | c <- s, not (esTautologia c)]
-- ---------------------------------------------------------------------
-- § Eliminación de cláusulas unitarias
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esUnitaria :: Clausula -> Bool
-- tal que (esUnitaria c) se verifica si la cláusula c es unitaria . Por
-- ejemplo,
-- esUnitaria [3] == True
-- esUnitaria [-3] == True
-- esUnitaria [3,2] == False
-- esUnitaria [] == False
-- ---------------------------------------------------------------------
esUnitaria :: Clausula -> Bool
esUnitaria [_] = True
esUnitaria _ = False
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- eliminaClausulaUnitaria :: Literal -> FNC -> FNC
-- tal que (eliminaClausulaUnitaria l s) es el conjunto obtenido al
-- reducir s por la eliminación de la cláusula unitaria formada por el
-- literal l. Por ejemplo,
-- λ> eliminaClausulaUnitaria (-1) [[1,2,-3],[1,-2],[-1],[3]]
-- [[2,-3],[-2],[3]]
-- λ> eliminaClausulaUnitaria (-2) [[2,-3],[-2],[3]]
-- [[-3],[3]]
-- λ> eliminaClausulaUnitaria (-3) [[-3],[3],[1]]
-- [[],[1]]
-- ---------------------------------------------------------------------
eliminaClausulaUnitaria :: Literal -> FNC -> FNC
eliminaClausulaUnitaria l s =
[delete (complementario l) c | c <- s, notElem l c]
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- clausulaUnitaria :: FNC -> Maybe Literal
-- tal que (clausulaUnitaria s) es la primera cláusula unitaria de s, si
-- s tiene cláusulas unitarias y nada en caso contrario. Por ejemplo,
-- clausulaUnitaria [[1,2],[1],[-2]] == Just 1
-- clausulaUnitaria [[1,2],[1,-2]] == Nothing
-- ---------------------------------------------------------------------
clausulaUnitaria :: FNC -> Maybe Literal
clausulaUnitaria [] = Nothing
clausulaUnitaria (c:cs)
| esUnitaria c = Just (head c)
| otherwise = clausulaUnitaria cs
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- eliminaClausulasUnitarias :: FNC -> FNC
-- tal que (eliminaClausulasUnitarias s) es el conjunto obtenido
-- aplicando el proceso de eliminación de cláusulas unitarias a s. Por
-- ejemplo,
-- λ> eliminaClausulasUnitarias [[1,2,-3],[1,-2],[-1],[3],[5]]
-- [[],[5]]
-- λ> eliminaClausulasUnitarias [[1,2],[-2],[-1,2,-3]]
-- []
-- λ> eliminaClausulasUnitarias [[-1,2],[1],[3,5]]
-- [[3,5]]
-- ---------------------------------------------------------------------
eliminaClausulasUnitarias :: FNC -> FNC
eliminaClausulasUnitarias s
| elem [] s = s
| clausulaUnitaria s == Nothing = s
| otherwise =
eliminaClausulasUnitarias (eliminaClausulaUnitaria c s)
where Just c = clausulaUnitaria s
-- ---------------------------------------------------------------------
-- Eliminación de literales puros --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- literales :: FNC -> [Literal]
-- tal que (literales f) es el conjunto de literales de f. Por ejemplo,
-- literales [[1,2,-3],[1,2,-1]] == [1,2,-3,-1]
-- ---------------------------------------------------------------------
literales :: FNC -> [Literal]
literales = unionGeneral
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esLiteralPuro :: Literal -> FNC -> Bool
-- tal que (esLiteralPuro l f) se verifica si l es puro en f. Por
-- ejemplo,
-- esLiteralPuro 1 [[1,2],[1,-2],[3,2],[3,-2]] == True
-- esLiteralPuro 2 [[1,2],[1,-2],[3,2],[3,-2]] == False
-- ---------------------------------------------------------------------
esLiteralPuro :: Literal -> FNC -> Bool
esLiteralPuro l f =
and [notElem l' c | c <- f]
where l' = complementario l
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- eliminaLiteralPuro :: Literal -> FNC -> FNC
-- tal que (eliminaLiteralPuro l f) es el conjunto obtenido eliminando
-- el literal puro l de f. Por ejemplo,
-- eliminaLiteralPuro 1 [[1,2],[1,-2],[3,2],[3,-2]] == [[3,2],[3,-2]]
-- eliminaLiteralPuro 3 [[3,2],[3,-2]] == []
-- ---------------------------------------------------------------------
eliminaLiteralPuro :: Literal -> FNC -> FNC
eliminaLiteralPuro l f =
[c | c <- f, l `notElem` c]
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- literalesPuros :: FNC -> [Literal]
-- tal que (literalesPuros f) es el conjunto de los literales puros de
-- f. Por ejemplo,
-- literalesPuros [[1,2],[1,-2],[3,2],[3,-2]] == [1,3]
-- ---------------------------------------------------------------------
literalesPuros :: FNC -> [Literal]
literalesPuros f =
[l | l <- literales f, esLiteralPuro l f]
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- eliminaLiteralesPuros :: FNC -> FNC
-- tal que (eliminaLiteralesPuros f) es el conjunto obtenido aplicando a
-- f el proceso de eliminación de literales puros. Por ejemplo,
-- eliminaLiteralesPuros [[1,2],[1,-2],[3,2],[3,-2]] == []
-- eliminaLiteralesPuros [[1,2],[3,-5],[-3,5]] == [[3,-5],[-3,5]]
-- ---------------------------------------------------------------------
eliminaLiteralesPuros :: FNC -> FNC
eliminaLiteralesPuros f
| null lp = f
| otherwise =
eliminaLiteralesPuros (eliminaLiteralPuro (head lp) f)
where lp = literalesPuros f
-- ---------------------------------------------------------------------
-- § Bifurcación
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- bifurcacion :: FNC -> Literal -> (FNC,FNC)
-- tal que (bifurcacion f l) es la bifurcación de f según el literal
-- l. Por ejemplo,
-- λ> bifurcacion [[1,-2],[-1,2],[2,-3],[-2,-3]] 1
-- ([[-2],[2,-3],[-2,-3]],[[2],[2,-3],[-2,-3]])
-- ---------------------------------------------------------------------
bifurcacion :: FNC -> Literal -> (FNC,FNC)
bifurcacion f l =
([delete l c | c <- f, elem l c] ++ cláusulas_sin_l_ni_l',
[delete l' c | c <- f, elem l' c] ++ cláusulas_sin_l_ni_l')
where l' = complementario l
cláusulas_sin_l_ni_l' = [c | c <- f, notElem l c, notElem l' c]
-- ---------------------------------------------------------------------
-- § Algoritmo de Davis y Putnam (DP)
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- tieneClausulasUnitarias :: FNC -> Bool
-- tal que (tieneClausulasUnitarias f) se verifica si f tiene cláusulas
-- unitarias. Por ejemplo,
-- tieneClausulasUnitarias [[1,2],[1],[-2]] == True
-- tieneClausulasUnitarias [[1,2],[1,-2]] == False
-- ---------------------------------------------------------------------
tieneClausulasUnitarias :: FNC -> Bool
tieneClausulasUnitarias f =
clausulaUnitaria f /= Nothing
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- tieneLiteralesPuros :: FNC -> Bool
-- tal que (tieneLiteralesPuros f) se verifica si f tiene literales
-- puros. Por ejemplo,
-- tieneLiteralesPuros [[1,2],[1,-2],[3,2],[3,-2]] == True
-- tieneLiteralesPuros [[1,2],[-1,-2],[-3,2],[3,-2]] == False
-- ---------------------------------------------------------------------
tieneLiteralesPuros :: FNC -> Bool
tieneLiteralesPuros f =
not (null (literalesPuros f))
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esInsatisfaciblePorDP :: FNC -> Bool
-- tal que (esInsatisfaciblePorDP f) se verifica si f es insatisfacible
-- mediante el algoritmo de Davis y Putnam. Por ejemplo,
-- esInsatisfaciblePorDP [[1,2],[1,2,-1]] == False
-- esInsatisfaciblePorDP [[1,2,-3],[1,-2],[-1],[3],[5]] == True
-- esInsatisfaciblePorDP [[1,2],[-2],[-1,2,-3]] == False
-- esInsatisfaciblePorDP [[-1,2],[1],[3,5]] == False
-- esInsatisfaciblePorDP [[1,2],[1,-2],[3,2],[3,-2]] == False
-- esInsatisfaciblePorDP [[1,2],[3,-4],[-3,4]] == False
-- ---------------------------------------------------------------------
esInsatisfaciblePorDP :: FNC -> Bool
esInsatisfaciblePorDP f =
esInsatisfaciblePorDP' (eliminaTautologias f)
esInsatisfaciblePorDP' :: FNC -> Bool
esInsatisfaciblePorDP' f
| null f = False
| elem [] f = True
| tieneClausulasUnitarias f =
esInsatisfaciblePorDP' (eliminaClausulasUnitarias f)
| tieneLiteralesPuros f =
esInsatisfaciblePorDP' (eliminaLiteralesPuros f)
| otherwise =
(esInsatisfaciblePorDP' s1) && (esInsatisfaciblePorDP' s2)
where l = head (head f)
(s1,s2) = bifurcacion f l
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la función
-- esSatisfaciblePorDP :: FNC -> Bool
-- tal que (esSatisfaciblePorDP f) se verifica si f es satisfacible
-- mediante el algoritmo de Davis y Putnam. Por ejemplo,
-- esSatisfaciblePorDP [[1,2],[1,2,-1]] == True
-- esSatisfaciblePorDP [[1,2,-3],[1,-2],[-1],[3],[5]] == False
-- ---------------------------------------------------------------------
esSatisfaciblePorDP :: FNC -> Bool
esSatisfaciblePorDP = not . esInsatisfaciblePorDP
-- ---------------------------------------------------------------------
-- § Corrección del algoritmo de Davis y Putnam --
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio. Comprobar con QuickCheck que el algoritmo De Davis y
-- Putnam es correcto; es decir, para toda fórmula f, f es
-- insatisfacible según el algoritmo de Davis y Putnam si,y solo si, f
-- es insatisfacible.
-- ---------------------------------------------------------------------
prop_CorreccionDP :: FNC -> Bool
prop_CorreccionDP f =
esInsatisfaciblePorDP f == esInsatisfacible f
-- La comprobación es
-- λ> quickCheckWith (stdArgs {maxSize=10}) prop_CorreccionDP
-- +++ OK, passed 100 tests.
