Ver el código de «El algoritmo de Davis-Putnam en Haskell»

<source lang="haskell">
-- 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.
</source>