Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proof complexity of positive branching programs

Anupam Das, Avgerinos Delkos

TL;DR

The paper analyzes the proof complexity of systems based on positive NBPs, showing that the positive-syntax variant $\mathsf{e}\mathsf{LNDT}^{+}$ polynomially simulates the original $\mathsf{eLNDT}$ on positive sequents. It develops the $\mathsf{eLNDT}^{+}$ calculus, leverages counting-function representations via polynomial-size NBPs (notably polynomial-size $\mathrm{OBDD}$-based constructions), and establishes polynomial-size proofs for counting properties and the propositional pigeonhole principle. The approach adapts counting-argument techniques from the MLK/Atserias–Jerábek lineage to the NBPs setting, including careful treatment of negative literals and iterative substitutions. Overall, the work advances monotone proof complexity for non-deterministic branching programs and demonstrates how positive representations yield efficient proofs for core combinatorial principles.

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, just 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.

Proof complexity of positive branching programs

TL;DR

The paper analyzes the proof complexity of systems based on positive NBPs, showing that the positive-syntax variant polynomially simulates the original on positive sequents. It develops the calculus, leverages counting-function representations via polynomial-size NBPs (notably polynomial-size -based constructions), and establishes polynomial-size proofs for counting properties and the propositional pigeonhole principle. The approach adapts counting-argument techniques from the MLK/Atserias–Jerábek lineage to the NBPs setting, including careful treatment of negative literals and iterative substitutions. Overall, the work advances monotone proof complexity for non-deterministic branching programs and demonstrates how positive representations yield efficient proofs for core combinatorial principles.

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, just 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.

Paper Structure

This paper contains 9 sections, 1 theorem, 3 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Contribution
  3. Preliminary version
  4. A terminological convention
  5. Preliminaries on proof complexity and branching programs
  6. Proof complexity
  7. Non-deterministic branching programs
  8. Representation of NBPs by extended formulas
  9. The system eLNDT

Key Result

Theorem 2.1

There is a propositional proof system with polynomial-size proofs of each tautology if and only if $\mathit{co}\mathbf{NP} = \mathbf{NP}$.

Figures (1)

  • Figure 1: A branching program computing the 2-out-of-4 Exact function. $0$-edges are indicated dotted, and $1$ edges are indicated solid.

Theorems & Definitions (8)

  • Theorem 2.1: Cook-Reckhow
  • Example 1: 2-out-of-4 Exact
  • Remark 2: Distinguishing extension variables
  • Definition 3: Extension axioms
  • Definition 4: Semantics of eNDT formulas
  • Example 5: 2-out-of-4 Exact, revisited
  • Remark 6: $\mathcal{A}$-induction
  • Definition 8: Systems $\mathsf{LNDT}$ and $\mathsf{e}\mathsf{LNDT}$