License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CCC.2021.17
URN: urn:nbn:de:0030-drops-142915
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14291/
Sofronova, Anastasia ;
Sokolov, Dmitry
Branching Programs with Bounded Repetitions and Flow Formulas
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. [László Lovász et al., 1995] 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. [Albert Atserias et al., 2018].
We study the branching programs with bounded repetitions, so-called (1,+k)-BPs (Sieling [Detlef Sieling, 1996]) 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 [Alexander Knop, 2017]).
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 [Detlef Sieling, 1996; Detlef Sieling and Ingo Wegener, 1994; Stasys Jukna and Alexander A. Razborov, 1998] with the modification of the "closure" technique [Michael Alekhnovich et al., 2004; Michael Alekhnovich and Alexander A. Razborov, 2003]. 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 [Michael Alekhnovich and Alexander A. Razborov, 2003].
BibTeX - Entry
@InProceedings{sofronova_et_al:LIPIcs.CCC.2021.17,
author = {Sofronova, Anastasia and Sokolov, Dmitry},
title = {{Branching Programs with Bounded Repetitions and Flow Formulas}},
booktitle = {36th Computational Complexity Conference (CCC 2021)},
pages = {17:1--17:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-193-1},
ISSN = {1868-8969},
year = {2021},
volume = {200},
editor = {Kabanets, Valentine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14291},
URN = {urn:nbn:de:0030-drops-142915},
doi = {10.4230/LIPIcs.CCC.2021.17},
annote = {Keywords: proof complexity, branching programs, bounded repetitions, lower bounds}
}
|
Keywords: |
|
proof complexity, branching programs, bounded repetitions, lower bounds |
|
Collection: |
|
36th Computational Complexity Conference (CCC 2021) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
08.07.2021 |
