Development of a SAT Solver

Author: Jannis Harder

Abstract

The boolean satisfiability problem (SAT) belongs to set of NP-complete problems. Nevertheless the advent of SAT solvers which are fast for many practical problem instances made reduction to SAT practical for different problems in a large number of areas.
Besides the commonly used complete SAT solvers based on the DPLL procedure there also exists Stålmarck's method which received comparatively little attention in the literature. A recent work by Thakur and Reps "A Generalization of Stålmarck's Method" combines Stålmarck's method with concepts of abstract interpretation, thereby creating a new variant of Stålmarck's method. This thesis extends upon this work by introducing two new modifications to the generalized variant of Stålmarck's method. The first modification provides additional flexibility for heuristics when using a set of constraints as an abstract domain. The other modification allows for new exploration strategies of the search space. A prototype implementation is described including the design choices made. This prototype is evaluated and compared to existing DPLL based SAT solvers.