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.
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.)
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.
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.
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.
Pebbling time-space trade-offs
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).
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).
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.
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.
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.
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.
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.
