Logic and Decision Procedures

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
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.

Wissenschaftliche Mitarbeiter

By sarameister23-3.jpg

Dr. Johannes Fichte



Dr. Norbert Manthey

Sibylle moehle.jpg

Dipl.-Inform. Sibylle Möhle


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

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