Standard

On tseitin formulas, read-once branching programs and treewidth. / Glinskih, Ludmila; Itsykson, Dmitry.

Computer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings. ed. / René van Bevern; Gregory Kucherov. Springer Nature, 2019. p. 143-155 (Lecture Notes in Computer Science; Vol. 11532).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Harvard

Glinskih, L & Itsykson, D 2019, On tseitin formulas, read-once branching programs and treewidth. in R van Bevern & G Kucherov (eds), Computer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings. Lecture Notes in Computer Science, vol. 11532, Springer Nature, pp. 143-155, 14th International Computer Science Symposium in Russia, CSR 2019, Novosibirsk, Russian Federation, 1/07/19. https://doi.org/10.1007/978-3-030-19955-5_13

APA

Glinskih, L., & Itsykson, D. (2019). On tseitin formulas, read-once branching programs and treewidth. In R. van Bevern, & G. Kucherov (Eds.), Computer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings (pp. 143-155). (Lecture Notes in Computer Science; Vol. 11532). Springer Nature. https://doi.org/10.1007/978-3-030-19955-5_13

Vancouver

Glinskih L, Itsykson D. On tseitin formulas, read-once branching programs and treewidth. In van Bevern R, Kucherov G, editors, Computer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings. Springer Nature. 2019. p. 143-155. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-19955-5_13

Author

Glinskih, Ludmila ; Itsykson, Dmitry. / On tseitin formulas, read-once branching programs and treewidth. Computer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings. editor / René van Bevern ; Gregory Kucherov. Springer Nature, 2019. pp. 143-155 (Lecture Notes in Computer Science).

BibTeX

@inproceedings{a2ef5c5faecb4c52b97827fdf1afc4eb,
title = "On tseitin formulas, read-once branching programs and treewidth",
abstract = "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).",
keywords = "Grid, Read-once branching program, Treewidth, Tseitin formula, WIDTH",
author = "Ludmila Glinskih and Dmitry Itsykson",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-19955-5_13",
language = "English",
isbn = "9783030199548",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature",
pages = "143--155",
editor = "{van Bevern}, Ren{\'e} and Gregory Kucherov",
booktitle = "Computer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings",
address = "Germany",
note = "14th International Computer Science Symposium in Russia, CSR 2019 ; Conference date: 01-07-2019 Through 05-07-2019",

}

RIS

TY - GEN

T1 - On tseitin formulas, read-once branching programs and treewidth

AU - Glinskih, Ludmila

AU - Itsykson, Dmitry

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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).

AB - 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).

KW - Grid

KW - Read-once branching program

KW - Treewidth

KW - Tseitin formula

KW - WIDTH

UR - http://www.scopus.com/inward/record.url?scp=85068599079&partnerID=8YFLogxK

UR - http://www.mendeley.com/research/tseitin-formulas-readonce-branching-programs-treewidth

U2 - 10.1007/978-3-030-19955-5_13

DO - 10.1007/978-3-030-19955-5_13

M3 - Conference contribution

AN - SCOPUS:85068599079

SN - 9783030199548

T3 - Lecture Notes in Computer Science

SP - 143

EP - 155

BT - Computer Science – Theory and Applications - 14th International Computer Science Symposium in Russia, CSR 2019, Proceedings

A2 - van Bevern, René

A2 - Kucherov, Gregory

PB - Springer Nature

T2 - 14th International Computer Science Symposium in Russia, CSR 2019

Y2 - 1 July 2019 through 5 July 2019

ER -

ID: 49785149