{"id":5600,"date":"2020-02-27T05:30:20","date_gmt":"2020-02-27T03:30:20","guid":{"rendered":"http:\/\/www.glc.us.es\/~jalonso\/exercitium\/?p=5600"},"modified":"2020-03-05T08:30:43","modified_gmt":"2020-03-05T06:30:43","slug":"reduccion-de-sat-a-clique","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/reduccion-de-sat-a-clique\/","title":{"rendered":"Reducci\u00f3n de SAT a Clique"},"content":{"rendered":"<p>Nota: En este ejercicio se usa la misma notaci\u00f3n que en los anteriores importando los m\u00f3dulos<\/p>\n<pre lang=\"text\">\n+ Evaluacion_de_FNC\n+ Modelos_de_FNC\n+ Problema_SAT_para_FNC\n+ Cliques\n+ KCliques\n+ Grafo_FNC\n<\/pre>\n<p>Definir las funciones<\/p>\n<pre lang=\"text\">\n   cliquesFNC :: FNC -> [[(Int,Literal)]]\n   cliquesCompletos :: FNC -> [[(Int,Literal)]]\n   esSatisfaciblePorClique :: FNC -> Bool\n<\/pre>\n<p>tales que<\/p>\n<ul>\n<li>(cliquesFNCf) es la lista de los cliques del grafo de f. Por ejemplo, <\/li>\n<\/ul>\n<pre lang=\"text\">  \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<\/pre>\n<ul>\n<li>(cliquesCompletos f) es la lista de los cliques del grafo de f que tiene tantos elementos como cl\u00e1usulas tiene f. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\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<\/pre>\n<ul>\n<li>(esSatisfaciblePorClique f) se verifica si f no contiene la cl\u00e1usula vac\u00eda, tiene m\u00e1s de una cl\u00e1usula y posee alg\u00fan clique completo. Por ejemplo, <\/li>\n<\/ul>\n<pre lang=\"text\">  \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<\/pre>\n<p>Comprobar con QuickCheck que toda f\u00f3rmula en FNC es satisfacible si, y solo si, es satisfacible por Clique.<\/p>\n<h4>Soluciones<\/h4>\n<pre lang=\"haskell\">\nmodule Reduccion_de_SAT_a_Clique where\n\nimport Evaluacion_de_FNC\nimport Modelos_de_FNC\nimport Problema_SAT_para_FNC\nimport Cliques\nimport KCliques\nimport Grafo_FNC\nimport Data.List (nub, sort)\nimport Test.QuickCheck\n\ncliquesFNC :: FNC -> [[(Int,Literal)]]\ncliquesFNC f = cliques (grafoFNC f)\n\ncliquesCompletos :: FNC -> [[(Int,Literal)]]\ncliquesCompletos cs = kCliques (grafoFNC cs) (length cs)\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-- La propiedad es\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<\/pre>\n<h4>Otras soluciones<\/h4>\n<ul>\n<li>Se pueden escribir otras soluciones en los comentarios.\n<li>El c\u00f3digo se debe escribir entre una l\u00ednea con &#60;pre lang=\u00bbhaskell\u00bb&#62; y otra con &#60;\/pre&#62;\n<\/ul>\n<h4>Pensamiento<\/h4>\n<blockquote><p>\n\u00abLa resoluci\u00f3n de problemas es una habilidad pr\u00e1ctica como, digamos, la nataci\u00f3n. Adquirimos cualquier habilidad pr\u00e1ctica por imitaci\u00f3n y pr\u00e1ctica. Tratando de nadar, imitas lo que otras personas hacen con sus manos y pies para mantener sus cabezas sobre el agua, y, finalmente, aprendes a nadar practicando la nataci\u00f3n. Al intentar resolver problemas, hay que observar e imitar lo que hacen otras personas al resolver problemas y, finalmente, se aprende a resolver problemas haci\u00e9ndolos.\u00bb <\/p>\n<p><a href=\"https:\/\/en.wikipedia.org\/wiki\/George_P%C3%B3lya\">George P\u00f3lya<\/a>.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Nota: En este ejercicio se usa la misma notaci\u00f3n que en los anteriores importando los m\u00f3dulos + Evaluacion_de_FNC + Modelos_de_FNC + Problema_SAT_para_FNC + Cliques + KCliques + Grafo_FNC Definir las funciones cliquesFNC :: FNC -> [[(Int,Literal)]] cliquesCompletos :: FNC -> [[(Int,Literal)]] esSatisfaciblePorClique :: FNC -> Bool tales que (cliquesFNCf) es la lista de los cliques&#8230;<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","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":[7],"tags":[28,10,181,27,24,141,11,14,146],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/posts\/5600"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/comments?post=5600"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/posts\/5600\/revisions"}],"predecessor-version":[{"id":5658,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/posts\/5600\/revisions\/5658"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/media?parent=5600"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/categories?post=5600"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/tags?post=5600"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}