Parametric SAT
In my diploma thesis I generalized successful algorithmic ideas for quantified satisfiability solving to the parametric case where there are parameters in the input problem. The output is then not necessarily a truth value but more generally a propositional formula in the parameters of the input. Since one can naturally embed propositional logic into first-order logic over Boolean algebras, the work amounts from a model-theoretic point of view to a quantifier elimination procedure for initial Boolean algebras.
Publications
- Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases
Christoph Zengler and Wolfgang Küchlin
12th International Workshop on Computer Algebra in Scientific Computing (CASC) 2010
Download Paper - Parametric Quantified SAT Solving
Christoph Zengler and Thomas Sturm
35th International Symposium on Symbolic and Algebraic Computation (ISSAC) 2010
Download Paper - Generalised SAT Checking in a First-Order Logic Framework
Christoph Zengler
Diploma Thesis at the University of Passau, 2008
Download Thesis
Talks
- Quantifier Elimination with SAT Solving Algorithms
Talk at the Universität Tübingen, Germany
Download slides of the talk - Generalised SAT-Checking in a First-Order Logic Framework
Defense of my diploma thesis
Download slides of the talk