On Tseitin Formulas, Read-Once Branching Programs and Treewidth

Abstract

We show that any nondeterministic read-once branching program that decides a satisfiable Tseitin formula based on an n × n grid graph has size at least 2^Ω(n). Then using the Excluded Grid Theorem by Robertson and Seymour we show that for an arbitrary graph G(V, E) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on G has size at least $2^{\Omega (\text {tw}(G)^{\delta })}$ for all δ < 1/36, where tw(G) is the treewidth of G (for planar graphs and some other classes of graphs the statement holds for δ = 1). We apply the mentioned results to the analysis of the complexity of derivations in the proof system OBDD(∧,reordering) and show that any OBDD(∧,reordering)-refutation of an unsatisfiable Tseitin formula based on a graph G has size at least $2^{\Omega (\text {tw}(G)^{\delta })}$. We also show an upper bound O(|E|2^pw(G)) on the size of OBDD representations of a satisfiable Tseitin formula based on G and an upper bound $O(|E||V| 2^{\text {pw}(G)}+|\text {TS}_{G,c}|^{2})$ on the size of OBDD(∧)-refutation of an unsatisifable Tseitin formula TS_{G, c}, where pw(G) is the pathwidth of G.

1 Introduction

This paper continues the study of representation of satisfiable Tseitin formulas by read-once branching programs.

A Tseitin formula TS_{G, c} [21] is defined for every undirected graph G(V, E) and a labeling function c : V →{0,1}. We introduce a propositional variable for every edge of G. The Tseitin formula TS_{G, c} represents a linear system over the field GF(2) that for every vertex v ∈ V states that the sum of all edges adjacent to v equals c(v). It is well known that a Tseitin formula is satisfiable if and only if the sum of values of the labeling function for all vertices in every connected component is even [22].

In 2017 Itsykson et al. [14] showed that any OBDD representing satisfiable Tseitin formulas based on d-regular expanders on n vertices has size at least 2^Ω(n). Then Glinskih and Itsykson [10] extended this lower bound to nondeterministic read-once branching programs (1-NBP).

In this paper we consider an n × n grid and study the complexity of representation of Tseitin formulas based on it by read-once branching programs. In Theorem 3.1 we prove that any 1-NBP computing a satisfiable Tseitin formula based on an n × n grid has size 2^Ω(n). Although an n × n grid graph has some edge-expansion properties, we could not prove the lower bound based only on these properties; our proof requires careful analysis and we use the geometric properties of the grid.

As an important corollary we establish a connection between the complexity of 1-NBP representation of a satisfiable Tseitin formula and the treewidth of the underlying graph. The treewidth is one of the most important structural measures of a graph and it is one of the main parametrizations for computational graph problems. Theorem 4.1 states that any 1-NBP computing a satisfiable Tseitin formula TS_{G, c} has size at least $2^{\Omega (\text {tw}(G)^{\delta })}$ for all δ < 1/36, where tw(G) denotes the treewidth of the graph G. The proof is based on the Excluded Grid Theorem by Robertson and Seymour [20]: there is a function g such that if a graph G has the treewidth at least g(t), then G contains a grid of size t × t as a minor. Recent results of Chekuri and Chuzhoy [4] and [5] give a polynomial upper bound on the function g. Hence we know that every graph G has a t × t grid as a minor, where t = Ω(tw(G)^δ) for all δ < 1/36. For several classes of graphs it is possible to improve the value of δ, for example, for planar graphs δ = 1 [12, 19]. Thus Theorem 4.1 is followed by Lemma 4.3 stating that if H is a minor of G, then for every S and for every 1-NBP of size S that computes a satisfiable Tseitin formula TS_{G, c} there is an 1-NBP that computes a satisfiable Tseitin formula $\text {TS}_{H,c^{\prime }}$ of size at most S. This lemma is proved separately for every operation: an edge deletion, a vertex deletion and an edge contraction. We use the non-determinism in the case of an edge contraction: we replace nodes labelled with contracted edges by guessing nodes.

In Theorem 6.1 we show that for every satisfiable Tseitin formula based on a graph G(V, E) has an OBDD of size O(|E|2^pw(G)), where pw(G) is the pathwidth of G (note that the pathwidth differs from the treewidth by at most a logarithmic factor: $\text {tw}(G)\le \text {pw}(G)\le O(\text {tw}(G) \log |V|)$). Since the pathwidth of an n × n grid is O(n), our upper and lower bounds for grids match up to a constant in the exponent.

There are several known approaches to defining the treewidth of CNF formulas. Ferrara, Pan and Vardi [7] considered a graph on variables of a CNF formula where two variables are connected iff they share a common clause. They proved that if a graph associated with CNF formula has the treewidth t, then the formula has an OBDD of size n^O(t) (it is very similar to Theorem 6.1 but it uses another notion of the treewidth). Razgon [18] showed that this bound is tight and there is a family of CNF formulas with the treewidth at most k that requires 1-NBP of size n^Ω(k). In the case of a Tseitin formula TS_{G, c}, the associated graph is the edge-graph of G, where the vertices are the edges of G and two edges are connected iff they are incident to the same vertex of G. For example, if G is a star on n + 1 vertices (a star is a tree and, hence, it has the treewidth 1), then the edge-graph is the complete graph K_n− 1 and it has the treewidth n − 2.

Applications to proof complexity

The interest of the study of Tseitin formulas comes from the propositional proof complexity; unsatisfiable Tseitin formulas are one of the basic examples of hard formulas for many proof systems.

The study of representations of satisfiable Tseitin formulas by read-once branching program was motivated by the study of proof systems based on OBDDs introduced by Atserias, Kolaitis and Vardi [2]. Itsykson et al. [14] studied the proof system OBDD(∧,reordering); a proof of unsatisfiability of a CNF formula φ in this proof system is a sequence of OBDDs: $D_{1}, D_{2}, \dots , D_{s}$ such that D_s is a constant false OBDD and for all i ∈ [s], D_i either represents a clause of φ, or represents the conjunction of D_k ∧ D_ℓ, where k, ℓ < i and D_i, D_k and D_ℓ use the same order, or represents the same function as D_ℓ but using another order, where ℓ < i. The paper [14] gives an exponential lower bound on size of OBDD(∧,reordering)-refutations of unsatisfiable Tseitin formulas based on constant degree expanders. The lower bound proof is organized as follows: for any refutation of Tseitin formula TS_{G, c} of size S it is possible to construct an OBDD of size at most S² representing a satisfiable Tseitin formula $\text {TS}_{G^{\prime },c^{\prime }}$, where $G^{\prime }$ is a graph obtained from G by the deletion of several edges. Thus it is sufficient to prove lower bound on the size of OBDD representation of $\text {TS}_{G^{\prime },c^{\prime }}$. We adapt this approach and show in Theorem 5.3 that our results imply that any OBDD(∧,reordering)-refutation of an unsatisfiable Tseitin formula TS_{G, c} has size at least $2^{\Omega (\text {tw}(G)^{\delta })}$, where δ is a constant as above. In particular we get a lower bound 2^Ω(n) on the complexity of OBDD(∧,reordering)-refutations of Tseitin formulas based on the n × n grid.

In Corollary 6.3 we show that every unsatisfiable Tseitin formula based on a graph G(V, E) has an OBDD(∧)-refutation of size $O(|E||V| 2^{\text {pw}(G)}+|\text {TS}_{G,c}|^{2})$, where OBDD(∧) is a subsystem of OBDD(∧,reordering) that do not use the reoredering rule.

The recent paper by Buss et al. [3] shows that OBDD(∧) cannot be polynomially simulated by Resolution and even by Cutting Planes. The paper shows that any Resolution proof of Tseitin formula based on the complete graph on $\log n$ vertices $K_{\log n}$ has size at least $2^{\Omega (\log ^{2} n)}$, while it has an OBDD(∧)-refutation of polynomial size. It is well known that the size of the shortest regular Resolution proof of any unsatisfiable CNF formula ϕ equals the size of the minimal read-once branching program for the following search problem Search_ϕ: given an assignment of variables of ϕ, find a clause that is refuted by this assignment [16, 17]. Our upper bound implies that a satisfiable $\text {TS}_{K_{\log n},c}$ can be computed by an OBDD of size poly(n). Thus we have that computing of $\text {Search}_{\text {TS}_{K_{\log n},c}}$ for an unsatisfiable $\text {TS}_{K_{\log n},c}$ is superpolynomially harder than computing of a satisfiable $\text {TS}_{K_{\log n},c^{\prime }}$ for read-once branching programs.

Tseitin formulas based on the grid graphs were studied in proof complexity. The first superpolynomial lower bound for regular resolution was proved for grid graphs in 1968 by Tseitin [21]. In 1987 Urquhart proved a lower bound for Tseitin formulas based on expanders in unrestricted Resolution [22] but tight lower bounds for grids were proved by Dantchev and Riis only in 2001 [6]. In the recent paper [13] Håstad proved lower bound on Bounded depth Frege refutations for Tseitin formulas based on n × n grid graphs that implies that polynomial size Frege proofs of such formulas should use formulas with almost logarithmic depth.

The treewidth was also studied in the context of resolution refutations of Tseitin formulas. Alekhnovich and Razborov [1] considered a hypergraph that corresponds to every CNF formula, where variables are vertices and clauses as sets of variables form hyperedges. For Tseitin formulas the branch-width of this hypergraph is up to a constant factor equal to the Resolution width [1]. For constant degree graphs the treewidth is equal to the branch-width of the hypergraph up to a multiplicative constant. Galesi, Talebanfard and Torán in the recent paper [9] consider cop-robber games on graphs that are very similar to games characterising the treewidth, they used such games in an analysis of the complexity parameters of resolution refutations of Tseitin formulas.

Galesi et al. [8] very recently extended Håstad argument for all graphs also using the Excluded Grid Theorem: there is a constant K such that any unsatisfiable TS_{G, c} requires proofs of size $2^{\text {tw}(G)^{\Omega (1/d)}}$ in depth-d Frege systems for $d<\frac {K \log n}{\log \log n}$. Furthermore, this result is tight up to a multiplicative constant in the top exponent: TS_{G, c} has a depth-d Frege proof of size $2^{\text {tw}(G)^{O(1/d)}} \text {poly}(|\text {TS}_{G,c}|)$ for all d. Together with our results it implies that complexities of derivation of Tseitin formulas in constant-depth Frege and in OBDD(∧,reordering) are quasi-polynomially related.

The short version of the paper was presented at CSR-2019 [11]. The full version in comparison to the short one contains proofs of Lemma 4.2, Theorem 5.3, Theorem 6.1 and the full proof of Theorem 5.1. The full version also contains an upper bound for the proof system OBDD(∧) (Corollary 6.3).

2 Preliminaries

Branching programs

A deterministic branching program (BP) is a form of representation of Boolean functions. A Boolean function $f(x_{1}, x_{2}, \dots , x_{n})$ is represented by a directed acyclic graph with exactly one source and two sinks. All nodes except sinks are labeled with a variable; every internal node has exactly two outgoing edges: one is labeled with 1 and the other is labeled with 0. One of the sinks is labeled with 1 and the other is labeled with 0. The value of the function for given values of variables is evaluated as follows: we start a path from the source such that for every node on its path we go along the edge that is labeled with the value of the corresponding variable. This path will end in a sink. The label of this sink is the value of the function.

A nondeterministic branching program (NBP) differs from a deterministic in the way that we also allow guessing nodes that are unlabeled and have two outgoing unlabeled edges. So nondeterministic branching program may have three types of nodes: guessing nodes, nodes labeled with a variable (we call them just labeled nodes) and two sinks; the source is either a guessing node or a labeled node. The result of a function represented by a nondeterministic branching program for given values of variables equals 1, if there exists at least one path from the source to the sink labeled with 1 such that for every node labeled with a variable on its path we go along an edge that is labeled with the value of the corresponding variable (for guessing nodes we are allowed to choose any of two outgoing edges). Note that deterministic branching programs constitute a special case of nondeterministic branching programs.

A deterministic or nondeterministic branching program is (syntactic) read-k (k-BP or k-NBP) if every path from the source to a sink contains at most k occurrences of each variable.

Let π be a permutation of the set $\{1, \dots , n\}$ (an order). A π-ordered binary decision diagram is a 1-BP such that on every path from the source to a sink 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 π.

Lemma 2.1 (Wegener 23)

Assume that Boolean functions f₁ and f₂ have π-ordered OBDDs of sizes k₁ and k₂ respectively, then 1) f₁ ∧ f₂ has a π-ordered OBDD of size at most k₁k₂; 2) for any partial assignment ρ, f₁|_ρ has a π-ordered OBDD of size at most k₁.

Tseitin formulas

Let G(V, E) be an undirected graph without loops but possibly with multiple edges, c : V →{0,1} be a labeling function that matches every vertex with a Boolean value. We associate every edge e ∈ E with a propositional variable x_e. A Tseitin formula TS_{G, c} based on a graph G and a labeling function c is the conjunction of the following parity conditions: for every vertex v the sum of variables x_e for all edges e that are incident to v equals c(v) modulo 2. More formally: $\bigwedge \limits _{v \in V}\left ({\sum \limits _{e\text { \scriptsize {is incident to} }v}{x_{e}}}=c(v) \bmod {2}\right )$.

Usually, Tseitin formulas are written in the CNF. If the maximal degree of a graph is upper bounded by a constant d, then a sum modulo 2 can be written as a d-CNF of size at most 2^d− 1, hence the size of CNF representation of TS_{G, c} is at most 2^d− 1|V |.

We will use the following criterion of the satisfiability of Tseitin formulas:

Lemma 2.2 (Urquhart 22)

A Tseitin formula TS_{G, c} is satisfiable if and only if for every connected component of the graph G the sum of values of the function c for all of the vertices is even. I.e., for every connected component U the following holds: $\sum \limits _{v \in U}{c(v)} = 0 \bmod 2$.

Remark 2.3

Note that an assignment of a value to a variable x_e := α transforms Tseitin formula TS_{G, c} to a Tseitin formula $\text {TS}_{G^{\prime },c^{\prime }}$, where graph $G^{\prime }$ is obtained from the graph G by deleting the edge e, $c^{\prime }$ equals c in every vertex except two vertices that are incident to edge e. On these two vertices the values of c and $c^{\prime }$ differ by α.

Lemma 2.4 (Glinskih and Itsykson 10, Lemma 2)

If a graph G(V, E) consists of k connected components, then a satisfiable Tseitin formula TS_{G, f} has exactly 2^{|E|−|V |+k} satisfying assignments.

Proof Proof sketch

Consider a spanning forest F(V, E_F) of G. F contains exactly |V |− k edges. Consider an arbitrary partial assignment of variables {x_e∣e ∈ E ∖ E_F}; this assignment can be uniquely extended to a satisfying assignment of TS_{G, f}. Hence, TS_{G, f} has exactly 2^{|E|−|V |+k} satisfying assignments. □

For a graph G(V, E) let k_G(l) be the maximal number of connected components that can be obtained from G by the deletion of l edges. The following lower bound on the size of 1-NBP for satisfiable Tseitin formula is known; we prove it for the sake of completeness.

Lemma 2.5 (Glinskih and Itsykson 10, Corollary 20)

For every connected graph G(V, E) and arbitrary 1 ≤ m ≤|E| any 1-NBP evaluating a satisfiable Tseitin formula TS_{G, c} has size at least $2^{|V|-k_{G}(m)-k_{G}(|E|-m)+1}$.

Proof

Let D be a minimal 1-NBP evaluating TS_{G, c}. Consider a node v of D. Since D is minimal, there exists a path p₁ from the source of D to v and a path p₂ from v to the 1-sink. Let ρ₁ and ρ₂ be partial assignments corresponding to p₁ and p₂. Let ρ₁ substitute values to l variables; since ρ₁ρ₂ satisfies TS_{G, c}, then ρ₂ substitute values to |E|− l variables. Remark 2.3 implies that the formula $\text {TS}_{G,c}|_{\rho _{2}}$ obtained from TS_{G, c} by the assignment ρ₂ is a Tseitin formula $\text {TS}_{G^{\prime \prime }, c^{\prime \prime }}$, where $G^{\prime \prime }$ can be obtained from G by removing |E|− l edges corresponding to ρ₂. The formula $\text {TS}_{G^{\prime \prime }, c^{\prime \prime }}$ is satisfiable since it is satisfied by ρ₁. Consider an arbitrary path q₁ from the source to v and denote the corresponding partial assignment by σ₁. Since the path q₁p₂ is accepting in D, then the assignment σ₁ρ₂ satisfies TS_{G, c}, hence σ₁ satisfies $\text {TS}_{G^{\prime \prime }, c^{\prime \prime }}$. Thus the number of different partial assignments corresponding to paths from the source to v is at most the number of satisfying assignments of $\text {TS}_{G^{\prime \prime }, c^{\prime \prime }}$; the latter equals $2^{l-|V|+\sharp G^{\prime \prime }}$ by Lemma 2.4, where ♯H denotes the number of connected components in the graph H. By the definition of k_G, $2^{l-|V|+\sharp G^{\prime \prime }}\le 2^{l-|V|+k_{G}(|E|-l)}$.

Similarly, Remark 2.3 implies that the formula $\text {TS}_{G,c}|_{\rho _{1}}$ is a Tseitin formula $\text {TS}_{G^{\prime }, c^{\prime }}$, where $G^{\prime }$ can be obtained from G by removing l edges corresponding ρ₁. And $\text {TS}_{G^{\prime }, c^{\prime }}$ is satisfiable since it is satisfied by ρ₂. Consider an arbitrary path q₂ from v to 1-sink and denote the corresponding partial assignment by σ₂. Since p₁q₂ is an accepting path in D, then ρ₁σ₂ satisfies TS_{G, c}, hence σ₂ satisfies $\text {TS}_{G^{\prime }, c^{\prime }}$. Thus, the number of different partial assignments corresponding to paths from v to 1-sink is at most the number of satisfying assignments of $\text {TS}_{G^{\prime }, c^{\prime }}$ that by Lemma 2.4 equals $2^{|E|-l-|V|+\sharp G^{\prime }}$ and does not exceed $2^{|E|-l-|V|+k_{G}(l)}$.

So we get that the number of different satisfying assignments of TS_{G, c} corresponding to accepting paths passing through v is at most $2^{|E|+k_{G}(|E|-l)+k_{G}(l)-2|V|}$.

Since G is connected, by Lemma 2.4, TS_{G, c} has exactly 2^{|E|−|V |+ 1} satisfying assignments. For every such assignment there is a corresponding accepting path in D. For every such accepting path p we mark a node v such that there are exactly m labelled edges between the source and v along p. We have shown above that every node was marked at most $2^{|E|+k_{G}(|E|-m)+k_{G}(m)-2|V|}$ times. Hence, there are at least $2^{|V|-k_{G}(|E|-m)-k_{G}(m)+1}$ different marked nodes in D. □

Lemma 2.6

Let G be an undirected graph, c and $c^{\prime }$ be such that Tseitin formulas TS_{G, c} and $\text {TS}_{G,c^{\prime }}$ are satisfiable. Then sizes of minimum-size 1-NBPs (1-BPs and OBDDs) for TS_{G, c} and $\text {TS}_{G,c^{\prime }}$ are equal.

Proof

We will show that the first Tseitin formula can be obtained from the second by the changing some variables by their negations and, hence a branching program for the first Tseitin formula can be obtained from a branching program for the second Tsetin formula just by changing labels of outgoing edges for some nodes. Consider one connected component U of G. By Lemma 2.2 for the both Tseitin formulas the sum of labels that correspond to this component is even: ${\sum }_{v\in U} c(u)={\sum }_{v\in U} c^{\prime }(u)=0$. Consider a set of vertices $U^{\prime }=\{v\in U\mid c(u)\neq c^{\prime }(u)\}$, the size of $U^{\prime }$ is even. Assume that $U=\{u_{1}, u_{2}, \dots , u_{2k}\}$. For every i ∈ [k] we consider a path from u_2i− 1 to u_2i and change signs to the opposite of variables corresponding to the edges of this path in the second Tseitin formula. Such operation for u_2i− 1 and u_2i corresponds to changing of the value of the labeling function in vertices u_2i− 1 and u_2i, labels for other vertices do not change since we change the signs for two edges. Applying this transformation for all connected components we transform the second Tseitin formula to the first. □

Treewidth, pathwidth and minors

A tree decomposition of an undirected graph G(V, E) is a tree T = (V_T, E_T) such that every vertex u ∈ V_T corresponds to a set $X_{u}\subseteq V$ and it satisfies the following properties: 1. The union of X_u for u ∈ V_T equals V. 2. For every edge (a, b) ∈ E there exists u ∈ V_T such that a, b ∈ X_u. 3. If a vertex a ∈ V is in the sets X_u and X_v for some u, v ∈ V_T, then it is also in X_w for all w on the path between u and v in T.

If a tree T is a path, then this representation is a path decomposition. The width of a tree decomposition is the maximum |X_u| for u ∈ V_T minus one. A treewidth of a graph G is the minimal value of the width among all tree decompositions of the graph G. We denote it as tw(G). The pathwidth of a graph G is the minimal value of the width among all path decompositions of a graph G. We denote it as pw(G).

Lemma 2.7 (Korach and Solel 15)

For every graph G on n vertices $\text {pw}(G)=O(\log (n) \cdot \text {tw}(G))$.

A minor of an undirected graph G is a graph that can be obtained from a graph G by a sequence of edge contractions, edge deletions and vertex deletions.

Theorem 2.8 (Chuzhoy 5)

For every constant δ < 1/36 every graph G contains a t × t grid as a minor, where t = Ω(tw(G)^δ).

3 Lower Bound for Grids

In this section we prove the following Theorem.

Theorem 3.1

Let T_n be an n × n grid graph. Then if a Tseitin formula $\text {TS}_{T_{n},c}$ is satisfiable, then every 1-NBP that computes $\text {TS}_{T_{n},c}$ has size at least 2^Ω(n).

Proof

Let us fix an orientation of the grid T_n such that all edges will be either horizontal or vertical. We assume that all vertices have coordinates such that horizontal coordinates increase from left to right and vertical coordinates increase from bottom to top.

T_n contains (n + 1)² vertices and 2n(n + 1) edges. In order to prove this theorem we use Lemma 2.5 for l = n(n + 1) (so l is the half of the number of edges). So we have to prove that if we delete half of the edges of T_n, then the resulting graph will have at most $\frac {(n+1)^{2}}{2} - \varepsilon \cdot n$ connected components for some constant ε > 0. Hence, by Lemma 2.5, every 1-NBP for $\text {TS}_{T_{n},c}$ has size at least 2^2εn+ 1.

We call a subgraph of T_n optimal if it contains l edges and has the maximal number of connected components. The plan of the proof is the following. At first we show that there exists an optimal subgraph H that has one connected component that contains all edges and all other connected components are isolated vertices. Then we estimate the number of connected components of H. □

Lemma 3.2

There is an optimal subgraph of T_n that has exactly one connected component with at least two vertices.

Proof

Consider all optimal subgraphs of T_n. Choose among them a subgraph H that contains a connected component M with the maximal number of edges. If M contains all edges of H, then the lemma is proved. Further we assume that not all edges are in M.

Consider the properties of the chosen graph H.

1. All the edges of the grid T_n between vertices of M are in M. Indeed, otherwise we can delete an edge from another connected component and add it to M. After this operation the number of connected components does not decrease, but the number of edges in M is strictly increased. This is a contradiction since M has the maximal number of edges among all the optimal subgraphs.

2. Every connected component, except M, is edge-biconnected (i.e. it is impossible to increase the number of connected components by the deletion of an edge from it). Indeed, assume that for some connected component except M it is possible to delete an edge from it such that the number of connected component increases. Then we delete this edge and add an edge of the grid that connects M with a vertex out of M. In this case the number of connected components is not changed but the number of edges in the maximal component would be increased. This is a contradiction.

3. There is no vertex v of T_n such that it is not in M but there are at least two edges between v and vertices of M in T_n. Proof by contradiction; assume that such a vertex exists. Consider a connected component K that differs from M and has edges. Let u be the leftmost vertex among the set of vertices in K with the minimal vertical coordinate. There are no edges going left or down from the vertex u in the graph H. Since the connected component K has edges, there is at least one edge that is incident to u. By the previous property, K is edge-biconnected, hence, u has precisely two incident edges. Let us delete two edges incident to u from K and add two edges that connect v and M. The number of connected components doesn’t decrease, but the number of edges in the maximal component increases. This is a contradiction.

4. Every 1 × 1 square of the grid T_n contains 0, 1 or 4 edges from M. A 1 × 1 square cannot contain exactly 3 edges because it contradicts the property 1. Let an 1 × 1 square contains exactly 2 edges from M. If these are two incident edges, then we get a contradiction with the property 3 or the property 1. If these are two opposite edges, then we get a contradiction with the property 1.

5. For every u, v ∈ M, the minimal rectangle of the grid that contains both u and v (with all interior edges) is a subgraph of M (one of the sides of the rectangle could be of zero length, in that case it is just a line of the grid). It can be easily shown by the induction on the length of the shortest path between u and v using the property 4.

6. M is a rectangle of the grid with all edges of this rectangle. Consider the maximal rectangle of the grid that is fully contained (with all edges) in M. If there are vertices in M that are not in this rectangle, then we could increase this rectangle using the property 5.

So M is a rectangle of the grid. We say that M can be moved one step to the left (right, down or up) if all left (right, down or up) neighbours of the left (right, down or up) border of M are isolated vertices in H. Such a move doesn’t change the number of connected components and the number of edges in them. Consider some connected component K that differs from M and contains edges. We move M one step closer to K in the way of decreasing the distance between them while it is possible. By the distance we understand the minimal L₁-distance between two vertices from M and K. After some step it is not possible anymore; it means that M has a neighbour v from another connected component that consist of more than one vertex. W.l.o.g. assume that v is above M.

Let M be a rectangle x × y, where x, y are non-negative integers. That means that every horizontal line of M contains x + 1 vertices. We call neighbours of M that are above M as upper neighbours of M. Assume that among upper neighbours of M there are m vertices that are in some connected component that consists of more than one vertex. Let these m vertices be in k connected components. Assume that there are r edges of the graph H between x + 1 upper neighbours of M (see an example on the left part of Fig. 1). Since every edge between upper neighbours of M decreases the number of connected components, the following inequality holds k ≤ m − r. Obviously, r ≤ x.

Fig. 1

Example: x = 6, y = 4, r = 3, k = 3, m = 7

Consider the following modification of the graph H: we move the rectangle M one step up and add edges down from r vertices on the bottom border of M (see example on the right part of Fig. 1). The number of edges after this transformation is not changed since r edges overlapped and we added r edges. Now we estimate the number of connected components. On the bottom border we add (x + 1) − r new connected components. On the upper border (x + 1) − m + k connected components disappeared (were merged to one). Finally, the number of connected components increased by m − k − r, that is at least zero since k ≤ m − r. But the number of edges in the maximal connected component increases, this contradicts the choice of the graph H. So we get a contradiction with the assumption that there are more than one connected components with at least one edge. □

So we may assume that there is an optimal graph H that has one connected component M with at least two vertices and t isolated vertices. Notice that M is not necessary a rectangle now (in Lemma 3.2 we only show that it has to be a rectangle under the assumption that the statement of the lemma is wrong). We are going to estimate $k_{T_{n}}(l)=t+1$ from the above.

For every connected component K we define a set of spines that go out of it. We assume that T_n is a part of the infinite grid. An edge e of the infinite grid is a spine of K if it connects a vertex u from K with a vertex out of K and u is the right or bottom endpoint of e (see Fig. 2). Note that spines can go outside of the square T_n if u is on the upper or left border of T_n. If a component is an isolated vertex, then it has exactly two spines.

Fig. 2

Spines

The same edge cannot be a spine for two different connected components since we choose only the edges that go up or to the left from the component. Let h be the total number of all spines for all of the connected components of H. Every spine is either an edge of the square T_n that is not in H or is among 2(n + 1) edges that go outside the square T_n. Hence, 2(n + 1) + n(n + 1) ≥ h.

Let X be the number of spines of the connected component M, then we get that h = 2t + X. Using the previous inequality we estimate t as follows: t ≤ (n + 1)(n + 2)/2 − X/2 = (n + 1)²/2 + (n + 1 − X)/2. Hence, we need to show that X ≥ (1 + 𝜖)n for some constant 𝜖.

Consider the minimal grid rectangle that contains M. Assume it has size (a − 1) × (b − 1), where a, b are natural numbers. Then there are spines of M in every of a vertical lines and in every of b horizontal lines. Then we get that $X\ge a+b \ge 2 \sqrt {ab}$. On the other hand, the component M contains exactly n(n + 1) edges, they need to be embedded into a rectangle (a − 1) × (b − 1) that contains a(b − 1) + b(a − 1) edges. Then we can estimate 2ab > a(b − 1) + b(a − 1) ≥ n(n + 1) and we get $X\ge \sqrt {2n(n+1)}>\sqrt {2} n$.

Using the upper bound on t, the number of connected components can be estimated as: $k_{T_{n}}(l)=t+1\le (n+1)^{2}/2 -(\sqrt {2}-1)n+\frac {3}{2}$. Then by Lemma 2.5, every 1-NBP for a satisfiable Tseitin formula $\text {TS}_{T_{n},c}$ has size at least $2^{2(\sqrt {2}-1)n-2}$.

4 Treewidth

The main goal of this section is to prove the following theorem.

Theorem 4.1

Let TS_{G, c} be a satisfiable Tseitin formula. Then every 1-NBP for TS_{G, c} has size at least $2^{\Omega \left (\text {tw}(G)^{\delta }\right )}$ for all δ < 1/36.

Lemma 4.2

Let D be a 1-NBP computing a Boolean function f : {0,1}ⁿ →{0,1}. If we change every node in D labeled with the variable x₁ by a guessing node and remove all labels of all its outgoing edges, then we obtain a valid 1-NBP that computes $\exists x_{1} f(x_{1}, x_{2},\dots , x_{n})$.

Proof

For every path from the source to a sink in $D^{\prime }$ every variable occurs at most once, so $D^{\prime }$ is a valid 1-NBP. Consider an assignment τ to the variables $x_{2},\dots , x_{n}$. Let us consider a path in $D^{\prime }$ from the source to the sink labeled with 1 that is consistent with τ. Consider the same path in D, it also finishes in the sink labeled with 1. Then there exists an assignment $\tau ^{\prime }$ that satisfies f and $\tau ^{\prime }$ extends τ on a value of the variable x₁. Now consider a satisfying assignment σ of the function $\exists x_{1} f(x_{1}, x_{2},\dots , x_{n})$. For some value of x₁ there exists a path from the source to the sink labeled with 1 in the branching program D that is consistent with this value and with σ. The copy of this path in the branching $D^{\prime }$ is consistent with σ and reaches the sink labeled with 1. □

Lemma 4.3

Let H be a minor of an undirected graph G and Tseitin formulas TS_{G, c} and $Ts_{H,c^{\prime }}$ be satisfiable. Then for every S and every 1-NBP of size S that computes TS_{G, c}, there is a 1-NBP that computes $\text {TS}_{H,c^{\prime }}$ of size at most S.

Proof

It suffices to prove the statement of the lemma for the case when H is obtained from G by the application of one operation. Let us consider all types of operations separately.

1. H is obtained from G by the deletion of an edge e. Let σ be a satisfying assignment of TS_{G, c}. We apply the partial assignment x_e := σ(x_e) to TS_{G, c} and get the satisfiable formula $\text {TS}_{H,c^{\prime \prime }}$. It is well known that the application of a substitution does not increase size of the 1-NBP. By Lemma 2.6, sizes of the minimal 1-NBPs for $\text {TS}_{H,c^{\prime \prime }}$ and $\text {TS}_{H,c^{\prime }}$ are equal.

2. H is obtained from G by the deletion of a vertex v. Since all the variables of Tseitin formulas are associated with edges, this case can be considered as a sequence of edge deletions.

3. A graph H(V_H, E_H) is obtained from a graph G(V, E) by the contraction of an edge e = (u, v). Let us define a labeling function $c^{\prime \prime }:V_{H}\to \{0,1\}$ as follows: for all the vertices that differ from the joined vertex {u, v} it has the same value as in the labeling function c and $c^{\prime \prime }(\{u,v\}) = (c(u)+c(v)) \bmod 2$. By the construction, every connected component U of H corresponds to a connected component $U^{\prime }$ of G with the same sum (over $\mathbb {F}_{2}$) of the labeling functions: ${\sum }_{w\in U}c^{\prime \prime }(w) = {\sum }_{w\in U^{\prime }} c(w)$. Hence, by Lemma 2.2, $\text {TS}_{H,c^{\prime \prime }}$ is satisfiable. □

Claim 4.3.1

Formulas $\text {TS}_{H, c^{\prime \prime }}$ and ∃x_eTS_{G, c} define the same function.

Proof

Formulas $\text {TS}_{H, c^{\prime \prime }}$ and ∃x_eTS_{G, c} depended on the same set of variables X = {x_l∣l ∈ E ∖{e}}, since H is obtained from G by the contraction of the edge e. Consider some assignment of these variables σ : X →{0,1}. Assume that σ satisfies $\text {TS}_{H, c^{\prime \prime }}$. Consider an assignment $\sigma ^{\prime }: X\cup \{x_{e}\}\to \{0,1\}$ such that for every x ∈ X, $\sigma ^{\prime }(x)=\sigma (x)$ and $\sigma ^{\prime }(x_{e})={\sum }_{t\in E_{u}}\sigma (x_{t})+c(u)\bmod 2$, where E_u is a set of edges that are incident to the vertex u in G except for the edge e. We need to check that $\sigma ^{\prime }$ satisfies TS_{G, c}. All conditions that are not related to vertices u and v are satisfied automatically, because they do not contain the edge e. The condition in the vertex u is satisfied because of the choice of the value of the variable x_e in $\sigma ^{\prime }$. Let E_v be a set of edges that are incident to the vertex v in G except for the edge e. To check the condition in the vertex v we should compute $\sigma ^{\prime }(x_{e})+{\sum }_{t\in E_{v}} \sigma (x_{t})$. By the definition of the value $\sigma ^{\prime }(x_{e})$ we get that the sum equals ${\sum }_{t\in E_{u}\cup E_{v}}\sigma (x_{t})+c(u)$ that is equal to c(v), because σ satisfies the condition in the vertex {u, v} in the formula $\text {TS}_{H,c^{\prime \prime }}$.

Now let σ be an assignment that satisfies ∃x_eTS_{G, c}. σ can be extended to an assignment $\sigma ^{\prime }$ that satisfies TS_{G, c}. Let us check that σ satisfies $\text {TS}_{H,c^{\prime \prime }}$. We should check the condition only for the vertex {u, v}: ${\sum }_{t\in E_{u}\cup E_{v}}\sigma (x_{t})=({\sum }_{t\in E_{u}}\sigma (x_{t})+\sigma ^{\prime }(x_{e}))+({\sum }_{t\in E_{v}}\sigma (x_{t})+\sigma ^{\prime }(x_{e}))=c(u)+c(v)$. □

By Lemma 4.2, the minimal size of a 1-NBP for ∃x_eTS_{G, c} (that is by Claim 4.3.1 equivalent to $\text {TS}_{H,c^{\prime \prime }}$) is at most the minimal size of a 1-NBP for TS_{G, c}. By Lemma 2.6, minimal sizes of 1-NBPs for $\text {TS}_{H,c^{\prime \prime }}$ and for $\text {TS}_{H,c^{\prime }}$ are equal.

Proof of Theorem 4.1

By Theorem 2.8, the graph G contains a t × t grid graph as a minor, where t = Ω(tw(G)^δ). The theorem follows from Theorem 3.1 and Lemma 4.3. □

5 Lower Bound in the Proof System OBDD(∧,reordering)

In this section we show that any refutation of an unsatisfiable Tseitin formula TS_{G, c} in the proof system OBDD(∧,reordering) has size at least $2^{\Omega \left (tw(G)^{\delta }\right )}$ for all δ < 1/36.

If F is a formula in CNF, we say that a sequence $D_{1}, D_{2}, \dots , D_{t}$ of OBDDs is an OBDD(∧,reordering)-refutation 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 from the previous D_j’s by one of the following inference rules: (conjunction or join) D_i is an OBDD with order π, that represents D_k ∧ D_l for 1 ≤ l, k < i, where D_k, D_l have the same order π; (reordering) D_i computes the same function as D_j with j < i (note that D_i and D_j may have different orders). The size of an OBDD(∧,reordering)-refutation is the total size of all OBDDs in it. An OBDD(∧)-refutation is a partial case of OBDD(∧,reordering)-refutation that do not use reordering rules.

We say that a graph H is t-good if H is connected and every OBDD-representation of any satisfiable Tseitin formula TS_{H, c} has size at least t. The following theorem can be proved using ideas from [14]:

Theorem 5.1

[cf. [14]] Let G(V, E) be a connected graph and degrees of all vertices of G be bounded by a constant. Assume that the graph G has the following properties: 1) if we delete any vertex from G, we get a t-good graph; 2) for every two vertices u and v of G there is a path p between them such that if we delete all vertices from p, we get a t-good graph. And if we delete from G vertices u and v and the edges of the path p, we also get a connected graph.

Then any OBDD(∧,reordering)-refutation of an unsatisfiable Tseitin formula TS_{G, c} has size at least ${\Omega }(\sqrt {t})$.

We start with the idea of the proof. We consider the last step of the OBDD(∧,reordering)-refutation: the conjunction of OBDDs F₁ and F₂ is the identically false function but both F₁ and F₂ are satisfiable. Both and F₂ are conjunctions of several clauses of TS_{G, c}. We will show that for any order π either F₁ or F₂ has large π−OBDD representation. We do not care about applications of the reordering rule, we only use that F₁ and F₂ has the same order.

Since G remains connected after removing of any single vertex, F₁ and F₂ together contain all clauses of TS_{G, c}. Assume that there are two nonadjacent vertices u and v such that F₁ does not contain a clause C_u that corresponds to the vertex u and F₂ does not contain a clause C_v that corresponds to v (if this assumption is false, the proof is rather straightforward). We consider two partial assignments ρ₁ and ρ₂ that are both defined on the edges adjacent to u and v and on the edges of the path p between u and v. The assignments ρ₁ and ρ₂ assign opposite values to edges of the path p and are consistent on all other edges. The assignment ρ₁ satisfies C_v and refutes C_u and ρ₂ satisfies C_u and refutes C_v.

By the construction $F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}}$ is almost 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. However, it is also possible that this formula does not contain some clauses for the vertices from p. Thus we make additional partial assignment τ that substitute values from a satisfying assignment for all remaining edges for vertices from p. $(F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}})|_{\tau }$ is satisfiable Tseitin formula based on the graph that is obtained from G by deletion of all vertices from the path p. The size of an OBDD representation of such a formula is at least t by the condition of the theorem. Hence by Lemma 2.1 we get that either F₁ or F₂ has size at least ${\Omega }(\sqrt {t})$ in the given order.

Proof Proof of Theorem 5.1

Consider the last step of the proof: conjunction of OBDDs F₁ and F₂ is the identically false function but F₁ and F₂ are satisfiable. Both F₁ and F₂ are conjunctions of several clauses of TS_{G, c}. Every clause of TS_{G, c} is either in F₁ or in F₂ since otherwise F₁ ∧ F₂ is satisfiable by Lemma 5.2. Our goal is to prove that either F₁ or F₂ has size at least $\sqrt {t}$. □

Lemma 5.2

Suppose Φ denotes the formula that can be obtained from TS_{G, c} by removing one arbitrary clause. Then Φ is satisfiable and every OBDD representation of Φ has size at least t.

Proof

Assume that TS_{G, c} = Φ ∧ C, where C is a clause that corresponds to the parity condition for a vertex v. Let H be the result of the removing of the vertex v from G. H is t-good and, hence, the graph H is connected. Consider an assignment σ to all variables of the clause C that falsifies C. Let ${\Phi }^{\prime }={\Phi }|_{\sigma }$. Since σ falsifies C, it satisfies all the other clauses in the parity condition for the vertex v. Since H is connected, the assignment σ changes the total parity of the labeling function of this component to be even. Thus, ${\Phi }^{\prime }$ corresponds to a satisfiable Tseitin formula based on H; hence, the size of every OBDD for ${\Phi }^{\prime }$ is at least t. ${\Phi }^{\prime }$ is the result of the assignment applied to Φ, hence by Lemma 2.1 the size of every OBDD representing Φ is at least t. □

We consider two cases:

• 1. There exist two non-adjacent vertices u and v from G such that F₁ does not include some clause C_v that corresponds to the vertex v and F₂ does not include some clause C_u for the vertex u.

  Consider a path p from v to u that exists by the property 2 from the conditions of the theorem. Let e_v be the first edge of p and e_u be the last edge (e_v≠e_u since u and v are non-adjacent). Consider two assignments ρ₁ and ρ₂ with the same support: all edges that are incident to vertices u and v and all edges from the path p. Assignments ρ₁ and ρ₂ 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). ρ₁ substitutes zeros to all edges from p except e_u and e_v, and substitutes a value to e_v that does not satisfy C_v, and a value to e_u that satisfies C_u. ρ₂ substitutes ones to all edges from p except e_u and e_v, and substitutes 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 ρ₁ and ρ₂; ρ₁ satisfies u and refutes v and ρ₂ refutes u and satisfies v.

  Consider the graph $G^{\prime }$ that can be obtained from G by removing u, v and all edges from the path p. The graph $G^{\prime }$ is connected by the property 2 from the conditions of the theorem.

  Let $c^{\prime }$ be a labeling function of the result of the assignment ρ₁ applied to TS_{G, c} and $c^{\prime \prime }$ be a restriction of $c^{\prime }$ on V ∖{u, v}. Note that ρ₂ corresponds to the same $c^{\prime \prime }$ since ρ₁ and ρ₂ identically change the value of the labelling function for all vertices except u and v. We claim that $\text {TS}_{G^{\prime }, c^{\prime \prime }}$ is Indeed if we make a assignment ρ₁ to TS_{G, c} the vertex v would be refuted, the vertex u would be would be satisfied, all other vertices are marked according $c^{\prime }$. Thus the sum of values of $c^{\prime \prime }$ is even and $\text {TS}_{G^{\prime }, c^{\prime \prime }}$ is satisfiable since $G^{\prime }$ is connected.

  We consider the conjunction $F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}}$. Any satisfying assignment of $\text {TS}_{G^{\prime }, c^{\prime \prime }}$ satisfies both $F_{1}|_{\rho _{1}}$ and $F_{2}|_{\rho _{2}}$, hence $F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}}$ is satisfiable. Suppose we represent $F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}}$ as a conjunction of clauses. For every vertex w that is not in p, the union of clauses of F₁ and F₂ contains all clauses that correspond to the equation at the vertex w, assignments ρ₁ and ρ₂ are consistent for all variables from this equation, hence $F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}}$ contains all clauses that correspond to the equation of the vertex w in formula $\text {TS}_{G^{\prime },c^{\prime \prime }}$. Consider a partial assignment τ that substitutes values to edges of that are incident to vertices of p according some satisfying assignment of $\text {TS}_{G^{\prime },c^{\prime \prime }}$. If we delete all vertices of the path p from $G^{\prime }$ we get a graph $G^{\prime \prime }$ that is connected by the property 2 of conditions of the theorem. Since τ is consistent with a satisfying assignment of $\text {TS}_{G^{\prime },c^{\prime \prime }}$, $\text {TS}_{G^{\prime },c^{\prime \prime }}$, then the application of the assignment τ converts $\text {TS}_{G^{\prime },c^{\prime \prime }}$ to a satisfiable Tseitin formula $\text {TS}_{G^{\prime \prime },c^{\prime \prime \prime }}$. And $\text {TS}_{G^{\prime \prime },c^{\prime \prime \prime }}$ coincides with $(F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}})|_{\tau }$.

  Size of any OBDD representation of the formula $\text {TS}_{G^{\prime \prime }, c^{\prime \prime \prime }}$ is at least t since $G^{\prime \prime }$ is t-good. Then any OBDD representing $(F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}})|_{\tau }$ has size at least t, hence by Lemma 2.1 any OBDD representing $F_{1}|_{\rho _{1}} \land F_{2}|_{\rho _{2}})$ has size at least t. Thus, by Lemma 2.1 for every given order of variables π either $F_{1}|_{\rho _{1}}$ or $F_{2}|_{\rho _{2}}$ has size of the minimal π−OBDD at least $\sqrt {t}$. Hence, the minimal π−OBDD for F₁ or F₂ has size at least $\sqrt {t}$.

• 2. In the second case there are no such non-adjacent vertices. Since F₁ is not identically false, there exists a vertex u such that F₁ does not include a clause that corresponds to a vertex u and by the assumption F₂ does not include clauses only for the vertex u and its neighbours. Hence, $\text {TS}_{G,c}=F_{2} \land \bigwedge _{i\in I} C_{i}$, where for all i ∈ I, C_i is a clause corresponding u or a neighbour of u that is not included in F₂. Notice that I≠∅; let us fix i₀ ∈ I. Then, $F_{2} \land \bigwedge _{i\in I\setminus \{i_0\}} C_i$ obtained from TS_{G, c} by removing of $C_{i_{0}}$, hence, by Lemmas 5.2, the size of any OBDD representation of $F_{2} \land \bigwedge _{i\in I\setminus \{i_{0}\}} C_{i}$ is Ω(t). Since G is a constant-degree graph, $\bigwedge _{i\in I} C_{i}$ depends on a constant number of variables. Hence $\bigwedge _{i\in I\setminus \{i_{0}\}} C_{i}$ can be represented as an OBDD of size O(1) for any order of variables. Thus, by Lemma 2.1, any OBDD representation of F₂ has size at least Ω(t).

Theorem 5.1 is used in the proof of the main result of this section:

Theorem 5.3

Let G be a connected graph and TS_{G, c} be an unsatisfiable formula. Then every OBDD(∧,reordering)-refutation of TS_{G, c} has size at least $2^{\Omega \left (\text {tw}(G)^{\delta }\right )}$ for all δ < 1/36. For planar graphs the lower bound holds and for δ = 1.

We will need the following lemmas.

Lemma 5.4

Let ϕ be an unsatisfiable CNF formula that has a refutation in the proof system OBDD(∧,reordering) of size S. Let ρ be a partial assignment of values of the formula ϕ. Then ϕ|_ρ has an OBDD(∧,reordering)-refutation of size at most S.

Proof

Let $D_{1}, D_{2}, \dots , D_{s}$ be a refutation of the formula ϕ, then $D_{1}|_{\rho },D_{2}|_{\rho },\dots , D_{s}|_{\rho }$ is a refutation of the formula ϕ|_ρ, where D_i|_ρ is a result of an assignment ρ to OBDD D_i. By Lemma 2.1, the application of an assignment does not increase the size of OBDD. □

Lemma 5.5

Let G(V, E) be a connected graph and $G^{\prime }(V^{\prime },E^{\prime })$ be a connected subgraph of G with $E^{\prime }\neq \emptyset$ that is obtained from G by the deletion of some vertices and edges. For every unsatisfiable Tseitin formula TS_{G, c} there exists an assignment ρ on variables $E\setminus E^{\prime }$, such that ρ does not falsify any clause of TS_{G, c}.

Proof

We substitute one-by-one values of variables that correspond to edges from $E\setminus E^{\prime }$ (and correspondingly modify the Tseitin formula) and we maintain the following invariant while deleting edges of G: a Tseitin formula corresponding to every connected component that doesn’t contain vertices from $V^{\prime }$ is satisfiable. The invariant holds at the beginning, since the graph $G^{\prime }$ is connected and thus there are no such connected components. Recall that an edge of a graph is a bridge if removing of this edge from the graph increases the number of connected components. Suppose we assign an edge e, if e is from an unsatisfiable connected component (i.e. a part of Tseitin formula corresponding to this component is unsatisfiable) and it is not a bridge of G, then we assign it with the value 0, after this transformation the component stays unsatisfiable. If e is a bridge of an unsatisfiable component, then we assign it with a value such that the new connected component that is obtained after the deletion of e and that does not contain vertices from $V^{\prime }$ would be satisfiable (such value exists by Lemma 2.2). If e is from a satisfiable connected component, then we assign a value from the satisfying assignment of this connected component. In the end the invariant implies that the resulting assignment does not falsify any clause of TS_{G, c}. □

Proof of Theorem 5.3

By Theorem 2.8 the graph G contains a s × s grid minor H, where $s={\Omega }\left (\text {tw}(G)^{\delta }\right )$. Consider a process of obtaining the minor H from the graph G such that this process contains the minimal possible number of operations of edge contractions. Since operations of edge and vertex deletions and edge contractions commute, we denote by $G^{\prime }$ a graph that is obtained from G after the application of all edge and vertex deletions. Then H can be obtained from $G^{\prime }$ by the application of only edge contractions. We assume that if during a step of edge contractions we get parallel edges, then all of them except one should be deleted.

In Lemmas 5.6, 5.7, 5.8 and 5.9 we verify that $G^{\prime }$ satisfies the conditions of Theorem 5.1. And then we conclude the proof by the application of Lemmas 5.5 and 5.4. □

Lemma 5.6

All vertices in the graph $G^{\prime }$ have a degree at most 4.

Proof

Note that after the application of an edge contraction the degree of a vertex cannot decrease, since otherwise it is possible to replace an edge contraction by a vertex deletion. Since all vertices in H have degrees at most 4, it must also be true for $G^{\prime }$. □

Lemma 5.7

After the deletion of any vertex from the graph $G^{\prime }$ we get a connected graph.

Proof

Suppose that we delete a vertex v from the graph $G^{\prime }$ and get a graph with at least two connected components K₁ and K₂. We know that we can obtain the s × s grid H from the graph $G^{\prime }$ by several edge contractions. Suppose the vertex v is transformed to the vertex $v^{\prime }$ of H after the application of these edge contractions. Since H remains connected after the deletion of the vertex $v^{\prime }$, it is not possible that some vertex a ∈ K₁ and some vertex b ∈ K₂ are transformed to vertices $a^{\prime }$ and $b^{\prime }$ from $H-v^{\prime }$. Indeed, $H-v^{\prime }$ is connected, hence there is a path in H connecting $a^{\prime }$ and $b^{\prime }$ that does not contain $v^{\prime }$, hence there is a path in $G^{\prime }$ connecting a and b that does not contain v; this is a contradiction since a and b are from different connected components of $G^{\prime }-v$. Thus for some i ∈{1,2} the component K_i is fully transformed to the vertex $v^{\prime }$. It means that we could just delete all vertices of K_i and do not contract anything, it decreases the number of contractions and contradicts the choice of the graph $G^{\prime }$. □

Consider the s × s grid square H and for every two vertices u and v of H we define a path $p^{\prime }_{u,v}$ between them. If at least one of u and v is not on the border of the square H, then $p^{\prime }_{u,v}$ consists of two straight-line parts, one of whose is horizontal and the other is vertical. If u and v belong to the border of H, then $p^{\prime }_{u,v}$ is the shortest path between u and v that only passes through vertices on the border. In both cases it can be easily verified that the s × s graph remains connected after the deletion of vertices u and v and edges of $p^{\prime }_{u,v}$, and also after the deletion of all vertices of $p^{\prime }_{u,v}$. Notice the following property: if two vertices of $p^{\prime }_{u,v}$ are connected by and edge of the grid, then they are consequent in the path $p^{\prime }_{u,v}$.

Consider two arbitrary vertices u and v of the graph $G^{\prime }$, suppose that after the application of edge contractions they are transformed to the vertices $u^{\prime }$ and $v^{\prime }$ ($u^{\prime }$ and $v^{\prime }$ might coincide) of the s × s grid H. Let p_{u, v} be a path between u and v in the graph $G^{\prime }$ that is transformed to $p^{\prime }_{u^{\prime },v^{\prime }}$. If u = v, we assume that p_{u, u} is a path with the only one vertex u.

Lemma 5.8

For every two vertices u, v of the graph $G^{\prime }$ if we delete u and v and edges of p_{u, v} from $G^{\prime }$ we obtain a connected graph. And if we delete all of the vertices of p_{u, v} we also obtain a connected graph.

Proof

At first we note that it is impossible that $G^{\prime }$ has two adjacent vertices a and b out of the path p_{u, v} such that a and b are transformed to different pair of distinct vertices $a^{\prime }$ and $b^{\prime }$ of path $p^{\prime }_{u^{\prime },v^{\prime }}$. Indeed, since we do not delete edges, $a^{\prime }$ and $b^{\prime }$ are connected by an edge in H, hence $a^{\prime }$ and $b^{\prime }$ are two consecutive vertices of $p^{\prime }_{u^{\prime },v^{\prime }}$. Since p_{u, v} is transformed to $p^{\prime }_{u,v}$, there are vertices s and t from p_{u, v} that are transformed to $a^{\prime }$ and $b^{\prime }$. Vertices s and t are connected by edges of p_{u, v}, hence there is an edge of p_{u, v} that is transformed to an edge between $a^{\prime }$ and $b^{\prime }$. The edge between a and b is also transformed to an edge between $a^{\prime }$ and $b^{\prime }$. This is a contradiction, since we get two edges between $a^{\prime }$ and $b^{\prime }$ that come from different edges of $G^{\prime }$, hence one of them should be deleted but we assume that there are no more deletions.

We claim that the graph $G^{\prime }$ remains connected if we delete from it vertices u, v and edges of the path p_{u, v}. Proof by contradiction. Suppose that after the deletion we will get a graph with at least two connected components K₁ and K₂. Since H remains connected after deletions of vertices $u^{\prime },v^{\prime }$ and edges of the path $p^{\prime }_{u^{\prime },v^{\prime }}$, then it is not possible that some vertices a ∈ K₁ and b ∈ K₂ are transformed to vertices $a^{\prime },b^{\prime }$ from $H-\{v^{\prime }, u^{\prime }\}$, because they are connected in $H-\{v^{\prime }, u^{\prime }\}$ and thus there is a path between them that does not go through vertices u, v and edges of the path p_{u, v} in the initial graph $G^{\prime }$. Thus, for some i ∈{1,2} every vertex of the component K_i is transformed to $v^{\prime }$ or to $u^{\prime }$. We have already shown that it is impossible that some vertices from K_i are transformed to $v^{\prime }$ and some to $u^{\prime }$ (otherwise there are two adjacent vertices with such property). Hence we may just delete all vertices from K_i and do not contract anything and this decreases the number of contractions. And we get a contradiction with the choice of the graph $G^{\prime }$.

By similar arguments the graph $G^{\prime }$ remains connected if we delete from it all vertices of p_{u, v}. □

Lemma 5.9

For every two vertices u, v of the graph $G^{\prime }$ the graph that is obtained from $G^{\prime }$ by the deletion of all vertices of p_{u, v} contains a ⌊s/3⌋×⌊s/3⌋ grid as a minor.

Proof

Consider some vertices u and v of the the s × s square. We show that if we delete all vertices of the path $p^{\prime }_{u,v}$ from the s × s square, then there is a sub-square of the size ⌊s/3⌋×⌊s/3⌋ that does not contain any deleted edge or vertex. Indeed, there are 9 squares of the size ⌊s/3⌋×⌊s/3⌋ that are fully contained in the square s × s and do not have common 1 × 1 squares. If the path goes only by the border of the square then it does not touch the central square ⌊s/3⌋×⌊s/3⌋. In the other case the path has two straight segments (may be of the zero length): vertical and horizontal. It is easy to see that such paths can have common vertices with at most 8 chosen squares, hence there is at least one ⌊s/3⌋×⌊s/3⌋ square that is not touched.

Suppose we deleted the path p_{u, v} between two vertices u and v from the graph $G^{\prime }$. We find in the square H a square T_⌊s/3⌋ of the size ⌊s/3⌋×⌊s/3⌋ such that it does not intersect with vertices $u^{\prime }$, $v^{\prime }$ and vertices of the path $p^{\prime }_{u^{\prime },v^{\prime }}$. Let U be the set of vertices of the graph $G^{\prime }$ that is contracted to vertices of T_⌊s/3⌋. The set of vertices U does not intersect with u, v and vertices of the path p_{u, v}, since in the other case the square T_⌊s/3⌋ would also intersect $u^{\prime },v^{\prime }$ or $p^{\prime }$. Thus T_⌊s/3⌋ is a minor of a subgraph $G^{\prime }$ that is induced by vertices from U, and, hence, a minor of the graph $G^{\prime }$. □

Let K be a graph obtained from $G^{\prime }$ by the deletion of a vertex u or by the deletion of vertices from a path p_{u, v} for some u, v. Lemmas 5.9 and 4.3 imply that size of 1-NBP for satisfiable Tseitin formula TS_{K, c} is at least the minimal size of 1-NBP for a satisfiable Tseitin formula $\text {TS}_{T_{\lfloor s/3 \rfloor },c^{\prime }}$ that by Theorem 3.1 is at least 2^Ω(s). and Lemmas 5.6, 5.7, 5.8 we get that $G^{\prime }$ satisfies the condition of Theorem 5.1 for t = 2^Ω(s).

By Lemma 5.5, there exists an assignment ρ of variables corresponding to edges of G that are not in $G^{\prime }$ that does not falsify clauses of the formula TS_{G, c}. The application of ρ to the formula TS_{G, c} transforms it to the formula $\text {TS}_{G^{\prime },c^{\prime }}$ (other clauses are satisfied). By Theorem 5.1 the size of every OBDD(∧,reordering)-refutation of the formula TS_{G, c} is 2^Ω(s). Then by Lemma 5.4 the size of every OBDD(∧,reordering)-refutation of the of the formula TS_{G, c} is 2^Ω(s).

6 Upper Bounds

In this section we prove upper bounds on the size of OBDD for satisfiable Tseitin formulas and on the size of OBDD(∧) refutations of unsatisfiable Tseitin formulas.

Theorem 6.1

Let F be a conjunction of several parity conditions of a Tseitin formula TS_{G, c} based on a graph G(V, E). Then F can be represented as an OBDD of size |E|2^pw(G)+ 1 + 2.

Proof

Consider a path decomposition of the graph G: $X_{1}, X_{2}, \dots , X_{s}$ such that |X_i|≤pw(G) + 1 for i ∈ [s]. We split the set of edges into disjoint (maybe empty) parts: $E_{1}, E_{2}, \dots , E_{s}$. E₁ is a set of edges between vertices X₁, if i > 1, then E_i is a set of edges between vertices in X_i that did not appear earlier (it is enough to require that no one of these edges is between vertices from X_i− 1, since a vertex can not disappear and then appear again). Since every edge occurs in at least one X_i, every edge will be in some set E_j.

We fix some order of edges in which the first are edges from E₁, then edges from E₂, $\dots$ and in the end there are edges from E_s. Let e_i be i th edge in this order.

Let D be the minimal OBDD using the order $x_{e_{1}}, x_{e_{2}},\dots , x_{e_{|E|}}$ computing F such that every path from the root to 1-sink contains all variables. Let us estimate the number of nodes in D on the distance l from the source of D for all l ∈ [|E|]. Every node of D computes some Boolean function. Since D is minimal, all nodes on the distance l from the sink compute pairwise different functions. We will estimate the number of different functions that can be obtained from F by the restriction of variables $x_{e_{1}}, x_{e_{2}},\dots , x_{e_{l}}$. One of such functions can be identically zero; we estimate the number of all other functions. Consider a partial assignment ρ to variables $x_{e_{1}}, x_{e_{2}},\dots , x_{e_{l}}$ such that F|_ρ is not identically zero. Assume that e_l ∈ E_j. Consider a vertex v ∈ V ∖ X_j and assume that v ∈ X_i. If i < j, then all incident edges of v are among $e_{1}, e_{2}, \dots , e_{l}$, hence the parity condition in the vertex v is either not included in F or is satisfied by ρ. If i > j, then edges $e_{1}, e_{2}, \dots , e_{l}$ are not incident to v. Thus, different functions F|_ρ may vary only in parities of sum of assigned incident edges for vertices from X_j. Since |X_j|≤pw(G) + 1, the number of different functions corresponding to nodes of D on the distance l (except is at most 2^pw(G)+ 1. There are |E| possible values of l and we also have the source and 0-sink, thus the size of D is at most |E|2^pw(G)+ 1 + 2. □

Corollary 6.2

Any satisfiable Tseitin formula based on a graph G(V, E) can be represented as OBDD of size O(|E||V |^O(tw(G))).

Proof

Follows from Theorem 6.1 and Lemma 2.7. □

Corollary 6.3

If TS_{G, c} is an unsatisfiable Tseitin formula based on a graph G(V, E), then it has an OBDD(∧)-refutation of size $O(|E||V| 2^{\text {pw}(G)}+|\text {TS}_{G,c}|^{2})$.

Proof

We chose the order π on variables of TS_{G, c} constructed in Theorem 6.1. All OBDDs in the refutation will have order π. At first we derive an OBDDs representing parity condition for all vertices of G. In order to do this we consequentially join OBDDs representing clauses for the corresponding parity vertex v has degree k, then the parity condition for v is represented in TS_{G, c} by 2^k− 1 clauses. The of several of these clauses is a function of k variables, hence it can be represented by an OBDD of size O(2^k) in order π. Thus the derivation of OBDD for the parity condition of the vertex v has size O(2^2k). If G has n vertices $v_{1}, v_{2}, \dots , v_{n}$ with degrees $k_{1}, k_{2}, \dots , k_{n}$, then TS_{G, c} has size at least ${\Omega }({\sum }_{i=1}^{n} 2^{k_{i}})$. Hence, the derivation of OBDDs for all parity conditions has size $O({\sum }_{i=1}^{n} 2^{2k_{i}})= O(|\text {TS}_{G,c}|^{2})$.

Then we consequentially apply the join rule to parity conditions and finally get the constant false OBDD representing TS_{G, c}. All OBDDs in this part of derivation have size at most O(|E|2^pw(G)+ 1) by Theorem 6.1. Thus the total refutation has size $O(|E||V| 2^{\text {pw}(G)}+|\text {TS}_{G,c}|^{2})$. □

7 Further Research

• 1. It is interesting to improve the lower bound on the size of 1−BP for Tseitin formulas based on arbitrary we conjecture that it should be 2^Ω(tw(G)). Is it possible to extract a tree decomposition from 1−BP directly?

• 2. Results of [8] implies lower bound $2^{\text {tw}(G)^{\Omega (1)}}$ on the size of constant-depth Frege refutations of TS_{G, c}. Can it be improved for resolution (resolution is a partial case of constant-depth Frege)?