• 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.
    • 24.09.18   14:00
    • 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 s-DNFs 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 k-Clique 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 k-Clique principle. In the talk we show a n^{Omega(k)} lower bound for the size of refutations of the binary k-Clique 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) k-Clique principle are known only when refutations are either treelike or read-once. 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
    • 17.09.18   14:00

    Pavel Pudlak, Neil Thapen