Christoph Berkholz: On the Complexity of Finding Width-k Resolution Refutations

Lunch is served at 12:00 noon (register at doodle.com/npng4d48ghc5sd95 by Friday the week before at 8 pm). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

ABSTRACT

One approach to attack NP-hard satisfiability problems such as 3-SAT or the Constraint Satisfaction Problem (CSP) is to design algorithms that run in polynomial time but do not always succeed. In this talk I gently introduce the approach of searching for width-k resolution refutations for 3-SAT (also known as k-consistency test in the CSP-community). This technique can be implemented in time n^O(k), hence is in polynomial time for every fixed k.

One drawback of this approach is that the degree of the polynomial increases with the parameter k. My main result is a lower bound showing that this cannot be avoided: Deciding whether there is a width-k resolution refutation requires time n^{ck} for an absolute constant c>0. Furthermore, the problem is EXPTIME-complete (if k is part of the input).