Logic and
Theory of
Discrete Systems

Informatik 7

Proof  Complexity and Lower Bounds for Generic Algorithms

Christoph Berkholz, Martin Grohe

One approach to attack NP-hard satisfiability problems such as 3-SAT or the Constraint Satisfaction Problem (CSP) is to design generic algorithms that run in polynomial time but do not always produce the correct answer. For the CSP these include constraint propagation techniques like arc-, path- and k-consistency algorithms. A similar approach for 3-SAT that has origins in proof complexity is to search for resolution refutations of bounded width. In this line of research we investigate the inherent complexity of these approaches: Can the techniques be implemented faster than with the currently known algorithms? We were able to obtain near optimal lower bounds using the connections to proof complexity and finite variable logics. From a practical point of view the lower bound proofs generate hard instances for these algorithms and determine their inherent limitations. From a theoretical point of view the results lead to a deeper understanding of the structure of finite variable formulas and resolution refutations.

Funding: DFG