We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2tw(G)Ω(1/d) in depth-d Frege systems for d < (Formula presented.) where tw(G) is the treewidth of G. This extends Håstad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size 2tw(G)O(1/d)poly(s). Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.

Original languageEnglish
Title of host publication44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019
EditorsJoost-Pieter Katoen, Pinar Heggernes, Peter Rossmanith
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959771177
ISBN (Print)9783959771177
DOIs
StatePublished - Aug 2019
Event44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019 - Aachen, Germany
Duration: 26 Aug 201930 Aug 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume138
ISSN (Print)1868-8969

Conference

Conference44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019
Country/TerritoryGermany
CityAachen
Period26/08/1930/08/19

    Research areas

  • AC0-Frege, Treewidth, Tseitin formula

    Scopus subject areas

  • Software

ID: 49785080