Implementação de um solucionador sat baseado no algoritmo DPLL com heurísticas de decisão

Abstract

This work presents the development of a solver for the problem of Boolean satisfiability (SAT), based on the Davis-Putnam-Logemann-Loveland algorithm (DPLL). The implemented tool performs formula verification, conversion to conjunctive normal form, and to the DIMACS standard input format, as well as the actual solving process. For comparative analysis, two decision heuristics were integrated: MOM’s, a static heuristic, and VSIDS, a dynamic and adaptive heuristic. The experimental evaluation was conducted using benchmark instances and manually inserted formulas. The results indicated superior performance of the MOM’s heuristic in most tests, while VSIDS showed advantage only in a specific case. It is concluded that the effectiveness of a heuristic depends on the balance between its theoretical complexity and the way it is implemented in practice. The results show that the theoretical advantage of a heuristic only translates into good practical results when accompanied by an efficient implementation. Hence, besides providing a functional tool, the study contributes to the practical understanding of the interaction between theory and implementation in the context of NP-complete problems.