{"id":6983,"date":"2020-02-06T10:03:21","date_gmt":"2020-02-06T09:03:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6983"},"modified":"2020-02-08T10:04:49","modified_gmt":"2020-02-08T09:04:49","slug":"ra2019-reduccion-de-sat-a-clique-en-haskell","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-reduccion-de-sat-a-clique-en-haskell\/","title":{"rendered":"RA2019: Reducci\u00f3n de SAT a Clique en Haskell"},"content":{"rendered":"

En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico<\/a> se ha estudiado una implementaci\u00f3n de la reducci\u00f3n del problema SAT al problema Clique.<\/p>\n

En primer lugar se ha estudiado una implementaci\u00f3n del problema del Clique en la que se ha definido los grafos no ordenados (como pares de nodos), los cliques y c\u00f3mo calcular los clique de un tama\u00f1o dado.<\/p>\n

A continuaci\u00f3n se ha estudiado c\u00f3mo asociar a una f\u00f3rmula en forma normal conjuntiva un grafo tal que la f\u00f3rmula es satisfacible si, y s\u00f3lo si, el grafo tiene un clique cuyo tama\u00f1o sea el n\u00famero de cl\u00e1usulas de la f\u00f3rmula<\/p>\n

Los c\u00f3digos usados en la presentaci\u00f3n son los siguientes:<\/p>\n

<\/p>\n

C\u00f3digo del prolblema del Clique<\/h2>\n
\n-- Cliques.hs\n-- El problema del clique.\n-- Jos\u00e9 A. Alonso Jim\u00e9nez\n-- Sevilla, 6 de febrero de 2020\n-- ---------------------------------------------------------------------\n\nmodule Cliques where\n\nimport Data.List\n\n-- ---------------------------------------------------------------------\n-- Un grafo no dirigido se representa por la lista de sus arcos. Por\n-- ejemplo, el grafo\n--              1  -- 2 -- 4\n--                    | \\  |\n--                    |  \\ |\n--                    3 -- 5\n-- se representa por [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)].\n\n--\n-- Definir el tipo Grafo.\n-- ---------------------------------------------------------------------\n\ntype Grafo a = [(a,a)]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    nodos :: Eq a => Grafo a -> [a]\n-- tal que (nodos g) es la lista de los nodos del grafo g. Por ejemplo,\n--    nodos [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)]  ==  [1,2,3,4,5]\n-- ---------------------------------------------------------------------\n\nnodos :: Eq a => Grafo a -> [a]\nnodos g = nub (concat [[x,y] | (x,y) <- g])\n\n-- ---------------------------------------------------------------------\n-- Ejercicio: Definir la funci\u00f3n\n--    conectados :: Eq a => Grafo a -> a -> a -> Bool\n-- tal que (conectados g x y) se verifica si el grafo no dirigido g\n-- posee un arco con extremos x e y. Por ejemplo,\n--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3 2  ==  True\n--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 2 3  ==  True\n--    conectados [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3 4  ==  False\n-- ---------------------------------------------------------------------\n\nconectados :: Eq a => Grafo a -> a -> a -> Bool\nconectados g x y =\n  (x,y) `elem` g || (y,x) `elem` g \n\n-- ---------------------------------------------------------------------\n-- Ejercicio: Definir la funci\u00f3n\n--    parejas :: [a] -> [(a,a)]\n-- tal que (parejas xs) es la lista de las parejas formados por los\n-- elementos de xs y sus siguientes en xs. Por ejemplo,\n--    parejas [1..4] == [(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)]\n-- ---------------------------------------------------------------------\n\nparejas :: [a] -> [(a,a)]\nparejas xs =\n  [(x,y) | (x:ys) <- tails xs\n         , y <- ys]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Un clique (en espa\u00f1ol, pandilla) de un grafo g es un\n-- conjunto de nodos de g tal que todos sus elementos est\u00e1n conectados\n-- en g.\n--\n-- Definir la funci\u00f3n\n--    esClique :: Eq a => Grafo a -> [a] -> Bool\n-- tal que (esClique g xs) se verifica si el conjunto de nodos xs del\n-- grafo g es un clique de g.Por ejemplo,\n--    esClique [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] [2,3,5]  ==  True\n--    esClique [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] [2,3,4]  ==  False\n-- ---------------------------------------------------------------------\n\nesClique :: Eq a => Grafo a -> [a] -> Bool\nesClique g xs =\n  and [conectados g x y | (x,y) <- parejas xs]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    cliques :: Eq a => Grafo a -> [[a]]\n-- tal que (cliques g) es la lista de los cliques del grafo g. Por\n-- ejemplo, \n--    \u03bb> cliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)]\n--    [[],[1],[2],[1,2],[3],[2,3],[4],[2,4],\n--     [5],[2,5],[3,5],[2,3,5],[4,5],[2,4,5]]\n-- ---------------------------------------------------------------------\n\ncliques :: Eq a => Grafo a -> [[a]]\ncliques g =\n  [xs | xs <- subsequences (nodos g)\n      , esClique g xs]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n \n--    kSubconjuntos :: [a] -> Int -> [[a]]\n-- tal que (kSubconjuntos xs k) es la lista de los subconjuntos de xs\n-- con k elementos. Por ejemplo,\n--    ghci> kSubconjuntos \"bcde\" 2\n--    [\"bc\",\"bd\",\"be\",\"cd\",\"ce\",\"de\"]\n--    ghci> kSubconjuntos \"bcde\" 3\n--    [\"bcd\",\"bce\",\"bde\",\"cde\"]\n--    ghci> kSubconjuntos \"abcde\" 3\n--    [\"abc\",\"abd\",\"abe\",\"acd\",\"ace\",\"ade\",\"bcd\",\"bce\",\"bde\",\"cde\"]\n-- ---------------------------------------------------------------------\n \nkSubconjuntos :: [a] -> Int -> [[a]]\nkSubconjuntos _ 0      = [[]]\nkSubconjuntos [] _     = []\nkSubconjuntos (x:xs) k = \n  [x:ys | ys <- kSubconjuntos xs (k-1)] ++ kSubconjuntos xs k  \n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    kCliques :: Eq a => Grafo a -> Int -> [[a]]\n-- tal que (cliques g k) es la lista de los cliques del grafo g de\n-- tama\u00f1o k. Por ejemplo, \n--    \u03bb> kCliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 3\n--    [[2,3,5],[2,4,5]]\n--    \u03bb> kCliques [(1,2),(2,3),(2,4),(2,5),(3,5),(4,5)] 2\n--    [[1,2],[2,3],[2,4],[2,5],[3,5],[4,5]]\n-- ---------------------------------------------------------------------\n\n-- 1\u00aa definici\u00f3n\nkCliques1 :: Eq a => Grafo a -> Int -> [[a]]\nkCliques1 g k =\n  [xs | xs <- cliques g\n      , length xs == k]\n\n-- 2\u00aa definici\u00f3n\nkCliques :: Eq a => Grafo a -> Int -> [[a]]\nkCliques g k =\n  [xs | xs <- kSubconjuntos (nodos g) k\n      , esClique g xs]\n\n-- Comparaci\u00f3n de eficiencia\n-- =========================\n\n--    \u03bb> kCliques1 [(n,n+1) | n <- [1..20]] 3\n--    []\n--    (4.28 secs, 3,204,548,608 bytes)\n--    \u03bb> kCliques [(n,n+1) | n <- [1..20]] 3\n--    []\n--    (0.01 secs, 3,075,768 bytes)\n<\/pre>\n
C\u00f3digo de la reducci\u00f3n de SAT a Clique<\/h2>\n
\n-- SAT_Clique.hs\n-- Reducci\u00f3n de SAT a Clique.\n-- Jos\u00e9 A. Alonso Jim\u00e9nez\n-- Sevilla, 6 de febrero de 2020\n-- ---------------------------------------------------------------------\n\nmodule SAT_Clique where\n\nimport SAT\nimport Cliques\nimport Data.List\nimport Test.QuickCheck\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    nodosFNC :: FNC -> [(Int,Literal)]\n-- tal que (nodosFNC f) es la lista de los literales de las cl\u00e1uslas de\n-- f junto con el n\u00famero de la cl\u00e1usula. Por ejemplo,\n--    \u03bb> nodosFNC [[1,-2,3],[-1,2],[-2,3]]\n--    [(0,1),(0,-2),(0,3),(1,-1),(1,2),(2,-2),(2,3)]\n-- ---------------------------------------------------------------------\n\nnodosFNC :: FNC -> [(Int,Literal)]\nnodosFNC f = \n  [(i,x) | (i,xs) <- zip [0..] f\n         , x <- xs]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. El grafo correspondiente a una f\u00f3rmula f en FNC tiene como\n-- nodos (nodosFNC f). Hay un arco entre los nodos correspondientes a\n-- cl\u00e1usulas distintas cuyos literales no son complementarios. Por\n-- ejemplo, \n-- \n-- Definir la funci\u00f3n\n--    grafoFNC :: FNC -> Grafo (Int,Literal)\n-- tal que (grafo FNC f) es el grafo de f. Por ejemplo, \n--    \u03bb> grafoFNC [[1,-2,3],[-1,2],[-2,3]]\n--    [ ((0,1),(1,2)),  ((0,1),(2,-2)), ((0,1),(2,3)),\n--      ((0,-2),(1,-1)),((0,-2),(2,-2)),((0,-2),(2,3)),\n--      ((0,3),(1,-1)), ((0,3),(1,2)),  ((0,3),(2,-2)),((0,3),(2,3)),\n--      ((1,-1),(2,-2)),((1,-1),(2,3)),\n--      ((1,2),(2,3))]\n--    \u03bb> grafoFNC [[1,2],[1,-2],[-1,2],[-1,-2]]\n--    [((0,1),(1,1)),((0,1),(1,-2)),((0,1),(2,2)),((0,1),(3,-2)),\n--     ((0,2),(1,1)),((0,2),(2,-1)),((0,2),(2,2)),((0,2),(3,-1)),\n--     ((1,1),(2,2)),((1,1),(3,-2)),\n--     ((1,-2),(2,-1)),((1,-2),(3,-1)),((1,-2),(3,-2)),\n--     ((2,-1),(3,-1)),((2,-1),(3,-2)),\n--     ((2,2),(3,-1))]\n-- ---------------------------------------------------------------------\n\ngrafoFNC :: FNC -> Grafo (Int,Literal)\ngrafoFNC f = \n  [ ((i,x),(i',x'))\n  | ((i,x),(i',x')) <- parejas (nodosFNC f)\n  , i' \/= i\n  , x' \/= complementario x]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    cliquesFNC :: FNC -> [[(Int,Literal)]]\n-- tal que (cliquesFNCf) es la lista de los cliques del grafo de f. Por\n-- ejemplo, \n--    \u03bb> cliquesFNC [[1,-2,3],[-1,2],[-2,3]]\n--    [[], [(0,1)], [(1,2)], [(0,1),(1,2)], [(2,-2)],\n--     [(0,1),(2,-2)], [(2,3)], [(0,1),(2,3)], [(1,2),(2,3)],\n--     [(0,1),(1,2),(2,3)], [(0,-2)], [(2,-2),(0,-2)], [(2,3),(0,-2)],\n--     [(1,-1)], [(2,-2),(1,-1)], [(2,3),(1,-1)], [(0,-2),(1,-1)],\n--     [(2,-2),(0,-2),(1,-1)], [(2,3),(0,-2),(1,-1)], [(0,3)],\n--     [(1,2),(0,3)], [(2,-2),(0,3)], [(2,3),(0,3)],\n--     [(1,2),(2,3),(0,3)], [(1,-1),(0,3)],\n--     [(2,-2),(1,-1),(0,3)], [(2,3),(1,-1),(0,3)]]\n-- ---------------------------------------------------------------------\n\ncliquesFNC :: FNC -> [[(Int,Literal)]]\ncliquesFNC f = cliques (grafoFNC f)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    cliquesCompletos :: FNC -> [[(Int,Literal)]]\n-- tal que (cliquesCompletos f) es la lista de los cliques del grafo de\n-- f que tiene elmismo n\u00famero de elementos que el n\u00famero de cl\u00e1usulas de\n-- f. Por ejemplo,\n--    \u03bb> cliquesCompletos [[1,-2,3],[-1,2],[-2,3]]\n--    [[(0,1),(1,2),(2,3)],   [(2,-2),(0,-2),(1,-1)],\n--     [(2,3),(0,-2),(1,-1)], [(1,2),(2,3),(0,3)],\n--     [(2,-2),(1,-1),(0,3)], [(2,3),(1,-1),(0,3)]]\n--    \u03bb> cliquesCompletos [[1,2],[1,-2],[-1,2],[-1,-2]]\n--    []\n-- ---------------------------------------------------------------------\n\ncliquesCompletos :: FNC -> [[(Int,Literal)]]\ncliquesCompletos cs = kCliques (grafoFNC cs) (length cs)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    esSatisfaciblePorClique :: FNC -> Bool\n-- tal que (esSatisfaciblePorClique f) se verifica si f no contiene la\n-- cl\u00e1usula vac\u00eda, tiene m\u00e1 de una cl\u00e1usula y posee alg\u00fan clique\n-- completo. Por ejemplo, \n--    \u03bb> esSatisfaciblePorClique [[1,-2,3],[-1,2],[-2,3]]\n--    True\n--    \u03bb> esSatisfaciblePorClique [[1,2],[1,-2],[-1,2],[-1,-2]]\n--    False\n-- ---------------------------------------------------------------------\n\nesSatisfaciblePorClique :: FNC -> Bool\nesSatisfaciblePorClique f =\n     [] `notElem` f'\n  && (length f' <= 1 || not (null (cliquesCompletos f')))\n  where f' = nub (map (nub . sort) f) \n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Comprobar con QuickCheck que toda f\u00f3rmula es satisfacible\n-- si, y solo si, es satisfacible por Clique.\n-- ---------------------------------------------------------------------\n\nprop_esSatisfaciblePorClique :: FNC -> Bool\nprop_esSatisfaciblePorClique f =\n  esSatisfacible f == esSatisfaciblePorClique f\n\n-- La comprobaci\u00f3n es\n--    \u03bb> quickCheckWith (stdArgs {maxSize=7}) prop_esSatisfaciblePorClique\n--    +++ OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Definir la funci\u00f3n\n--    modelosCliqueFNC :: FNC -> [Interpretacion]\n-- tales que (modelosCliqueFNC f) es la lista de los modelos de f\n-- calculados mediante los cliques completos del grafo de f. Por ejemplo,\n--    \u03bb> modelosCliqueFNC [[1,-2,3],[-1,2],[-2,3]]\n--    [[],[1,2,3],[2,3],[3]]\n--    \u03bb> modelosCliqueFNC [[1,-2,3],[3,2],[-2,3]]\n--    [[1,2,3],[1,3],[2,3],[3]]\n-- ---------------------------------------------------------------------\n\nmodelosCliqueFNC :: FNC -> [Interpretacion]\nmodelosCliqueFNC f \n  | [] `elem` f'   = []\n  | length f' == 1 = [[a | c <- f', a <- c, a > 0]]\n  |otherwise       = sort (nub (map nub [ modeloClique xs\n                                        | xs <- cliquesCompletos f]))\n  where f' = nub (map (nub . sort) f) \n        modeloClique xs = [x | (_,x) <- xs, x > 0]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio. Comprobar con QuickCheck que, para toda f\u00f3rmula f en FNC,\n-- todos los elementos de (modelosCliqueFNC f) son modelos de f.\n-- ---------------------------------------------------------------------\n\nprop_modelosPorClique :: FNC -> Bool\nprop_modelosPorClique f =\n  and [esModelo i f | i <- modelosCliqueFNC f]\n\n-- La comprobaci\u00f3n es\n--    \u03bb> quickCheckWith (stdArgs {maxSize=7}) prop_modelosPorClique\n--    +++ OK, passed 100 tests.\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado una implementaci\u00f3n de la reducci\u00f3n del problema SAT al problema Clique. En primer lugar se ha estudiado una implementaci\u00f3n del problema del Clique en la que se ha definido los grafos no ordenados (como pares de nodos), los…<\/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\/6983"}],"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=6983"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6983\/revisions"}],"predecessor-version":[{"id":6985,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6983\/revisions\/6985"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6983"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6983"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6983"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}