Logik in der Informatik Prof. Dr. Martin Grohe

Constraint Satisfaction Problems (CSP) form a natural class of algorithmic problems with important applications in several areas such as artificial intelligence, databases, automated verification, and statistical physics. The most prominent example of a CSP is the satisfiability problem (SAT) for formulas of propositional logic.

It is well-known that, in general, CSP are NP-hard and thus, at least theoretically, not efficiently solvable. However, in practice there has been tremendous progress in recent years. In particular, the SAT problem is solved routinely in industrial applications for instances with more than 10,000 Variables.

Thus we see a clear discrepancy between the theoretical worst-case prediction and practice. A reason often given for this discrepancy is that instances in practice can be expected to be "structured". It is completely unclear, however, which structural properties of instances are relevant here and how they are exploited by the standard algorithms. These questions are addressed in the present project. Besides CSP and SAT as the main example, we will also consider related problems, such as counting problems.

The project is funded by the Deutsche Forschungsgemeinschaft (German Research Foundation).