Logic and Decision Procedures

From International Center for Computational Logic
Toggle side column

Logic and Decision Procedures

Satisfiability testing (SAT) is a very generic decision problem, which can be used to solve many industrial problems, such as hardware verification, configuration, planning, or for tasks in bio informatics. Hence, improvements of SAT technology have a direct impact to all the fields that exploit SAT solvers in their tool chain.

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 Models

Besides 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.

Scientific Staff

Bbe new.jpg

Bartosz Bednarczyk

By sarameister23-3.jpg

Dr. Johannes Fichte

Former Members

Proceedings Articles

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
Details Download

Book Chapters

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
Details Download

Sebastian Rudolph
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
Details Download


A Grand Unified Theory of Decidability in Logic-Based Knowledge Representation

A fast, highly scalable rule engine for existential rules and Datalog.