Proof Complexity of Monotone Branching Programs

Anupam Das; Avgerinos Delkos

doi:10.1007/978-3-031-08740-0_7

Proof Complexity of Monotone Branching Programs

Anupam Das^*, Avgerinos Delkos

^*Corresponding author for this work

Computer Science

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

Abstract

We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC¹, respectively.

The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT⁺ is obtained by restricting their systems to a positive syntax, similarly to how the ‘monotone sequent calculus’ MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas.

Our main result is that eLNDT⁺ polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudlák, that was recently improved to a bona fide polynomial simulation via works of Jeřábek and Buss, Kabanets, Kolokolova and Koucký. Along the way we formalise several properties of counting functions within eLNDT⁺ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.

Original language	English
Title of host publication	Revolutions and Revelations in Computability
Subtitle of host publication	18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings
Editors	Ulrich Berger, Johanna N.Y. Franklin, Florin Manea, Arno Pauly
Publisher	Springer
Pages	74-87
Number of pages	14
Edition	1
ISBN (Electronic)	9783031087400
ISBN (Print)	9783031087394
DOIs	https://doi.org/10.1007/978-3-031-08740-0_7
Publication status	Published - 26 Jun 2022
Event	18th Conference on Computability in Europe, CiE 2022 - Swansea, United Kingdom Duration: 11 Jul 2022 → 15 Jul 2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13359
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	18th Conference on Computability in Europe, CiE 2022
Country/Territory	United Kingdom
City	Swansea
Period	11/07/22 → 15/07/22

Bibliographical note

Funding Information:
Acknowledgments. This work was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Keywords

Branching Programs
Monotone Complexity
Proof Complexity

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-031-08740-0_7

Structure vs. Invariants in Proofs (StrIP)
Das, A.
Medical Research Council
1/05/20 → 31/07/24
Project: Research Councils

Cite this

Das, A., & Delkos, A. (2022). Proof Complexity of Monotone Branching Programs. In U. Berger, J. N. Y. Franklin, F. Manea, & A. Pauly (Eds.), Revolutions and Revelations in Computability: 18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings (1 ed., pp. 74-87). (Lecture Notes in Computer Science; Vol. 13359). Springer. https://doi.org/10.1007/978-3-031-08740-0_7

Das, Anupam ; Delkos, Avgerinos. / Proof Complexity of Monotone Branching Programs. Revolutions and Revelations in Computability: 18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings. editor / Ulrich Berger ; Johanna N.Y. Franklin ; Florin Manea ; Arno Pauly. 1. ed. Springer, 2022. pp. 74-87 (Lecture Notes in Computer Science).

@inproceedings{b0f847c9fd3447b5981f722c680ff80f,

title = "Proof Complexity of Monotone Branching Programs",

abstract = "We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC1, respectively. The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT+ is obtained by restricting their systems to a positive syntax, similarly to how the {\textquoteleft}monotone sequent calculus{\textquoteright} MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas. Our main result is that eLNDT+ polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudl{\'a}k, that was recently improved to a bona fide polynomial simulation via works of Je{\v r}{\'a}bek and Buss, Kabanets, Kolokolova and Kouck{\'y}. Along the way we formalise several properties of counting functions within eLNDT+ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.",

keywords = "Branching Programs, Monotone Complexity, Proof Complexity",

author = "Anupam Das and Avgerinos Delkos",

note = "Funding Information: Acknowledgments. This work was supported by a UKRI Future Leaders Fellowship, {\textquoteleft}Structure vs Invariants in Proofs{\textquoteright}, project reference MR/S035540/1. Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 18th Conference on Computability in Europe, CiE 2022 ; Conference date: 11-07-2022 Through 15-07-2022",

year = "2022",

month = jun,

day = "26",

doi = "10.1007/978-3-031-08740-0_7",

language = "English",

isbn = "9783031087394",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "74--87",

editor = "Ulrich Berger and Franklin, {Johanna N.Y.} and Florin Manea and Arno Pauly",

booktitle = "Revolutions and Revelations in Computability",

edition = "1",

}

Das, A & Delkos, A 2022, Proof Complexity of Monotone Branching Programs. in U Berger, JNY Franklin, F Manea & A Pauly (eds), Revolutions and Revelations in Computability: 18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings. 1 edn, Lecture Notes in Computer Science, vol. 13359, Springer, pp. 74-87, 18th Conference on Computability in Europe, CiE 2022, Swansea, United Kingdom, 11/07/22. https://doi.org/10.1007/978-3-031-08740-0_7

Proof Complexity of Monotone Branching Programs. / Das, Anupam; Delkos, Avgerinos.
Revolutions and Revelations in Computability: 18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings. ed. / Ulrich Berger; Johanna N.Y. Franklin; Florin Manea; Arno Pauly. 1. ed. Springer, 2022. p. 74-87 (Lecture Notes in Computer Science; Vol. 13359).

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

TY - GEN

T1 - Proof Complexity of Monotone Branching Programs

AU - Das, Anupam

AU - Delkos, Avgerinos

N1 - Funding Information: Acknowledgments. This work was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1. Publisher Copyright: © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2022/6/26

Y1 - 2022/6/26

N2 - We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC1, respectively. The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT+ is obtained by restricting their systems to a positive syntax, similarly to how the ‘monotone sequent calculus’ MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas. Our main result is that eLNDT+ polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudlák, that was recently improved to a bona fide polynomial simulation via works of Jeřábek and Buss, Kabanets, Kolokolova and Koucký. Along the way we formalise several properties of counting functions within eLNDT+ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.

AB - We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC1, respectively. The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT+ is obtained by restricting their systems to a positive syntax, similarly to how the ‘monotone sequent calculus’ MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas. Our main result is that eLNDT+ polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudlák, that was recently improved to a bona fide polynomial simulation via works of Jeřábek and Buss, Kabanets, Kolokolova and Koucký. Along the way we formalise several properties of counting functions within eLNDT+ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.

KW - Branching Programs

KW - Monotone Complexity

KW - Proof Complexity

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

U2 - 10.1007/978-3-031-08740-0_7

DO - 10.1007/978-3-031-08740-0_7

M3 - Conference contribution

AN - SCOPUS:85134184636

SN - 9783031087394

T3 - Lecture Notes in Computer Science

SP - 74

EP - 87

BT - Revolutions and Revelations in Computability

A2 - Berger, Ulrich

A2 - Franklin, Johanna N.Y.

A2 - Manea, Florin

A2 - Pauly, Arno

PB - Springer

T2 - 18th Conference on Computability in Europe, CiE 2022

Y2 - 11 July 2022 through 15 July 2022

ER -

Das A, Delkos A. Proof Complexity of Monotone Branching Programs. In Berger U, Franklin JNY, Manea F, Pauly A, editors, Revolutions and Revelations in Computability: 18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings. 1 ed. Springer. 2022. p. 74-87. (Lecture Notes in Computer Science). Epub 2022 Jun 25. doi: 10.1007/978-3-031-08740-0_7