Algoritmos para SAT basados en la representación de tablas booleanas

Abstract

[ES] El problema SAT (satisfacibilidad en lógica proposicional) es muy importante, ya que fue el primer problema que se probó que era NP-completo y muchos otros problemas se resuelven mediante su reducción a SAT. Es por ello, que se está dedicando un gran esfuerzo al desarrollo de algoritmos eficientes para SAT. La mayoría de los algoritmos usan conjuntos de cláusulas como representación básica, pero recientemente se han desarrollado algoritmos basados en la representación mediante tablas implementadas por Numpy. Este trabajo, propone estudiar y profundizar en esta línea. En concreto, consistiría de los siguientes puntos: - Estudio de los fundamentos del problema SAT y de los principales algoritmos existentes para su resolución. - Implementación de algoritmos básicos como el backtraking no-cronológico con aprendizaje de cláusulas. - Extensión de estos algoritmos a la representación mediante tablas booleanas.

[EN] The SAT (satisfiability in propositional logic) problem is very important as it was the first problem proven to be NP-complete and many other problems are solved by reducing it to SAT. That is why a great effort is being dedicated to the development of efficient algorithms for SAT. Most algorithms use sets of clauses as a basic representation, but recently algorithms based on the representation using tables implemented by Numpy. This work proposes to study and deepen this line. Specifically, it would consist of the following points: - Study of the foundations of the SAT problem and the main existing algorithms for its resolution. - Implementation of basic algorithms such as non-chronological backtraking with clause learning. - Extension of these algorithms to the representation using Boolean tables.