Logic and Decision Procedures
Logic and Decision Procedures
Sequential and Parallel SAT Solving
We develop a generic SAT-solver that serves as a basis for various solver configurations via combination of solver components. It shall offer great flexibility in deriving different SAT-solver instances from available components and existing parameters. This is of importance in many respects, e.g. in optimizing solvers for a particular domain by automatically tuning solver parameters and in constructing portfolio-based solvers. We consider components from classical DPLL-based to CDCL-based solvers, from principal components (e.g. search, unit propagation, decision heuristics, backtracking) to secondary components (e.g. learning, clause forgetting heuristics, restart heuristics). A special focus is put on simplification and formula rewriting techniques.
Given a good sequential SAT solver, parallel solvers are investigated to improve the performance of SAT technology on modern multi-core architectures. Here, the focus is to partition the search space recursively, to benefit from the increasing number of available computing resources.
As SAT systems become more and more complex, verifiable output is required. Hence, we study how to produce unsatisfiability proofs for existing SAT techniques and parallel SAT solvers, to allow to use as many existing techniques as possible and still being able to verify the result of the SAT solver.
Encoding Real-World Problems
Furthermore, encoding real world problems into the language of SAT is often non-trivial. Hence, encodings for commonly used constraints are studies and new ways to describe these constraints in propositional logic are developed. We currently focus on cardinality constraints and pseudo Boolean constraints, which are frequently used in configuration, car sequencing, or planning.
Optimization and Enumerating all ModelsBesides solving a single decision problem with a SAT solver, finding an optimal solution, or finding all solutions are two common tasks as well. In our group, we extend SAT solvers to encounter all solutions of a formula, or the related real world problem. Furthermore, we develop an optimization solver.
Sebastian Rudolph, Mantas Simkus
The Triguarded Fragment of First-Order Logic
In Gilles Barthe, Geoff Sutcliffe, Margus Veanes, eds., Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in Computing, 604-619, 2018. EasyChair
Ana Ozaki, Markus Krötzsch, Sebastian Rudolph
Temporally Attributed Description Logics
In Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter, eds., Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, volume 11560 of LNCS, 441-474. Springer, 2019
Presburger Concept Cardinality Constraints in Very Expressive Description Logics – Allegro sexagenarioso ma non ritardando
In Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter, eds., Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, volume 11560 of LNCS, 542-561. Springer, 2019