{"id":6979,"date":"2020-02-06T09:42:55","date_gmt":"2020-02-06T08:42:55","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6979"},"modified":"2020-02-08T09:53:22","modified_gmt":"2020-02-08T08:53:22","slug":"ra2019-el-algoritmo-de-davis-putnam-en-haskell","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-el-algoritmo-de-davis-putnam-en-haskell\/","title":{"rendered":"RA2019: El algoritmo de Davis-Putnam en Haskell"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-19\">Razonamiento autom\u00e1tico<\/a> se ha estudiado una implementaci\u00f3n del algoritmo de Davis-Putnam en Haskell y comprobado su correcci\u00f3n con QuickCheck.<\/p>\n<p>En primer lugar se ha estudiado una implementaci\u00f3n de la l\u00f3gica clausal en Haskell en la que se han definido los \u00e1tomos, literales, cl\u00e1usulas, f\u00f3rmulas en forma normal conjuntiva (FNC), interpretaciones, modelos y la clasificaci\u00f3n de FNC en satisfacibles, insatisfacibles y v\u00e1lidas.<\/p>\n<p>A continuaci\u00f3n se ha estudiado una implementaci\u00f3n del algoritmo de Davis-Putnam en Haskell.<\/p>\n<p>Los c\u00f3digos y las transparencias usados en la presentaci\u00f3n son los siguientes:<\/p>\n<p><!-- more --><\/p>\n<h2>C\u00f3digo de SAT en Haskell<\/h2>\n<pre lang=\"haskell\">\n-- SAT.hs\n-- El problema SAT para f\u00f3emulas en FNC.\n-- Jos\u00e9 A. Alonso Jim\u00e9nez <jalonso@us,es>\n-- Sevilla, 4 de febrero de 2020\n-- ---------------------------------------------------------------------\n\nmodule SAT where\n\nimport Data.List\n\n-- ---------------------------------------------------------------------\n-- \u00a7 \u00c1tomos, literales, cl\u00e1usulas y FNC\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Usareremos las siguientes representaciones:\n-- + Los \u00e1tomos se representan por enteros positivos. Por ejemplo, 3\n--   representa x(3). \n-- + Los literales se representa por enteros. Por ejemplo, 3 reprsenta\n--   el literal positivo x(3) y -5 el literal negativo -x(3).\n-- + Una cl\u00e1usula es una lista de literales que representa su\n--   disyunci\u00f3n. Por ejemplo, [3,2,-4] representa a x(3) v x(2) v -x(4).\n-- + Una f\u00f3rmula en forma normal conjuntiva (FNC) es una lista de\n--   cl\u00e1usulas que representa su conjunci\u00f3n. Por ejemplo, [[3,2],[-1,2,5]]\n--   representa a (x(3) v x(2)) & (-x(1) v x(2) v x(5)).\n--\n-- Definir los tipo de datos Atomo, Literal, Clausula y FNC.\n-- ---------------------------------------------------------------------\n\ntype Atomo    = Int\ntype Literal  = Int\ntype Clausula = [Literal]\ntype FNC      = [Clausula]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    complementario :: Literal -> Literal\n-- tal que (complementario l) es el complementario de l. Por ejemplo,\n--    complementario 3  ==  -3\n--    complementario (-3)  ==  3\n-- ---------------------------------------------------------------------\n\ncomplementario :: Literal -> Literal\ncomplementario l = (-1) * l\n\n-- ---------------------------------------------------------------------\n-- \u00a7 \u00c1tomos de cl\u00e1usulas y de FNC\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    atomosClausula :: Clausula -> [Prop]\n-- tal que (atomosClausula c) es el conjunto de los \u00e1tomos de c. Por\n-- ejemplo, \n--    atomosClausula [1,3,-1] == [1,3]\n-- ---------------------------------------------------------------------\n\natomosClausula :: Clausula -> [Atomo]\natomosClausula c = nub (map abs c)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    unionGeneral :: Eq a => [[a]] -> [a]\n-- tal que (unionGeneral x) es la uni\u00f3n de los conjuntos de la lista de\n-- conjuntos x. Por ejemplo,\n--    unionGeneral []                 ==  []\n--    unionGeneral [[1]]              ==  [1]\n--    unionGeneral [[1],[1,2],[2,3]]  ==  [1,2,3]\n-- ---------------------------------------------------------------------\n\nunionGeneral :: Eq a => [[a]] -> [a]\nunionGeneral []     = []\nunionGeneral (x:xs) = x `union` unionGeneral xs \n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    atomosFNC :: FNC -> [Prop]\n-- tal que (atomosFNC f) es el conjunto de los \u00e1tomos de f. Por ejemplo, \n--    atomosFNC [[1,2],[4,-2]] == [1,2,4]\n-- ---------------------------------------------------------------------\n\natomosFNC :: FNC -> [Atomo]\natomosFNC f = unionGeneral [atomosClausula c | c <- f]\n\n-- ---------------------------------------------------------------------\n-- \u00a7 Interpretaciones \n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Una interpretaci\u00f3n I es un conjunto de \u00e1tomos. Se supone\n-- que los \u00e1tomos de I son verdaderos y los restantes son falsos.\n--\n-- Definir el tipo de dato Interpretacion.\n-- ---------------------------------------------------------------------\n\ntype Interpretacion = [Atomo]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    interpretacionesClausula :: Clausula -> [Interpretacion]\n-- tal que (interpretacionesClausula c) es el conjunto de\n-- interpretaciones de c. Por ejemplo,\n--    interpretacionesClausula [1,2,-1]  ==  [[],[1],[2],[1,2]]\n--    interpretacionesClausula []        ==  [[]]\n-- ---------------------------------------------------------------------\n\ninterpretacionesClausula :: Clausula -> [Interpretacion]\ninterpretacionesClausula c = subsequences (atomosClausula c)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    interpretaciones :: FNC -> [Interpretacion]\n-- tal que (interpretaciones f) es el conjunto de interpretaciones de\n-- f. Por ejemplo, \n--    interpretaciones [[1,-2],[-1,2]] == [[],[1],[2],[1,2]]\n--    interpretaciones []              == [[]]\n-- ---------------------------------------------------------------------\n\ninterpretaciones :: FNC -> [Interpretacion]\ninterpretaciones f = subsequences (atomosFNC f)\n\n-- ---------------------------------------------------------------------\n-- \u00a7 Modelos de literales, cl\u00e1usulas y FNC \n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esModeloLiteral :: Interpretacion -> Literal -> Bool\n-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por\n-- ejemplo, \n--    esModeloLiteral [3,5] 3     ==  True\n--    esModeloLiteral [3,5] 4     ==  False\n--    esModeloLiteral [3,5] (-3)  ==  False\n--    esModeloLiteral [3,5] (-4)  ==  True\n-- ---------------------------------------------------------------------\n\nesModeloLiteral :: Interpretacion -> Literal -> Bool\nesModeloLiteral i l\n  | l > 0     = l `elem` i\n  | otherwise = complementario l `notElem` i\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esModeloClausula :: Interpretacion -> Clausula -> Bool\n-- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por\n-- ejemplo, \n--    esModeloClausula [3,5] [2,3,-5]  ==  True\n--    esModeloClausula [3,5] [2,4,-1]  ==  True\n--    esModeloClausula [3,5] [2,4,1]  ==  False\n-- ---------------------------------------------------------------------\n\nesModeloClausula :: Interpretacion -> Clausula -> Bool\nesModeloClausula i c = or [esModeloLiteral i l | l <- c]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    modelosClausula :: Clausula -> [Interpretacion]\n-- tal que (modelosClausula c) es la lista de los modelos de c. Por\n-- ejemplo, \n--    modelosClausula [-1,2]  ==  [[],[2],[1,2]]\n--    modelosClausula [-1,1]  ==  [[],[1]]\n--    modelosClausula []      ==  []\n-- ---------------------------------------------------------------------\n\nmodelosClausula :: Clausula -> [Interpretacion]\nmodelosClausula c =\n  [i | i <- interpretacionesClausula c,\n       esModeloClausula i c]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esModelo :: Interpretacion -> FNC -> Bool\n-- tal que (esModelo i f) se verifica si i es modelo de f. Por ejemplo,\n--    esModelo [1,3] [[1,-2],[3]]  ==  True\n--    esModelo [1]   [[1,-2],[3]]  ==  False\n--    esModelo [1]   []            ==  True\n-- ---------------------------------------------------------------------\n\nesModelo :: Interpretacion -> FNC -> Bool\nesModelo i s =\n  and [esModeloClausula i c | c <- s]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    modelos :: FNC -> [Interpretacion]\n-- tal que (modelos f) es la lista de los modelos de f. Por ejemplo, \n--    modelos [[-1,2],[-2,1]]    ==  [[],[1,2]]\n--    modelos [[-1,2],[-2],[1]]  ==  []\n--    modelos [[1,-1,2]]         ==  [[],[1],[2],[1,2]]\n-- ---------------------------------------------------------------------\n\nmodelos :: FNC -> [Interpretacion]\nmodelos s =\n  [i | i <- interpretaciones s,\n       esModelo i s] \n\n-- ---------------------------------------------------------------------\n-- \u00a7 Cl\u00e1usulas v\u00e1lidas, satisfacibles e insatisfacibles                \n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esSatisfacibleClausula :: Clausula -> Bool\n-- tal que (esSatisfacibleClausula c) se verifica si la cl\u00e1usula c es\n-- satisfacible. Por ejemplo, \n--    esSatisfacibleClausula [1,2,-1]  ==  True\n--    esSatisfacibleClausula [1,2,-3]  ==  True\n--    esSatisfacibleClausula []        ==  False\n-- ---------------------------------------------------------------------\n\n-- 1\u00aa definici\u00f3n\nesSatisfacibleClausula1 :: Clausula -> Bool\nesSatisfacibleClausula1 c =\n  or [esModeloClausula i c | i <- interpretacionesClausula c]\n\n-- 2\u00aa definici\u00f3n\nesSatisfacibleClausula :: Clausula -> Bool\nesSatisfacibleClausula = not . null \n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esInsatisfacibleClausula :: Clausula -> Bool\n-- tal que (esInsatisfacibleClausula c) se verifica si la cl\u00e1usula c es\n-- insatisfacible. Por ejemplo, \n--    esInsatisfacibleClausula [1,2,-1]  ==  False\n--    esInsatisfacibleClausula [1,2,-3]  ==  False\n--    esInsatisfacibleClausula []        ==  True\n-- ---------------------------------------------------------------------\n\n-- 1\u00aa definici\u00f3n\nesInsatisfacibleClausula1 :: Clausula -> Bool\nesInsatisfacibleClausula1 c =\n   and [not (esModeloClausula i c) | i <- interpretacionesClausula c]\n\n-- 2\u00aa definici\u00f3n\nesInsatisfacibleClausula :: Clausula -> Bool\nesInsatisfacibleClausula  = null\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esValidaClausula :: Clausula -> Bool\n-- tal que (esValidaClausula c) se verifica si la cl\u00e1usula c es\n-- v\u00e1lida. Por ejemplo, \n--    esValidaClausula [1,2,-1]  ==  True\n--    esValidaClausula [1,2,-3]  ==  False\n--    esValidaClausula []        ==  False\n-- ---------------------------------------------------------------------\n\n-- 1\u00aa definici\u00f3n\nesValidaClausula1 :: Clausula -> Bool\nesValidaClausula1 c =\n  and [esModeloClausula i c | i <- interpretacionesClausula c]\n\n-- 2\u00aa definici\u00f3n\nesValidaClausula :: Clausula -> Bool\nesValidaClausula c =\n  not (null [l | l <- c, complementario l `elem` c])\n\n-- ---------------------------------------------------------------------\n-- \u00a7 FNC v\u00e1lidas, satisfacible e insatisfacibles\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esSatisfacible :: FNC -> Bool\n-- tal que (esSatisfacible f) se verifica si la FNC f es\n-- satistacible. Por ejemplo, \n--    esSatisfacible [[-1,2],[-2,1]]  ==  True\n--    esSatisfacible [[-1,2],[-2,2]]  ==  True\n--    esSatisfacible [[-1,1],[-2,2]]  ==  True\n--    esSatisfacible []               ==  True\n-- ---------------------------------------------------------------------\n\nesSatisfacible :: FNC -> Bool\nesSatisfacible s =\n  not (null (modelos s))\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esInsatisfacible :: FNC -> Bool\n-- tal que (esInsatisfacible f) se verifica si la FNC f es\n-- insatisfacible. Por ejemplo,\n--    esInsatisfacible [[-1,2],[-2,1]]  ==  False\n--    esInsatisfacible [[-1],[1]]       ==  True\n-- ---------------------------------------------------------------------\n\nesInsatisfacible :: FNC -> Bool\nesInsatisfacible f =\n  null (modelos f)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esValida :: FNC -> Bool\n-- tal que (esValida f) se verifica si f es v\u00e1lida. Por ejemplo, \n--    esValida [[-1,2],[-2,1]]  ==  False\n--    esValida [[-1,1],[-2,2]]  ==  True\n--    esValida []               ==  True\n-- ---------------------------------------------------------------------\n\n-- 1\u00aa definici\u00f3n\nesValida1 :: FNC -> Bool\nesValida1 f =\n  modelos f == interpretaciones f\n\n-- 2\u00aa definici\u00f3n\nesValida :: FNC -> Bool\nesValida f =\n  and [esValidaClausula c | c <- f]\n<\/pre>\n<h2>Presentaci\u00f3n del algoritmo de Davis-Putnam<\/h2>\n<p>La presentaci\u00f3n se ha basado en las 12 primeras p\u00e1ginas del siguiente tema<br \/>\n<iframe src=\"\/\/docs.google.com\/viewer?url=https%3A%2F%2Fwww.cs.us.es%2F%7Ejalonso%2Fcursos%2Flmf-17%2Ftemas%2Ftema-6.pdf&hl=es&embedded=true\" class=\"gde-frame\" style=\"width:100%; height:500px; border: none;\" scrolling=\"no\"><\/iframe>\n<p class=\"gde-text\"><a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-17\/temas\/tema-6.pdf\" class=\"gde-link\">Descargar (PDF, 283KB)<\/a><\/p><\/p>\n<h2>C\u00f3digo del algoritmo de Davis-Putnam en Haskell<\/h2>\n<pre lang=\"haskell\">\n-- DavisPutnam.hs\n-- El procedimiento de Davis y Putnam para SAT\n-- Jos\u00e9 A. Alonso Jim\u00e9nez <jalonso@us,es>\n-- Sevilla, 4 de febrero de 2020\n-- ---------------------------------------------------------------------\n\nmodule SAT_DavisPutnam where\n\nimport SAT\nimport Data.List \nimport Test.QuickCheck\n\n-- ---------------------------------------------------------------------\n-- \u00a7 Eliminaci\u00f3n de tautolog\u00edas\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esTautologia :: Clausula -> Bool\n-- tal que (esTautologia c) se verifica si c es una tautolog\u00eda. Por\n-- ejemplo, \n--    esTautologia [1,2,-1]  ==  True\n--    esTautologia [1,2,-3]  ==  False\n--    esTautologia []        ==  False\n-- ---------------------------------------------------------------------\n\nesTautologia :: Clausula -> Bool\nesTautologia = esValidaClausula\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    eliminaTautologias :: FNC -> FNC\n-- tal que (eliminaTautologias s) es el conjunto obtenido eliminando las\n-- tautolog\u00edas de s. Por ejemplo,\n--    eliminaTautologias [[1,2],[1,3,-1]]  ==  [[1,2]]\n-- ---------------------------------------------------------------------\n\neliminaTautologias :: FNC -> FNC\neliminaTautologias s =\n  [c | c <- s, not (esTautologia c)]\n\n-- ---------------------------------------------------------------------\n-- \u00a7 Eliminaci\u00f3n de cl\u00e1usulas unitarias\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esUnitaria :: Clausula -> Bool\n-- tal que (esUnitaria c) se verifica si la cl\u00e1usula c es unitaria . Por\n-- ejemplo, \n--    esUnitaria [3]    ==  True\n--    esUnitaria [-3]   ==  True\n--    esUnitaria [3,2]  ==  False\n--    esUnitaria []     ==  False\n-- ---------------------------------------------------------------------\n\nesUnitaria :: Clausula -> Bool\nesUnitaria [_] = True\nesUnitaria _   = False\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    eliminaClausulaUnitaria :: Literal -> FNC -> FNC\n-- tal que (eliminaClausulaUnitaria l s) es el conjunto obtenido al\n-- reducir s por la eliminaci\u00f3n de la cl\u00e1usula unitaria formada por el\n-- literal l. Por ejemplo,\n--    \u03bb> eliminaClausulaUnitaria (-1) [[1,2,-3],[1,-2],[-1],[3]]\n--    [[2,-3],[-2],[3]]\n--    \u03bb> eliminaClausulaUnitaria (-2) [[2,-3],[-2],[3]]\n--    [[-3],[3]]\n--    \u03bb> eliminaClausulaUnitaria (-3) [[-3],[3],[1]]\n--    [[],[1]]\n-- ---------------------------------------------------------------------\n\neliminaClausulaUnitaria :: Literal -> FNC -> FNC\neliminaClausulaUnitaria l s =\n  [delete (complementario l) c | c <- s, notElem l c]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    clausulaUnitaria :: FNC -> Maybe Literal\n-- tal que (clausulaUnitaria s) es la primera cl\u00e1usula unitaria de s, si\n-- s tiene cl\u00e1usulas unitarias y nada en caso contrario. Por ejemplo,\n--    clausulaUnitaria [[1,2],[1],[-2]]  ==  Just 1\n--    clausulaUnitaria [[1,2],[1,-2]]  ==  Nothing\n-- ---------------------------------------------------------------------\n\nclausulaUnitaria :: FNC -> Maybe Literal\nclausulaUnitaria [] = Nothing\nclausulaUnitaria (c:cs) \n  | esUnitaria c = Just (head c)\n  | otherwise    = clausulaUnitaria cs\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    eliminaClausulasUnitarias :: FNC -> FNC\n-- tal que (eliminaClausulasUnitarias s) es el conjunto obtenido\n-- aplicando el proceso de eliminaci\u00f3n de cl\u00e1usulas unitarias a s. Por\n-- ejemplo, \n--    \u03bb> eliminaClausulasUnitarias [[1,2,-3],[1,-2],[-1],[3],[5]]\n--    [[],[5]]\n--    \u03bb> eliminaClausulasUnitarias [[1,2],[-2],[-1,2,-3]]\n--    []\n--    \u03bb> eliminaClausulasUnitarias [[-1,2],[1],[3,5]]\n--    [[3,5]]\n-- ---------------------------------------------------------------------\n\neliminaClausulasUnitarias :: FNC -> FNC\neliminaClausulasUnitarias s \n  | elem [] s                     = s\n  | clausulaUnitaria s == Nothing = s \n  | otherwise                     =\n      eliminaClausulasUnitarias (eliminaClausulaUnitaria c s)\n  where Just c = clausulaUnitaria s\n\n-- ---------------------------------------------------------------------\n-- Eliminaci\u00f3n de literales puros                                     --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    literales :: FNC -> [Literal]\n-- tal que (literales f) es el conjunto de literales de f. Por ejemplo,\n--    literales [[1,2,-3],[1,2,-1]]  ==  [1,2,-3,-1]\n-- ---------------------------------------------------------------------\n\nliterales :: FNC -> [Literal]\nliterales = unionGeneral\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esLiteralPuro :: Literal -> FNC -> Bool\n-- tal que (esLiteralPuro l f) se verifica si l es puro en f. Por\n-- ejemplo, \n--    esLiteralPuro 1 [[1,2],[1,-2],[3,2],[3,-2]]  ==  True\n--    esLiteralPuro 2 [[1,2],[1,-2],[3,2],[3,-2]]  ==  False\n-- ---------------------------------------------------------------------\n\nesLiteralPuro :: Literal -> FNC -> Bool\nesLiteralPuro l f =\n  and [notElem l' c | c <- f]\n  where l' = complementario l\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    eliminaLiteralPuro :: Literal -> FNC -> FNC\n-- tal que (eliminaLiteralPuro l f) es el conjunto obtenido eliminando\n-- el literal puro l de f. Por ejemplo,\n--    eliminaLiteralPuro 1 [[1,2],[1,-2],[3,2],[3,-2]]  ==  [[3,2],[3,-2]]\n--    eliminaLiteralPuro 3 [[3,2],[3,-2]]  ==  []\n-- ---------------------------------------------------------------------\n\neliminaLiteralPuro :: Literal -> FNC -> FNC\neliminaLiteralPuro l f =\n  [c | c <- f, l `notElem` c]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    literalesPuros :: FNC -> [Literal]\n-- tal que (literalesPuros f) es el conjunto de los literales puros de\n-- f. Por ejemplo, \n--    literalesPuros [[1,2],[1,-2],[3,2],[3,-2]]  ==  [1,3]\n-- ---------------------------------------------------------------------\n\nliteralesPuros :: FNC -> [Literal]\nliteralesPuros f =\n  [l | l <- literales f, esLiteralPuro l f] \n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    eliminaLiteralesPuros :: FNC -> FNC\n-- tal que (eliminaLiteralesPuros f) es el conjunto obtenido aplicando a\n-- f el proceso de eliminaci\u00f3n de literales puros. Por ejemplo,\n--    eliminaLiteralesPuros [[1,2],[1,-2],[3,2],[3,-2]]  ==  []\n--    eliminaLiteralesPuros [[1,2],[3,-5],[-3,5]]  ==  [[3,-5],[-3,5]]\n-- ---------------------------------------------------------------------\n\neliminaLiteralesPuros :: FNC -> FNC\neliminaLiteralesPuros f \n  | null lp   = f\n  | otherwise = \n      eliminaLiteralesPuros (eliminaLiteralPuro (head lp) f)\n  where lp = literalesPuros f\n\n-- ---------------------------------------------------------------------\n-- \u00a7 Bifurcaci\u00f3n\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    bifurcacion :: FNC -> Literal -> (FNC,FNC)\n-- tal que (bifurcacion f l) es la bifurcaci\u00f3n de f seg\u00fan el literal\n-- l. Por ejemplo, \n--    \u03bb> bifurcacion [[1,-2],[-1,2],[2,-3],[-2,-3]] 1\n--    ([[-2],[2,-3],[-2,-3]],[[2],[2,-3],[-2,-3]])\n-- ---------------------------------------------------------------------\n\nbifurcacion :: FNC -> Literal -> (FNC,FNC)\nbifurcacion f l =\n  ([delete l c  | c <- f, elem l c]  ++ cl\u00e1usulas_sin_l_ni_l',\n   [delete l' c | c <- f, elem l' c] ++ cl\u00e1usulas_sin_l_ni_l')\n  where l'                    = complementario l\n        cl\u00e1usulas_sin_l_ni_l' = [c | c <- f, notElem l c, notElem l' c]\n\n-- ---------------------------------------------------------------------\n-- \u00a7 Algoritmo de Davis y Putnam (DP)\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    tieneClausulasUnitarias :: FNC -> Bool\n-- tal que (tieneClausulasUnitarias f) se verifica si f tiene cl\u00e1usulas\n-- unitarias. Por ejemplo, \n--    tieneClausulasUnitarias [[1,2],[1],[-2]]  ==  True\n--    tieneClausulasUnitarias [[1,2],[1,-2]]  ==  False\n-- ---------------------------------------------------------------------\n\ntieneClausulasUnitarias :: FNC -> Bool\ntieneClausulasUnitarias f =\n  clausulaUnitaria f \/= Nothing\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    tieneLiteralesPuros :: FNC -> Bool\n-- tal que (tieneLiteralesPuros f) se verifica si f tiene literales\n-- puros. Por ejemplo, \n--    tieneLiteralesPuros [[1,2],[1,-2],[3,2],[3,-2]]    ==  True\n--    tieneLiteralesPuros [[1,2],[-1,-2],[-3,2],[3,-2]]  ==  False\n-- ---------------------------------------------------------------------\n\ntieneLiteralesPuros :: FNC -> Bool\ntieneLiteralesPuros f =\n  not (null (literalesPuros f))\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esInsatisfaciblePorDP :: FNC -> Bool\n-- tal que (esInsatisfaciblePorDP f) se verifica si f es insatisfacible\n-- mediante el algoritmo de Davis y Putnam. Por ejemplo, \n--    esInsatisfaciblePorDP [[1,2],[1,2,-1]]                ==  False\n--    esInsatisfaciblePorDP [[1,2,-3],[1,-2],[-1],[3],[5]]  ==  True\n--    esInsatisfaciblePorDP [[1,2],[-2],[-1,2,-3]]          ==  False\n--    esInsatisfaciblePorDP [[-1,2],[1],[3,5]]              ==  False\n--    esInsatisfaciblePorDP [[1,2],[1,-2],[3,2],[3,-2]]     ==  False\n--    esInsatisfaciblePorDP [[1,2],[3,-4],[-3,4]]           ==  False\n-- ---------------------------------------------------------------------\n\nesInsatisfaciblePorDP :: FNC -> Bool\nesInsatisfaciblePorDP f =\n  esInsatisfaciblePorDP' (eliminaTautologias f)\n\nesInsatisfaciblePorDP' :: FNC -> Bool\nesInsatisfaciblePorDP' f\n  | null f = False\n  | elem [] f = True\n  | tieneClausulasUnitarias f = \n      esInsatisfaciblePorDP' (eliminaClausulasUnitarias f)\n  | tieneLiteralesPuros f =\n      esInsatisfaciblePorDP' (eliminaLiteralesPuros f)\n  | otherwise = \n      (esInsatisfaciblePorDP' s1) && (esInsatisfaciblePorDP' s2)\n  where l       = head (head f)\n        (s1,s2) = bifurcacion f l\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esSatisfaciblePorDP :: FNC -> Bool\n-- tal que (esSatisfaciblePorDP f) se verifica si f es satisfacible\n-- mediante el algoritmo de Davis y Putnam. Por ejemplo, \n--    esSatisfaciblePorDP [[1,2],[1,2,-1]]                ==  True\n--    esSatisfaciblePorDP [[1,2,-3],[1,-2],[-1],[3],[5]]  ==  False\n-- ---------------------------------------------------------------------\n\nesSatisfaciblePorDP :: FNC -> Bool\nesSatisfaciblePorDP = not . esInsatisfaciblePorDP \n\n-- ---------------------------------------------------------------------\n-- \u00a7 Correcci\u00f3n del algoritmo de Davis y Putnam                       --\n-- ---------------------------------------------------------------------\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Comprobar con QuickCheck que el algoritmo De Davis y\n-- Putnam es correcto; es decir, para toda f\u00f3rmula f, f es\n-- insatisfacible seg\u00fan el algoritmo de Davis y Putnam si,y solo si, f\n-- es insatisfacible.\n-- ---------------------------------------------------------------------\n\nprop_CorreccionDP :: FNC -> Bool\nprop_CorreccionDP f =\n  esInsatisfaciblePorDP f == esInsatisfacible f\n\n-- La comprobaci\u00f3n es\n--    \u03bb> quickCheckWith (stdArgs {maxSize=10}) prop_CorreccionDP\n--    +++ OK, passed 100 tests.\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado una implementaci\u00f3n del algoritmo de Davis-Putnam en Haskell y comprobado su correcci\u00f3n con QuickCheck. En primer lugar se ha estudiado una implementaci\u00f3n de la l\u00f3gica clausal en Haskell en la que se han definido los \u00e1tomos, literales, cl\u00e1usulas,&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[333],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6979"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=6979"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6979\/revisions"}],"predecessor-version":[{"id":6982,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6979\/revisions\/6982"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6979"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6979"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6979"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}