Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › научная › Рецензирование
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 авг 2019 → 30 авг 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/19 → 30/08/19 |
ID: 49785080