Structure Based Algorithm Engineering for SAT-Solving

Given a boolean formula the satisfiability problem (SAT) asks if there exists a truth assignment to the variables of the formula such that the formula evaluates to true. Even though this problem seems to be purely theoretical there are several real-world problems that can be formulated as a SAT problem. From the theoretical point of view SAT is NP-complete and should thus be not solvable in feasible time. However, in the last 15 years state-of-the-art SAT Solvers became able to solve many real-world SAT instances with hundreds and thousands of variables. This is reasond by the fact that real-world SAT problems exhibit some internal structure that can be somehow exploited by SAT Solvers.

In the last years we have worked out a general methological approach that can be used to analyze the structure of real-world problems. One of our goals is to apply this methodology for solving SAT problems. We aim to develop and implement a SAT Solver that analyzes the structure of the underlying SAT instance and uses these information for the solving process. One big challange is to handle the trade-off between the quality of structural information and on the other hand the complexity to compute these information in the first phase of the algorithm.
We have implemented and analysed several different approaches for sequential and mult-threaded SAT solving. The different solver implementations are presented here.

Events

Workshop on SAT 2011

Related Publications

Stephan Kottler and Michael Kaufmann: SArTagnan - A parallel portfolio SAT solver with lockless physical clause sharing, Pragmatics of SAT, 2011
Michael Kaufmann and Stephan Kottler: Beyond Unit Propagation in SAT Solving, Symposium on Experimental Algorithms 2011
Michael Kaufmann and Stephan Kottler: A parallel portfolio SAT solver with lockless physical clause sharing, Technical Report, 2011
Stephan Kottler: Description of the SApperloT, SArTagnan and MoUsSaka solvers for the SAT-Competition 2011, SAT 2011, USA
Stephan Kottler: SAT Solving with Reference Points, Theory and Applications of Satisfiability Testing - SAT 2010, 2010
Stephan Kottler: Description of the SApperloT solver for the SAT-Race 2010, SAT 2010, Scotland
Stephan Kottler: Description of the parallel solver SArTagnan for the SAT-Race 2010, SAT 2010, Scotland
Michael Kaufmann, Stephan Kottler: Proving or Disproving Planar Straight-Line Embeddability onto given Rectangles, 17th International Symposium on Graph Drawing (GD '09), 2010
Stephan Kottler: Description of the SApperloT solvers for the SAT-Competition 2009, SAT 2009, Wales
Stephan Kottler, Michael Kaufmann, Carsten Sinz: A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors, Theory and Applications of Satisfiability Testing - SAT 2008, 2008
Stephan Kottler, Michael Kaufmann, Carsten Sinz: Computation of Renameable Horn Backdoors, Theory and Applications of Satisfiability Testing - SAT 2008, 2008

Software

Source code of MoUsSaka as submitted to the SAT-competition 2011. It is an extension of SApperloT that allows to find Minimal Unsatisfiable Subsets (MUS) of a CNF formula. It supports the plain MUS computation where the minimisation considers the number of clauses in the final unsatisfiable subset. Furthermore, the computation can be set to minimise the number of categories or groups of clauses that appear in the unsatisfiable subset.
Source code of SApperloT for Linux as submitted to the SAT-competition 2011. Some information can be found in the solver description for the SAT-competition.
Source code of SArTagnan for Linux as submitted to the SAT-competition 2011. SArTagnan is a parallel portfolio SAT solver that runs different strategies in different threads. Clauses can be shared logically and physically among all threads without the use of operation system locks. In particular, one thread extensively applies simplification techniques and another thread uses DMRP. More information can be found in the technical report or in the solver description for the SAT Race 2010 and the SAT-competition 2011.
Source code of SApperloT for Linux as submitted to the SAT-Race 2010. This version combines DMRP with state-of-the-art CDCL solving. For more information please take a look at my paper about DMRP or the solver description for the SAT-Race. The preprocessor of this version of SApperloT was written by Christian Zielke.
The tool GridFit can be used to prove or disprove whether or not a plane graph can be embedded onto a given rectangle/grid. The embedding assumes edges to be drawn straight-line and without crossings. Internally GridFit encodes this problem into SAT and uses a modified version of SApperloT to solve the transformed problem. Source code for Linux of a preliminary version of GridFit is available for download. Just invoke 'make' in the top level directory and execute 'GridFit' to see the options. GridFit can be used for small graphs but it might get into trouble with larger graphs!
Source code of SApperloT-base for Linux as submitted to the SAT-competition 2009. Note that this version is a bit more verbose than the submitted one. More information about SApperloT can be found here.
SatIn is a visualisation tool for SAT instances (Sat Insight) written in Java on top of the yFiles library. It allows for depicting different kinds of graphs that can be gained from SAT instances in conjunctive normal form. The layout of a graph can be chosen from a set of available automated layouts and, moreover, can be modiefied manually. Selecting an element in one graphical representation automatically highlights the according elements in all other graphical representations. Execute it with the command: java -jar SatIn.jar.

Affiliates

Support

Deutsche Forschungsgemeinschaft (DFG) within Priority Programme 1307 "Algorithm Engineering"