TY - GEN

T1 - Branching programs with bounded repetitions and flow formulas

AU - Sofronova, Anastasia

AU - Sokolov, Dmitry

N1 - Publisher Copyright: © Anastasia Sofronova and Dmitry Sokolov; licensed under Creative Commons License CC-BY 4.0

PY - 2021/7/1

Y1 - 2021/7/1

N2 - Restricted branching programs capture various complexity measures like space in Turing machines or length of proofs in proof systems. In this paper, we focus on the application in the proof complexity that was discovered by Lovasz et al. [14] who showed the equivalence between regular Resolution and read-once branching programs for “unsatisfied clause search problem” (Searchφ). This connection is widely used, in particular, in the recent breakthrough result about the Clique problem in regular Resolution by Atserias et al. [5]. We study the branching programs with bounded repetitions, so-called (1,+k)-BPs (Sieling [21]) in application to the Searchφ problem. On the one hand, it is a natural generalization of read-once branching programs. On the other hand, this model gives a powerful proof system that can efficiently certify the unsatisfiability of a wide class of formulas that is hard for Resolution (Knop [13]). We deal with Searchφ that is “relatively easy” compared to all known hard examples for the (1,+k)-BPs. We introduce the first technique for proving exponential lower bounds for the (1,+k)-BPs on Searchφ. To do it we combine a well-known technique for proving lower bounds on the size of branching programs [12,21,22] with the modification of the “closure” technique [1,3]. In contrast with most Resolution lower bounds, our technique uses not only “local” properties of the formula, but also a “global” structure. Our hard examples are based on the Flow formulas introduced in [3].

AB - Restricted branching programs capture various complexity measures like space in Turing machines or length of proofs in proof systems. In this paper, we focus on the application in the proof complexity that was discovered by Lovasz et al. [14] who showed the equivalence between regular Resolution and read-once branching programs for “unsatisfied clause search problem” (Searchφ). This connection is widely used, in particular, in the recent breakthrough result about the Clique problem in regular Resolution by Atserias et al. [5]. We study the branching programs with bounded repetitions, so-called (1,+k)-BPs (Sieling [21]) in application to the Searchφ problem. On the one hand, it is a natural generalization of read-once branching programs. On the other hand, this model gives a powerful proof system that can efficiently certify the unsatisfiability of a wide class of formulas that is hard for Resolution (Knop [13]). We deal with Searchφ that is “relatively easy” compared to all known hard examples for the (1,+k)-BPs. We introduce the first technique for proving exponential lower bounds for the (1,+k)-BPs on Searchφ. To do it we combine a well-known technique for proving lower bounds on the size of branching programs [12,21,22] with the modification of the “closure” technique [1,3]. In contrast with most Resolution lower bounds, our technique uses not only “local” properties of the formula, but also a “global” structure. Our hard examples are based on the Flow formulas introduced in [3].

KW - Bounded repetitions

KW - Branching programs

KW - Lower bounds

KW - Proof complexity

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

UR - https://www.mendeley.com/catalogue/d50c21ab-8b76-3fde-b281-86d56f0ccee9/

U2 - 10.4230/LIPIcs.CCC.2021.17

DO - 10.4230/LIPIcs.CCC.2021.17

M3 - Conference contribution

AN - SCOPUS:85115333845

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 36th Computational Complexity Conference, CCC 2021

A2 - Kabanets, Valentine

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 36th Computational Complexity Conference, CCC 2021

Y2 - 20 July 2021 through 23 July 2021

ER -