License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2019.49
URN: urn:nbn:de:0030-drops-109932
URL: https://drops.dagstuhl.de/opus/volltexte/2019/10993/
Go to the corresponding LIPIcs Volume Portal


Galesi, Nicola ; Itsykson, Dmitry ; Riazanov, Artur ; Sofronova, Anastasia

Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs

pdf-format:
LIPIcs-MFCS-2019-49.pdf (0.5 MB)


Abstract

We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2^{tw(G)^{Omega(1/d)}} in depth-d Frege systems for d<(K log n)/(log log n), 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 2^{tw(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.

BibTeX - Entry

@InProceedings{galesi_et_al:LIPIcs:2019:10993,
  author =	{Nicola Galesi and Dmitry Itsykson and Artur Riazanov and Anastasia Sofronova},
  title =	{{Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{49:1--49:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Peter Rossmanith and Pinar Heggernes and Joost-Pieter Katoen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10993},
  URN =		{urn:nbn:de:0030-drops-109932},
  doi =		{10.4230/LIPIcs.MFCS.2019.49},
  annote =	{Keywords: Tseitin formula, treewidth, AC0-Frege}
}

Keywords: Tseitin formula, treewidth, AC0-Frege
Collection: 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Issue Date: 2019
Date of publication: 20.08.2019


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI