PPC on Friday, July 9th

14:00‑15:00 Session 1
Chair: Stefan Dantchev
Location: AT 2.12
14:00 Nicola Galesi (Universita di Roma)
The Complexity of Proofs in Parameterized Resolution
15:30‑16:30 Session 2
Chair: Olga Tveretina
Location: AT 2.12
15:30 Eli Ben-Sasson and Jakob Nordström
Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions

For current state-of-the-art satisfiability algorithms based on the DPLL procedure and clause learning, the two main bottlenecks are the amounts of time and memory used. In the field of proof complexity, these resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There has been a long line of research investigating these proof complexity measures, but while strong results have been established for length, our understanding of space and how it relates to length has remained quite poor. In particular, the question whether resolution proofs can be optimized for length and space simultaneously, or whether there are trade-offs between these two measures, has remained essentially open apart from a few results in restricted settings.

In this paper, we remedy this situation by proving a host of length-space trade-off results for resolution in a completely general setting. Our collection of trade-offs cover space ranging over the whole interval from constant to O(n / log log n), and most of them are superpolynomial or even exponential and essentially tight. Using similar techniques, we show that these trade-offs in fact extend (albeit with worse parameters) to the stronger k-DNF resolution proof systems, which operate with formulas in disjunctive normal form with terms of bounded arity k. We also establish that the k-DNF resolution systems form a strict hierarchy with respect to space.

Our key technical contribution is the following, somewhat surprising, theorem: Any CNF formula F can be transformed by simple variable substitution into a new formula F' such that if F has the right properties, F' can be proven in essentially the same length as F while the minimal space needed for F' is lower-bounded by the number of variables mentioned simultaneously in any proof for F. Applying this theorem to so-called pebbling formulas defined in terms of pebble games on directed acyclic graphs yields our results.

16:00 Stefan Dantchev
Parameterized Proof Complexity

We propose a proof-theoretic approach for gaining evidence that certain parameterized problems are not fixed-parameter tractable. We consider proofs that witness that a given propositional formula cannot be satisfied by a truth assignment that sets at most k variables to TRUE, considering k as the parameter (we call such a formula a parameterized contradiction). One could separate the parameterized complexity classes FPT and W[2] by showing that there is no proof system (for CNF formulas) that admits proofs of size f(k)n^{O(1)} where f is a computable function and n represents the size of the propositional formula. By way of a first step, we introduce the system of parameterized tree-like resolution, and show that this system does not admit such proofs. We obtain this result as a corollary to a meta-theorem, the main result of this paper. The meta-theorem extends Riis's Complexity Gap Theorem for tree-like resolution. Riis's result establishes a dichotomy between polynomial and exponential size tree-like resolution proofs for propositional formulas that uniformly encode a first-order principle over a universe of size n:

(1) either there are tree-like resolution proofs of size polynomial in n, or

(2) the proofs have size at least 2^{\epsilon n} for some constant \epsilon;

the second case prevails exactly when the first-order principle has no finite but some infinite model. We show that the parameterized setting allows a refined classification, splitting the second case into two subcases:

(2a) there are parameterized tree-like resolution proofs of size at most \beta^k n^\alpha for some constants \alpha,\beta; or

(2b) every parameterized tree-like resolution proof has size at least n^{k^\gamma} for some constant \gamma in [0,1);

the latter case prevails exactly if for every infinite model, a certain associated hypergraph has no finite dominating set. We provide examples of first-order principles for all three cases.

Finally, we consider how the set of parameterized contradictions may be embedded into the set of (ordinary) contradictions by the addition of new axioms. Given a certain proof system, this embedding itself gives rise to a parameterized proof system. When embedded into general (DAG-like) resolution, we demonstrate that the pigeonhole principle has a proof of size 2^k n^2. This contrasts with the case of tree-like resolution where the embedded pigeonhole principle is shown to fall into the "harder" category (2b).

This is a joint work with B. Martin and S. Szeider, which appeared at FOCS'07

17:00‑18:00 Session 3
Chair: Stefan Dantchev
Location: AT 2.12
17:00 Uwe Bubeck, Hans Kleine Büning, Anja Remshagen and Xishun Zhao
Expressiveness and Complexity of Subclasses of Quantified Boolean Formulas

We give a brief overview of expressiveness and complexity results for a hierarchy of subclasses of quantified Boolean formulas with close connections to Boolean circuits and minimal unsatisfiability.

17:30 Olga Tveretina
Ordered Binary Decision Diagrams Do Not Simulate Resolution Polynomially

Groote and Zantema proved that limited OBDD derivations cannot simulate resolution polynomially. Tveretina, Sinz and Zantema have presented a family of CNFs that show an exponential blow-up for all OBDD refutations compared to unrestricted resolution refutations.