Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People
Events

The Taub Faculty of Computer Science Events and Talks

Theory Seminar: The Strength of Parameterized Tree-like Resolution
event speaker icon
Massimo Lauria (Università di Roma)
event date icon
Wednesday, 10.02.2010, 13:30
event location icon
Taub 201
We examine the proof-theoretic strength of parameterized tree-like resolution---a proof system for the $\co\W[2]$-complete set of parameterized tautologies.

Parameterized resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al.\ show a complexity gap in parameterized tree-like resolution for propositional formulas arising from translations of first-order principles.

Here we pursue a purely combinatorial approach to obtain lower bounds to the proof size in parameterized tree-like resolution. For this we devise a prover-delayer game suitable for parameterized resolution. By exhibiting good delayer strategies we then show lower bounds for the pigeonhole principle as well as the order principle. On the other hand, we demonstrate that parameterized tree-like resolution is a very powerful system, as it allows short refutations of all parameterized contradictions given as bounded-width CNF's. Thus, a number of principles such as Tseitin tautologies, pebbling contradictions, or random 3-CNF's which serve as hard examples for classical resolution become easy in the parameterized setting.

Joint work with Olaf Beyersdorff and Nicola Galesi.