Dissertação de Mestrado

The Boolean satisfiability problem is the most notorious and first ever discovered NP-Complete problem. To solve it, state-of-the-art methods still rely on techniques that yield exponential running time in the worst case. The goal of this work is to study methods used on correlated problems in order to approach solving a SAT instance from a different angle, that can be seen as the generation of non-analytic cuts supported by a linear algebra. In particular, linear programming methods have obtained good results when dealing with a closely related problem, the satisfiability problem in infinitely valued logics. With that in mind, we will study the original SAT as an optimization problem. We present a new way of generating non-analytic cuts for a boolean formula by solving a linear programming problem. From the linear solution, boolean values are extracted, and a partial solution is constructed and evolved until a conflict is detected. Using the conflict, we implement clausal learning to produce a new clause. We also present a complete SAT solving algorithm designed to leverage this method, show soundness and completeness results for it and investigate its empirical performance.

O problema da satisfatibilidade booleana (SAT) é o problema mais notório e o primeiro já descoberto a ser NP-Completo. Para resolvê-lo, os métodos mais avançados ainda dependem de técnicas que produzem um tempo de execução exponencial no pior caso. O objetivo deste trabalho é estudar métodos usados em problemas correlatos para abordar a resolução de uma instância do SAT de um ângulo diferente, que pode ser visto como a geração de cortes não analíticos apoiados por uma álgebra linear. Em particular, os métodos de programação linear obtiveram bons resultados ao lidar com um problema intimamente relacionado: o problema da satisfatibilidade em lógicas infinitamente valoradas. Com isso em mente, estudaremos o SAT original como um problema de otimização. Apresentamos uma nova maneira de gerar cortes não analíticos para uma fórmula booleana, resolvendo um problema de programação linear específico. A partir da solução linear, valores booleanos são extraídos e uma solução parcial é construída e evoluída até que um conflito seja detectado. Com o conflito, implementamos a aprendizagem de cláusulas para produzir uma nova cláusula. Também apresentamos um algoritmo completo de resolução de SAT projetado para aproveitar esse método, mostramos resultados de soundness (correção) e completude para ele e investigamos o seu desempenho empírico.