Study of SAT solvers improvement techniques

Details

Supervisors

Pecheur, Charles ; Gillard, Xavier

Faculty

Ecole polytechnique de Louvain

Degree label

Master [120] : ingénieur civil en informatique

Abstract

The satisfiability problem (SAT) is a well known problem in propositional logic. Actually, SAT was the first problem to be proven NP-complete by Cook in 1971. SAT solvers have been developed to solve this specific problem efficiently and have been the subject of remarkable improvements since the mid 90s. Many different solvers and techniques were devised to enhance the solver. This started a race to come up with more and more performing solvers. Each solver has its own architecture making it difficult to compare the techniques with one another. This thesis proposes an extension of Rsolve solver. Different techniques were added to this solver and thus share the same architecture. A analysis of the different techniques of the same kind between them is shown. These techniques are the variable selection heuristics, the restart strategies and inprocessing techniques. Sharing the same architecture allows fair comparison, eschewing implementation tricks and optimisations implemented by some state of the art solvers.