Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR21-028 | 27th February 2021 20:24

Branching Programs with Bounded Repetitions and $\mathrm{Flow}$ Formulas

RSS-Feed




TR21-028
Authors: Anastasia Sofronova, Dmitry Sokolov
Publication: 27th February 2021 21:40
Downloads: 109
Keywords: 


Abstract:

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. '95 who showed the equivalence between regular Resolution and read-once branching programs for ``unsatisfied clause search problem'' ($\mathrm{Search}_{\varphi}$). This connection is widely used, in particular, in the recent breakthrough result about the Clique problem in regular Resolution by Atserias et al. '18.

We study the branching programs with bounded repetitions, so-called $(1, +k)$-BPs (Sieling '96) in application to the $\mathrm{Search}_{\varphi}$ 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 '17).

We deal with $\mathrm{Search}_{\varphi}$ 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 $\mathrm{Search}_{\varphi}$. To do it we combine a well-known technique for proving lower bounds on the size of branching programs (Sieling '96; Sieling, Wegener '94; Jukna, Razborov '98) with the modification of the ``closure'' technique (Alekhnovich et al. 04; Alekhnovich, Razborov '03). In contrast with the 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 $\mathrm{Flow}$ formulas introduced in (Alekhnovich, Razborov '03).



ISSN 1433-8092 | Imprint