
Navid Talebanfard

(Institute of Mathematics)

Structure in Proof Complexity: The Case of Tseitin and Tree Decompositions
 Abstract:

One of the main difficulties of proving lower bounds in proof complexity is that we cannot (seemingly) make structural assumptions about the proof and thus our argument should work against any conceivable proof (which may not even exist). I will survey a few old results showing that in some cases it is possible to prove structural properties of proofs of specific formulas or minimal proofs of arbitrary formulas. Then I will give a more direct proof of our result with Nicola Galesi and Jacobo Toran showing that the minimum width of Tseitin formulas is the same in general and regular resolution.

Nicola Galesi

(Sapienza University of Rome)

Resolution and the binary encoding of combinatorial principles
 Abstract:

We investigate the size complexity of proofs in RES(s)  an extension of Resolution working on sDNFs instead of clauses  for families of contradictions given in the unusual binary encoding.
A motivation of our work is to approach size lower bounds of refutations in Resolution for families of contradictions in the usual unary encoding. Our main interest is the kClique principle, whose Resolution complexity is still unknown. The approach is justified by the observation that for a large class of combinatorial principles short RES(log n) refutations for the binary encoding are obtained from short Resolution refutations of the unary encoding, in particular for the kClique principle.
In the talk we show a n^{Omega(k)} lower bound for the size of refutations of the binary kClique Principle in RES(log log n). This improves a result of Lauria, Pudlák, Rödl and Thapen, who proved the lower bound for Resolution, that is RES(1). Resolution lower bounds for the (unary) kClique principle are known only when refutations are either treelike or readonce.
The result is part of a larger work investigating the complexity of proofs in RES(s) for binary encodings of combinatorial principles, written jointly with Stefan Dantchev and Barnaby Martin and available at https://arxiv.org/abs/1809.02843
Pavel Pudlak, Neil Thapen
organizers