Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › научная › Рецензирование
We show that any nondeterministic read-once branching program that decides a satisfiable Tseitin formula based on an n× n grid graph has size at least 2Ω(n). Then using the Excluded Grid Theorem by Robertson and Seymour we show that for arbitrary graph G(V, E) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on G has size at least (formula presented) for all (formula presented)1/36, where tw (G) is the treewidth of G (for planar graphs and some other classes of graphs the statement holds for δ= 1). We also show an upper bound of (formula presented), where pw (G) is the pathwidth of G. We apply the mentioned results to the analysis of the complexity of derivations in the proof system OBDD (∧, reordering) and show that any OBDD (∧, reordering) -refutation of an unsatisfiable Tseitin formula based on a graph G has size at least (formula presented).
Язык оригинала | английский |
---|---|
Название основной публикации | Computer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings |
Редакторы | René van Bevern, Gregory Kucherov |
Издатель | Springer Nature |
Страницы | 143-155 |
Число страниц | 13 |
ISBN (печатное издание) | 9783030199548 |
DOI | |
Состояние | Опубликовано - 1 янв 2019 |
Событие | 14th International Computer Science Symposium in Russia, CSR 2019 - Novosibirsk, Российская Федерация Продолжительность: 1 июл 2019 → 5 июл 2019 |
Название | Lecture Notes in Computer Science |
---|---|
Издатель | SPRINGER INTERNATIONAL PUBLISHING AG |
Том | 11532 |
ISSN (печатное издание) | 0302-9743 |
конференция | 14th International Computer Science Symposium in Russia, CSR 2019 |
---|---|
Страна/Tерритория | Российская Федерация |
Город | Novosibirsk |
Период | 1/07/19 → 5/07/19 |
ID: 49785149