Design and implementation of exact max-sat solvers

• Autores: Jordi Planes Cid
• Directores de la Tesis: Felip Manyà Serres (dir. tes.) , Min Li Chu (dir. tes.)
• Lectura: En la Universitat de Lleida ( España ) en 2007
• Idioma: español
• Tribunal Calificador de la Tesis: Pedro Meseguer González (presid.) , Jordi Levy Díaz (secret.) , Francisco Javier Larrosa Bondia (voc.) , Daniel Le Berre (voc.) , Hans Van Maaren (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • El problema de la satisfactibilidad (SAT) es el problema que trata de decidir si una assignación de verdad satisface una fórmula CNF, Hoy en día, diferentes problemas combinatorios duros tales como problemas de verificación de hardware y software se pueden solucionar eficientmente codificándolos en SAT.

    En esta tesis, nos centramos en el problema de máxima satisfactibilidad (MAX-SAT), una versión de optimización de SAT que consiste en encontrar la assignación de verdad que satisface el máximo número de cláusulas en una fórmula CNF. También consideramos una variante de MAX-SAT, llamada MAX-SAT ponderado, donde cada cláusula tiene un peso asociado y el problema consiste en encontrar la asignación de verdad en que la suma de los pesos de las cláusulas violadas es minimal. Mientras SAT es NP-completo y apropiado para codificar y resolver problemas de decisión, MAX-SAT y MAX-SAT ponderado son NP-difíciles y apropiados para codificar y resolver problemas de optimitzación.

    Esta tesis se centra en el diseño, la implementación y la evaluación de resolvedores exactos de MAX-SAT basados en el esquema de ramificación y poda, con un énfasis especial en el disseño de buenas cotas inferiores, buenas técnicas de inferencia y estructuras de datos apropiadas.

    En primer lugar, hemos definido tres métodos de computación de cotas inferiores: la regla estrella, UP, y UP mejorado con detección de literales fallidos. Todos ellos computan una estimación del número de cláusulas que se van a insatisfacer si la asignación parcial se completa. Esta estimación es el número de subconjuntos disjuntos que pueden ser declarados insatisfactibles derivando, en tiempo polinomial, una refutación de resolución de las cláusulas del subconjunto. La regla estrella considera subconjutos formados por n cláusulas unitarias y una cláusula n-aria que es la disjunción de los literales complementarios de los literales que ocurren en les cláusulas unitarias; una refut