Proof complexity of systems of branching programs

Delkos, Avgerinos (2024). Proof complexity of systems of branching programs. University of Birmingham. Ph.D.

Preview

Delkos2024PhD.pdf
Text - Accepted Version
Available under License Creative Commons Attribution Non-commercial.
Download (1MB) | Preview

Abstract

This work investigates the proof complexity of multiple systems about deterministic and non-deterministic branching programs (BPs and NBPs respectively). It is based on work by Buss, Das and Knop, where they defined the systems eLpNqDT reasoning with (N)BPs by using extension variables/axioms to represent the dag-structure, over a language of (non-deterministic) decision trees.
We start by focusing on positive branching programs (PBPs) i.e. NBPs where, for any 0-transition between two nodes, there is also a 1-transition. PBPs compute mono-tone Boolean functions, much like negation-free circuits or formulas do, but constitute a positive version of (non- uniform) NL, rather than P or NC1, respectively. We introduce eLNDT`, the positive fragment of eLNDT, that reasons about PBPs by considering restrictions on the form of inference rules we consider. The main result is that eLNDT` polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK (␣-free LK) and LK by Atserias, Galesi and Pudl´ak.
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 proofs of thepropositional pigeonhole principle.

Our second contribution aims at defining Prover-Adversary games bespoke to the setting of branching programs. It builds upon work by Pudl´ak and Buss who defined a game with Boolean formulas as queries that corresponds to Hilbert-Frege/LK i.e. the canonical systems for reasoning about Boolean formulas. We adopt their definition to fit in our setting and provide games that correspond to eLDT and eLNDT. While the deterministic case is simple enough, the non-deterministic one requires simulating negations of NBPs for which, through a series of technical results, we formalize a (partial) non-uniform version of the Immerman-Szelepcs´enyi Theorem: NL “ coNL.
The last part of this thesis presents the system o-eLDT, a specifically designed fragment of eLDT that reasons about ordered BPs (OBDDs).These are BPs whose paths only exhibit variables under a fixed order. Due to their ‘restricted’ nature, they posses
multiple nice properties, for example, easy checking for equivalence between OBDDs. They have recently received wide interest in the literature with their proof (complexity) theoretic analysis initiated by work from Atserias, Kolaitis and Vardi where they, among others, defined the system OBDDp^, wq. We finish by comparing the expressive strength of o-eLDT and OBDDp^, wq, concluding that the former polynomially
simulates the latter.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):