School of
Electrical Engineering
and Computer Science
 KTH / CSC / Theory Group / Jakob Nordström / Teaching / DD3501 Current Research in Proof Complexity 2011/12 / Possible themes for remaining lectures

# Possible Themes for Remaining Lectures

We should be able to cover 6–7 of the suggestions below during the remaining lectures of the course.

Therefore, please vote for the 6–7 alternatives (or less, but not more) that you find the most interesting. Votes will be collected in class on Wednesday January 25, but later votes by e-mail are also possible.

Everybody attending the course is welcome and encouraged to vote, including listeners.

1. Gröbner bases and SAT solving

How can one build SAT solvers on top of polynomial calculus? (It seemed we had a tentative guest lecturer here, but it might be falling through. If there is strong interest, however, I will see if we can find another solution.)

2. Cutting planes lower bounds

Overview of the only known exponential lower bounds on proof length in cutting planes based on Pavel Pudlák: Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations (free version). Doing the full details of the proof is outside the scope of this course, but we could have a look at the main ingredients in the proof and how they mix together.

3. Trade-offs between proof size and proof space for PC and PCR

Some work on previously open questions that is being done as we speak joint with Chris Beck and Bangsheng Tang.

4. Trade-offs between proof length and proof space for CP

Overview of very recent work (unpublished and in some sense ongoing) on proving trade-offs, or actually rather conditional space lower bounds, for cutting planes. This is joint with Trinh Huynh. Going into all details requires some heavy-duty communication complexity which is beyond the scope of this course, but we could give an outline of how the proof goes.

We have proven (in class and in lecture 4½) that pebbling trade-offs give rise to resolution trade-offs, and then have used this to claim strong results for length versus clause space in resolution. However, we never proved that there are any pebbling trade-offs in the first place. If there is interest, we could prove (or at least outline a proof of) such a pebbling result, probably based on the paper Jakob Nordström: On the Relative Strength of Pebbling and Resolution (but note that this has no relation to proof complexity per se—it just turns out that pebbling has been very useful as a tool to obtain proof complexity results).

6. Lower bounds for k-DNF resolution

Lower bounds on proof length for proof systems extending resolution by working with k-DNF formulas (i.e., replacing literals with conjuctions of bounded size) based on Nathan Segerlind, Sam Buss, and Russell Impagliazzo: A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution (free version). Again, this would be more of an overview, where we would skip most of the detailed proofs (since otherwise this would probably take 2–3 lectures).

7. Non-automatizability of resolution

It is (probably) impossible to search for short resolution proofs with theoretical guarantees to find them quickly. Based on Michael Alekhnovich and Alexander Razborov: Resolution Is Not Automatizable Unless W[P] Is Tractable (free version). Brief 1-lecture overview without too many proofs.

8. Non-approximability of proof length

Given a resolution refutation, can we decide whether the length of this refutation is close to optimal? No, not unless P = NP. Based on Michael Alekhnovich, Sam Buss, Shlomo Moran, and Toniann Pitassi: Minimum Propositional Proof Length Is NP-Hard to Linearly Approximate (free version). Brief 1-lecture overview without too many proofs.

9. If refutation width is small, then CDCL runs fast (sort of)

If the minimum width refuting a formula in resolution is small, then a (reasonable matemathical model of a) CDCL solver will find a refutation fast (although it is not at all looking for a narrow resolution refutation). Based on Albert Atserias, Johannes Fichte, and Marc Thurley: Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution. Brief 1-lecture overview without too many proofs.

10. CDCL solvers have to learn wide clauses to make progress

A crucial component in a CDCL solver is which clauses it should learn and keep. An early heuristic was to focus on only small clauses, but there is theoretical (as well as practical) evidence this is not too great an idea. Based on Eli Ben-Sasson and Jan Johannsen: Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas (free version). Brief 1-lecture overview without too many proofs.

11. CDCL (viewed as a proof system) polynomially simulates resolution

How strong are CDCL solvers? We know that they will find resolution proofs, but which kind of proofs? Are they only searching for proofs in some limited subsystem of resolution, or can they find essentially any resolution proof? The paper Knot Pipatsrisawat and Adnan Darwiche: On the Power of Clause-Learning SAT Solvers as Resolution Engines (free version) claims the latter—i.e., intuitively CDCL is (potentially) an efficient search procedure for the full resolution proof system. Brief 1-lecture overview without too many proofs.