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).