Systematic and local search algorithms for regular-SAT

• Autores: Ramón Béjar Torres
• Directores de la Tesis: Felip Manyà Serres (dir. tes.) , Xavier Binefa i Valls (dir. tes.)
• Lectura: En la Universitat Autònoma de Barcelona ( España ) en 2001
• Idioma: inglés
• Tribunal Calificador de la Tesis: Francesc Esteva i Massaguer (presid.) , Gonzalo Escalada Imaz (secret.) , Reiner Mähnle (voc.) , Carla Pedro Gomes (voc.) , Álvaro del Val Latorre (voc.)
• Enlaces
  • Tesis en acceso abierto en: TDX
• Resumen

  • Regular-SAT es el problema de decidir la satisfactibilidad de una clase de fórmulas proposicionales multivaluadas llamadas fórmulas CNF regulares, Una fórmula CNF regular es una forma normal conjuntiva clásica basada en una noción generalizada de literal, llamada literal regular. Dado un conjunto de valores de verdad N, con al menos dos valores de verdad, equipado con un orden total, un literal regular es una expresión de la forma S:p, donde p es una variable proposicional y S es un subconjunto de N el cual es o de la forma i o de la forma i, para algún i de N. Una interpretación multivaluada dada satisface un literal regular S:p sii asigna i de N. Una interpretación multivaluada dada satisface un literal regular S:p sii asigna a p un valor de verdad de S, y satisface una cláusula regular sii satisface al menos uno de sus literales. Una fórmula CNF regular es satisfactible sii existe una interpretación que satisface todas sus cláusulas, en caso contrario, es insatisfactible.

    En esta tesis nos centramos en el diseño, implementación y análisis de algoritmos de búsqueda sistemática y local para Regular-SAT, y definimos un método generico para resolución de problemas el cual consiste en modelar problemas combinatorios como instancias de Regular-SAT y entonces resolver las fórmulas resultantes con algoritmos para Regular-SAT. En particular, prestamos especial atención a la definición de estructuras de datos adecuadas para representar fórmulas, heurísticas para explorar eficientemente el espacio de búsqueda, estrategias para escapar de mínimos locales en algoritmos de busqueda local, y codificaciones adecuadas basadas en Regular-SAT para modular problemas combinatorios.

    En lo concerniente a algoritmos de búsqueda sistemática hemos diseñado e implementado una variante de Regular-DP, el cual es un algoritmo estilo Davis-Putnam para fórmulas CNF regulares. Respecto a algoritmos de búsqueda local hemos diseña