The research activities in the KRR group can be broadly grouped under the four headings:
You may also want to look at the list of recent publications by group members.
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. p>
Logic and Human Reasoning
Human Reasoning, Computational Logic, and Connectionism
The project aims at developing non-classical logics as well as connectionist realizations thereof which are adequate for human reasoning.
Human Reasoning in Computational Logic
Until now there are no widely accepted theories that give formal representations of sophisticated human reasoning. In our project we address this issue by exploring current results from relevant research areas. The goal is to formalize a framework that allows the expression of reasoning processes which are fundamental in order to explain human behaviour. Conventional formal approaches such as classical logic are not appropriate for this purpose as they cannot deal with the most elementary parts humans are confronted with e.g. incomplete information. Alternatives can be found in formalizations of weaker logics such as non-monotonic logics or three-valued logics. Furthermore, in the field of neurosicence (e.g. connectionist networks) and cognitive science (e.g. studies from psychological reasoning such as the selection and suppression task) a lot of reaserach is going on in understanding and simulating human reasoning processes. Their results are important for our purpose as they deal with similar fundamental questions about human behaviour.
Training and Education
International Master's Program in Computational Logic (MCL)
Information on MCL can be found on the Web site http://www.computational-logic.org/.
European Master's Program in Computational Logic (EMCL)
Please see the dedicated Web site of this Master's program http://www.emcl-study.eu/.
European PhD Program in Computational Logic (EPCL)
The creation and implementation of the European PhD Program in Computational Logic (EPCL) is funded by the German Academic Exchange Service DAAD within the program International Promovieren in Deutschland (IPID). The objectives of the European PhD program in Computational Logic (EPCL) are to prepare highly qualified researchers in Computational Logic who will further strengthen the European presence in the field, to deepen the student's knowledge and consolidate his/her comprehension of the field of Computational Logic, to provide the student with the necessary skills to collaborate in an international and intercultural environment, and to advance the state of the art in Computational Logic by facilitating the collaboration between leading institutions through joint PhD projects. EPCL is an integrated and structured PhD program, jointly offered by Technische Universität Dresden (Germany, coordinator), the Libera Universita di Bolzano - Freie Universität Bozen (Italy), the Universidade Nova de Lisboa (Portugal) and the Technische Universität Wien (Austria). It involves further associated partner universities in Australia, Latin America and North America as well as industrial partners. It consists of a training program, the PhD thesis and its defense in front of a joint commission. Each doctoral candidate will stay at least at two of the European partner universities and will receive a joint PhD degree from these universities upon successful completion of his/her studies. http://www.epcl-study.eu/.
Prof. Steffen Hölldobler
Acting Director of the Institute
Head of the group
Telephone +49 (0)351 463 38340
Telefax +49 (0)351 463 38342
Ms. Sylvia Wünsch
Telephone +49 (0)351 463 38341
Telefax +49 (0)351 463 38342
Nöthnitzer Straße 46
Faculty of Computer Science