Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Bounded-depth frege complexity of tseitin formulas for all graphs. / Galesi, Nicola; Itsykson, Dmitry; Riazanov, Artur; Sofronova, Anastasia.
44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019. ed. / Joost-Pieter Katoen; Pinar Heggernes; Peter Rossmanith. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2019. 49 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 138).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
TY - GEN
T1 - Bounded-depth frege complexity of tseitin formulas for all graphs
AU - Galesi, Nicola
AU - Itsykson, Dmitry
AU - Riazanov, Artur
AU - Sofronova, Anastasia
PY - 2019/8
Y1 - 2019/8
N2 - 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.
AB - 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.
KW - AC0-Frege
KW - Treewidth
KW - Tseitin formula
UR - http://www.scopus.com/inward/record.url?scp=85071743099&partnerID=8YFLogxK
UR - http://www.mendeley.com/research/boundeddepth-frege-complexity-tseitin-formulas-graphs
U2 - 10.4230/LIPIcs.MFCS.2019.49
DO - 10.4230/LIPIcs.MFCS.2019.49
M3 - Conference contribution
AN - SCOPUS:85071743099
SN - 9783959771177
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019
A2 - Katoen, Joost-Pieter
A2 - Heggernes, Pinar
A2 - Rossmanith, Peter
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019
Y2 - 26 August 2019 through 30 August 2019
ER -
ID: 49785080