# On Obdd-Based Algorithms and Proof Systems that Dynamically Change Order of Variables

Dmitry Itsykson, Alexander Knop, Andrei Romashchenko, Dmitry . Sokolov

► To cite this version:

Dmitry Itsykson, Alexander Knop, Andrei Romashchenko, Dmitry . Sokolov. On Obdd-Based Algorithms and Proof Systems that Dynamically Change Order of Variables. The Journal of Symbolic Logic, 2020, 85 (2), pp.632-670. 10.1017/jsl.2019.53 . lirmm-02885744v2

HAL Id: lirmm-02885744

https://hal-lirmm.ccsd.cnrs.fr/lirmm-02885744v2

Submitted on 10 Nov 2020

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On OBDD-based algorithms and proof systems that dynamically change order of variables

Dmitry Itsykson³, Andrei Romashchenko², ⁵, Alexander Knop³, ⁴, and Dmitry Sokolov¹, ³

¹KTH Royal Institute of Technology

²LIRMM, Univ Montpellier, CNRS, Montpellier, France

³St. Petersburg Department of V.A. Steklov Institute of Mathematics of the Russian Academy of Sciences

⁴University of California, San Diego

⁵On leave from IITP RAS

dmitrits@pdmi.ras.ru, aknop@ucsd.edu, andrei.romashchenko@lirmm.fr, sokolovd@kth.se

January 4, 2019

## Abstract

In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. We initiate the study of OBDD based proof systems that additionally contain a rule that allows changing the order in OBDDs. At first we consider a proof system $OBDD(\wedge, \text{reordering})$ that uses the conjunction (join) rule and the rule that allows changing the order. We exponentially separate this proof system from $OBDD(\wedge)$ proof system that uses only the conjunction rule. We prove two exponential lower bounds on the size of $OBDD(\wedge, \text{reordering})$ refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for $OBDD(\wedge)$ proofs and the second one extends the result of Tveretina et al. from $OBDD(\wedge)$ to $OBDD(\wedge, \text{reordering})$.

In 2004 Pan and Vardi proposed an approach to the propositional satisfiability problem based on OBDDs and symbolic quantifier elimination (we denote algorithms based on this approach as $OBDD(\wedge, \exists)$ algorithms). An instance of the propositional satisfiability problem is considered as an existential quantified propositional formula. The algorithm chooses an order on variables and creates an ordered binary decision diagram (OBDD) $D$ that initially represents the constant 1 function. Then the algorithm downloads to $D$ clauses of the CNF one by one, and applies to $D$ the elimination of the existential quantifier for variable $x$ if all clauses that contain $x$ are already downloaded. We augment these algorithms with the operation of reordering of variables and call the new scheme $OBDD(\wedge, \exists, \text{reordering})$ algorithms. We notice that there exists an $OBDD(\wedge, \exists)$ algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time. In contrast, we show that there exist formulas representing systems of linear equations over $\mathbb{F}_2$ that are hard for $OBDD(\wedge, \exists, \text{reordering})$ algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over $\mathbb{F}_2$ that correspond to some checksum matrices of error correcting codes.

## 1 Introduction

An ordered binary decision diagram (OBDD) represents a Boolean function. A Boolean function is represented as a branching program with two sinks such that on every path from the source to a sink variable appears in the same order. This restriction on the order of variables allows handling the diagrams (compute binary Boolean operations on diagrams, compute projections, or test satisfiability) very efficiently.

Atserias, Kolaitis and Vardi [2] proposed an OBDD-based proof system. This system is meant to prove that a given CNF formula is unsatisfiable. For some order of variables $\pi$ we represent clauses of the input
formula as a π-ordered BDD; we may derive a new OBDD applying either the conjunction rule or the weakening rule. (The authors of [2] supplied the system with one more rule — the projection, which derives ∃xD from D; we consider this rule as a special case of the weakening rule, so we do not need to allow it explicitly.) A proof in this system is a derivation of an OBDD that represents the constant false function. We refer to this proof system as the OBDD(∧, weakening) proof system. The OBDD(∧, weakening) proof system simulates Cutting Planes with unary coefficients and thus it is stronger than Resolution. This proof system provides also short refutations for the formulas that represent unsatisfiable systems of linear equations over F₂ [2], while linear systems are hard for Resolution. This observation motivates the study of the OBDD-based algorithms (notice that the popular DPLL and CDCL algorithms correspond to tree-like and DAG-like Resolutions).

Several strong lower bounds are known for different versions of OBDD proof systems. Segerlind [20] proved an exponential lower bound for the tree-like version of OBDD(∧, weakening) proof system using the communication complexity technique proposed in [3]. Krajicek [14] proved an exponential lower bound for the DAG-like version of it using monotone feasible interpolation. Several papers study the OBDD-based proof system that has only one inference rule — the conjunction rule (we refer to this system as OBDD(∧) proof system). Groote and Zantema [11] showed that there is a formula φ (not in CNF) such that Tseitin transformation of this formula does not have a short resolution proof but φ has short OBDD(∧) proof. Tveretina, Sinz and Zantema [22] proved the lower bound 2<sup>Ω(n)</sup> for the pigeonhole principle $PHP_n^{n+1}$ in the OBDD(∧) proof system. Friedman and Xu [9] proved an exponential lower bound for the complexity of random unsatisfiable 3CNF formulas in restricted versions of OBDD(∧) proof systems (with a fixed order of the variables) and an exponential lower bound for the running time on random unsatisfiable 3XOR formulas of restricted versions of OBDD(∧) proof systems (with fixed orders of application of rules).

An interesting approach to solving propositional satisfiability was suggested by Pan and Vardi [19]. They proposed an algorithm that chooses some order π on the variables of the input CNF formula *F* and creates the current π-ordered BDD *D* that initially represents the constant true function, and a set of clauses *S* that initially consists of all clauses of the formula *F*. Then the algorithm applies the following operations in an arbitrary order:

**conjunction (or join):** choose a clause *C* ∈ *S*, delete it from *S* and replace *D* by the π-ordered BDD representing *C ∧ D*;

**projection (or ∃-elimination):** choose a variable *x* that has no occurrence in the clauses from *S* and replace *D* by the π-ordered BDD representing ∃xD.

When *S* becomes empty, the algorithm stops and reports “unsatisfiable” if *D* represents the constant false function and “satisfiable” otherwise. Every particular instance of this algorithm uses its own strategies to choose an order of variables π and an order of application of the operations. We refer to these algorithms as OBDD(∧, ∃) algorithms.

Pan and Vardi [19] investigated some specific strategies and compared them with DPLL based SAT solvers and SAT solvers based on OBDDs without quantifier eliminations (we call them OBDD(∧) algorithms). Experiments showed in particular that OBDD(∧, ∃) algorithms are faster than OBDD(∧) algorithms [19]. A result of [6] implies that an OBDD(∧, ∃) algorithm can solve $PHP_n^{n+1}$ in polynomial time. The lower bounds for the OBDD(∧, weakening) proof systems mentioned above imply the same lower bounds for the OBDD(∧, ∃) algorithms.

## 1.1 Statement of the problem

It is known that changing the order of the variables in an OBDD can be performed in time polynomial in the sizes of the input and the output [17]. So it seems to be very restrictive to use the same order of variables in all OBDDs in the proof. Hence, we propose to strengthen the OBDD proof systems with a supplementary rule that dynamically reorders the variables in OBDDs.

In OBDD proofs, reordering rule may be applied to an arbitrary OBDD from the proof but the conjunction rule may be applied only to OBDDs with the same order since the verification of the application of the
conjunction to OBDDs in different orders is hard (this problem is coNP-complete, see [18, Lemma 8.14]).

The first aim of this paper is to prove lower bounds for the OBDD-based algorithms and proof systems that use the reordering rule. The second aim is to show that reordering of the variables is really useful; we give examples of formulas that are hard for the OBDD-based proof systems without reordering and easy with reordering.

## 1.2 Our results

In Section 3, we consider the $OBDD(\wedge, \text{reordering})$ proof system. We prove two exponential lower bounds for size of $OBDD(\wedge, \text{reordering})$-derivations of the pigeonhole principle $PHP_n^{n+1}$ and Tseitin formulas based on constant-degree algebraic expanders. The lower bound for pigeonhole principle extends the result of Tveretina et al. [22] from $OBDD(\wedge)$ proofs to $OBDD(\wedge, \text{reordering})$ proofs. (Besides, we believe that our argument is simpler than the proof in [22].) The result for Tseitin formulas, to the best of our knowledge, was not known even for the more restrictive $OBDD(\wedge)$ proofs. In both arguments we use the same strategy:

* At first step, we prove an exponential lower bound on the size of the OBDD-representation for an appropriate satisfiable formula. Assume that the original unsatisfiable formula is minimally unsatisfiable. Roughly speaking, the satisfiable formula under consideration is equal to the original unsatisfiable formula with one canceled clause. For example, for the pigeonhole principle the appropriate satisfiable formula would be $PHP_n^n$; for the Tseitin formulas such an appropriate formula is a satisfiable Tseitin formula. This part of the proof is quite cumbersome but it involves only rather elementary techniques of lower bounds for OBDD.

* Consider the last derivation step. It consists in the conjunction for $F_1$ and $F_2$ in the same order $\pi$. Our goal is to prove that at least one of $F_1$ and $F_2$ has an exponential size. Both $F_1$ and $F_2$ are satisfiable and they are conjunctions of different sets of clauses of the initial formulas. The idea is to construct partial substitutions $\rho_1$ and $\rho_2$ with the same support such that the formula $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is isomorphic to the satisfiable formula from the first step. Then any OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has exponential size. Hence, the size of either $F_1|_{\rho_1}$ or $F_2|_{\rho_2}$ is large for the order $\pi$. Thus, the size of either $F_1$ or $F_2$ is large for the order $\pi$.

In Section 4, we construct an example of a family of formulas that are easy for the $OBDD(\wedge, \text{reordering})$ proof system but hard for the $OBDD(\wedge)$ proof system.

In Section 5, we study $OBDD(\wedge, \exists, \text{reordering})$ algorithms. At first, we notice that there exists an $OBDD(\wedge, \exists)$ algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time. In contrast, we show that there exist formulas representing systems of linear equations over $\mathbb{F}_2$ that are hard for $OBDD(\wedge, \exists, \text{reordering})$ algorithms. More specifically, we describe a construction of a family of satisfiable formulas $F_n$ on $n$ variables in $O(1)$-CNF such that every $OBDD(\wedge, \exists, \text{reordering})$ algorithm runs at least $2^{\Omega(n)}$ steps on $F_n$.

The plan of the proof is as follows.

* We prove that if $C \subseteq \{0, 1\}^n$ is the set of codewords of a list-decodable code that allows to correct $\frac{2}{3}n$ of erasures, then every OBDD that represents the characteristic function of $C(\chi_C)$ has a big size (this size proved to be close to the number of all codewords in the code). Moreover, this property holds even for the projections of $\chi_C$ onto any $\frac{1}{6}n$ coordinates. Notice that a similar result was known for error-correcting codes with large enough minimal distance (see for example the paper of Duris et al. [8]). Guruswami [12] showed that the codes with large enough minimal distance are erasure list-decodable but the opposite statement does not hold.

* In Section 6.1, we give a randomized construction of the required linear code. This construction is based on random checksum matrix. We use the codes of Gallager [10] that contain $O(1)$ ones per row. We prove that such a random code with a high probability enjoys the following expansion property: every $\frac{1}{6}n$ columns of the matrix contain ones in almost all rows. And in Section 6.2 we give an explicit construction of the required linear code.
• We consider the execution of an OBDD($\wedge, \exists$, reordering) algorithm on CNF formula that corresponds to the CNF representation of the checksum matrix of the code. We study two cases:

1. the algorithm applies the projection rule less than $\frac{n}{6}$ times;

2. the projection rule is applied at least $\frac{n}{6}$ times.

In the first case, we focus on the OBDD at the end of the execution of the algorithm; its size should be exponential due to the properties of the code. In the second case, we consider the first moment in the computational process when we apply exactly $\frac{n}{6}$ projection operations. By the expansion property, OBDD $D$ is a projection of almost the entire formula, thus its size should be close to the size of the OBDD of the characteristic function of the code. That is, the size of $D$ should be large enough.

As we mentioned above, the previously known lower bounds for tree-like and DAG-like OBDD($\wedge, \text{weakening}$) proofs imply lower bounds for OBDD($\wedge, \exists$) algorithms. So, what is new in our results comparative to the lower bounds proven by Segerlind [21] and Krajíček [14]? First of all, our lower bound also works for the reordering operation. The second advantage of our construction is that we come up with quite a natural class of formulas (our formulas represent linear systems of equations that define some error correcting codes), while the constructions in [14,21] seem to be rather artificial. Further, we prove the lower bound $2^{\Omega(n)}$ for a formula with $n$ variables, whereas the previously known lower bounds are of the type $2^{n^\epsilon}$ (for some $\epsilon < 1/5$). Besides, we proposed a new technique that might be applicable for other classes of formulas.

# 2 Preliminaries

## 2.1 OBDD

An ordered binary decision diagram (OBDD) is a data structure that is used to represent Boolean functions. Let $\Gamma = \{x_1, \dots, x_n\}$ be a set of propositional variables. A binary decision diagram is a directed acyclic graph with one source. Every vertex of the graph is labeled by a variable from $\Gamma$ or by constants 0 or 1. If a vertex is labeled by a constant, then it is a sink (has out-degree 0). If a vertex is labeled by a variable, then it has exactly two outgoing edges: one edge is labeled by 0 and the other edge is labeled by 1. Every binary decision diagram defines a Boolean function $\{0,1\}^n \rightarrow \{0,1\}$. The value of the function for given values of $x_1, \dots, x_n$ is computed as follows: we start a path at the source and on every step we go along the edge that corresponds to the value of the variable at the current vertex. Every such path reaches a sink labeled by the constant; this constant is the value of the function. The size of an OBDD is equal to the number of vertices in the graph.

Let $\pi$ be a permutation of the set $\{1, \dots, n\}$. A $\pi$-ordered binary decision diagram (BDD) is a binary decision diagram such that on every path from the source to a sink every variable has at most one occurrence and variable $x_{\pi(i)}$ can not appear before $x_{\pi(j)}$ if $i > j$. An ordered binary decision diagram (OBDD) is a $\pi$-ordered binary decision diagram for some permutation $\pi$. Additionally, a binary decision diagram is called $k$-OBDD if every path from the source to a leaf can be split into at most $k$ parts such that in each part the variables appears with respect to a fixed order $\pi$.

OBDDs have the following nice property: for every order of variables every Boolean function has a unique minimal OBDD. For a given order $\pi$, the minimal OBDD of a function $f$ may be constructed in polynomial time from any $\pi$-ordered BDD for the same $f$. There are also known polynomial-time algorithms that efficiently perform the operations of conjunction, negation, disjunction, and projection (elimination of the existential quantifier) to $\pi$-ordered BDDs [17]. There is an algorithm running in time polynomial in the size of the input and the output that gets as an input a $\pi$-ordered diagram $A$, a permutation $\rho$ and returns the minimal $\rho$-ordered diagram that represents the same function as $A$ [17].
## 2.2 Communication Complexity

In order to prove lower bounds on the size of an OBDD representation of a function we will use communication complexity.

Let $f: \{0,1\}^n \to \{0,1\}$ be some function and $\Pi = (\Pi_0, \Pi_1)$ be a partition of $[n]$ i.e. $\Pi_0 \cup \Pi_1 = [n]$ and $\Pi_0 \cap \Pi_1 = \emptyset$. Two players Alice and Bob want to compute $f(x)$ for some $x$. However, Alice knows only bits of $x$ with indices from $\Pi_0$ and Bob knows bits of $x$ with indices from $\Pi_1$. In order to compute the value they can use a two-sided communication channel. They agreed in advance about a protocol; on each step of the protocol one of them send a bit string to another, at the end of the protocol both Alice and Bob should know $f(x)$. The cost of the protocol is the maximal number of bits they sent to each other. The communication complexity of $f$ with respect to the partition $\Pi$ is equal to the minimal cost of the protocols for $f$ (for the formal definition see [15]).

It is well-known that there is a connection between communication complexity and the minimal size of an OBDD representation.

**Lemma 2.1 ([15]).** Let $f: \{0,1\}^n \to \{0,1\}$ be a Boolean function, $\Pi$ be a partition of $[n]$. Then for any order $\pi$ such that elements of $\Pi_0$ precedes elements of $\Pi_1$ in this order, any $\pi$-OBDD representation of $f$ has size at least $2^C$ where $C$ is equal to the communication complexity of $f$ with respect to $\Pi$.

Moreover, the size of every $\pi$-$k$-OBDD representation of $f$ is at least $2^C/2k$.

*Proof.* Let us fix some $\pi$-$k$-OBDD representation $D$ of $f$. Let us consider the path $p$ in $D$ from the source to a sink corresponding to the Alice and Bob's input $x$.

Since $D$ is a $k$-OBDD, this path can be split into $k$ parts so that in each part all variables appear according to the order $\pi$. This implies that the path can be split into $2k$ blocks so that in each block either all variables are known to Alice or all variables are known to Bob.

Let us show that Alice and Bob can find the sink of the path using $2k \log |D|$ bits of communication. They do it in $2k$ rounds; starting from the source (which is known to both of them) they follow the path, and on each round one of the players sends to the other the name of the vertex where the current block ends; at the end, when one player reaches the sink, this player communicate the name of the sink to the other one. The value $f(x)$ is determined by the sink vertex. Hence, the communication complexity of $f$ is at most $(2k+1) \log |D|$. $\square$

In what follows, we will need to prove lower bounds on communication complexity. First of all we recall the technique of combinatorial rectangles. Let $f: X \times Y \to \{0,1\}$ be a function. We say that $R = A \times B$ is a 1-monochromatic rectangle for $f$ iff $A \subseteq X$, $B \subseteq Y$, and for every $a \in A$ and $b \in B$, $f(a,b) = 1$. We say that a sequence of rectangles $R_1, \dots, R_\ell$ is a partition of $X \times Y$ into 1-monochromatic rectangles iff

* $R_i \cap R_j = \emptyset$ for every $i, j \in [\ell]$ and

* for every $x \in X$ and $y \in Y$, $f(x,y) = 1$ iff $(x,y) \in R_i$, for some $i$.

**Lemma 2.2 ([15]).** Let $f: \{0,1\}^n \to \{0,1\}$ be a Boolean function and $\Pi$ be a partition of $[n]$. If any partition of $\{0,1\}^{\Pi_0} \times \{0,1\}^{\Pi_1}$ into 1-monochromatic rectangles has at least $T$ rectangles, then the communication complexity of $f$ is at least $\log T$.

**Lemma 2.3.** Let $f: \{0,1\}^n \to \{0,1\}$ be a Boolean function and $\Pi$ be a partition of $[n]$. If there are substitutions $\rho_1, \dots, \rho_\ell$ to the variables $\{x_i \mid i \in \Pi_0\}$ such that

* for every $i \in [\ell]$ the function $f|_{\rho_i}$ is satisfiable and

* for every $i \neq j \in [\ell]$ the satisfying assignments of $f|_{\rho_i}$ and $f|_{\rho_j}$ are disjoint.

Then the communication complexity of $f$ with respect to $\Pi$ is at least $\lceil \log \ell \rceil$.

To prove this lemma we need the following lemma.
**Lemma 2.4 ([15]).** Let $\mathbf{EQ}_n(x_1, \dots, x_n, y_1, \dots, y_n)$ be a Boolean function such that $\mathbf{EQ}_n(x_1, \dots, x_n, y_1, \dots, y_n) = 1$ iff $x_i = y_i$ for all $i \in [n]$ and $\Pi = ([1, n], [n+1, 2n])$ be a partition.

*The Communication complexity of $\mathbf{EQ}_n$ with respect to the partition $\Pi$ is equal to $n+1$.*

*Proof of Lemma 2.3.* Let us assume that there is a communication protocol $\mathcal{P}$ for $f$ of cost $S$. We are going to show that there is a protocol for $\mathbf{EQ}_{\lfloor \log \ell \rfloor}$ of cost $S$ and hence, by Lemma 2.4, $S \ge \lfloor \log \ell \rfloor$.

Let us assume that Alice knows $x \in \{0, 1\}^{\lfloor \log \ell \rfloor}$ and Bob knows $y \in \{0, 1\}^{\lfloor \log \ell \rfloor}$ and they wish to check whether $x = y$.

Let $y$ be the binary representation of $j$ and $x$ be the binary representation of $i$. In order to check whether $x=y$, Bob finds a satisfying assignment $\tau$ for $f|_{\rho_j}$. After that they run the protocol $\mathcal{P}$ for $\rho_i$ and $\tau$. Note that if $x=y$, then $\rho_i = \rho_j$ and $\tau$ satisfies $f|_{\rho_i} = f|_{\rho_j}$, i.e., $f|_{\rho_i \tau} = 1$; otherwise $i \neq j$ and sets of satisfying assignments of $f|_{\rho_i}$ and $f|_{\rho_j}$ are disjoint, hence, $f|_{\rho_i \tau} = 0$. $\square$

## 2.3 OBDD proofs

If $F$ is a formula in CNF, we say that the sequence $D_1, D_2, \dots, D_t$ is an OBDD-derivation of $F$ if $D_t$ is an OBDD that represents the constant false function, and for all $1 \le i \le t$, $D_i$ is an OBDD that represents a clause of $F$ or can be obtained from the previous $D_j$'s by one of the following inference rules:

**conjunction or join:** $D_i$ is a $\pi$-ordered OBDD, that represents $D_k \wedge D_l$ for $1 \le l, k < i$, where $D_k, D_l$ have the same order $\pi$;

**weakening:** there exists a $j < i$ such that $D_j$ and $D_i$ have the same order $\pi$, and $D_j$ semantically implies $D_i$. The latter means that every assignment that satisfies $D_j$ also satisfies $D_i$;

**reordering:** $D_i$ is an OBDD that is equivalent to an OBDD $D_j$ with $j < i$ (note that $D_i$ and $D_j$ may have different orders).

We consider several different OBDD proof systems with different sets of allowed rules. When we need to denote some specific proof system, we indicate the rules specific for this system in brackets. For example, the $\text{OBDD}(\wedge)$ proof system uses only conjunction rule and hence, we may assume that all OBDDs in a proof have the same order. We use the notation $\pi$-$\text{OBDD}(\wedge)$ proof if all diagrams in this proof have order $\pi$.

## 2.4 OBDD algorithms for SAT

Pan and Vardi [19] proposed for the Boolean satisfiability problem the following family of algorithms based on OBDDs and the symbolic quantifier elimination.

The algorithm gets as an input a CNF formula $F$, it chooses some order $\pi$ on the variables and creates both a $\pi$-ordered OBDD $D$ (which initially is equal to the constant true function) and a set of clauses $S$ (which initially consists of all clauses of the formula $F$). While $S$ is not empty the algorithm applies one of the following three operations:

**join or conjunction** delete some clause $C$ from $S$ and replace $D$ by a $\pi$-ordered BDD that represents the conjunction $D \wedge C$;

**projection** choose a variable $x$ that has no occurrences in the clauses from $S$ and replace $D$ by a $\pi$-ordered BDD for the function $\exists x D$;

**reordering** choose a new order on variables $\pi'$ and replace $D$ by the equivalent $\pi'$-ordered diagram. Assign $\pi := \pi'$. (Note that Pan and Vardi did not consider this rule in [19]).

After every step of the algorithm, the following invariant is maintained: $F$ is satisfiable if and only if $\bigwedge_{C \in S} C \wedge D$ is satisfiable. After the termination of the algorithm the set $S$ is empty; if the diagram $D$ has a path from the source to a vertex labeled by 1, then the algorithm returns "Satisfiable" and returns "Unsatisfiable" otherwise.
We refer to the algorithms of this type as OBDD(∧, ∃, reordering) algorithms. Besides, we use a similar notation for algorithms that use some of the rules: we just enumerate the used rules in the brackets. For example, the OBDD(∧) algorithms use only the conjunction rule and the OBDD(∧, ∃) algorithms use only the conjunction and projection rules.

Since join and projection for OBDDs may be performed in polynomial time and reordering may be performed in time polynomial on the sizes of the input and the output, the running time of an OBDD(∧, ∃, reordering) algorithm are polynomially related with the total sum of the sizes of all values in the diagram *D* we ignore the time spent on choosing π and other operations with the permutation.

## 2.5 Error-correcting codes

By a code we mean a subset of binary strings with a fixed length. A code $\mathcal{C} \subseteq \{0,1\}^n$ has a relative distance $\delta$ if for any two codewords $c_1, c_2 \in \mathcal{C}$ the Hamming distance between $c_1$ and $c_2$ is at least $\delta n$.

A linear code is a set of all $n$-bits vectors $x = (x_1 \dots x_n)$ from some linear subspace in $\mathbb{F}_2^n$. If $k$ is the dimension of this space, then the ratio $k/n$ is called the *rate* of the code.

A linear code can be specified by a system of linear equations. For a code of dimension $k$ this system should consist of $m \ge n - k$ linear equations involving $n$ variables. The set of all solutions of the system should give exactly our code, so the rank of the system must be equal to $n-k$. If we require in addition that the equations in the system are linearly independent, then the number of equations is equal to $m = n - k$. The matrix of this linear system is called a *checksum matrix* of the code.

For a checksum matrix ($h_{ij}$) over $\mathbb{F}_2$ we say that a column $i$ intersects a row $j$, if $h_{ij} = 1$. Further, we say that a tuple of columns $(i_1, \dots, i_s)$ intersects some row $j$ if at least one of the columns $i_1, \dots, i_s$ intersects row $j$.

We say that a code $\mathcal{C}$ recovers $\rho$ fraction of erasures by a list of size $L$ (or $\mathcal{C}$ is $(\rho, L)$-erasure list-decodable) if for any $w \in \{0, 1, ?\}^n$ such that the number of ? in $w$ does not exceed $\rho n$, there exist at most $L$ elements in $\mathcal{C}$ that are consistent with $w$. A string $s \in \{0, 1\}^n$ is consistent with $w$ if for all $i$, $w_i \in \{0, 1\}$ implies $s_i = w_i$.

**Theorem 2.5** ([12, Lemma 2]). If $\mathcal{C}$ is a code with relative distance $\delta$, then for every $\epsilon > 0$ the code $\mathcal{C}$ is (($2 - \epsilon)\delta$, $\frac{2}{\epsilon}$)-erasure list-decodable.

# 3 Lower bounds for $\text{OBDD}(\wedge, \text{reordering})$

## 3.1 Tseitin formulas

In this Section, we prove an exponential lower bound on the size of $\text{OBDD}(\wedge, \text{reordering})$ proofs of Tseitin formulas.

A Tseitin formula $\text{TS}_{G,c}$ is based on an undirected graph $G = (V, E)$ with degree bounded by a constant $d$. Every edge $e \in E$ has the corresponding propositional variable $p_e$. There is a function $c: V \to \{0, 1\}$, we call it the labelling function. For every vertex $v \in V$ we write down a formula in CNF that encodes $\sum_{u \in V: (u,v) \in E, u \neq v} p_{(u,v)} \equiv c(v) \pmod 2$. The conjunction of the formulas described above is called a Tseitin formula. If $\sum_{v \in U} c(v) \equiv 1 \pmod 2$ for some connected component $U \subseteq V$, then the Tseitin formula is unsatisfiable. Indeed, if we sum up (modulo 2) all equalities stated in vertices from $U$ we get 0 = 1 since every variable has exactly 2 occurrences. If $\sum_{v \in U} c(v) = 0$ for every connected component $U$, then the Tseitin formula is satisfiable ([23, Lemma 4.1]).

Note that if formulas $\text{TS}_{G,c}$ and $\text{TS}_{G,c'}$ are satisfiable and $c \neq c'$ then $\text{TS}_{G,c}$ and $\text{TS}_{G,c'}$ are different functions; moreover, any satisfying assignment of $\text{TS}_{G,c}$ can not satisfy $\text{TS}_{G,c'}$.

In the following, we denote the number of connected components of a graph $G$ by $|\tilde{G}|$.
**Theorem 3.1.** Let graph $G$ with vertices $V$ and edges $E$ have the following property: for some $m \in [|E|]$ and $k > 0$ for all subsets $E' \subseteq E$ of the size $m$ the inequality $\#G' + \#G'' \le k$ holds, where $G'$ and $G''$ are graphs with vertices $V$ and edges $E'$ and $E \setminus E'$ respectively. If $\mathbf{TS}_{G,c}$ is satisfiable then communication complexity of $\mathbf{TS}_{G,c}$ is at least $|V| - k$.

*Proof.* Let us fix an order $\pi$ of the variables of $\mathbf{TS}_{G,c}$ (i.e. $\pi$ orders the edges of $G$). Let $E'$ be the set of the first $m$ edges in this order. We show that there are at least $2^{|V|-k}$ substitutions to the variables from $E'$ such that applying each of these substitutions to $\mathbf{TS}_{G,c}$ results in $2^{|V|-k}$ satisfiable functions with disjoint sets of satisfying assignments. Then due to Lemma 2.3, the communication complexity of $\mathbf{TS}_{G,c}$ is at least $|V| - k$.

Let $c' : V \to \{0,1\}$ be a labeling function that corresponds to a partial substitution with support $E'$: in every vertex $v$, $c(v)$ is the sum modulo 2 of the values of all edges from $E'$ that are incident to $v$. Note that making a partial substitution to a Tseitin formula $\mathbf{TS}_{G,c}$ gives as the resulting formula again a Tseitin formula — some formula $\mathbf{TS}_{G'',c+c'}$, where $G''$ is a graph with vertices $V$ and edges $E \setminus E'$, and $c+c'$ is the sum of the functions $c$ and $c'$ modulo 2.

We will prove a lower bound for the number of different $c'$ such that they can be obtained by a substitution and $\mathbf{TS}_{G'',c+c'}$ is satisfiable. The required properties of $c'$ can be described by a system of linear equations with variables $c'(v)$ for $v \in V$: for every connected component $U$ of graph $G'$ with vertices $V$ and edges $E'$ we put down the equation: $\sum_{v \in U} c'(v) = 0$ (this subsystem states that $c'$ can be obtained by a substitution or in other words that $\mathbf{TS}_{G',c'}$ is satisfiable) and for each connected component $W$ of $G''$ we put down the equation: $\sum_{v \in W} c'(v) + c'(v) = 0$ (this subsystem corresponds to the satisfiability of $\mathbf{TS}_{G'',c+c'}$).

The system has a solution since $\mathbf{TS}_{G,c}$ is satisfiable. There are $|V|$ variables and at most $\#G' + \#G'' \le k$ equations. Hence, there is at least $2^{|V|-k}$ solutions. Different solutions correspond to different satisfiable formulas $\mathbf{TS}_{G'',c+c'}$ and thus their sets of satisfying assignments are disjoint. $\square$

We will apply Theorem 3.1 to algebraic expanders.

**Definition 3.2.** A graph $G$ with vertices $V$ and edges $E$ is an $(n, d, \alpha)$-algebraic expander, if $|V| = n$, the degree of any vertex in $V$ equals $d$ and the absolute value of the second largest eigenvalue of the adjacency matrix of $G$ is not greater than $\alpha d$.

It is well known that for all $\alpha > 0$ and all large enough constants $d$ there exists a family $G_n$ of $(n, d, \alpha)$-algebraic expanders. There are explicit constructions such that $G_n$ can be constructed in poly($n$) time [16]. Also, it is known that a random $d$-regular graph is a good expander with high probability.

**Lemma 3.3 ([1]).** (Expander mixing lemma) Let $G(V, E)$ be an $(n, d, \alpha)$-expander. For any two subsets $S, T \subseteq V$ the following inequality holds: $|E(S, T)| - \frac{d|S||T|}{n} \le \alpha d \sqrt{|S||T|}$, where $E(S, T) = \{(u, v) | u \in S, v \in T, (u, v) \in E\}$.

**Lemma 3.4 ([5]).** (Cheeger's inequality) Let $G(V, E)$ be an $(n, d, \alpha)$-expander. For every set $S \subseteq V$, $|S| \le \frac{n}{2}$ the following inequality holds: $|E(S, V \setminus S)| \ge \frac{1-\alpha}{2} d|S|$.

**Theorem 3.5.** Let $G(V, E)$ be an $(n, d, \alpha)$-algebraic expander for $\alpha < \frac{1}{2}$. Then for any $E' \subseteq E$ if $|E'| = \frac{n}{4d}$, then $\#G' + \#G'' \le n(1-\epsilon) + 2$, where $G'$ is a graph with vertices $V$ and edges $E'$, $G''$ is a graph with vertices $V$ and edges $E \setminus E'$ and $\epsilon = \frac{1}{8d(\alpha d+1)} - \frac{1}{d^2}$. Note that $\epsilon > 0$ if $\alpha < 1/32$ and $d \ge 4$.

*Proof.* At first we prove the following proposition.

**Proposition 3.6.** For any connected component $C$ of $G''$ either $|C| \le \frac{4|E'|}{d}$ or $|C| > \frac{|V|}{2}$.

*Proof.* Assume for the sake of contradiction that there is a connected component $C$ such that $\frac{4|E'|}{d} < |C| \le \frac{|V|}{2}$. By Lemma 3.4 applied to the graph $G$, we have that $|E(C, V \setminus C)| \ge \frac{1-\alpha}{2} d|C| \ge \frac{d}{4}|C| > |E'|$. Hence, there are edges between $C$ and $V \setminus C$ in $G''$, we get a contradiction. $\square$
Let us prove that $\sharp G'' \le \frac{4|E'|}{d} + 2$. By Proposition 3.6, if the size of a connected component of $G''$ is at least $\frac{4|E'|}{d}$ then the size of this component is greater than $\frac{|V|}{2}$; hence, there is at most one component with size at least $\frac{4|E'|}{d}$. Consider all other components. If the number of these components is at least $\frac{4|E'|}{d} + 1$, we choose several of them such that the total number of vertices in the chosen components is in the interval $[\frac{4|E'|}{d} + 1, \frac{8|E'|}{d} + 1]$. We denote the set of vertices in these components by $T$. Since $T$ consists of several connected components in $G''$ we have that $|E(T, V \setminus T)| = 0$ in $G''$ and thus $E(T, V \setminus T) \le |E'|$ in $G$. Since $|T| \le \frac{8|E'|}{d} + 1 = \frac{2n}{d^2} + 1 \le \frac{n}{2}$, it follows from Lemma 3.4 that $|E(T, V \setminus T)| \ge \frac{1-\alpha}{2}d|T| > |E'|$ in $G$; so we get a contradiction.

Now we prove that $\sharp G' \le n - \frac{|E'|}{2(\alpha d+1)}$. Let $S$ be a set of a vertices incident to $E'$. Note that if $H$ is the graph with vertices $S$ and edges $E'$ then $|V| - \sharp G' = |S| - \sharp H$ and the degree of each vertex of $H$ is at least one. Hence, $\sharp H \le \frac{|S|}{2}$ and $\sharp G' \le n - \frac{|S|}{2}$.

By Lemma 3.3 for the graph $G$ we have that $|E(S, S)| \le \frac{d}{|V|}|S|^2 + \alpha d|S| \le |S|(\alpha d + \frac{d}{|V|}|S|) \le |S|(\alpha d + \frac{2d}{|V|}|E'|) \le |S|(\alpha d + 1)$. However $|E(S, S)| \ge |E'|$ since we count each edge from $E'$ at least once in $E(S, S)$. Hence, $|S| \ge \frac{|E'|}{\alpha d+1}$ and $\sharp G' \le n - \frac{|E'|}{2(\alpha d+1)}$.

Finally, we get $\sharp G' + \sharp G'' \le n - \frac{|E'|}{2(\alpha d+1)} + \frac{4|E'|}{d} + 2 = n(1 - (\frac{1}{8d(\alpha d+1)} - \frac{1}{d^2})) + 2$. $\square$

**Corollary 3.7.** Let $G$ be an $(n, d, \alpha)$-algebraic expander with $\alpha < \frac{1}{32}$ and $d \ge 4$. Assume that a Tseitin formula $\mathbf{TS}_{G,c}$ is satisfiable. Then for every partition $\Pi$ of the variables of $\mathbf{TS}_{G,c}$ such that $|\Pi_0| = \frac{n}{4d}$, communication complexity of $\mathbf{TS}_{G,c}$ is at least $\Omega(n)$.

*Proof.* Follows from Theorems 3.1 and 3.5. $\square$

**Corollary 3.8.** If $k > 0$ is an integer constant, a graph $G$ is an $(n, d, \alpha)$-algebraic expander for $\alpha < \frac{1}{32}$ and $d \ge 4$, and a Tseitin formula $\mathbf{TS}_{H,n,c}$ is satisfiable, then every $k$-OBDD representing $\mathbf{TS}_{H,n,c}$ has size at least $2^{\Omega(n)}$.

*Proof.* Follows from Corollary 3.7 and Lemma 2.1. $\square$

**Corollary 3.9.** Let graph $H_n$ be obtained from an $(n, d, \alpha)$-expander $G(V, E)$ with $\alpha < \frac{1}{32}$ and $d \ge 4$ by removing $o(n)$ edges. If $\mathbf{TS}_{H,n,c}$ is satisfiable, then every OBDD representation of $\mathbf{TS}_{H,n,c}$ has size at least $2^{\Omega(n)}$.

*Proof.* Let $M$ be a set of edges of $H_n$, $E' \subset M$ such that $|E'| = \frac{n}{4d}$, and $H', G'', H''$ be graphs with vertices $V$ and edges $E'$, $M \setminus E'$ and $E \setminus E'$ respectively. Obviously $\sharp H'' \le \sharp G'' + o(n)$. By Corollary 3.8 size of an OBDD for $\mathbf{TS}_{H,n,c}$ is at least $2^{\Omega(n)}$ since $\sharp H' + \sharp G'' \le (1 - \epsilon)n + 1$. $\square$

**Lemma 3.10 ([24]).** 1. If for functions $f_1: \{0,1\}^n \to \{0,1\}$ and $f_2: \{0,1\}^n \to \{0,1\}$ there exist $\pi$-ordered BDDs (for some order $\pi$) with sizes $k_1$ and $k_2$ respectively then there exists a $\pi$-ordered BDD of size at most $k_1k_2$ for $f_1 \wedge f_2$.

2. If for a function $f: \{0,1\}^n \to \{0,1\}$ there exists a $\pi$-ordered BDD of a size $k$ then for any substitution $\rho$ there exists a $\pi$-ordered BDD for $f|_{\rho}$ of size at most $k$.

**Lemma 3.11.** Assume that all OBDDs representing a CNF formula $\phi$ have the size at least $k$. Assume that a CNF formula $\psi$ can be obtained from $\phi$ by removing several clauses that are dependent on at most $t$ variables in total. Then the size of any OBDD representing $\psi$ is at least $k2^{-t-1}$.

*Proof.* The conjunction of the removed clauses is a function of $t$ variables, hence it can be represented as OBDD of size at most $2^{t+1}$ for every order. Thus if $\psi$ has OBDD representation of size less than $k2^{-t-1}$ by Lemma 3.10, then $\phi$ has OBDD representation of size $k$. $\square$

**Lemma 3.12.** Let $G(V, E)$ be an $(n, d, \alpha)$-algebraic expander with $\alpha < \frac{1}{20}$ and $d \ge 50$. Then $G$ is connected and it remains connected after removing of any vertex or any two vertices and the shortest path between them.
**Proof.** It is sufficient to prove that $G$ is connected after removing any two vertices and the shortest path between them. Consider arbitrary two vertices $x, y \in V$ and consider an arbitrary set $S \subseteq V \setminus \{x, y\}$ such that $|S| \le |V \setminus \{\{x, y\} \cup S\}|$. We will show that there is $v \in S$ such that $E(\{v\}, V \setminus \{\{x, y\} \cup S\}) \ge 3$. This will imply that after removing $x$ and $y$ and the shortest $xy$-path from $G$ the resulting graph is connected. Indeed if it is not connected, then we get a contradiction for $S$ that is equal to the smallest connected component. In this case the shortest $xy$-path may contain at most 2 edges incident to $v$, hence, there is an edge that goes from $S$ to $V \setminus \{\{x, y\} \cup S\}$.

By Cheeger's inequality (Lemma 3.4) $|E(S, V \setminus S)| \ge \frac{1-\alpha}{2} d|S|$. Since the degrees of $x$ and $y$ are at least $d$, we get $E(S, V \setminus (S \cup \{x, y\})) \ge \frac{1-\alpha}{2} d|S| - 2d$. If $|E(S, V \setminus (S \cup \{x, y\}))| > 2|S|$, then the required $v$ exists by the averaging principle. Assume that $E(S, V \setminus (S \cup \{x, y\})) \le 2|S|$, hence $\frac{1-\alpha}{2} d|S| - 2d \le 2|S|$ and $(\frac{1-\alpha}{2} d - 2)|S| \le 2d$, and since $\alpha < \frac{1}{20}$ and $d > 50$, then $|S| < 5$.

If $|S| < 5$, then the expander mixing lemma implies that $|E(S, \{x, y\})| \le \frac{d}{n} 2|S| + \alpha d \sqrt{2|S|} \le 5\alpha d$. By Cheeger's inequality $|E(S, V \setminus S)| \ge \frac{1-\alpha}{2} d|S|$ and $|E(S, V \setminus (S \cup \{x, y\}))| \ge \frac{1-\alpha}{2} d|S| - 5\alpha d \ge 10 > 2|S|$ for $\alpha < \frac{1}{20}$ and $d > 50$; and this is a contradiction. $\square$

**Lemma 3.13.** Let $G$ be an $(n, d, \alpha)$-algebraic expander with $d \ge 4$, $\alpha < \frac{1}{32}$. Let Tseitin formula $\mathbf{TS}_{G,c}$ be unsatisfiable and $\Phi$ denote the formula that can be obtained from $\mathbf{TS}_{G,c}$ by removing one arbitrary clause. Then $\Phi$ is satisfiable and every OBDD representation of $\Phi$ has the size $2^{\Omega(n)}$.

**Proof.** Assume that $\mathbf{TS}_{G,c} = \Phi \wedge C$, where $C$ is a clause that corresponds to the equation in a vertex $v$. Let $H$ be the result of removing the vertex $v$ from $G$. By Lemma 3.12 the graph $H$ is connected. Let us make a substitution to all variables of the clause $C$ that falsifies $C$. Let $\Phi'$ denote the result of this substitution applied to $\Phi$. Since the substitution falsifies the parity condition at the vertex $v$, $\Phi'$ corresponds to a satisfiable Tseitin formula based on $H$. By Corollary 3.9 the size of every OBDD for $\Phi'$ is at least $2^{\Omega(n)}$. (Formally we apply Corollary 3.9 to the graph $H$ with one additional isolated vertex $v$. Note that a Tseitin formula does not change if we add isolated vertex to the graph). $\Phi'$ is the result of the substitution applied to $\Phi$, hence, the size of every OBDD representing $\Phi$ is at least $2^{\Omega(n)}$. $\square$

**Theorem 3.14.** Let $G$ be an $(n, d, \alpha)$-algebraic expander with $d \ge 50$, $\alpha < \frac{1}{32}$. Then any OBDD($\wedge$, reordering) proof of any unsatisfiable Tseitin formula $\mathbf{TS}_{G,c}$ has the size at least $2^{\Omega(n)}$.

Before we present the formal proof of the theorem let us sketch the argument. We consider the last step of the OBDD proof: the conjunction of OBDDs $F_1$ and $F_2$ is the identically false function but both $F_1$ and $F_2$ are satisfiable. Both $F_1$ and $F_2$ are conjunctions of several clauses of $\mathbf{TS}_{G,c}$. We use the fact that a satisfiable Tseitin formula based on an expander has only exponential sized OBDDs. Moreover, if the underlying graph differs from some expander by $o(n)$ edges, then any of its OBDD representations has also an exponential size, since the number of connected component of graphs $G'$ and $G''$ in Theorem 3.5 changes by at most $o(n)$.

Note that $F_1$ and $F_2$ together contain all clauses of $\mathbf{TS}_{G,c}$. The main case is the following: there are two nonadjacent vertices $u$ and $v$ such that $F_1$ does not contain a clause $C_u$ that corresponds to the vertex $u$ and $F_2$ does not contain a clause $C_v$ that corresponds to $v$. We consider two partial substitutions $\rho_1$ and $\rho_2$ that are both defined on the edges adjacent to $u$ and $v$ and on the edges of a fixed shortest path $p$ between $u$ and $v$. The substitutions $\rho_1$ and $\rho_2$ assign opposite values to edges of the path $p$ and are consistent on all other edges. The substitution $\rho_1$ satisfies $C_v$ and refutes $C_u$ and $\rho_2$ satisfies $C_u$ and refutes $C_v$.

By the construction $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is a satisfiable Tseitin formula based on the graph that is obtained from $G$ by deletion of the vertices $u$ and $v$ and all edges from the path $p$ (it is also possible that this formula does not contain some clauses for the vertices from $p$). The size of an OBDD representation of such a formula is exponential since the underlying graph is obtained from an expander by removing at most $o(n)$ vertices. (Note that $p$ is the shortest path in the expander, thus $p$ contains at most $O(\log n)$ edges.) Hence, we get that either $F_1$ or $F_2$ has an exponential size in the given order.

**Proof.** We consider the last step of the proof: conjunction of OBDDs $F_1$ and $F_2$ is the identically false function but $F_1$ and $F_2$ are satisfiable. Both $F_1$ and $F_2$ are conjunctions of several clauses of $\mathbf{TS}_{G,c}$. Every
clause of $\mathbf{TS}_{G,c}$ is either in $F_1$ or in $F_2$ since otherwise $F_1 \wedge F_2$ is satisfiable by Lemma 3.13. Our goal is to prove that either $F_1$ or $F_2$ has size $2^{\Omega(n)}$.

We consider two cases:

1. There exist two non-adjacent vertices $u$ and $v$ from $G$ such that $F_1$ does not include some clause $C_v$ that corresponds to vertex $v$ and $F_2$ does not include some clause $C_u$ for vertex $u$.

Consider a shortest path $p$ from $v$ to $u$. Let $e_v$ be the first edge of $p$ and $e_u$ be the last edge ($e_v \neq e_u$ since $u$ and $v$ are non-adjacent). Consider two substitutions $\rho_1$ and $\rho_2$ with the same support: all edges that are incident to $u$ or $v$ and all edges from $p$. Substitutions $\rho_1$ and $\rho_2$ are consistent on edges that are out of $p$: all edges that are adjacent to $u$ or $v$ but not in $p$ have values that do not satisfy $C_u$ and $C_v$ (this is possible since $u$ and $v$ are non-adjacent). $\rho_1$ substitute zeros to all edges from $p$ except $e_u$ and $e_v$ and substitute a value to $e_v$ that does not satisfy $C_v$ and a value to $e_u$ that satisfies $C_u$. $\rho_2$ substitute ones to all edges from $p$ except $e_u$ and $e_v$ and substitute a value to $e_v$ that satisfies $C_v$ and a value to $e_u$ that does not satisfy $C_u$. So edges from $p$ have different values in $\rho_1$ and $\rho_2$; $\rho_1$ satisfies $u$ and refutes $v$ and $\rho_2$ refutes $u$ and satisfies $v$.

Consider the graph $G'$ that can be obtained from $G$ by removing $u$, $v$ and all edges from the path $p$. The graph $G'$ is connected since by Lemma 3.12 after removing any two vertices with the shortest path between them the graph $G$ remains connected.

Let $c'$ be a labeling function of the result of the substitution $\rho_1$ applied to $\mathbf{TS}_{G,c}$ and $c''$ be a restriction of $c'$ on $V \setminus \{u, v\}$. Note that $\rho_2$ corresponds to the same $c''$ since $\rho_1$ and $\rho_2$ identically change the value of the labelling function for all vertices except $u$ and $v$. We claim that $\mathbf{TS}_{G',c''}$ is satisfiable. Indeed if we make a substitution $\rho_1$ to $\mathbf{TS}_{G,c}$ the vertex $v$ would be refuted (it has no edges and it is labeled by 1), the vertex $u$ would be satisfied (it has no edges and it is labeled by 0), all other vertices are marked according $c'$. Thus the sum of values of $c''$ is even and $\mathbf{TS}_{G',c''}$ is satisfiable since $G'$ is connected.

We consider the conjunction $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$. Any satisfying assignment of $\mathbf{TS}_{G',c''}$ satisfies both $F_1|_{\rho_1}$ and $F_2|_{\rho_2}$, hence, $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is satisfiable. Let us represent $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ as a conjunction of clauses. For every vertex $w$ that is not in $p$, the union of clauses of $F_1$ and $F_2$ contains all clauses that correspond to the equation at vertex $w$, substitutions $\rho_1$ and $\rho_2$ are consistent for all variables from this equation, hence, $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ contains all clauses that correspond to the equation of vertex $w$ in formula $\mathbf{TS}_{G',c''}$. Consider a vertex $w$ from $p$ ($w \notin \{u, v\}$). Let $\rho_1$ and $\rho_2$ substitute some values to variables $x$ and $y$ that correspond to $w$. Note that by the construction $\rho_1(x) + \rho_1(y) = \rho_2(x) + \rho_2(y)$. Hence, each of $F_1|_{\rho_1}$ and $F_2|_{\rho_2}$ contains several clauses from the equation that corresponds to $w$ in $\mathbf{TS}_{G',c''}$. And it is not necessary that $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ contains all clauses from the equation that correspond to $w$. Finally, $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ can be obtained from $\mathbf{TS}_{G',c''}$ by the removing of several clauses corresponding to the vertices from the path $p$. It is well known that the diameter of any $(n, d, \alpha)$-expander is $O(\log n)$, hence, $p$ contains at most $O(\log n)$ vertices.

The size of any OBDD representation of the formula $\mathbf{TS}_{G',c''}$ is at least $2^{\Omega(n)}$ by Corollary 3.9, since $G'$ can be obtained from an $(n, d, \alpha)$-algebraic expander by the removing of $O(\log n)$ edges (formally we add two isolated vertices $u$ and $v$ to $G'$; adding isolated vertices does not change Tseitin formulas). Then by Lemma 3.11, any OBDD representing $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has the size at least $2^{\Omega(n)}$. Thus, by Lemma 3.10, for every given order of variables $\pi$ either $F_1|_{\rho_1}$ or $F_2|_{\rho_2}$ has the size of the minimal $\pi$-OBDD at least $2^{\Omega(n)}$. Hence, the minimal $\pi$-OBDD for $F_1$ or $F_2$ has the size of the at least $2^{\Omega(n)}$.

2. In the second case there are no such non-adjacent vertices. Since $F_1$ is not identically false, there exists a vertex $u$ such that $F_1$ does not include a clause that corresponds to a vertex $u$ and by the assumption $F_2$ does not include clauses only for the vertex $v$ and its neighbors. In this case $F_2$ differs from a Tseitin formula without one clause by a constant number of clauses that depend on a constant number of variables. Thus any OBDD representation of $F_2$ by Lemmas 3.13 and 3.11 has size at least $2^{\Omega(n)}$.

<figure><img src="image_2.png" /></figure>
## 3.2 Pigeonhole principle

In this section we consider formulas that encode the pigeonhole principle and prove an exponential lower bound on the size of $OBDD(\wedge, \text{reordering})$ proofs of them.

Let $m$ and $n$ be integers and $p_{i,j}$ be different variables; $p_{i,j}$ states whether the $i$th pigeon is in the $j$th hole or not. The formula $\text{PHP}_n^m$ has two types of clauses. The clauses of the first type (long clauses) state that every pigeon is in at least one hole: $\bigvee_{j=1}^n p_{i,j}$ for all $i \in [m]$. The clauses of the second type (short clauses) state that in every hole there is at most one pigeon: $\neg p_{i,k} \lor \neg p_{j,k}$ for all $k \in [n]$ and all $i \neq j \in [m]$.

**Lemma 3.15.** For every partition $\Pi$ such that $|\Pi_0| = \frac{n^2}{96}$, the communication complexity of $\text{PHP}_n^m$ with respect to $\Pi$ at is least $\Omega(n)$.

*Proof.* Let us fix some partition of variables $\Pi$ such that $|\Pi_0| = \frac{n^2}{96}$.

Consider a bipartite graph $G(L, R, E)$ with two parts $L$ and $R$ associated with $[n]$ and the set of edges $E$ associated with $\Pi_0$, i.e., $(i, j) \in E$ iff $p_{i,j} \in \Pi_0$. Let $G'(L, R, E')$ be the complement bipartite graph, i.e., $E' = [n] \times [n] \setminus E$. Let $v_1, v_2, \dots, v_n$ be the vertices of $R \cup L$ sorted by decreasing of their degrees in $G$: $\deg v_1 \ge \deg v_2 \ge \dots \ge \deg v_{2n}$.

Let $k$ be the maximum number such that $\deg v_k \ge 3k$. Note that $\frac{n^2}{48} = 2|E| \ge \sum_{i=1}^k \deg v_i \ge 3k^2$, and therefore $k \le \frac{n}{12}$. Further, $2|\Pi_0| = \frac{n^2}{48} = \sum_{i=1}^{2n} \deg v_i \le nk + (2n-k)(3k+2) = 7nk - 3k^2 + 4n - 2k \le 11nk$. Hence, $k \ge \frac{n}{11 \cdot 48}$. Let $B = \{v_1, v_2, \dots, v_k\}$. Note that every vertex from $B$ is connected with at least $2k$ vertices outside of $B$.

Let $\mathfrak{M}$ be the set of all matchings of size $k$ that cover $B$ and do not connect two vertices from $B$. Let us prove that $|\mathfrak{M}| \ge \frac{(2k)!}{k!}$. Note that the number of possibilities for the $i$th vertex from $B$ to find a pair is at least $3k - |B| - (i-1) = 2k - i$. Hence, there are at least $\frac{(2k)!}{k!}$ matchings of this type. So there are at least $\frac{(2k)!}{k!k!} = \binom{2k}{k}$ different sets that are sets of endpoints of matchings from $\mathfrak{M}$.

For every $M \in \mathfrak{M}$ we define a partial substitution $\rho_M$ with the support $\Pi_0$ such that $\rho_M(p_{i,j}) = 1$ if $(i, j) \in M$ and $\rho_M(p_{i,j}) = 0$ if $(i, j) \in E \setminus M$. We claim that $\text{PHP}_n^n|_{\rho_M}$ is satisfiable for all $M \in \mathfrak{M}$.

Let $V(M)$ denote the set of endpoints of edges from $M$. $\text{PHP}_n^n|_{\rho_M}$ is satisfiable if the graph $G' - V(M)$ (which is obtained from $G'$ by removing of all vertices from $M$) has a perfect matching. Since $M$ is a matching, $G'$ has the same number of vertices in its parts. We are going to use Hall's theorem to show that $G' - V(M)$ has a perfect matching. To this end we have to show that every set $A \subseteq L \setminus V(M)$ has at least $|A|$ neighbors in $G'$. Consider two cases: in the first case $|A| \le \frac{n}{2}$ and every vertex from $A$ has degree at least $n - 4k - 2 \ge n - 6k \ge \frac{n}{2}$. In the second case $|A| > \frac{n}{2}$. We need to show that every vertex from $R \setminus V(M)$ has a neighbor in $A$ and thus the number of neighbors of $A$ is precisely $|R \setminus V(M)| = |L \setminus V(M)| \ge |A|$. Indeed, every vertex from $R \setminus V(M)$ has degree at least $n - 4k - 2 \ge \frac{n}{2}$ and $|L \setminus R| < n$, so it has a neighbor in $A$.

Let us consider $M_1, M_2 \in \mathfrak{M}$ with $V(M_1) \neq V(M_2)$. Functions $\text{PHP}_n^n|_{\rho_{M_1}}$ and $\text{PHP}_n^n|_{\rho_{M_2}}$ have disjoint sets of satisfiable assignments since $M_1$ and $M_2$ are matchings covering different sets of vertices. Thus, by Lemma 2.3, the communication complexity of $\text{PHP}_n^n$ is at least $\log \binom{2k}{k} = \Omega(n)$. $\square$

**Corollary 3.16.** For every fixed constant $k$, every $k$-OBDD-representation of $\text{PHP}_n^n$ has size at least $2^{\Omega(n)}$.

**Theorem 3.17.** Any $OBDD(\wedge, \text{reordering})$ proof of pigeonhole principle formula $\text{PHP}_n^{n+1}$ has size at least $2^{\Omega(n)}$.

*Proof.* We consider the last step of the $OBDD$ proof: the conjunction of $OBDDs$ $F_1$ and $F_2$ is the identically false function but $F_1$ and $F_2$ are satisfiable. Both $F_1$ and $F_2$ represent conjunctions of several clauses of $\text{PHP}_n^{n+1}$ and have the same order $\pi$. Every clause of $\text{PHP}_n^{n+1}$ is either in $F_1$ or in $F_2$ since otherwise $F_1 \wedge F_2$ is satisfiable. Our goal is to prove that either $F_1$ or $F_2$ has size $2^{\Omega(n)}$.

We consider three cases and apply Corollary 3.16 in each of them:
1. Assume that there exist an $i_1 \in [n+1]$ and an $i_2 \in [n+1]$ ($i_1 \neq i_2$) such that $F_1$ does not contain a long clause that corresponds to $i_1$ and $F_2$ does not contain a long clause that corresponds to $i_2$. Let us fix any $j \in [n]$ and consider substitutions $\rho_1$ and $\rho_2$ with the support

$$ \{p_{s,t} | (s,t) \in \{i_1, i_2\} \times [n] \cup [n+1] \times \{j\}\} $$

that substitute zero to all variables with two exceptions: $\rho_1(p_{i_2,j}) = 1$ and $\rho_2(p_{i_1,j}) = 1$. Note that the Boolean function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is equivalent to $\text{PHP}_{n-1}^{n-1}$ and thus by Corollary 3.16 the $\pi$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is of size at least $2^{\Omega(n)}$. Hence, either $F_1$ or $F_2$ has size of its minimal $\pi$-OBDD at least $2^{\Omega(n)}$.

2. Assume that there are $i_1, i_2 \in [n+1]$, $j \in [n]$ and $i \in [n+1]$ such that $F_1$ does not contain the short clause ($\neg p_{i_1,j} \lor \neg p_{i_2,j}$) and $F_2$ does not contain a long clause that corresponds to $i$. Let us consider two sub-cases.

* In the first case $i \notin \{i_1, i_2\}$. Let us fix any $j' \in [n] \setminus \{j\}$ and consider substitutions $\rho_1$ and $\rho_2$ with the support

$$ \{p_{s,t} | (s,t) \in \{i_1, i_2, i\} \times [n] \cup [n+1] \times \{j, j'\}\} $$

that substitute zero to all variables with five exceptions: $\rho_1(p_{i_1,j}) = 1, \rho_1(p_{i_2,j}) = 1, \rho_1(p_{i,j'}) = 1, \rho_2(p_{i_1,j}) = 1$, and $\rho_2(p_{i_2,j'}) = 1$. Note that the Boolean function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is equivalent to $\text{PHP}_{n-2}^{n-2}$; hence, by Corollary 3.16 the $\pi$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has size $2^{\Omega(n)}$. Hence, either for $F_1$ or for $F_2$, the size of its minimal $\pi$-OBDD at least $2^{\Omega(n)}$.

* In the second case $i \in \{i_1, i_2\}$. Without loss of generality $i_2 = i$. Consider substitutions $\rho_1$ and $\rho_2$ with the support

$$ \{p_{s,t} | (s,t) \in \{i_1, i_2\} \times [n] \cup [n+1] \times \{j\}\} $$

that substitute zero to all variables with three exceptions: $\rho_1(p_{i_1,j}) = 1, \rho_1(p_{i_2,j}) = 1$, and $\rho_2(p_{i_1,j}) = 1$. Note that the Boolean function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is equivalent to $\text{PHP}_{n-1}^{n-1}$; hence, by Corollary 3.16 the $\pi$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has size $2^{\Omega(n)}$. Hence, either for $F_1$ or for $F_2$, the size of the minimal $\pi$-OBDD at least $2^{\Omega(n)}$.

3. Assume that there are $i_{1,1}, i_{1,2} \in [n+1]$, $j_1 \in [n]$, $i_{2,1}, i_{2,2} \in [n+1]$ and $j_2 \in [n]$ such that $F_1$ does not contain the short clause ($\neg p_{i_{1,1},j_1} \lor \neg p_{i_{1,2},j_1}$) and $F_2$ does not contain the short clause ($\neg p_{i_{2,1},j_2} \lor \neg p_{i_{2,2},j_2}$). Let us consider five cases.

* The first case is when $i_{1,1}, i_{1,2} \notin \{i_{2,1}, i_{2,2}\}$ and $j_1 \neq j_2$. Let us fix any $j \in [n] \setminus \{j_1, j_2\}$ and consider substitutions $\rho_1$ and $\rho_2$ with the support

$$ \{p_{s,t} | (s,t) \in \{i_{1,1}, i_{1,2}, i_{2,1}, i_{2,2}\} \times [n] \cup [n+1] \times \{j_1, j_2, j\}\} $$

that substitute zero to all variables with eight exceptions: $\rho_1(p_{i_{1,1},j_1}) = 1, \rho_1(p_{i_{1,2},j_1}) = 1, \rho_1(p_{i_{2,1},j_2}) = 1, \rho_1(p_{i_{2,2},j_2}) = 1, \rho_2(p_{i_{2,1},j_2}) = 1, \rho_2(p_{i_{2,2},j_2}) = 1, \rho_1(p_{i_{1,1},j_1}) = 1, \text{ and } \rho_1(p_{i_{1,2},j_1}) = 1$. Note that the Boolean function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is equivalent to $\text{PHP}_{n-3}^{n-3}$ and thus by Corollary 3.16 the $\pi$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has size $2^{\Omega(n)}$.

* The second case is when $i_{1,1} \notin \{i_{2,1}, i_{2,2}\}$, $i_{1,2} \in \{i_{2,1}, i_{2,2}\}$, and $j_1 \neq j_2$. Without loss of generality $i_{1,2} = i_{2,1}$. Let us consider substitutions $\rho_1$ and $\rho_2$ with the support

$$ \{p_{s,t} | (s,t) \in \{i_{1,1}, i_{1,2}, i_{2,2}\} \times [n] \cup [n+1] \times \{j_1, j_2\}\} $$

that substitute zero to all variables with six exceptions: $\rho_1(p_{i_{1,1},j_1}) = 1, \rho_1(p_{i_{1,2},j_1}) = 1, \rho_1(p_{i_{2,1},j_2}) = 1, \rho_1(p_{i_{1,1},j_1}) = 1, \rho_1(p_{i_{1,2},j_1}) = 1, \text{ and } \rho_1(p_{i_{2,1},j_2}) = 1$. Note that the Boolean function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is equivalent to $\text{PHP}_{n-2}^{n-2}$ and thus by Corollary 3.16 the $\pi$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has size $2^{\Omega(n)}$.
* The third case is when $i_{1,1}, i_{1,2} \in \{i_{2,1}, i_{2,2}\}$ and $j_1 \neq j_2$. Without loss of generality $i_{1,1} = i_{2,1}$ and $i_{1,2} = i_{2,2}$. Let us consider substitutions $\rho_1$ and $\rho_2$ with the support

$$ \{p_{s,t} | (s,t) \in \{i_{1,1}, i_{1,2}\} \times [n] \cup [n+1] \times \{j_1, j_2\}\} $$

that substitute zero to all variables with four exceptions: $\rho_1(p_{i_{1,1},j_1}) = 1$, $\rho_1(p_{i_{1,2},j_1}) = 1$, $\rho_1(p_{i_{1,1},j_2}) = 1$, $\rho_1(p_{i_{1,2},j_2}) = 1$. Note that the Boolean function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is equivalent to $\text{PHP}_{n-1}^{n-1}$ and thus by Corollary 3.16 the $\pi$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has size $2^{\Omega(n)}$.

* The fourth case is when $i_{1,1} \notin \{i_{2,1}, i_{2,2}\}$, $i_{1,2} \in \{i_{2,1}, i_{2,2}\}$, and $j_1 = j_2$. Without loss of generality $i_{1,2} = i_{2,1}$. Let us fix any $j \in [n] \setminus \{j_1\}$ and consider substitutions $\rho_1$ and $\rho_2$ with the support

$$ \{p_{s,t} | (s,t) \in \{i_{1,1}, i_{1,2}, i_{2,2}\} \times [n] \cup [n+1] \times \{j_1, j\}\} $$

that substitute zero to all variables with six exceptions: $\rho_1(p_{i_{1,1},j_1}) = 1$, $\rho_1(p_{i_{1,2},j_1}) = 1$, $\rho_1(p_{i_{2,2},j}) = 1$, $\rho_1(p_{i_{1,1},j}) = 1$, $\rho_1(p_{i_{1,2},j}) = 1$, $\rho_1(p_{i_{2,2},j_1}) = 1$, and $\rho_1(p_{i_{2,2},j_2}) = 1$, Note that the Boolean function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is equivalent to $\text{PHP}_{n-2}^{n-2}$ and thus by Corollary 3.16 the $\pi$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has size $2^{\Omega(n)}$.

* The fifth case is when $i_{1,1}, i_{1,2} \notin \{i_{2,1}, i_{2,2}\}$ and $j_1 = j_2$. Let us fix any $j_3, j_4 \in [n] \setminus \{j_1\}$ and consider substitutions $\rho_1$ and $\rho_2$ with the support

$$ \{p_{s,t} | (s,t) \in \{i_{1,1}, i_{1,2}, i_{2,1}, i_{2,2}\} \times [n] \cup [n+1] \times \{j_1, j_3, j_4\}\} $$

that substitute zero to all variables with eight exceptions: $\rho_1(p_{i_{1,1},j_1}) = 1$, $\rho_1(p_{i_{1,2},j_1}) = 1$, $\rho_1(p_{i_{2,1},j_3}) = 1$, $\rho_1(p_{i_{2,2},j_4}) = 1$, $\rho_1(p_{i_{1,1},j_3}) = 1$, $\rho_1(p_{i_{1,2},j_4}) = 1$, $\rho_1(p_{i_{2,1},j_1}) = 1$, and $\rho_1(p_{i_{2,2},j_1}) = 1$. Note that the Boolean function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is equivalent to $\text{PHP}_{n-3}^{n-3}$ and thus by Corollary 3.16 the $\pi$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ has size $2^{\Omega(n)}$.

□

# 4 OBDD($\wedge$, reordering) is stronger than OBDD($\wedge$)

In this section we give an example of a family of unsatisfiable formulas $\Phi_n$ that have OBDD($\wedge$, reordering) proofs of polynomial size while all OBDD($\wedge$) proofs of it have size at least $2^{\Omega(n)}$.

**Theorem 4.1.** Let $\Psi_n(x_1, x_2, \dots, x_n)$ be a family of unsatisfiable formulas of size poly(n) that satisfies the following conditions:

* there exists an order $\tau$ such that $\Psi_n$ has $\tau$-OBDD($\wedge$) refutation of size poly(n);

* there exists a polynomial $p(n)$, an integer $k \le \log(p(n))$ and permutations $\sigma_1, \sigma_2, \dots, \sigma_{2^k} \in S_n$ such that for any permutation $\pi \in S_n$ there exists $i \in [2^k]$ such that any $\pi\sigma_i$-OBDD($\wedge$) proof of $\Psi_n$ has size at least $2^{\Omega(n)}$.

Then the formula

$$ \Phi_n(w_1, w_2, \dots, w_k, x_1, x_2, \dots, x_n) = \bigwedge_{i=1}^{2^k} ((w = i-1) \rightarrow \Psi(x_{\sigma_i(1)}, x_{\sigma_i(2)}, \dots, x_{\sigma_i(n)})) $$

has an OBDD($\wedge$, reordering) proof of size poly(n), but any OBDD($\wedge$) proof has size at least $2^{\Omega(n)}$. Here the equality $w = i-1$ means that $w_1w_2\dots w_k$ is a binary representation of $i-1$. We assume that $\Phi_n$ is written in CNF as follows: we add a clause $\neg(w = i-1)$ to every clause of $\Psi(x_{\sigma_i(1)}, x_{\sigma_i(2)}, \dots, x_{\sigma_i(n)})$.
Let us consider the following sketch of the proof, before we give a complete proof of this theorem. The lower bound. Consider an OBDD($\wedge$) proof $T$ of the formula $\Phi_n$, let $\tau$ be the order of the variables $x_1, x_2, \dots, x_n$ that is induced by the order from $T$. By the statement of the theorem, there exists $1 \le i \le 2^k$ such that all $(\tau\sigma_i)$-OBDD($\wedge$) proofs of $\Psi$ have at least the exponential size. We make a substitution $w = i-1$ to the proof $T$. This substitution converts the proof of $\Phi_n$ into a proof of $\Psi_n$ with the order $\tau\sigma_i$. Hence, $T$ has the exponential size.

The upper bound. Since there exists a polynomial sized OBDD($\wedge$) proof of $\Psi_n$, then for all $i$ there is an order $\pi_i$ (we may assume after the permutation $\pi$ the variables $w$ get the leftmost positions) such that there is a $\pi_i$-OBDD($\wedge$) derivation of the diagram representing $w \ne i - 1$. From all such diagrams for different $i$ we may construct a polynomial sized refutation of $\Phi_n$, since $w$ contains only $O(\log n)$ variables.

*Proof.* The lower bound. Consider an $\alpha$-OBDD($\wedge$) proof $T$ of the formula $\Phi_n$ for some order $\alpha$. We consider $\alpha$ as a permutation of $[n+k]$. Let $\pi$ be a permutation of $[n]$ (or variables $x_1, x_2, \dots, x_n$) that is induced by $\alpha$ (formally $\pi(j) = |\{i \in [n] \mid \alpha(i+k) \le \alpha(j+k)\}|$).

By the statement of the theorem there exists an $i_0 \in [2^k]$ such that any $\pi\sigma_{i_0}$-OBDD($\wedge$) proof of $\Psi_n$ has size at least $2^{\Omega(n)}$. Consider a partial substitution $\rho$ that assign to the variables $w_1, w_2, \dots, w_k$ a binary representation of $i_0 - 1$. Consider the formula $\Phi_n|_{\rho}$. Clauses that represent $(w = i-1) \rightarrow \Psi(x_{\sigma_i(1)}, x_{\sigma_i(2)}, \dots, x_{\sigma_i(n)})$ for $i \ne i_0$ are satisfied by $\rho$. Hence, $\Phi_n|_{\rho}$ is equal to $\Psi(x_{\sigma_{i_0}(1)}, x_{\sigma_{i_0}(2)}, \dots, x_{\sigma_{i_0}(n)})$. Thus, if we substitute $\rho$ to the proof $T$ we get a $\pi$-OBDD($\wedge$) proof $\Psi(x_{\sigma_{i_0}(1)}, x_{\sigma_{i_0}(2)}, \dots, x_{\sigma_{i_0}(n)})$; this proof can be seen as a $\pi\sigma_{i_0}$-OBDD($\wedge$) proof of $\Psi(x_1, x_2, \dots, x_n)$ that has size at least $2^{\Omega(n)}$ by choice of $i_0$.

The upper bound. Let $\tau$ be an order of variables $x_1, x_2, \dots, x_n$ such that $\Psi(x_1, x_2, \dots, x_n)$ has a short $\tau$-OBDD($\wedge$) proof.

We describe a short OBDD($\wedge$, reordering) proof of $\Phi_n$. Let $\mu_i$ be orders of variables $w_1, w_2, \dots, w_k, x_1, x_2, \dots, x_n$ such that $x_1, x_2, \dots, x_n$ are ordered by $\tau\sigma_i^{-1}$ and the variables $w_1, w_2, \dots, w_k$ appear before the variables $x_1, x_2, \dots, x_n$. In other words, $\mu_i$ orders variables as follows: $w_1, w_2, \dots, w_k, x_{\tau\sigma_i^{-1}(1)}, x_{\tau\sigma_i^{-1}(2)}, \dots, x_{\tau\sigma_i^{-1}(n)}$.

Consider a polynomial sized $\tau$-OBDD($\wedge$) proof of $\Psi_n$. It is easy to see that this derivation may be transformed into a $\mu_i$-OBDD($\wedge$) derivation of a diagram that represents $w \ne i$ from the formula $(w=i) \rightarrow \Psi(x_{\sigma_i(1)}, x_{\sigma_i(2)}, \dots, x_{\sigma_i(n)})$. Indeed, the variables $w_1, w_2, \dots, w_k$ in the order $\mu_i$ appear in the beginning, hence, every diagram $D$ from the original proof will be transformed to a diagram that represents $D \vee \neg(w=i)$ and the latter diagram has size at most $|D| + O(k)$, where $|D|$ is size of the diagram $D$.

So we have all diagrams that represent $w \ne i$ for all $i \in [2^k]$. Formally these diagrams use different orders $\mu_i$ but in fact the diagrams depend essentially only on the variables $w_1, w_2, \dots, w_k$, and all $\mu_i$ order them in the same way. Thus, if we change orders in all of these diagrams to some "standard" one, the diagrams will be not changed. Then we apply the conjunction rule to these diagrams and get a constant false diagram since $w_1w_2\dots w_k$ is a binary representation of $i-1$ for some $i \in [2^k]$. All intermediate diagrams have size at most $2^k \text{poly}(n)$. Hence, we get a proof of size $\text{poly}(n)$. $\square$

Now we construct a family of unsatisfiable formulas $\Psi_n$ that satisfies the conditions of Theorem 4.1. We use an argument similar to the proofs of the lower bounds for OBDD($\wedge$, reordering) proofs. At first, we construct a function that has sizes of OBDD representations in different orders close to the required sizes of proofs for $\Psi_n$.

Let $\text{EQ}_n: \{0,1\}^{2n} \rightarrow \{0,1\}$ be *equality function*; i.e., the function that is true on an input $s \in \{0,1\}^{2n}$, if and only if $s_i = s_{i+n}$ for all $i \in [n]$. It is convenient to use the following notation for variables: $\text{EQ}_n(x_1, x_2, \dots, x_n, x_{n+1}, \dots, x_{2n})$; in this notation the function is true iff $x_1x_2\dots x_n = x_{n+1}x_{n+2}\dots x_{2n}$.

**Proposition 4.2.** In the order $x_1, x_{n+1}, x_2, x_{n+2}, \dots, x_n, x_{2n}$ the function $\text{EQ}_n$ has an OBDD representation of size $3n+2$.

*Proof.* The proof can be easily done by induction, using the following equation: $\text{EQ}_n(x_1, x_2, \dots, x_n, x_{n+1}, \dots, x_{2n}) = (x_1 = x_{n+1} \wedge \text{EQ}_{n-1}(x_2, \dots, x_n, x_{n+2}, \dots, x_{2n})$. $\square$
The proof of the following lemma is similar to the proof of the $\Omega(n)$ lower bound on the best communication complexity of the shifted equality function [15, Example 7.9].

**Lemma 4.3.** Let $\sigma_i$ for $i \in [n]$ be a permutation such that $\sigma_i(j) = j$ for $j \in [n]$ and $\sigma_i(n + j) = n + (i + j - 1 \mod n) + 1$ for $j \in [n]$. Then for any balanced partition $\Pi = (\Pi_0, \Pi_1)$ of $2n$ variables $x_1, \dots, x_{2n}$ there exists $i \in [n]$ such that communication complexity of $\mathbf{EQ}_n$ with respect to $\sigma_i \Pi$ is at least $\Omega(n)$, where

$$ \Pi\sigma_i = (\{j \mid \sigma_i(j) \in \Pi_0\}, \{j \mid \sigma_i(j) \in \Pi_1\}). $$

*Proof.* Let $\Gamma$ be a partition of $[2n]$, $V_x^\Gamma = \{i \in [n] \mid i \in \Pi_0\}$, and $V_y^\Gamma = \{i \in [n] \mid (i + n) \in \Pi_0\}$.

We denote by $B^\Gamma = V_x^\Gamma \oplus V_y^\Gamma$ the symmetric difference of $V_x^\Gamma$ and $V_y^\Gamma$.

**Claim 4.3.1.** *Communication complexity of $\mathbf{EQ}_n$ with respect to a partition $\Gamma$ is at least $|B^\Gamma|$.*

*Proof.* Let $V_x^\Gamma \setminus V_y^\Gamma = \{i_1, \dots, i_{\ell_1}\}$ and $V_x^\Gamma \setminus V_y^\Gamma = \{j_1, \dots, j_{\ell_2}\}$. Note that the communication complexity

of $\mathbf{EQ}_{\ell_1+\ell_2}$ is at least $\ell_1 + \ell_2 = |B^\Gamma|$. Additionally, if we define $v_k = \begin{cases} x_{k'} & \text{if } k = i_{k'} \\ x_{k'} & \text{if } k = j_{k'} + n \\ x_{k'+\ell_1+\ell_2} & \text{if } k = i_{k'} + n \text{ for } k \in [2n], \\ x_{k'+\ell_1+\ell_2} & \text{if } k = j_{k'} \\ 0 & \text{otherwise} \end{cases}$

then $\mathbf{EQ}_n(v_1, \dots, v_{2n}) = \mathbf{EQ}(x_1, \dots, x_{\ell_1+\ell_2}, \dots, x_{2(\ell_1+\ell_2)})$. Since Alice and Bob can independently compute $v_1, \dots, v_n$ and $v_{n+1}, \dots, v_{2n}$, respectively, we prove that communication complexity of $\mathbf{EQ}_n$ with respect to a partition $\Gamma$ is at least $|B^\Gamma|$. $\square$

If for some $i \in [n]$ size $|B^{\Pi\sigma_i}| \ge \frac{n}{32}$, then by Claim 4.3.1, communication complexity of $\mathbf{EQ}_n$ with respect to $\Pi\sigma_i$ is at least $n/32$. Assume that for all $i$ the following holds: $|B^{\Pi\sigma_i}| < \frac{n}{32}$.

Let us show that $|V_y^\Pi| \ge n/2$. Indeed, we know that $|V_x^\Pi| + |V_y^\Pi| = n$, hence, $|V_x^\Pi \cup V_y^\Pi| \ge \frac{n}{2}$. Since $\sigma_n$ is the identical permutation, we get $n/32 > |V_x^\Pi \oplus V_y^\Pi| = |V_x^\Pi \cup V_y^\Pi| - |V_x^\Pi \cap V_y^\Pi| \ge \frac{n}{2} - |V_y^\Pi|$, and therefore $|V_y^\Pi| \ge \frac{15n}{32}$.

By definition, $B^{\Pi\sigma_i} = V_x^{\Pi\sigma_i} \oplus V_y^{\Pi\sigma_i}$. Since the permutation $\sigma_i$ does not move variables $x_j$ for $j \in [n]$, we get $V_x^{\Pi\sigma_i} = V_x^\Pi$ for all $i \in [n]$. Note that if $|V_x^\Pi \oplus V_y^\Pi\sigma_i| < n/32$ and $|V_x^\Pi \oplus V_y^\Pi\sigma_j| < n/32$, then $|V_y^{\Pi\sigma_i} \oplus V_y^{\Pi\sigma_j}| < n/16$ for all $i, j \in [n]$.

We show that there exists a $j \in [n]$ such that $|V_y^\Pi \oplus V_y^{\Pi\sigma_j}| \ge n/16$. The latter would be a contradiction with our assumption since $\sigma_n$ is an identical substitution. Consider the sum $\sum_{k=1}^n |V_y^\Pi \cap V_y^{\Pi\sigma_k}|$. From the one hand this sum equals $|V_y^\Pi|^2$. Indeed,

$$ \begin{aligned} \sum_{k=1}^{n} |V_y^\Pi \cap V_y^{\Pi\sigma_k}| &= \sum_{k=1}^{n} \sum_{i \in V_y^\Pi} \mathbf{1}_{i \in V_y^{\Pi\sigma_k}} = \sum_{k=1}^{n} \sum_{i \in V_y^\Pi} \mathbf{1}_{\sigma_k(i+n) \in \Pi_0} = \\ & \sum_{k=1}^{n} \sum_{i \in V_y^\Pi} \mathbf{1}_{\sigma_k(i+n)-n \in V_y^\Pi} = \sum_{i \in V_y^\Pi} \sum_{j \in V_y^\Pi} |\{k \in [n] \mid \sigma_k(i+n) - n = j\}| = \sum_{i \in V_y^\Pi} \sum_{j \in V_y^\Pi} 1 = |V_y^\Pi|^2. \end{aligned} $$

From the other hand

$$ \sum_{k=1}^{n} |V_y^\Pi \cap V_y^{\Pi\sigma_k}| \ge \sum_{k=1}^{n} (|V_y^\Pi \cup V_y^{\Pi\sigma_k}| - |V_y^\Pi \oplus V_y^{\Pi\sigma_k}|) \ge \sum_{k=1}^{n} (|V_y^\Pi| - |V_y^\Pi \oplus V_y^{\Pi\sigma_k}|) > n|V_y^\Pi| - \frac{n^2}{16}. $$

Note that if $|V_y^\Pi| \ge \frac{n}{2} + \frac{n}{64}$, then $|V_x^\Pi| < \frac{n}{2} - \frac{n}{64}$ and $|V_x^\Pi \oplus V_y^\Pi\sigma_i| \ge \frac{n}{32}$ which contradicts the assumption. If $|V_y^\Pi| < \frac{n}{2} + \frac{n}{64}$, then $|V_y^\Pi|^2 \le \frac{n^2}{4} + \frac{n^2}{32}$ but $n|V_y^\Pi| - \frac{n^2}{16} \ge \frac{15n^2}{32} - \frac{n^2}{16}$ and this is a contradiction. $\square$
**Corollary 4.4.** Let $\sigma_i$ for $i \in [n]$ be a cyclic permutation of variables $y$ that maps $y_j$ to $y_{i+j \bmod n+1}$ for any $j \in [n]$. Formally $\sigma_i(j) = j$ for $j \in [n]$ and $\sigma_i(n+j) = n + (i+j-1 \bmod n) + 1$ for $j \in [n]$. Then for any order $\pi$ on $2n$ variables there exists $i \in [n]$ such that every $\pi\sigma_i$-OBDD representation of $\mathbf{EQ}_n$ has size at least $2^{\Omega(n)}$.

Now we are ready to construct a formula that may be used in Theorem 4.1. Consider a formula $\Psi_n(x, y, z)$ from $3n + 1$ variables (here $x, y$ are vectors of $n$ variables and $z$ is a vector of $n + 1$ variables) that is the conjunction of CNF representations of the following conditions:

* $x_i = y_i$ for all $i \in [n]$;

* $z_0$;

* $(x_i = y_i) \rightarrow (z_{i-1} \rightarrow z_i)$ for all $i \in [n]$;

* $\neg z_n$.

Note that $\Psi_n(x, y, z)$ is unsatisfiable since we have that $x_i = y_i$ for all $i$; it implies that $z_i = 1$ for all $i$, but $z_n$ should be zero. The following statement is straightforward.

**Proposition 4.5.** $\Psi_n$ has a proof of polynomial size in the order $z_0, x_1, y_1, z_1, x_2, y_2, z_2, \dots, x_n, y_n, z_n$.

**Proposition 4.6.** $\Psi_n(x, y, z)$ is minimally unsatisfiable, i.e., it becomes satisfiable after removing any of its clauses.

*Proof.* We consider 3 cases.

1. If we remove the clause $\neg z_n$ (or $z_0$), then identically 1 (or identically 0) assignment satisfies all other clauses.

2. If we remove a clause that represents $x_i = y_i$ (w.l.o.g. assume that this is the clause $\neg x_i \lor y_i$), then we assign $x_j = 1$ for all $j, y_j = 1$ for all $j \neq i, y_i = 0$ and $z_j = 1$ for $j < i$ and $z_j = 0$ for $j \geq i$.

3. If we remove a clause that represents $(x_i = y_i) \rightarrow (z_{i-1} \rightarrow z_i)$ (w.l.o.g. assume that this is the clause $x_i \lor y_i \lor \neg z_{i-1} \lor z_i$), then we assign $x_j = y_j = 0$ for all $j \in [n]$ and $z_j = 1$ for $j < i$ and $z_j = 0$ for $j \geq i$.

□

**Lemma 4.7.** For any order $\pi$ on the variables $x, y, z$ size of a $\pi$-OBDD($\wedge$) proof of $\Psi_n$ is at least $\frac{1}{\sqrt{10}}\sqrt{S}$, where $S$ is the size of the shortest $\pi'$-OBDD representation of $\mathbf{EQ}_n(x, y)$, where $\pi'$ is the order induced by $\pi$ on the variables $x, y$.

*Proof.* Assume that in the last step of the proof we apply the conjunction operation to $F_1$ and $F_2$ and get a contradiction. By Proposition 4.6, $\Psi_n$ is minimal unsatisfiable; hence, every clause of $\Psi_n$ was joined either to $F_1$ or to $F_2$. $F_1$ and $F_2$ are not identically false functions. By the argument similar to the proof of Proposition 4.6 there exists a satisfying assignment $\tau_1$ for $F_1$ and there exists a set $I_1 \subseteq [n]$ of size at least $(n-1)$ such that for all $i \in I_1$ the values of variables $\tau_1(x_i) = \tau_1(y_i)$. Moreover, if for arbitrary set $J \subseteq I_1$ we simultaneously change values of variables $x_j$ and $y_j$ for $j \in J$, then $\tau_1$ remains satisfiable. Let $\rho_1$ be a partial substitution that does not substitute values for $x_i$ and $y_i$ for $i \in I$ and for all other variables it is consistent with $\tau_1$. We define $I_2$ and $\rho_2$ analogously. Let us consider the function $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$; it contains all clauses of $\mathbf{EQ}_n(x, y)$ that have occurrences of $x_i$ and $y_i$ for $i \in I_1 \cap I_2$ and possibly several remaining clauses of $\mathbf{EQ}_n(x, y)$. Hence, $\mathbf{EQ}_n(x, y)$ can be obtained from $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ by addition of at most four clauses, and each of them depends on two variables. Hence, $S$ (recall that $S$ is the shortest $\pi'$-OBDD representation of $\mathbf{EQ}_n(x, y)$) is at most 100 times the size of any $\pi'$-OBDD representation of $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$. Therefore, an $\pi$-OBDD-representation of either $F_1$ or $F_2$ has size at least $\frac{1}{\sqrt{10}}\sqrt{S}$. □

**Theorem 4.8.** There exists an unsatisfiable CNF formula $\Phi_n$ of size poly($n$) such that there exists a polynomial size OBDD($\wedge$, reordering) proof of $\Phi_n$ but every OBDD($\wedge$) proof of $\Phi_n$ has size $2^{\Omega(n)}$.
*Proof.* By Lemma 4.7 for every order $\pi$ a size of $\pi$-OBDD($\wedge$) proof of $\Psi_n$ is at least $\frac{1}{10}\sqrt{S}$, where $S$ is the size of the shortest $\pi$'-OBDD representation of $\mathbb{E}Q_n$. By Lemma 4.4 there exists a family of permutations $\sigma_i$ of $[2n]$ for $i \in [n]$ such that for every order $\tau$ there exists an $i \in [n]$ such that size of any $\tau\sigma_i$-OBDD($\wedge$) proof of $\Psi_n$ is at least $2^{\Omega(n)}$. By Proposition 4.5 there exists a required order $\tau$ and a $\tau$-OBDD($\wedge$) proof of $\Psi_n$ of size poly($n$). Theorem 4.1 gives a construction of the desired formula $\Phi_n$. $\square$

# 5 OBDD($\wedge, \exists$, reordering) algorithms

It is known that OBDD($\wedge, \exists$) algorithms can prove $\text{PHP}_n^{n+1}$ in polynomial time [6]. Now we show that the Tseitin formulas are also easy for OBDD($\wedge, \exists$) algorithms.

**Proposition 5.1.** *There exists an OBDD($\wedge, \exists$) algorithm that solves Tseitin formulas in polynomial time.*

Informally the proof of this theorem is the following. Notice that the projection of two linear equations over the common variable is just the sum of these equations. Since every variable has exactly two occurrences in Tseitin formulas, we can sum up all equations in every connected component.

*Proof.* Consider the following OBDD($\wedge, \exists$) algorithm.

1. If $S \neq \emptyset$, choose $C \in S$ and apply join operation; otherwise goto Step 5.

2. If $D$ depends on some variable $x$, apply join operation to all clauses in $S$ that depend on $x$.

3. Apply projection operation over variable $x$.

4. If $D$ represents a constant then go to Step 1, otherwise goto Step 2.

5. If $D$ is satisfiable then return 1, otherwise return 0.

We prove that this algorithm solves Tseitin formulas in polynomial-time. We note that after Step 2 the current diagram $D$ represents the conjunction of two linear equations and after Step 3 the current diagram $D$ represents one linear equation. Indeed every variable of Tseitin formula has occurrences in exactly two equations. And the projection of two linear equations over the common variable is just the sum of this equations.

It is easy to see that the algorithm chooses a connected component of the graph and sums up all equations from this component. If the component is unsatisfiable the algorithm stops and return 0; otherwise it goes to the next component. Finally if all components are satisfiable it returns 1.

Any OBDD that represents one linear equation have linear size. We need to check that if we join to $D$ a subset of clauses representing linear equation we still have small diagram. Consider some equation from a Tseitin formula that depends on $d$ variables, the maximum size of OBDD for the subset of clauses has size at most $2^{d+1} - 1$ (the size of a decision tree). The size of any CNF representation of a linear equation is at least $2^{d-1}$. Hence, the OBDD size of conjunction of the clauses is less than the size of the formula multiplied by 4. $\square$

Now we show that every OBDD for a characteristic function of a good enough code has at least exponential size.

**Theorem 5.2.** Let $C \subseteq \{0,1\}^n$ be a $(\frac{1}{2} + \epsilon, L)$-erasure list decoding code. Then for every partition $\Pi$ such that $|\Pi_0| = \frac{n}{2}$ the communication complexity of the characteristic function of $C$ (i.e. function $\chi_C: \{0,1\}^n \to \{0,1\}: \forall c \in \{0,1\}^n \chi_C(x) = 1 \Leftrightarrow c \in C$) with respect to $\Pi$ is at least $\log \frac{|C|}{L^2}$.

Moreover, for every tuple of $k$ different indices $i_1, \dots, i_k \in [n]$ ($0 \le k \le 2\epsilon n$) and every partition $\Pi$ such that $|\Pi_0| = \frac{n-k}{2}$, communication complexity of the Boolean function $\exists x_{i_1} \dots \exists x_{i_k} \chi_C(x_1, \dots, x_n)$ with respect to $\Pi$ is at least $\log \frac{|C|}{L^2}$.
*Proof.* It is enough to prove the "moreover" part of the statement since the first part is its special case (with $k=0$). Without loss of generality we may assume that $\Pi = (\{1, \dots, \frac{n-k}{2}\}, \{\frac{n-k}{2} + 1, \dots, n-k\})$ and $i_j = n-k+j$ for all $j \in [k]$.

We prove that any 1-monochromatic rectangle for $\chi(x_1, \dots, x_{n-k}) =$ $\exists y_1, \dots, y_k \ \chi_C(x_1, \dots, x_{n-k}, y_1, \dots, y_k)$ contains at most $L^2$ elements. Let $R = A \times B$ be some 1-monochromatic rectangle and $a \in A$. Consider the string $c = a^{?n-|v|}$: it has at most $\frac{n+k}{2} \le (\frac{1}{2} + \epsilon)n$ symbols ?, hence, there are at most $L$ codewords that are consistent with $c$. As a result, $|B| \le L$. $|A| \le L$, by the same argument.

Hence, there are at least $\frac{|C|}{L^2}$ 1-monochromatic rectangles and communication complexity of $\chi$ is at least $\log \frac{|C|}{L^2}$. $\square$

**Theorem 5.3.** Let $C \subseteq \{0,1\}^n$ be a linear code with the relative distance $\frac{1}{3}$ such that the checksum matrix $H$ of the code $C$ has the following properties:

* $H$ has size $\alpha n \times n$, where $\alpha \in (0,1)$ is a constant;

* every row of $H$ contains at most $t(n)$ ones, where $t$ is some function;

* every $\frac{1}{6}n$ columns of $H$ intersect (contains ones in) at least $(\alpha - \delta)n$ rows, where $\delta \in (0, \frac{1-\alpha}{2})$ is a constant.

Let a formula $F_n$ be a standard representation of $H(x) = 0$ as a $t$-CNF of size at most $\alpha n 2^{t(n)-1}t(n)$ (every equation is represented in a straightforward way, without any additional variables). Then every OBDD($\wedge, \exists$, reordering) algorithm runs on the formula $F_n$ for at least $2^{\Omega(n)}$ steps.

*Proof.* The code $C$ has relative distance $\frac{1}{3}$. Hence, $C$ is $(\frac{7}{12}, 8)$-erasure list-decodable by Theorem 2.5, choosing $\epsilon = 1/4$. We consider the execution of an OBDD($\wedge, \exists$) algorithm on the formula $F_n$. We prove that in some moment size of a diagram $D$ will be at least $2^{\Omega(n)}$. Assume that the algorithm during its execution applies the projection operation at least $k = \frac{1}{6}n$ times. We consider the diagram $D$ just after the first moment when the algorithm applies the projection operation $k$ times. Let $D$ represent a function of type $\exists y_1, \dots, y_k \phi(x_1, \dots, x_{n-k}, y_1, \dots, y_k)$, where $\phi$ is the conjunction of several clauses from $F_n$. The projection operation on a variable $x$ can be applied only if all clauses from $S$ do not depend on $x$. Then all clauses corresponding to linear equations with the variable $x$ must be among clauses of $\phi$. By the assumption of the theorem any $k$ columns of $H$ have ones in at least $(\alpha - \delta)n$ rows. Thus, $\phi$ contains all clauses from the representation of $(\alpha - \delta)n$ equations and possibly several other clauses from other equations.

**Lemma 5.4.** Let $A$ be an $m \times n$ checksum matrix of a $(\rho, L)$-erasure list decodable code. The matrix $A'$ is the result of deleting $r$ rows from $A$. Then $A'$ is a checksum matrix of a $(\rho, 2^r L)$-erasure list-decodable code.

*Proof.* Consider an arbitrary $n$-dimensional vector $z$ with variables at $\rho n$ coordinates and $\{0,1\}$ constants at other coordinates. We have to show that the number of solutions of the system $A'z = 0$ is at most $2^r L$. Consider an $n$-dimensional vector $z'$ with variables in the same positions as in $z$ and with zeros in all other positions. Since $A$ is the checksum matrix of a $(\rho, L)$-erasure list decodable code, the system $Az' = 0$ has at most $L$ solutions. The system $Az' = 0$ is homogeneous, hence, the number of its solutions is exactly $2^{\rho n - \ell}$, where $\ell$ is the rank of the linear system. Note that $\ell$ is not necessary equal to the rank of $A$ since not all components of $z'$ contains variables, some of them contains constants. But the rank of this system equals to the rank of the system $Az = 0$. Since $A'$ can be obtained from $A$ by deleting of $r$ rows, rank of the system $A'z' = 0$ is at least $\ell - r$. Hence, $A'z = 0$ has at most $2^{\rho n - \ell + r} \le 2^r L$ solutions. Rank of the system $A'z = 0$ equals to the rank of the homogeneous system $A'z' = 0$. Thus, the number of solution of $A'z = 0$ is at most $2^r L$. $\square$

Lemma 5.4 implies that $\phi$ is a characteristic function of a $(\frac{7}{12}, 8 \cdot 2^{\delta n})$-erasure list-decodable code. The number of satisfying assignments of $\phi$ is at least the number of solutions of the system $Hx = 0$, hence, size of the code defined by $\phi$ is at least $2^{(1-\alpha)n}$. By Theorem 5.2 size of every OBDD for $\exists y_1, \dots, y_k \phi(x_1, \dots, x_{n-k}, y_1, \dots, y_k)$ is at least $2^{(1-\alpha)n} 2^{-2\delta n} \frac{1}{16} > 2^{(1-\alpha-2\delta)n-4}$ for every order of variables.
**Proposition 6.1** (see [10]). Most (say, at least 90%) of matrices in Gallager's family define a linear code with parameters approaching Gilbert-Varshamov bound. More precisely, for every $\delta \in (0, \frac{1}{2})$ and for every $t$ there exists $r = r(t)$ such that for large enough $n$ most matrices from the defined family have minimal distance $\ge \delta n$. Moreover, the ratio $r(t)/t$ approaches $h(2\delta)$ as $t$ goes to infinity, where $h(x) = -x \log x - (1-x) \log(1-x)$ (the binary entropy). This means that the rate of the code can be made arbitrarily close to $1-h(2\delta)$ (i.e., to the Gilbert-Varshamov bound).

A family of linear codes defined above can be specified by parameters $r, t, n$. However, it is more convenient to specify these codes by another triple of numbers — by $(\delta, t, n)$ (assuming that the value $r = r(\delta, t, n)$ is defined implicitly as the minimal integer such that most codes of the family have minimal distance greater than $\delta n$). Now we can state the main technical lemma of this section.

**Lemma 6.2.** For all $\beta \in (0, 1)$, $\gamma < 1$, and $\delta \in (0, \frac{1}{2})$, for all large enough $t$ most (say, at least 90%) of linear codes from Gallager's family with parameters $(\delta, t, n)$ satisfy the following property: every $\beta n$ columns in the checksum matrix of the code intersect at least a fraction $\gamma$ of all rows of the matrix.

*Proof.* By construction, every checksum matrix from Gallager's codes family consists of $r$ blocks of size $(n/t) \times n$ (where each if these blocks is a permutation of columns of the basic matrix $A$ defined above). Let us fix some real $\rho > 0$. We say that some tuple of $\beta n$ columns is *poor* for some block of the matrix, if these columns intersect with at most $\rho \cdot (n/t)$ rows of the block. We will proceed as follows.

**Step 1.** We estimate the probability of the event that one fixed tuple of $\beta n$ columns is poor for a randomly chosen block (which is obtained as a random permutation of columns in $A$).

**Step 2.** We estimate the probability that one fixed tuple of $\beta n$ columns is poor for more than $\rho r$ randomly chosen blocks.

**Step 3.** At last, we estimate the probability that *at least one* tuple of $\beta n$ columns is poor for more than $\rho r$ (independently) randomly chosen blocks.

We are going to show that the probability estimated on Step 3 becomes very small for a suitable $t$. It follows that for most Gallager's codes, every tuple of $\beta n$ columns intersects all but $2\rho n/t$ rows (one fraction of $\rho$ rows comes from all blocks where these columns are poor, and another fraction of $\rho$ rows comes from all other blocks). We can choose $\rho$ so that $1-2\rho > \gamma$, and the Lemma will follow. Thus, it remains to bound the probabilities in Steps 1-3.

*Step 1:* We fix some tuple of $\beta n$ indices of columns, then take a random permutation of columns in a matrix $A$ and count the total number of intersected rows. These random procedure can be equivalently explained in other words: we fix the original matrix $A$ and choose at random a tuple of $\beta n$ columns. By the construction of the matrix $A$, every column from the chosen tuple intersects with only one row. We need to estimate the number of rows that intersect with at least one of these $\beta n$ columns. We have to show that for $\beta n \gg n/t$ a “typical” tuple of columns $\langle i_1, \dots, i_{\beta n} \rangle$ intersects with almost all rows. Let us estimate the probability of the “bad” event, when the randomly chosen columns intersect with only $s \le (1-\rho)(n/t)$ rows. This bad event means that we can select $s$ positions in the sequence of indices $1, \dots, \beta n$ so that

(i) the $s$ columns with “selected” indices $i_{l_1}, \dots, i_{l_s}$ intersect pairwise different rows of the matrix $A$, and

(ii) each of the other $(\beta n-s)$ columns intersects once again the same row as one of the $s$ “selected” columns. Probability of this event is not greater than

$$ \sum_{s=1}^{(1-\rho)n/t} \binom{\beta n}{s} \Pr[\text{columns } i_{l_1}, \dots, i_{l_s} \text{ intersect pairwise different rows}](1-\rho)^{\beta n-s} \le \sum_{s=1}^{(1-\rho)n/t} \binom{\beta n}{s} (1-\rho)^{\beta n-s}. \quad (1) $$
Indeed, for each $s$ we have $\binom{\beta n}{s}$ ways to choose $s$ indices in the list $1, \dots, \beta n$. When the positions of the $s$ “selected” columns are fixed, every next randomly chosen column intersects with one of the previously counted rows with a probability less than

$$ \frac{[\text{columns intersecting with given } s \text{ rows}]}{[\text{total number of columns}]} = \frac{s \cdot t}{n} < 1 - \rho. $$

For a fixed $\rho$ and $(n/t) \ll \beta n$, the sum (1) is less than $2^{-c\beta n}$, where $c > 0$ depends on $\rho$ (and not on $n$).

**Step 2:** Let us fix some tuple of $\beta n$ columns. At Step 1 we proved that the probability to get one poor block is $p_n < 2^{-c\beta n}$. Since all $r$ blocks in the checksum matrix are chosen independently, the probability that at least $k = (1 - \rho)r$ of them are poor for the fixed columns is less than $\binom{r}{k} \cdot (p_n)^k \le 2^r \cdot 2^{-c\beta kn}$. As we increase $t$, the corresponding values of $r = r(t)$ and $k(t) = (1 - \rho)r(t)$ grow linearly. It follows that $2^r \cdot 2^{-c\beta kn}$ decreases as $2^{-\Theta(\beta tn)+O(t)}$ (the multiplicative constants hidden in the terms $\Theta(\beta tn)$ and $O(t)$ depend on $\rho$ but not on $t$).

**Step 3:** It remains to multiply the probability from Step 2 by the number of all tuples of $\beta n$ columns. We get the bound $\binom{n}{\beta n} \cdot 2^{-\Theta(\beta tn)+O(t)} = 2^{h(\beta)n+o(n)} \cdot 2^{-\Theta(\beta tn)+O(t)}$ for the probability that at least one tuple of $\beta n$ columns intersects too few rows. It remains to choose a suitable $t = t(\beta)$ and make this probability less than 0.1. $\square$

**Corollary 6.3.** For the distribution defined above, the system of linear equations $Hx = 0$ with probability close to 1 can be represented as a CNF of size $O(n)$.

Thus, we obtain a weak version of Corollary 5.5 (without the moreover part) for CNF of size $O(n)$ with $n$ Boolean variables. In other words, for every $N$ there exists a CNF formula of size $N$ such that every OBDD($\wedge, \exists$) algorithm runs on this formula at least $2^{\Omega(N)}$ steps. In the next section we prove a similar result for an explicitly constructed code.

## 6.2 An explicit construction of suitable linear codes

In this section we present an explicit construction of a linear code with the property of list decoding and a check-sum matrix that is sparse and strongly mixing. More technically, we construct explicitly a code that enjoys the properties from Proposition 6.1 and Lemma 6.2 (in the previous section we proved that this property holds with high probability for randomly chosen code from Gallager's family of linear codes).

### 6.2.1 The large-scale scheme of the construction

Our aim is to construct an explicit family of linear codes with the properties discussed in the previous section. To be more specific, we fix a triple of real parameters $(\alpha, \beta, \gamma)$ and define four properties of a linear code (more precisely, we define properties of a checksum matrix of a linear code).

(G) The number of codewords matching this matrix is equal to $2^{\Omega(n)}$ (the code is asymptotically good).

(S) **Sparseness:** every row contains only $O(1)$ ones (the other matrix elements are zeros)

(L) **List decoding:** for every set of $\alpha n$ positions in a codeword

$$ 1 \le i_1 < \dots < i_{\alpha n} \le n, $$

and for every assignment of bits $b_j$ to these positions, there exist at most $O(1)$ codewords $\bar{x} = (x_1, \dots, x_n)$ corresponding to this checksum matrix such that $x_{i_j} = b_j$ for $j = 1, \dots, \alpha n$.

(M) **Mixing:** For every set of $\beta n$ columns (between the 1-st and the $n$-th) there exist $\ge \gamma n$ rows of the matrix intersecting at least one of these columns with 1.

Now we can formulate the main result of this section.
**Theorem 6.4.** For any values of parameters $\alpha > 0$, $\beta > 0$, and $\gamma < 1$ there exists a polynomial-time computable algorithm that finds for inputs $n$ from a dense enough sequence of integers $n$ (technically, for an arithmetic series of $n$) a (binary) checksum matrix $M_n$ of size $n \times k(n)$ (with $n$ columns and $k(n)$ linearly independent rows) that satisfies the conditions (G), (S), (L'), and (M).

Together with Theorem 5.3 this statement implies Corollary 5.5. Indeed, to prove Corollary 5.5 it is enough to take the natural representation of the linear system constructed in Theorem 6.4.

In the proof of Theorem 6.4 we prefer to use instead of (L) another property that can be defined in terms of the code distance:

(L') **Code distance:** the distance between every two codewords in the code is $\ge (\frac{1}{2} - \delta)n$.

Notice that (L') implies (L) due to Theorem 2.5. Thus, to prove the theorem it is enough to provide an explicit construction of codes that satisfy (G), (S), (L'), and (M). Also for some technical reason we will need in the proof a stronger version of (M) with some suitable parameter $q > 0$:

(M') **Strong mixing:** for every set of $\beta n$ columns there exist $\ge \gamma n$ rows of the matrix intersecting at least $q$ of these columns with 1.

The rest of this section is organized as follows. In Section 6.2.2 we explain an explicit construction of a code that satisfies (L'). In Section 6.2.3 we explain an explicit construction of a code that satisfies (M'). In Section 6.2.4 we merge these two constructions. At last, in Section 6.2.5 we briefly discuss the explicit construction of algebraic expanders involved in the previous sections.

## 6.2.2 A code with a very high distance.

Our construction is iterative: we start with some asymptotically good explicitly constructed linear code and then amplify its parameters by iterating $O(1)$ times some transformation of this code, as explained below.

The starting point of our construction is an asymptotically good linear code with the code length $N$ and code distance $\rho N$ for some constant $\rho > 0$. For instance, we can take the explicit construction of expander codes suggested by Zémor, [25]. So far we only assume that $\rho > 0$ (so the code distance can be much less than $N/2$). In what follows we apply ($O(1)$ times) to this code some amplification procedure. Each iteration of this procedure

* extends the length of codewords by some constant factor,

* does not change the number of codewords,

* makes the code distance closer to $1/2$ of the code length.

The amplification procedure decreases the rate of the code by some constant factor. However, the code remains asymptotically good. After $O(1)$ iteration of this procedure we will obtain a code that satisfies properties (G), (S), and (L'). At this stage we cannot guarantee the property (M) (to achieve (M) we will need some more work, see the next section). To "amplify" a code with the length $N$ and the distance $\rho N$ we will use an (explicitly constructed) expander graph $G = (V, E)$ on $N$ vertices, with the following property of strong $\varepsilon$-expansion:

For every set of vertices $S \subset V$ of size $\le (\frac{1}{2} - \varepsilon)n$ the number of neighbors of this set (i.e., the number if vertices $w \in V$ that are connected by an edge with at least on vertex $v \in S$) is not less that $(2 + \varepsilon)|S|$.

*Remark:* A graph with the property of strong $\varepsilon$-expansion can be easily constructed from any algebraic expander with parameters $(N, d, 1/2)$. It is enough to add a loop to each vertex and then take a suitable degree $r$ of this graph. In other words, the edges of the new graph are paths of length $\le r$ in the initial algebraic expander. The less is the value of $\varepsilon$, the bigger length of the path $r = r(\varepsilon)$ we need to take, and the bigger is the degree of the resulting graph. However, for every constant $\varepsilon$ we obtain a graph with the property of strong $\varepsilon$-expansion and some degree $D = D(\varepsilon)$, which does not depend on $N$. We may assume that $\varepsilon$ is less than the value of $\delta$ from (L').
<figure><img src="image_3.png" /><figcaption>Figure 1: The bits $(x_1x_2x_3)$ assigned to the six ends of edges of the triangle graph.</figcaption></figure>

In what follows we describe the amplification procedure. We assume that we are given a linear code $\mathcal{C}$ with the code length $N$ and the code distance $\rho N$. We fix some one-to-one correspondence between the bits of the codewords of $\mathcal{C}$ ($i = 1, \dots, n$) and the vertices of a graph $G$ (with $N$ vertices, of some degree $D$) with the property of strong $\varepsilon$-expansion defined above. In what follows we transform $\mathcal{C}$ into a code $\mathcal{C}'$, and then into another code $\mathcal{C}''$. The last one will be the required “amplified” code.

**The first stage of the amplification: from $\mathcal{C}$ to $\mathcal{C}'$.** We construct a new code $\mathcal{C}'$ where each codeword will consist of $N' := DN$ bits, with the distance $\rho N'$ (i.e., the relative code distance in the new code $\mathcal{C}'$ is the same as in the original code $\mathcal{C}$). The bits of the codeword in $\mathcal{C}'$ correspond to the ends of edges in the graph $G$ (in a uniform graph of degree $D$ with $N'$ vertices we have $DN/2$ edges, and each edge has 2 ends).

The transformation from $\mathcal{C}$ to $\mathcal{C}'$ is quite trivial: we place the bits a codeword $\bar{x} = (x_1, \dots, x_N)$ from $\mathcal{C}$ to the corresponding vertices $(v_1, \dots, v_N)$ of $G$, and then rewrite the value of each bit $x_i$ to the opposite ends of the edges $(v_i, v_j)$ incident to $v_i$. In other words, for each edge $(v_i, v_j)$ of the graph we assign the bits $x_i$ and $x_j$ from the codeword $\bar{x}$ to the opposite ends of this edge ($x_i$ is assigned to the end incident to $v_j$, and $x_j$ is incident to the end incident to $v_i$, see an example in Fig. 1).

Thus, we essentially duplicate $D$ times each bit of a codewords and then redistribute these values between the ends of the edges of $G$.

**The second stage of the amplification: from $\mathcal{C}'$ to $\mathcal{C}''$.** We construct another code $\mathcal{C}''$, where each codeword consists of $N'' := 2^D N$ bits. To transform a codeword of $\mathcal{C}'$ in a codeword of $\mathcal{C}''$, we split the codeword in blocks of $D$ bits corresponding to the ends of edges incident to one vertex. Then we separately encode each of these blocks by the Hadamard code. (In fact, instead of the Hadamard code with the relative code distance $1/2$ we could take any other linear code with the relative code distance close enough to $1/2$).

Let us estimate the distance of $\mathcal{C}''$. The distance of the initial code $\mathcal{C}$ is equal to $\rho N$, so every non-zero codeword $\bar{x}$ in this code contains at least $\rho N$ ones. If $\rho < \frac{1}{2} - \varepsilon$, then in the corresponding codeword $\bar{x}'$ in $\mathcal{C}'$ contains $\ge (2+\varepsilon)\rho N$ blocks (with $D$ bits in each block) that involve at least one non-zero bit. By applying the Hadamard code we obtain a codeword $\bar{x}''$ in $\mathcal{C}''$ with $\ge (2+\varepsilon)\rho N$ non-zero blocks of size $2^D$, where each of these blocks contains exactly $D/2$ zeros and $D/2$ ones. Hence, the code distance of $\mathcal{C}''$ is not less than

$$ \frac{(2 + \varepsilon)\rho}{2} N'' = \left(1 + \frac{\varepsilon}{2}\right) \rho N''. $$

Thus, we have “amplified” the relative code distance from $\rho$ to $(1 + \frac{\varepsilon}{2}) \rho$.

This described amplification procedure does not change the number of codewords in a code, and increases the code length by a constant factor. Hence, if the original family of codes $\mathcal{C}$ is asymptotically good, then the amplified codes $\mathcal{C}''$ are also asymptotically good.
What is the structure of the checksum matrix of the new code? W.l.o.g. we may assume that the Hadamard code is systematic, so each bit of a codeword of C is just transferred to some position of the amplified C'''. Hence, for the amplified code we inherit all equations that define the original code C without any changes (up to renaming of the variables). If the checksum matrix of C is sparse, then each of these equations involve only O(1) variables. Besides the equation inherited from C, we add the equation that define the Hadamard code for each block of 2^D bits (one block for each vertex of G). Each of these equations contains at most 2^D = O(1) variables. Thus, the transformation preserves the property of sparsity of the checksum matrix. If the resulting family of linear constraints is not linearly independent, we can eliminate the redundant equations.

By repeating this amplification procedure O(1) times we obtain a linear code with the relative distance $\ge \frac{1}{2} - \delta$. This code satisfies condition (L'), and therefore (L). The properties (G) and (S) are satisfied for this code, as explained above. It remains to achieve the property (M). We discuss in the next section.

### 6.2.3 A checksum matrix with the mixing property

In this section we focus on the properties of a checksum matrix that look more natural being formulated as properties of a system of linear equations. Given a real $\sigma > 0$ and an integer $q > 0$, we study the following problem of linear algebra: we need to construct a system of $m \le \sigma n$ linear equations with $n$ variables, with the properties of sparsity (S) and mixing (M'). This problem can be reformulated as follows: we need to construct a bipartite graph $G = (V_L, V_R, E)$ with $n$ vertices in the left part (the $n$ vertices in $V_L$ correspond to the variables of the system) and $m$ vertices in the right part (the $m$ vertices in $V_R$ correspond to the linear equations of the system); an edge connects $v_i \in V_L$ with $w_j \in V_R$ (i.e., $(v_i, w_j) \in E$), if and only if the $i$-th variable is involved in the $j$-th $l$ equation of the linear system. In terms of this graph, the property of sparsity means that the degrees of all vertices in the right part are bounded by O(1), and the property of mixing means that for every set $S$ of $\beta n$ vertices on the left there exists a set $T$ of $\gamma m$ vertices on the right such that every $w \in T$ is connected with $S$ by at least $q$ edges.

We construct the required bipartite graph using an algebraic expander. Let us fix an algebraic expander $H$ with parameters $(N, d, \lambda)$. In our construction the vertices in $V_R$ (the linear equations) will correspond to the vertices of this expander, and the vertices in $V_L$ (the variables of the linear system) correspond to the paths of length $t$ in the expander. Thus, the number of variables in the system is $n = Nd^t$, and the number of equations is $m = N$. The $i$-th variable is involved in the $j$-th equation, if and only if the $i$-th path of length $t$ in $H$ contains the $j$-th vertex of $H$. If $t$ is a constant (does not depend on $n$), then this construction gives a sparse linear system: every variable is involved in $(t+1) \cdot d^t = O(1)$ equations. By choosing $t$ large enough, we can make the fraction $m/n$ less than the given parameter $\sigma$.

With a large enough $t$ we obtain a linear system with the strong property mixing. Indeed, let us fix in $H$ some set of vertices $S$ of size $\gamma N$. Then the fraction of paths $P$ of length $t$ where all but $q$ vertices belong to $S$, is not greater than

$$ (\gamma + \lambda)^{t-q} \cdot \binom{t}{q} $$

see [13, Theorem 3.10]. We can choose $t$ and $\lambda$ so that this fraction is less than $\beta$. Thus, we can achieve the property of strong mixing for the required values of $\beta, \gamma, q$.

### 6.2.4 Merging two constructions

Let us summarize the constructions discussed in two previous sections. In Section 6.2.2 we obtained a system of linear equations

$$ \left\{ \begin{array}{l} a_{1,1}x_1 + \cdots + a_{1,n}x_n = 0, \\ \vdots \\ a_{m,1}x_1 + \cdots + a_{m,n}x_n = 0, \end{array} \right. $$

with $n$ variables, with the dimension of the solution space $> c_1 n$ (property (G)), where every equation involves $\le c_2$ variables (property (S)), for some positive constants $c_1, c_2$ that does not depend on $n$. In
Section 6.2.3 we constructed another linear system

$$
\left\{
\begin{array}{l}
b_{1,1}x_1 + \cdots + b_{1,n}x_n = 0, \\
\vdots \\
b_{\ell,1}x_1 + \cdots + b_{\ell,n}x_n = 0,
\end{array}
\right.
$$

with $n$ variables and $\ell = \sigma n$ equations, with the property of strong mixing (M') from some $\beta, \gamma, q$. We are free to choose the parameters, so we may assume that $q > c_2$. Moreover, we can achieve the property (M') with arbitrarily small positive $\sigma$.

Now we joint together these two linear systems (we just take the union of linear equations from both
systems). The resulting linear system is defined by the matrix

$$
\begin{pmatrix}
a_{1,1} & a_{1,2} & a_{1,3} & \dots & a_{1,n} \\
a_{2,1} & a_{2,2} & a_{2,3} & \dots & a_{2,n} \\
\vdots & \vdots & \vdots & & \vdots \\
a_{m,1} & a_{m,2} & a_{m,3} & \dots & a_{m,n} \\
b_{1,1} & b_{1,2} & b_{1,3} & \dots & b_{1,n} \\
\vdots & \vdots & \vdots & & \vdots \\
b_{\ell,1} & b_{\ell,2} & b_{\ell,3} & \dots & b_{\ell,n}
\end{pmatrix}
$$

This linear system defines a code which is still asymptotically good provided that $\sigma < c_1$ (we may choose the value of $\sigma$ small enough). We refer to the $m$ linear constraints that came to the joint system from the construction of Section 6.2.2 as *primary equations*, and to the $\ell$ linear constraints that came from the construction of Section 6.2.2 as *auxiliary equations*.

The new code has only a weak version of the mixing property: the property (M') holds only for the auxiliary equations. How to spread the property (M') to the entire linear system? To this end we xor the auxiliary equations with the primary equations. More precisely, we add (in the sense of linear algebra) each of the auxiliary equations to the fraction $1/\ell$ of the primary equations. The same time, the auxiliary equations remain intact. Thus, we obtain a linear system with the matrix

$$
\left(
\begin{array}{c c c c c}
\begin{array}{c}
a_{1,1} \oplus b_{1,1} \\
a_{2,1} \oplus b_{2,1} \\
\vdots \\
a_{\ell,1} \oplus b_{\ell,1}
\end{array}
&
\begin{array}{c}
a_{1,2} \oplus b_{1,2} \\
a_{2,2} \oplus b_{2,2} \\
\vdots \\
a_{\ell,2} \oplus b_{\ell,2}
\end{array}
&
\begin{array}{c}
a_{1,3} \oplus b_{1,3} \\
a_{2,3} \oplus b_{2,3} \\
\vdots \\
a_{\ell,3} \oplus b_{\ell,3}
\end{array}
&
\begin{array}{c}
\dots \\
\dots \\
\vdots \\
\dots
\end{array}
&
\begin{array}{c}
a_{1,n} \oplus b_{1,n} \\
a_{2,n} \oplus b_{2,n} \\
\vdots \\
a_{\ell,n} \oplus b_{\ell,n}
\end{array} \\
\\
\begin{array}{c}
a_{\ell+1,1} \oplus b_{1,1} \\
a_{\ell+2,1} \oplus b_{2,1} \\
\vdots \\
a_{2\ell,1} \oplus b_{\ell,1}
\end{array}
&
\begin{array}{c}
a_{\ell+1,2} \oplus b_{1,2} \\
a_{\ell+2,2} \oplus b_{2,2} \\
\vdots \\
a_{2\ell,2} \oplus b_{\ell,2}
\end{array}
&
\begin{array}{c}
a_{\ell+1,3} \oplus b_{1,3} \\
a_{\ell+2,3} \oplus b_{2,3} \\
\vdots \\
a_{2\ell,3} \oplus b_{\ell,3}
\end{array}
&
\begin{array}{c}
\dots \\
\dots \\
\vdots \\
\dots
\end{array}
&
\begin{array}{c}
a_{\ell+1,n} \oplus b_{1,n} \\
a_{\ell+2,n} \oplus b_{2,n} \\
\vdots \\
a_{2\ell,n} \oplus b_{\ell,n}
\end{array} \\
\\
\begin{array}{c}
a_{2\ell+1,1} \oplus b_{1,1} \\
a_{2\ell+2,1} \oplus b_{2,1} \\
\vdots \\
a_{3\ell,1} \oplus b_{\ell,1}
\end{array}
&
\begin{array}{c}
a_{2\ell+1,2} \oplus b_{1,2} \\
a_{2\ell+2,2} \oplus b_{2,2} \\
\vdots \\
a_{3\ell,2} \oplus b_{\ell,2}
\end{array}
&
\begin{array}{c}
a_{2\ell+1,3} \oplus b_{1,3} \\
a_{2\ell+2,3} \oplus b_{2,3} \\
\vdots \\
a_{3\ell,3} \oplus b_{\ell,3}
\end{array}
&
\begin{array}{c}
\dots \\
\dots \\
\vdots \\
\dots
\end{array}
&
\begin{array}{c}
a_{2\ell+1,n} \oplus b_{1,n} \\
a_{2\ell+2,n} \oplus b_{2,n} \\
\vdots \\
a_{3\ell,n} \oplus b_{\ell,n}
\end{array} \\
\\
\vdots \\
\vdots \\
\\
b_{1,1} & b_{1,2} & b_{1,3} & \dots & b_{1,n} \\
\vdots \\
b_{\ell,1} & b_{\ell,2} & b_{\ell,3} & \dots & b_{\ell,n}
\end{array}
\right)
$$
This transform does not change the solution space of the system. The same time, the transformed system satisfies the mixing property (spread on all equations). Notice that when we xor an auxiliary equation with some of the primary equations, some 1's from both equations may cancel out. So we cannot claim that the modified system satisfies (M'). However, since $q > c_2$, we can claim that the entire matrix satisfies the weaker property (M).

If the equations of the resulting system are not linearly independent, we can eliminate the redundant equations. The number of eliminated equations is not greater than $\sigma n$ (the number of all auxiliary equations), and therefore this operation will not much affect the mixing property: in the worst case the value of parameter $\gamma$ shrinks to $\gamma' = \gamma - \sigma$. Since the constructions in Sections 6.2.2–6.2.3 work for any $\gamma < 1$ and any $\sigma > 0$, we can obtain as the result any $\gamma' < 1$.

### 6.2.5 The algebraic expanders involved in the construction

In our construction we employed algebraic expanders with different parameters. In Section 6.2.2 we used a series of algebraic expanders with parameters

$$ (N_0, d, 1/2), (N_1 = N_0 \cdot 2^{D(\epsilon)}, d, 1/2), \dots, (N_s = N_0 \cdot 2^{sD(\epsilon)}, d, 1/2) $$

for some constants $d$ and $s$. In Section 6.2.3 we used another algebraic expanders with parameters $(n_s, d, \lambda)$ for a small enough $\lambda$ and a suitable $d$. The required algebraic expanders can be constructed explicitly, for example, by using the recursive schemes based on the zig-zag product, see [13]. This observation concludes the proof of Theorem 6.4.

## 7 Conclusion

In the prolific paper [7], Cook and Reckhow proposed a very general definition of a *proof system*. The OBDD($\wedge$) and OBDD($\wedge$, reordering) studied in this paper are two specific examples of proof systems. Indeed, it is enough to observe that the following three properties are satisfied for these OBDDs:

1. There is a polynomial-time algorithm that verifies whether a function represented by an OBDD is satisfiable.

2. Let $D_1, D_2, D_3$ be some OBDDs in the same order. It is possible to check whether $D_1 = D_2 \wedge D_3$ in polynomial time.

3. There is a polynomial-time algorithm that verifies whether an OBDD $D_1$ in an order $\pi_1$ and an OBDD $D_2$ in an order $\pi_2$ represent the same function.

From Properties 1–3 it easily follows that the OBDD($\wedge$) and OBDD($\wedge$, reordering) are proof systems by Cook and Reckhow.

We believe that our techniques can be applied in a more general setting and extended to some other proof systems, with possibly other data structures representing the Boolean functions. More specifically, we argue that our techniques apply to the k-OBDDs. To outline this generalization, we survey our proofs and take inventory of the properties of the OBDD($\wedge$, reordering)s that were used in our argument. In our lower bounds we used the following property of the OBDDs:

4. If $f: \{0, 1\}^n \to \{0, 1\}$ is represented by a $\pi$-OBDD of size $S$, then for every partition $(\Pi_0, \Pi_1)$ of $[n]$ such that elements of $\Pi_0$ precede elements of $\Pi_1$ in the order $\pi$, the communication complexity of $f$ with respect to $(\Pi_0, \Pi_1)$ is $O(\log S)$.

These are essentially the only property of OBDD($\wedge$, reordering) used in Section 3. Indeed, a lower bounds on complexity OBDD($\wedge$, reordering) can be proven by the following argument:
* On the first step, we prove exponential lower bounds on the OBDD complexity of a satisfiable formula $\Phi$. Actually, in each case we prove a linear lower bound on the communication complexity of computing $\Phi$ with respect to every nearly balanced partition of the input.

* We focus on the last step of the derivation. This step is the conjunction of $F_1$ and $F_2$ in the same order $\pi$. We need to prove that at least one of $F_1$ and $F_2$ has exponential size. Both $F_1$ and $F_2$ are satisfiable, and they are conjunctions of different sets of clauses of the initial formula. We construct partial substitutions $\rho_1$ and $\rho_2$ with the same support such that the formula $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is isomorphic to $\Phi$. Then the communication complexity of computing $F_1|_{\rho_1} \wedge F_2|_{\rho_2}$ is linear with respect to any nearly balanced partition $\Pi$ consistent with $\pi$. Hence, the communication complexity of $F_1|_{\rho_1}$ or $F_2|_{\rho_2}$ with respect to $\Pi$ is linear. Thus, the communication complexity of either $F_1$ or $F_2$ with respect to $\pi$ is linear. Therefore, by Property 4 of OBDDs it follows that for the order $\pi$ either $F_1$ or $F_2$ has exponential size.

Thus, only Property 4 is needed to prove a lower bound for OBDDs. It is known that $k$-OBDDs enjoy Properties 1-3 and Property 4 as well (see for example [24]). Therefore, our lower bounds and separations proven (for $\text{OBDD}(\wedge)$ and $\text{OBDD}(\wedge, \text{reordering})$) in Section 3, equally apply to the proof systems based on $k$-OBDDs.

In Section 4, we constructed a family of formulas that have short $\text{OBDD}(\wedge, \text{reordering})$ proofs but all the $\text{OBDD}(\wedge)$ proofs of them have exponential size. And again, to get the lower bound, we used only Property 4 of OBDDs. So this lower bound holds for $k$-OBDD($\wedge$) as well.

Finally, in Section 5, we proved that while an $\text{OBDD}(\wedge, \exists, \text{reordering})$ algorithm processes a formula, at some moment it comes to a diagram $D$ that computes a function with a linear communication complexity. By Property 4, this implies an exponential lower bound on the size of $D$. Therefore, the proven lower bound holds also for the $k$-OBDD($\wedge, \exists, \text{reordering}$) algorithms.

## 7.1 Further research

The major open problem is to prove superpolynomial lower bounds for $\text{OBDD}(\wedge, \text{weakening}, \text{reordering})$ proofs.

Recently Buss et al. [4] established an exponential separation between $\text{OBDD}(\wedge, \text{weakening}, \text{reordering})$ and $\text{OBDD}(\wedge, \text{weakening})$ proof systems. Tseitin formulas based on expanders are easy for $\text{OBDD}(\wedge, \text{weakening})$, but by Theorem 3.14 they are hard for $\text{OBDD}(\wedge, \text{reordering})$. The paper [4] presented a family of formulas such that their shortest $\text{OBDD}(\wedge, \text{weakening})$ proof is *superpolynomially* larger than every $\text{OBDD}(\wedge, \text{reordering})$ proof of these formulas; it would be interesting to to strengthen this result and establish an *exponential* separation.

**Acknowledgements.** The authors are grateful to Sam Buss for fruitful discussions and to the anonymous reviewers for useful comments.

The research presented in Sections 3, 4, and 5 was supported by Russian Science Foundation (project 16-11-10123). The work of the third author on the research presented in Section 6 was partially supported by RFBR grant 16-01-00362.

## References

[1] Noga Alon and Fan R. K. Chung. Explicit construction of linear sized tolerant networks. *Discrete Mathematics*, 306(10-11):1068–1071, 2006.

[2] Albert Atserias, Phokion G. Pg Kolaitis, and Moshe Y Vardi. Constraint propagation as a proof system. In Mark Wallace, editor, *Principles and Practice of Constraint Programming - CP 2004*, volume 3258 of *Lecture Notes in Computer Science*, pages 77–91. Springer, 2004.
[3] Paul Beame, Toniann Pitassi, and Nathan Segerlind. Lower bounds for Lovász–Schrijver systems and beyond follow from multiparty communication complexity. *SIAM J. Comput.*, 37(3):845–869, 2007.

[4] Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering rule makes OBDD proof systems stronger. In *33rd Computational Complexity Conference, CCC 2018, June 22-24, 2018, San Diego, CA, USA*, pages 16:1–16:24, 2018.

[5] J Cheeger. A lower bound for the smallest eigenvalue of the laplacian. *Problems Anal.*, page 195, 1970.

[6] Wěi Chén and Wenhui Zhang. A direct construction of polynomial-size OBDD proof of pigeon hole problem. *Information Processing Letters*, 109(10):472–477, 2009.

[7] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. *The Journal of Symbolic Logic*, 44(1):36–50, 1979.

[8] Pavol Duris, Juraj Hromkovic, Stasys Jukna, Martin Sauerhoff, and Georg Schnitger. On multi-partition communication complexity. *Inf. Comput.*, 194(1):49–75, 2004.

[9] Luke Friedman and Yixin Xu. Exponential lower bounds for refuting random formulas using ordered binary decision diagrams. In Andrei A Bulatov and Arseny M Shur, editors, *CSR 2013, volume 7913 of Lecture Notes in Computer Science*, pages 127–138. Springer, 2013.

[10] Robert G Gallager. Low-density parity-check codes. *Information Theory, IRE Transactions on*, 8(1):21–28, 1962.

[11] Jan Friso Groote and Hans Zantema. Resolution and binary decision diagrams cannot simulate each other polynomially. *Discrete Applied Mathematics*, 130(2):157–171, 2003.

[12] Venkatesan Guruswami. List decoding from erasures: bounds and code constructions. *Information Theory, IEEE Transactions on*, 49(11):2826–2833, 2003.

[13] Shlomo Hoory, Nathan Linial, and Avi Wigderson. Expander graphs and their applications. *Bulletin of the American Mathematical Society*, 43(4):439–561, 2006.

[14] Jan Krajíček. An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. *Journal of Symbolic Logic*, 73(1):227–237, 2008.

[15] Eyal Kushilevitz and Noam Nisan. *Communication complexity*. Cambridge University Press, 1997.

[16] A Lubotzky, R Phillips, and P Sarnak. Ramanujan graphs. *Combinatorica*, 8(3):261–277, 1988.

[17] Christoph Meinel and Anna Slobodova. On the complexity of constructing optimal ordered binary decision diagrams. *Proceedings of Mathematical Foundations of Computer Science*, 841:515–524, 1994.

[18] Christoph Meinel and Thorsten Theobald. *Algorithms and data structures in VLSI design: OBDD - foundations and applications*. Springer, 1998.

[19] Guoqiang Pan and Moshe Y. Vardi. Search vs. symbolic techniques in satisfiability solving. *7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, Revised Selected Papers*, 3542:235–250, 2005.

[20] Nathan Segerlind. Nearly-exponential size lower bounds for symbolic quantifier elimination algorithms and OBDD-based proofs of unsatisfiability. *CoRR*, abs/cs/0704.40, 2007.

[21] Nathan Segerlind. On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs. *Electronic Colloquium on Computation Complexity*, (126), 2007.
[22] Olga Tveretina, Carsten Sinz, and Hans Zantema. An exponential lower bound on OBDD refutations for pigeonhole formulas. *Proceedings Fourth Athens Colloquium on Algorithms and Complexity*, 4(Acac):13–21, 2009.

[23] Alasdair Urquhart. Hard examples for resolution. JACM, 34(1):209–219, 1987.

[24] Ingo Wegener. *Branching Programs and Binary Decision Diagrams*. SIAM, 2000.

[25] Gillés Zémor. On expander codes. *IEEE Transactions on Information Theory*, 47(2):835–837, 2001.