Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
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 language | English |
---|---|
Title of host publication | 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019 |
Editors | Joost-Pieter Katoen, Pinar Heggernes, Peter Rossmanith |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
ISBN (Electronic) | 9783959771177 |
ISBN (Print) | 9783959771177 |
DOIs | |
State | Published - Aug 2019 |
Event | 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019 - Aachen, Germany Duration: 26 Aug 2019 → 30 Aug 2019 |
Name | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 138 |
ISSN (Print) | 1868-8969 |
Conference | 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019 |
---|---|
Country/Territory | Germany |
City | Aachen |
Period | 26/08/19 → 30/08/19 |
ID: 49785080