{"id":57551,"date":"2018-03-09T22:45:19","date_gmt":"2018-03-09T22:45:19","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/design-and-implementation-of-exact-max-sat-solvers\/"},"modified":"2018-03-09T22:45:19","modified_gmt":"2018-03-09T22:45:19","slug":"design-and-implementation-of-exact-max-sat-solvers","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/ciencias-tecnologicas\/design-and-implementation-of-exact-max-sat-solvers\/","title":{"rendered":"Design and implementation of exact max-sat solvers"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Jordi Planes Cid <\/strong><\/h2>\n<p>El problema de la satisfactibilidad (sat) es el problema que trata de decidir si una assignaci\u00f3n de verdad satisface una f\u00f3rmula cnf. Hoy en d\u00eda, diferentes problemas combinatorios duros tales como problemas de verificaci\u00f3n de hardware y software se pueden solucionar eficientmente codific\u00e1ndolos en sat. en esta tesis, nos centramos en el problema de m\u00e1xima satisfactibilidad (max-sat), una versi\u00f3n de optimizaci\u00f3n de sat que consiste en encontrar la assignaci\u00f3n de verdad que satisface el m\u00e1ximo n\u00famero de cl\u00e1usulas en una f\u00f3rmula cnf. Tambi\u00e9n consideramos una variante de max-sat, llamada max-sat ponderado, donde cada cl\u00e1usula tiene un peso asociado y el problema consiste en encontrar la asignaci\u00f3n de verdad en que la suma de los pesos de las cl\u00e1usulas violadas es minimal. Mientras sat es np-completo y apropiado para codificar y resolver problemas de decisi\u00f3n, max-sat y max-sat ponderado son  np-dif\u00edciles y apropiados para codificar y resolver problemas de optimitzaci\u00f3n. esta tesis se centra en el dise\u00f1o, la implementaci\u00f3n y la evaluaci\u00f3n de resolvedores exactos de max-sat basados en el esquema de ramificaci\u00f3n y poda, con un \u00e9nfasis especial en el disse\u00f1o de buenas cotas inferiores, buenas t\u00e9cnicas de inferencia y estructuras de datos apropiadas. en primer lugar, hemos definido tres m\u00e9todos de computaci\u00f3n de cotas inferiores: la regla estrella, up, y up mejorado con detecci\u00f3n de literales fallidos. Todos ellos computan una estimaci\u00f3n del n\u00famero de cl\u00e1usulas que se van a insatisfacer  si la asignaci\u00f3n parcial se completa. Esta estimaci\u00f3n es el n\u00famero de subconjuntos disjuntos que pueden ser declarados insatisfactibles derivando, en tiempo polinomial, una refutaci\u00f3n de resoluci\u00f3n de las cl\u00e1usulas del subconjunto. La regla estrella considera subconjutos formados por n cl\u00e1usulas unitarias y una cl\u00e1usula n-aria que es la disjunci\u00f3n de los literales complementarios de los literales que ocurren en les cl\u00e1usulas unitarias; una refut<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Design and implementation of exact max-sat solvers<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Design and implementation of exact max-sat solvers <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Jordi Planes Cid <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Lleida<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 16\/03\/2007<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Felip Many\u00c1\u00a0 Serres<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: pedro Meseguer gonz\u00e1lez <\/li>\n<li>hans Van maaren (vocal)<\/li>\n<li>Francisco Javier Larrosa bondia (vocal)<\/li>\n<li>daniel Le berre (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Jordi Planes Cid El problema de la satisfactibilidad (sat) es el problema que trata de decidir si [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[332,18842,3747],"tags":[127164,40763,97219,127163,127162,78299],"class_list":["post-57551","post","type-post","status-publish","format-standard","hentry","category-ciencias-tecnologicas","category-lleida","category-logica","tag-daniel-le-berre","tag-felip-manya-serres","tag-francisco-javier-larrosa-bondia","tag-hans-van-maaren","tag-jordi-planes-cid","tag-pedro-meseguer-gonzalez"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/57551","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=57551"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/57551\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=57551"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=57551"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=57551"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}