Structure-based Algorithm Engineering for SAT-Solving
Final Report Abstract
In our project we focus on the analysis and engineering of practiced SAT solving with the aim to make the success of SAT solvers better understandable and to make solvers more robust. Within the first funding period we created our own SAT solver as a source for profound research on SAT solving. We have analyzed the use of structural information for practiced solving. A large part of the second funding period focused on the analysis and engineering of alternative hybrid and parallel SAT solving. In the spirit of algorithm engineering we combine methodological approaches with extensive experimental studies on real-world applications. This goes along with continuous development and improvement of our SAT solving software. To evaluate our methods, we participate regularly in the international SAT Competition and the SAT Race. While in the first two periods of the project, our emphasis was on the engineering and elaboration of the methodologies for SAT solving, we did use our experience gathered over four years together with our highly optimized solver to place a further focal point on applications in the last period. The most prominent application from the first two funding periods - automotive product configuration - was also one of the reasons to develop MUStICCa, a tool that gives the user full control over each step of the algorithm that computes minimal reasons of unsatisfiability of an instance by interactively focusing on or eliminating parts of the search space. Domain experts, who usually have good intuitions about the parts of the formula that are relevant for good explanations of unsatisfiabiltiy are able to guide the algorithm in their preferred direction. Other applications of SAT we elaborated during the last period are based in Bioinformatics, namely the Maximum Quartet Consistency Problem, Graph Problems, like Maximum Independent Set and Minimum Vertex Cover, Artificial Intelligence and Computational Linguistics (Symbolic Grammar Engineering). The mixed results we obtained in these areas show that trying to solve problems via SAT is possible for a broad range of tasks, but to be competetive against state-of-the-art approaches solving optimization problems, a lot of engineering towards the best encodings and solver strategies is required. To support this engineering and help the researchers to understand the success of the wellknown CDCL-approacb and its small derivations in each particular SAT solver we developed the tool CoPAn. With the help of CoPAn anyone can analyze a whole solver run of an instance based on the structural information of each conflict, that occurred until finding a model or proving unsatisfiability. Subtle changes in parameter choices can influence the behaviour of any SAT solver immensely. Therefore it is tremendously important to be able to gain more knowledge about the effects of these small changes on the execution and in particular on the conflict patterns that were used to solve an instance. New techniques are very hard to establish in praticed SAT solving due to the always imminent comparison with the highly-optimized solvers. Thus from our point of view it is important to shift the focus while evaluating new ideas off of the amount of solved instances, respectively the used time to solve these, more towards other criteria. We used the amount of saved propagations and deleted literals during each invocation of a simplification technique like Hyper Binary Resolution, to be able to see the potential of further investigations in these approaches. With our contributions during the whole project we showed that the algorithm engineering community is the prime candidate to establish new quality measures.
Publications
- A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors. In SAT, pages 161-167, 2008
Stephan Kottler and Michael Kaufmann and Carsten Sinz
- Computation of Renameable Horn Backdoors. In SAT, pages 154-160, 2008
Stephan Kottler and Michael Kaufmann and Carsten Sinz
- Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases. In CASC, pages 293-302, 2010
Christoph Zengler and Wolfgang Küchlin
- Model counting in product configuration. In International Workshop on Logic in Component Configuration (Lo- CoCo), pages 44-53, 2010
Andreas Kübler, Christoph Zengler, and Wolfgang Küchlin
- SAT Solving with Reference Points. In SAT, pages 143-157, 2010
Stephan Kottler
- Beyond Unit Propagation in SAT Solving. In Symposium on Experimental Algorithms, pages 267-279, 2011
Michael Kaufmann and Stephan Kottler
- CoPAn: Exploring Recurring Patterns in Conflict Analysis of CDCL SAT Solvers (Tool Presentation). In SAT, pages 449-455, 2012
Stephan Kottler and Christian Zielke and Paul Seitz and Michael Kaufmann
- Creating Industrial-Like SAT Instances by Clustering and Reconstruction. In SAT, pages 471-472, 2012
Sebastian Burg and Stephan Kottler and Michael Kaufmann
- Advanced Methods for SAT Solving. Phd Thesis, 2013
Stephan Kottler
- Boolean Quantifier Elimination for Automotive Configuration - A Case Study. In Formal Methods for Industrial Critical Systems (FMICS), pages 48-62, 2013
Christoph Zengler and Wolfgang Küchlin
- MUStICCa: MUS Extraction with Interactive Choice of Candidates (Tool Paper). In SAT, pages 408-414, 2013
Johannes Dellert and Christian Zielke and Michael Kaufmann
