DOI

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.

Язык оригиналаанглийский
Название основной публикации44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019
РедакторыJoost-Pieter Katoen, Pinar Heggernes, Peter Rossmanith
ИздательSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (электронное издание)9783959771177
ISBN (печатное издание)9783959771177
DOI
СостояниеОпубликовано - авг 2019
Событие44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019 - Aachen, Германия
Продолжительность: 26 авг 201930 авг 2019

Серия публикаций

НазваниеLeibniz International Proceedings in Informatics, LIPIcs
Том138
ISSN (печатное издание)1868-8969

конференция

конференция44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019
Страна/TерриторияГермания
ГородAachen
Период26/08/1930/08/19

    Предметные области Scopus

  • Программный продукт

ID: 49785080