Dmitry Itsykson

Alexander Knop
email: aaknop@gmail.com

Andrey Romashchenko
email: andrei.romashchenko@lirmm.fr

Dmitry Sokolov
email: dmitrits@pdmi.ras.ru

On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables *

Keywords: 1998 ACM Subject Classification F.2.2 [Nonnumerical Algorithms and Problems] Complexity of proof procedures, F.4.1 [Mathematical Logic] Proof Theory Proof complexity, OBDD, error-correcting codes, Tseitin formulas, expanders Digital Object Identifier 10.4230/LIPIcs.STACS.2017.43

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 to change the order in OBDDs. At first we consider a proof system OBDD(∧, reordering) that uses the conjunction (join) rule and the rule that allows to change the order. We exponentially separate this proof system from OBDD(∧)-proof system that uses only the conjunction rule. We prove two exponential lower bounds on the size of OBDD(∧, reordering)-refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD(∧)-proofs and the second one extends the result of Tveretina et al. from OBDD(∧) to OBDD(∧, 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(∧, ∃)-algorithms). We notice that there exists an OBDD(∧, ∃)-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 F 2 that are hard for OBDD(∧, ∃, reordering)-algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F 2 that correspond to some checksum matrices of error correcting codes.

Introduction

An ordered binary decision diagram (OBDD) is a way to represent Boolean functions [START_REF] Bryant | Symbolic manipulation of boolean functions using a graphical representation[END_REF]. A Boolean function is represented as a branching program with two sinks such that on every path from the source to a sink variables appear in the same order. This restriction on the order of variables allows to handle the diagrams (compute binary Boolean operations on diagrams, compute projections, or test satisfiability) very efficiently. Atserias, Kolaitis and Vardi [START_REF] Atserias | Constraint propagation as a proof system[END_REF] proposed an OBDD-based proof system. This system is meant to prove that a given CNF formula is unsatisfiable. For some order of variables π 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 [START_REF] Atserias | Constraint propagation as a proof system[END_REF] 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 Plane 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 [START_REF] Atserias | Constraint propagation as a proof system[END_REF], 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 exponential lower bounds are known for different versions of OBDD-proof systems. Segerlind [START_REF] Segerlind | Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability[END_REF] proved an exponential lower bound for the tree-like version of OBDD(∧, weakening)-proof system using the communication complexity technique proposed in [START_REF] Beame | Lower Bounds for Lovász-Schrijver Systems and Beyond Follow from Multiparty Communication Complexity[END_REF]. Krajíček [START_REF] Krajíček | An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams[END_REF] 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 [START_REF] Friso | Resolution and binary decision diagrams cannot simulate each other polynomially[END_REF] showed that Resolution does not simulate OBDD(∧). Tveretina, Sinz and Zantema [START_REF] Tveretina | An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas[END_REF] proved the lower bound 2 Ω(n) for the pigeonhole principle PHP n+1 n in the OBDD(∧)-proof system and proved that OBDD(∧) does not simulate Resolution. Friedman and Xu [START_REF] Friedman | Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams[END_REF] proved an exponential lower bound for the complexity of random unsatisfiable 3-CNF 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 [START_REF] Pan | Search vs. Symbolic Techniques in Satisfiability Solving[END_REF]. 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:

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

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

The lower bounds for the OBDD(∧, weakening)-proof systems mentioned above imply the same lower bounds for the OBDD(∧, ∃)-algorithms.

Pan and Vardi [START_REF] Pan | Search vs. Symbolic Techniques in Satisfiability Solving[END_REF] investigated some specific strategies and compared them with DPLL based SAT solvers and compared the strategies with 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 and DPLL based algorithms on many natural formulas.

One of these formulas was PHP n+1 n . The result of [START_REF] Chén | A direct construction of polynomial-size OBDD proof of pigeon hole problem[END_REF] implies that an OBDD(∧, ∃)-algorithm can solve PHP n+1 n in polynomial time in compare to OBDD(∧)-algorithms and DPLL based algorithms.

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. So it seems to be very restrictive to use the same order of variables in all OBDDs in the proof. Hence we propose to supply the proof system with a supplementary rule that dynamically reorders the variables in OBDDs.

In OBDD-proofs, the 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 indeed coNP-complete, see [START_REF] Meinel | Algorithms and Data Structures in VLSI Design: OBDD -Foundations and Applications[END_REF]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.

Our results

In Section 3 we consider the OBDD(∧, reordering)-proof system. We prove two exponential lower bounds for the size of a OBDD(∧, reordering)-derivation of the pigeonhole principle PHP n+1 n and Tseitin formulas based on constant-degree algebraic expanders. The lower bound for pigeonhole principle extends the result of Tveretina et al. [START_REF] Tveretina | An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas[END_REF] from OBDD(∧)-proofs to OBDD(∧, reordering)-proofs. (Besides, we believe that our argument is simpler than the proof in [START_REF] Tveretina | An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas[END_REF]). The result for Tseitin formulas, to the best of out knowledge, was not known even for the more restrictive OBDD(∧)-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 for simplicity 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 π. 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 from the initial formulas. The idea is to construct partial substitutions ρ 1 and ρ 2 with the same support such that the formula Hence, the size of either F 1 | ρ1 or F 2 | ρ2 is large for the order π. Thus, the size of either F 1 or F 2 is large for the order π. Though our method has limitations, it may be applied to not minimally unsatisfiable formulas as well. Roughly speaking, our proof requires that all minimally unsatisfiable subformulas of the formula have simple structures. For example, our proof for PHP n+1 n transfers to onto-FPHP n+1 n almost literally since the unique minimal unsatisfiable subformula of onto-FPHP n+1 n is exactly PHP n+1 n . We do not believe that the same technique applies to a random 3-XOR.

F 1 | ρ1 ∧ F 2 | ρ2 is isomorphic
In Section 4 we construct an example of a family of formulas that are easy for the OBDD(∧, reordering)-proof system but hard for the OBDD(∧)-proof system.

In Section 5 we study OBDD(∧, ∃, reordering)-algorithms. At first, we notice that there exists an OBDD(∧, ∃)-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 F 2 that are hard for OBDD(∧, ∃, reordering)-algorithms. More specifically, we describe a randomized construction of a family of satisfiable formulas F n on n variables in O( 1)-CNF such that every OBDD(∧, ∃, reordering)-algorithm runs at least 2 Ω(n) steps on F n .

The plan of the proof is as follows.

We prove that if C ⊆ {0, 1} n is the set of codewords of a list-decodable code that allows to correct 2 3 n of erasures, then every OBDD that represents the characteristic function of C (χ C ) has a big size (this size proves to be close to the number of all codewords in the code). Moreover, this property holds even for the projections of χ C onto any 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. [START_REF] Duris | On multi-partition communication complexity[END_REF]). Guruswami [START_REF] Guruswami | List decoding from erasures: bounds and code constructions[END_REF] showed that the codes with large enough minimal distance are erasure list-decodable but the opposite statement does not hold. We give a randomized construction of the required linear code. This construction is based on random checksum matrix. We use the codes of Gallager [START_REF] Robert | Low-density parity-check codes[END_REF] that contain O(1) ones per row. We prove that such a random code with a high probability enjoys the following expansion property: every 1 6 n columns of the matrix contain ones in almost all rows. We consider the execution of an OBDD(∧, ∃, reordering)-algorithm on a 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 n 6 times; 2. the projection rule is applied at least 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 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(∧, weakening)-proofs imply lower bounds for OBDD(∧, ∃)-algorithms. So, what is new in our results comparative to the lower bounds proven by Segerlind [17] and Krajíček [START_REF] Krajíček | An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams[END_REF]? 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 [17] and [START_REF] Krajíček | An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams[END_REF] seem to be rather artificial. Further, we prove the lower bound 2 Ω(n) for a formula with n variables, whereas the previously known lower bounds are of the type 2 n (for some < 1/5). Besides, we proposed a new technique that might be applicable for other classes of formulas.

Open problems

The first open problem is to prove a superpolynomial lower bound for the OBDD(∧, weakening, reordering)-proofs. The second open problem is to separate the OBDD(∧, weakening, reordering) and the OBDD(∧, weakening) proof systems.

Preliminaries

Ordered binary decision diagrams

An ordered binary decision diagram (OBDD) is a data structure that is used to represent Boolean function [START_REF] Bryant | Symbolic manipulation of boolean functions using a graphical representation[END_REF]. Let Γ = {x 1 , . 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 the vertex labeled by the constant; this constant is the value of the function.

Let π be a permutation of the set {1, . . . , n}. A π-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 π(i) can not appear before x π(j) if i > j. An ordered binary decision diagram (OBDD) is a π-ordered binary decision diagram for some permutation π. The size of an OBDD is the number of vertices in it.

OBDDs have the following nice property: for every order of variables every Boolean function has a unique minimal OBDD. For a given order π, the minimal OBDD of a function f may be constructed in polynomial time from any π-ordered BDD for the same f . There are also known polynomial-time algorithms that efficiently perform the operations of conjunction, negation, disjunction and projection (operation that maps diagram D computing Boolean function f (x, y 1 , . . . , y n ) to diagram D computing Boolean function ∃x f (x, y 1 , . . . , y n )) to π-ordered ODDs [START_REF] Meinel | On the complexity of Constructing Optimal Ordered Binary Decision Diagrams[END_REF]. There is an algorithm running in time polynomial in the size of the input and the output that gets as input a π-ordered diagram A, a permutation ρ and returns the minimal ρ-ordered diagram that represents the same function as A [START_REF] Meinel | On the complexity of Constructing Optimal Ordered Binary Decision Diagrams[END_REF].

OBDD-proofs

If F is a CNF formula, we say that the sequence D 1 , D 2 , . . . , D t is an OBDD-derivation of F if D t is an OBDD that represents the constant false function, and for all 1 ≤ i ≤ t, D i is an OBDD that represents a clause of F or can be obtained by one of the following inference rules:

1. (conjunction or join) D i is a π-ordered OBDD, that represents D k ∧ D l for 1 ≤ l, k < i,
where D k , D l have the same order π; 2. (weakening) there exists a j < i such that D j and D i have the same order π, and D j semantically implies D i , that is every assignment that satisfies D j also satisfies D i ; 3. (reordering) D i is an OBDD that is equivalent to an OBDD D j with j < i.

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 OBDD(∧)-proof system uses only the conjunction rule and hence we may assume that all OBDDs in a proof have the same order. We use the notation π-OBDD(∧)-proof if all diagrams in this proof have order π.

OBDD-algorithms for SAT

Pan and Vardi [START_REF] Pan | Search vs. Symbolic Techniques in Satisfiability Solving[END_REF] proposed for the Boolean satisfiability problem the following family of algorithms based on OBDDs and symbolic quantifier elimination.

The algorithm gets as an input a CNF formula F , it chooses some order π on the variables and creates a π-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: [START_REF] Pan | Search vs. Symbolic Techniques in Satisfiability Solving[END_REF]). After every step of the algorithm, the following invariant is mainteined: F is satisfiable if and only if C∈S C ∧ 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.

Error-correcting codes

By a code we mean a subset of binary strings with a fixed length. A code C ⊆ {0, 1} n has a relative distance δ if for any two codewords c 1 , c 2 ∈ C the Hamming distance between c 1 and c 2 is at least δn.

A linear code a set of all n-bits vectors x = (x 1 . . . x n ) from some linear subspace in F n 2 . 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 ≥ 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 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 , . . . , i s intersects some row j if at least one of the columns i 1 , . . . , i s intersects row j.

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

Theorem 1 ([9, Lemma 2]). If C is a code with relative distance δ, then for every > 0 the code C is ((2 -)δ, 2 )-erasure list-decodable.

3

Lower bounds for OBDD(∧, reordering)

Tseitin formulas

In this Section we prove an exponential lower bound on the size of OBDD(∧, reordering)proofs of Tseitin formulas.

A Tseitin formula T S G,c is based on an undirected graph G(V, E) with degree bounded by a constant d. Every edge e ∈ E has the corresponding propositional variable p e (in fact variables for loops are not used). There is a function c : V → {0, 1}, we call it the labelling function. For every vertex v ∈ V we write down a formula in CNF that encodes u∈V :(u,v)∈E,u =v p (u,v) ≡ c(v) (mod 2). The conjunction of the formulas described above is called a Tseitin formula. If v∈U c(v) = 1 for some connected component U ⊆ 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 v∈U c(v) = 0 for every connected component U , then the Tseitin formula is satisfiable ([19, Lemma 4.1]).

Note that if formulas T S G,c and T S G,c are satisfiable and c = c then T S G,c and T S G,c are different functions since any satisfying assignment of T S G,c can not satisfy T S G,c .

In the following, we denote the number of connected components of a graph G by G. Proof. Let us fix an order π of the variables of T S G,c (i.e. π 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 T S G,c results in 2 |V |-k different functions. It implies that the size of every OBDD representing T S G,c has at least 2 |V |-k vetices on the distance m from the source, since these substitutions correspond to paths in the OBDD with different endpoints.

Let c : V → {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 T S G,c gives as the resulting formula again a Tseitin formula -some formula T S G ,c+c , where G is a graph with vertices V and edges E \ 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 T S G ,c+c is satisfiable. The required properties of c can be described

43:8

On OBDD-Based Algorithms and Proof Systems That Change Order of Variables by a system of linear equations with variables c (v) for v ∈ V : for every connected component U of graph G with vertices V and edges E we put down the equation: v∈U c (v) = 0 (this subsystem states that c can be obtained by a substitution or in other words that T S G ,c is satisfiable) and for each connected component W of G we put down the equation: v∈W c(v) + c (v) = 0 (this subsystem corresponds to the satisfiability of T S G ,c+c ). The system has a solution since T S G,c is satisfiable. There are |V | variables and at most G + G ≤ k equations. Hence there is at least 2 |V |-k solutions. Different solutions corresponds to different satisfiable formulas T S G ,c+c and thus to different functions.

We will apply Theorem 2 to algebraic expanders. Definition 3. A graph G with vertices V and edges E is an (n, d, α)-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 αd.

It is well known that for all α > 0 and all large enough constants d there exists a family G n of (n, d, α)-algebraic expanders. There are explicit constructions such that G n can be constructed in poly(n) time [START_REF] Lubotzky | Ramanujan graphs[END_REF]. Also, it is known that a random d-regular graph is a good enough expander with high probability.

Theorem 4. Let G(V, E) be an (n, d, α)-algebraic expander for α < 1 2 . Then for any

E ⊆ E if |E | = n 4d , then G + G ≤ n(1 -) + 2,
where G is a graph with vertices V and edges E , G is a graph with vertices V and edges E \ E and =

1 8d(αd+1) -1 d 2 . Note that > 0 if α < 1/32 and d ≥ 4. Corollary 5. If graph G is an (n, d, α)-algebraic expander for α < 1
32 and d ≥ 4, and a Tseitin formula T S G,c is satisfiable, then the size of any OBDD for T S G,c is 2 Ω(n) .

Proof. Follows from Theorems 2 and 4. Theorem 6. Let G be an (n, d, α)-algebraic expander with d ≥ 50, α < 1 32 . Then any OBDD(∧, reordering)-proof of any unsatisfiable Tseitin formula T S G,c has the size at least 2 Ω(n) . Sketch of the Proof. We consider the last step of the 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 T S G,c . We use 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 4 changes by at most o(n).

Note that F 1 and F 2 together contains all clauses of T S 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 ρ 1 and ρ 2 that are defined on edges adjacent with u and v and on the edges of the shortest path p between u and v. The substitutions ρ 1 and ρ 2 assign opposite values to edges from the path p and are consistent on all other edges. The substitution ρ 1 satisfies C v and refutes C u and ρ 2 satisfies C u and refutes C v .

By the construction F 1 | ρ1 ∧ F 2 | ρ2 is the 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 difference of the underlying graph from the expander is at most o(n). (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.

Pigeonhole principle

Let m and n be integers and p i,j be different variables; p i,j states whether the ith pigeon is in the jth hole or not. A formula PHP m n has two types of clauses. Clauses of the first type (long clauses) states that every pigeon is in at least one hole:

OBDD(∧, reordering) is stronger than OBDD(∧)

In this section we give an example of a family of unsatisfiable formulas Φ n that have OBDD(∧, reordering)-proofs of polynomial size while all OBDD(∧)-proofs have size at least 2 Ω(n) .

Theorem 8. Let Ψ n (x 1 , x 2 , . . . , x n ) be a family of unsatisfiable formulas of size poly(n) that satisfies the following conditions:

there exists an order τ such that Ψ n has τ -OBDD(∧) refutation of the size poly(n); there exists a polynomial p(n), a function k : N → N with k(n) ≤ log p(n) and permutations σ 1 , σ 2 , . . . , σ 2 k(n) ∈Sn such that for any permutation π ∈ S n there exists i ∈ [2 k(n) ] such that any πσ i -OBDD(∧)-proof of Ψ n has the size at least 2 Ω(n) . Then the formula

Φ n (w 1 , w 2 , . . . , w k , x 1 , x 2 , . . . , x n ) = 2 k(n) i=1 (w = i -1) → Ψ(x σi(1) , x σi(2) , . . . , x σi(n) )
has an OBDD(∧, reordering)-proof of the size poly(n), but any OBDD(∧)-proof has the size at least 2 Ω(n) . Here the equality w = i-1 means that w 1 w 2 . . . w k(n) is a binary representation of the integer i -1. We assume that Φ n is written in CNF as follows: we add a clause ¬(w = i -1) to every clause of Ψ(x σi(1) , x σi(2) , . . . , x σi(n) ).

The similar construction was used by Segerlind [17] in order to show that tree-like OBDD(∧, weakening) does not sumulate Resolution.

Sketch of the Proof. The lower bound. Consider an OBDD(∧)-proof T of the formula Φ n , let τ be the order of the variables x 1 , x 2 , . . . , x n that is induced by the order from T . By the statement of the theorem, there exists 1 ≤ i ≤ 2 k such that all (τ σ i )-OBDD(∧)-proofs of Ψ have at least exponential size. We make a substitution w = i -1 to the proof T . This substitution converts the proof of Φ n into a proof of Ψ n with the order τ σ i . Hence, T has an exponential size.

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

S TA C S 2 0 1 7

43:10

On OBDD-Based Algorithms and Proof Systems That Change Order of Variables Now we construct a family of unsatisfiable formulas Ψ n that satisfies the conditions of Theorem 8. We use an argument similar to the proofs of the lower bounds for OBDD(∧, reordering)proofs. At first, we construct a function that has the sizes of OBDD representations in different orders close to the required sizes of proofs for Ψ n .

Let EQ n : {0, 1} 2n → {0, 1} be the equality predicate on pairs of n-bits strings. We denote it EQ n (x 1 , x 2 , . . . , x n , y 1 , . . . , y n ); in this notation the value of EQ n is true iff x 1 x 2 . . . x n = y 1 y 2 . . . y n . Proposition 9. In the order x 1 , y 1 , x 2 , y 2 , . . . , x n , y n the function EQ n has an OBDD representation of the size 3n + 2.

Proof. The proof can be easily done by induction, using the following equation: EQ n (x 1 , x 2 , . . . , x n , y 1 , . . . , y n ) = (x 1 = y 1 ) ∧ EQ n-1 (x 2 , . . . , x n , y 2 , . . . , y n ).

The proof of the following lemma is similar to the proof of the Ω(n) lower bound on the best communication complexity of the shifted equality function [START_REF] Kushilevitz | Communication complexity[END_REF]Example 7.9]. Lemma 10. Let σ i for i ∈ [n] be a cyclic permutation of the variables y that maps y j to y i+j mod n+1 for any j ∈ [n]. Formally σ i (j) = j for j ∈ [n] and σ i (n + j) = n + (i + j -1 mod n) + 1 for j ∈ [n]. Then for any order π on 2n variables there exists i ∈ [n] such that every πσ i -OBDD representation of EQ n has the size at least 2 Ω(n) . Now we are ready to construct a formula that may be used in Theorem 8. Consider a formula Ψ 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 ∈ [n]; z 0 ; (x i = y i ) → (z i-1 → z i ) for all i ∈ [n]; ¬z n . Note that Ψ 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 11. Ψ n has a OBDD(∧)-proof of polynomial size in the order z 0 , x 1 , y 1 , z 1 , x 2 , y 2 , z 2 , . . . , x n , y n , z n . Lemma 12. For any order π on the variables x, y, z the size of a π-OBDD(∧)-proof of Ψ n is at least 1

10

√

S, where S is the size of the shortest π -OBDD representation of EQ n (x, y), where π is the order induced by π on the variables x, y. Theorem 13. There exists an unsatisfiable CNF formula Φ n of size poly(n) such that there exists a polynomial size OBDD(∧, reordering)-proof of Φ n but every OBDD(∧)-proof of Φ n has the size 2 Ω(n) . Proof. By Lemma 12 for every order π a size of π-OBDD(∧)-proof of Ψ n is at least 1 10 √ S, where S is the size of the shortest π -OBDD representation of EQ n and π is the order induced by π. By Lemma 10 there exists a family of permutations σ i of [2n] for i ∈ [n] such that for every order τ there exists an i ∈ [n] such that the size of any τ σ i -OBDD(∧)-proof of Ψ n is at least 2 Ω(n) . By Proposition 11 there exists a required order τ and a τ -OBDD(∧)-proof of Ψ n of size poly(n). Theorem 8 gives a construction of the desired formula Φ n .

OBDD(∧, ∃, reordering)-algorithms

It is known that OBDD(∧, ∃)-algorithms can prove PHP n+1 n in polynomial time [START_REF] Chén | A direct construction of polynomial-size OBDD proof of pigeon hole problem[END_REF]. Now we show that the Tseitin formulas are also easy for OBDD(∧, ∃)-algorithms.

  to the satisfiable formula from the first step. Then any OBDD representation of F 1 | ρ1 ∧ F 2 | ρ2 has exponential size. Algorithms and Proof Systems That Change Order of Variables

1 .

 1 (join or conjunction) delete some clause C from S and replace D by a π-ordered BDD that represents the conjunction D ∧ C; 2. (projection) choose a variable x that has no occurrences in the clauses from S and replace D by a π-ordered BDD for the function ∃x D; 3. (reordering) choose a new order on variables π and replace D by the equivalent π -ordered diagram. Assign π := π . (Note that Pan and Vardi did not consider this rule in

Theorem 2 .

 2 Let graph G with vertices V and edges E have the following property: for some m ∈ [|E|] and k > 0 for all subsets E ⊆ E of the size m the inequality G + G ≤ k holds, where G and G are graphs with vertices V and edges E and E \ E respectively. If T S G,c is satisfiable then any OBDD for T S G,c has at least 2 |V |-k vetices on the distance m from the source.

nTheorem 7 .

 7 j=1 p i,j for all i ∈ [m].Clauses of the second type (short clauses) states that in every hole there is at most one pigeon: ¬p i,k ∨ ¬p j,k for all k ∈ [n] and all i = j ∈ [m]. Any OBDD(∧, reordering)-proof of the pigeonhole principle formula PHP n+1 n has size at least 2 Ω(n) .

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. † On leave from IITP RAS.

Proposition 14. There exists an OBDD(∧, ∃)-algorithm that solves Tseitin formulas in polynomial time.

Sketch of the Proof. 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. Now we show that there are satisfiable linear systems over F 2 that are hard for OBDD (∧, ∃, reordering). At first we notice that every OBDD for a characteristic function of a good enough code has at least exponential size.

Lemma 16.

Let A be an m × n checksum matrix of a (ρ, 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 (ρ, 2 r L)-erasure list-decodable code.

Theorem 17. Let C ⊆ {0, 1} n be a linear code with relative distance 1 3 such that the checksum matrix H of the code C has the following properties:

H has size αn × n, where α ∈ (0; 1) is a constant; every row of H contains at most t(n) ones, where t is some function; every 1 6 n columns of H intersect (contains ones in) at least (α -δ)n rows, where δ ∈ (0, 1-α 2 ) is a constant. Let the formula F n be the standard representation of H(x) = 0 as a t-CNF of size at most αn2 t(n)-1 t(n) (every equation is represented in a straightforward way, without any additional variables). Then every OBDD(∧, ∃, reordering)-algorithm runs on the formula F n for at least 2 Ω(n) steps.

Proof. The code C has the relative distance 1 3 . Hence, C is ( 712 , 8)-erasure list-decodable by Theorem 1, choosing = 1 4 . We consider the execution of an OBDD(∧, ∃)-algorithm on the formula F n . We prove that at some moment size of a diagram D will be at least 2 Ω(n) . Assume that the algorithm during its execution applies the projection operation at least k = 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 ∃y 1 , . . . , y k φ(x 1 , . . . , x n-k , y 1 , . . . , y k ), where φ 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 the linear equations with the variable x must be among clauses of φ. By the assumption of the theorem any k columns of H have ones in at least (α -δ)n rows. Thus, φ contains all clauses from the representation of (α -δ)n equations and possibly several other clauses from other equations.

Lemma 16 implies that φ is a characteristic function of a ( 7 12 , 8 • 2 δn )-erasure list-decodable code. The number of satisfying assignments of φ is at least the number of solutions of the system Hx = 0, hence size of the code defined by φ is at least 2 (1-α)n . By Theorem 15 size of every OBDD for ∃y 1 , . . . , y k φ(x 1 , . . . , x n-k , y 1 , . . . , y k ) is at least 2 (1-α)n 2 -2δn 1 16 > 2 (1-α-2δ)n-4 for every order of variables.

If the algorithm applies the projection operations less than 1 6 n times, the argument is similar; we just need to consider the last diagram D.

S TA C S 2 0 1 7

43:12 On OBDD-Based Algorithms and Proof Systems That Change Order of Variables

In the next section, we will show that there exist linear codes matching the requirements of Theorem 17. These constructions together with Theorem 17 imply the following result: Corollary 18. For all large enough n there exists a CNF formula of size O(n) with n Boolean variables, such that every OBDD(∧, ∃, reordering)-algorithm runs on this formula at least 2 Ω(n) steps.

Code construction

In this section, we use Low Density Parity Codes (LDPC) of Gallager [START_REF] Robert | Low-density parity-check codes[END_REF] with quite standard parameters (a constant number of ones in each row and in each column of the checksums matrix). We supplement the usual definition of LDPCs with a rather nonconventional property of uniformity. In what follows we prove that most random Gallager's codes with suitably chosen parameters enjoy this property.

First of all we recall the classic construction of random LDPC from [START_REF] Robert | Low-density parity-check codes[END_REF]. Let us fix some integer parameters t, r, and n (assuming that t divides n). Define the "basic" matrix A of size (n/t) × n as a concatenation of t copies of the identity matrix (n/t) × (n/t).

Notice that each column of A contains one non-zero element; in each row of A there are exactly t non-zero elements. Further, we consider the family of all matrices H of size (rn/t) × n that consist of r horizontal "blocks" of size (n/t) × n, where each block is obtained as a permutation of columns of A. It is easy to see that in each column of this matrix there are r ones, and in each row there are exactly t ones. We introduce the uniform distribution on all matrices of this type. We can interpret these matrices H as checksums matrices of some linear codes. Gallager proved that most of these codes have rather large minimal distance.

Proposition 19 (see [START_REF] Robert | Low-density parity-check codes[END_REF]). 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 δ ∈ (0, 1 2 ) and for every t there exists r = r(t) such that for large enough n most matrices from the defined family have the minimal distance ≥ δn. Moreover, the ratio r(t)/t approaches h(2δ) 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δ) (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 (δ, t, n) (assuming that the value r = r(δ, t, n) is defined implicitly as the minimal integer such that most codes of the family have the minimal distance greater than δn). Now we can state the main technical lemma of this section.

Lemma 20. For all β ∈ (0, 1), γ < 1, and δ ∈ (0, 1 2 ), for all large enough t most (say, at least 90%) of linear codes from Gallager's family with parameters (δ, t, n) satisfy the following property: every βn columns in the checksum matrix of the code intersect at least a fraction γ of all rows of the matrix.

Corollary 21. 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 Corollary 18 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(∧, ∃, reordering)algorithm runs on this formula at least 2 Ω(N ) steps.