Нижние оценки для ветвящихся программ с ограниченными повторениями на задачи поиска

Propositional proof complexity theory studies proof systems for UNSAT, the language of unsatisfiable propositional formulas. Studying lower bounds on size of such proofs is closely related to the question whether NP and coNP coincide or not. Non-equivalence of those classes would be equivalent to existence of hard formulas for any propositional proof system — that is, formulas which do not have short, polynomial-size proofs.
There exists so-called Cook’s program, which proposes to prove superpolynomial lower bounds for stronger and stronger proof systems until the techniques are developed to do it in a general case. Currently there exist lower bounds only for some specific proof systems.
For many proof systems, the proofs describe the runs of specific classes of SAT-solving al- gorithms. Which means that lower bounds of the size of proofs give us lower bounds on run- ning time of SAT- solvers, as well as some other algorithms. For example, Resolution describes DPLL algorithms [DLL62; Gol79], Cutting Planes corresponds to combinatorial optimization [Gom58; Gom60; Gom63], Nullstellensatz and Polynomial Calculus are related to calculating Gröbner basis [CEI96; Bus+97]. For all those systems there are known lower bounds. The majority of theorem-proving systems is based on propositional proofs as well.
Proofs of unsatisfiability of a formula are closely connected to a certain search relation: given an assignment, it is required to find an unsatisfied clause. Formally it is defined in the following way:

Definition 1.2
An unsatisfied clause search problem Search for an unsatisfiable CNF formula ≔ ⋀ on variables is defined as follows:
∈
input: an -variable assignment ∈ {0, 1} ;
output: an element ∈ such that clause of is falsified by .
Informally speaking, we may think that if we can solve the Search problem in some computational model C, then the description of ∈ C that solves Search is a “certificate of unsatisfiability” of a formula . So we may think of this model as a proof system.
We study a computational model named branching programs. A proof system based on 3
this model could be defined in a way described above [Kno17]. Regular Resolution, which is the restriction of general Resolution, is, in those terms, equivalent to a read-once branching program that searches for an unsatisfied clause [Lov+95].
Branching program is a computational model that is described by a directed acyclic graph. In each vertex a variable is queried, and we proceed along one of the outgoing edges depending on its value. A total assignment corresponds to a path from source to one of the sinks (a computation path), and in the sink a value of a function is written. Let us state the formal definition.
Definition 1.3
Let ≔ { 1, … , } be a set of propositional variables and be a finite set.
A branching program for a relation ⊆ {0, 1} × is a directed acyclic graph with one source. Every sink of the graph is labeled with ∈ , every inner vertex is
labeled with ∈ and it has exactly two outgoing edges labeled by 0 and 1.
Every total assignment : → {0, 1} to variables induces a path in a branch- ing program in the following way. We start in the root of the program. If the current
vertex is labeled with variable , we proceed along the edge ( ).
Let ∈ be the label in the sink we ended up in. We require the following property:
( ( 1), … , ( ), ) ∈ .
This is one of the most fundamental models in theoretical computer science: it captures the space complexity of many versions of restricted and unrestricted Turing machine etc. The read-once version queries each bit only once on every path. This model corresponds to the eraser Turing machines. Exponential lower bounds for this model were proven in [Weg88; Žák86].
The connection between regular Resolution and branching programs makes it interesting to consider some less restricted models of branching programs in application to the Search problems. Some of these models were considered in [Kno17]. In this paper we focus on (1, + )-BPs (branching programs with bounded repetitions).
It is a natural generalization of read-once branching programs that was described in [Sie96]. In this model, we allow our branching programs to requery variables, but on each computation only input bits may be queried more than one time. There are two natural points of view on this model:
syntactic: if we apply the restriction on every path;
semantic: if we apply the restriction on consistent paths
(for formal definition see section 2.1). The semantic version is more powerful and may capture
strong Turing machine models (for details see [JR98]). 4

Exponential lower bounds on (1, + )-BP were shown in [SŽ97; Sie96; SW94; JR98] for various parameters . Lower bounds from [JR98] hold for = Ω ( ) and the lower bound
log
from [Juk08] holds even for = Ω( ), where is the number of input bits. We refer the
reader to the books [Juk12; Weg00] with the detailed description of results related to branching programs.
Described lower bounds for (1, + )-BP are given for “complicated” functions (usually it is characteristic functions of an error-correcting code with additional properties). In particular, these functions are complicated in terms of the certificate complexity, which is not true for Search relation, so the usual techniques do not work in this case. Despite the success in proving lower bounds on the Resolution (and hence read-once programs) the lower bounds for (1, + )-BP on the Search are an open question even for = 1.
Apart from small certificate complexity, there arises another issue in proving lower bounds on Search . It is that (1, + )-BP is much stronger than general Resolution on some classes of formulas [Kno17] even for small constant and syntactic model. This is a crucial observation and it means that we cannot directly apply general techniques for proving lower bounds in proof complexity like [BW01; AR03] etc., since these techniques cannot distinguish between considered classes of formulas and other hard examples for Resolution. Hence if we want to prove lower bound for (1, + )-BP on Search we need some additional arguments in comparison to Resolution lower bounds.
In this work, we introduce a technique for proving such lower bounds on the semantic (1, + )-BP where = (log / log log ) where is the number of variables.
1.1 Our results
The main result is an exponential lower bound on the size of (1, + )-BPs in application
to Search

for = ( log ). log log