Bounded-depth Frege complexity of Tseitin formulas for all graphs

doi:10.1016/j.apal.2022.103166

Annals of Pure and Applied Logic

Volume 174, Issue 1, January 2023, 103166

, , ,

^a: Dipartimento Ingegneria Informatica Automatica e Gestionale “A. Ruberti”, Sapienza Università di Roma, Italy

^b: St. Petersburg Department of V.A. Steklov Institute of Mathematics of the Russian Academy of Sciences, Russian Federation

^c: St. Petersburg State University, Russian Federation

Received 24 December 2020, Revised 30 June 2022, Accepted 1 July 2022, Available online 11 July 2022, Version of Record 22 July 2022.

https://doi.org/10.1016/j.apal.2022.103166 Get rights and content

Abstract

We prove that there is a constant K such that Tseitin formulas for a connected graph G requires proofs of size $2^{tw {(G)}^{Ω (1 / d)}}$ in depth-d Frege systems for $d < \frac{K \log n}{\log \log n}$ , where $tw (G)$ is the treewidth of G. This extends Håstad's recent lower bound from grid graphs to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size $2^{tw {(G)}^{O (1 / d)}} poly (s)$ . Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.

MSC

03F20

03B05

05C83

68Q27

Keywords

Proof complexity

Bounded-depth Frege

Resolution

Tseitin formulas

Treewidth

1. Introduction

Propositional proof complexity is motivated by the result of Cook and Reckhow [15] saying that if there is a propositional proof system in which any unsatisfiable formula F has a short proof of unsatisfiability (of size polynomial in the size of F), then $NP = coNP$ . In the last 30 years the complexity of proofs was investigated for several proof systems with the aim of finding concrete evidence, and eventually a proof, that for all proof systems there is a propositional formula which is not efficiently provable, i.e. requires super-polynomial proof size. The approach followed to prove such lower bounds was essentially borrowed from circuit complexity. Lines in a proof are Boolean formulas and we can define different proof system according to the circuit complexity of such formulas. For example resolution, a well-known refutational system for CNFs, corresponds to a system where formulas are of depth 1. In circuit complexity we keep on trying to strengthen lower bounds to computationally more powerful class of circuits. In proof complexity we follow the analogous approach: to strengthen lower bounds to systems working on formulas computationally more powerful. The hope is that techniques used to prove lower bounds for classes of Boolean circuits could be lifted to work with proof systems operating with formulas in the same circuit class. At present however we are far from such ideal situation and in fact, in terms of circuit classes, lower bounds for proof systems are well below those for Boolean circuits.

The complexity of proofs in resolution is largely studied. The first lower bound for (a restriction of) resolution was given by Tseitin in [43]. To obtain his result Tseitin introduced a class of formulas (nowadays known as Tseitin formulas) encoding a generalisation of the principle that the sum of the degrees of all vertices in a graph is an even number. A Tseitin formula $T (G, f)$ is defined for every undirected graph $G (V, E)$ and a charging function $f : V \to {0, 1}$ . We introduce a propositional variable for every edge of G so that $T (G, f)$ is a CNF representation of a linear system over the field $GF (2)$ such that each equation corresponds to a vertex $v \in V$ ans states that the sum of all edges incident to v equals $f (v)$ . Together with the unsatisfiable formulas ${PHP}_{n}$ encoding the Pigeonhole principle, Tseitin formulas are among the most commonly used examples to prove hardness results for proof systems. Haken [25], Beame and Pitassi [6] and Ben-Sasson Wigderson [10] proved exponential resolution lower bounds for the CNF formula encoding the negation of ${PHP}_{n}$ , results which were later generalized and improved in several other works [11], [16], [30], [37], [39], [40]. For unrestricted resolution it was Urquhart in [44] and later Ben-Sasson and Wigderson [10] who proved exponential lower bounds for Tseitin formulas defined over constant-degree expander graphs.

Bounded-depth Frege extends resolution since the formulas in the proof-lines are computable by ${AC}^{0}$ -circuits, i.e. constant-depth circuits with unbounded fan-in gates. The importance of understanding the complexity of proofs in bounded-depth-Frege systems was due at least to two reasons: (1) for general Frege systems, where formulas have no restrictions, i.e. are of depth $O (\log n)$ , Buss in [12] proved that the Pigeonhole principle can be proved in polynomial size, hence obtaining an exponential separation with resolution. (2) Lower bounds for ${AC}^{0}$ -circuits were known [20], [27] and hence we could hope for applying lower bound techniques for ${AC}^{0}$ to lower bounds to bounded-depth Frege. Studying the complexity of proofs in bounded-depth Frege is of the utmost importance since it is a frontier proof system, i.e. is one of the strongest propositional proof systems with known significant lower bounds at the moment. Any advance is then a step towards proving lower bounds for ${AC}^{0} [2]$ -Frege, i.e. a bounded-depth Frege admitting also formulas with parity gates, which are unknown at the moment, though we know since a long time exponential lower bounds for ${AC}^{0} [2]$ circuits [32], [38], [42]. In this work we contribute to the complexity of proofs in bounded-depth Frege proving new lower bounds for Tseitin formulas.

Ajtai in [1] was the first to prove a lower bound in bounded-depth Frege. He showed that a refutation of ${PHP}_{n}$ must have a super-polynomial size. His result was later followed by several results simplifying his technique [7] and improving the lower bound [33], [34] showing that any polynomial-size Frege refutation of ${PHP}_{n}$ must have depth $Ω (\log \log n)$ . The proof complexity of Tseitin formulas in bounded-depth Frege was first considered by Urquhart and Fu in [45], a work where they simplified and adapted the lower bound for the ${PHP}_{n}$ to the case of Tseitin formulas over a complete graph. Ben-Sasson in [9], proved exponential lower bounds for the Tseitin formulas over constant-degree expander graphs using a new reduction from the pigeonhole principle [45]. All these lower bounds are adaptation of the technique of [33], [34], hence vanish when the depth of formulas in the proof is more than $\log \log n$ . In a very recent major breakthrough [35] showed that Tseitin formulas over a 3-expander graph on n nodes requires super-polynomial bounded-depth Frege refutations at depth $O (\sqrt{\log n})$ . This result was later improved to depth up to $\frac{C \log n}{\log \log n}$ by Håstad in [28] but for Tseitin formulas defined only on the 2-dimensional grid, where C is a positive constant.

Proofs of $T (G, f)$ were studied in terms of the treewidth of G, $tw (G)$ , for resolution [3], [22] and for OBDD proof systems [23]. We use Håstad result to prove tight bounds on the size of refutations in bounded-depth Frege of $T (G, f)$ over any graph G in terms of the treewidth of G. Our main result is the following theorem:

Theorem 1

There is a constant K such that for any connected graph G over n nodes and for all $d ⩽ K \frac{\log n}{\log \log n}$ , every depth-d Frege proof of $\neg T (G, f)$ has size at least $2^{tw {(G)}^{Ω (1 / d)}}$ . Furthermore, for all large enough d there exist depth-d Frege proofs of $\neg T (G, f)$ of size $2^{tw {(G)}^{O (1 / d)}} poly (| T (G, f) |)$ .

1.1. Overview of the proof technique

In Theorem 18 we prove the lower bound from Theorem 1. The proof is based on the improvement of the Excluded Grid Theorem by Robertson and Seymour recently obtained by Chuzhoy [13]: an arbitrary graph G contains as a minor a $r \times r$ grid, where $r = Ω (tw {(G)}^{λ})$ and λ is a constant; the latest improvement [14] establishes the theorem for $λ < 1 / 10$ , however, it is known that λ can not be greater than 1/2. For several classes of graphs it is possible to improve the value of λ, for example, for planar graphs $λ = 1$ [24], [41]. More precisely we use the corollary of this result (see Corollary 9) stating that any graph G has a wall of size r as a topological minor (i.e. can be obtained from G by several removing of vertices, edges and suppressions, see Fig. 1 and Fig. 3). Our proof consists of two parts: at first, we show that if H is a topological minor of G, then any bounded-depth Frege proof of $\neg T (G, f)$ can be transformed to a proof of $\neg T (H, f^{'})$ , with constant increase in depth and polynomial increase in size. And then we prove a lower bound on the size of depth-d Frege proof of $\neg T (H, f^{'})$ based on walls. In this proof we use the lower bound for grid graphs proved by Håstad [28].

In Theorem 19 we prove the upper bound from Theorem 1. We consider the compact representation of linear functions $F_{2}^{n} \to F_{2}$ on variables $x_{1}, x_{2}, \dots, x_{n}$ by propositional formulas of depth d and of size $2^{n^{O (1 / d)}}$ . We show that for linear functions f and g if the equations $f (x) = a$ and $g (x) = b$ are given in our representation, then there is a derivation of $(f + g) (x) = a + b$ of depth d and of size $2^{n^{O (1 / d)}}$ . We also show that if a linear equation is represented in CNF, then it is possible to infer its compact representation with depth d and size $2^{n^{O (1 / d)}}$ . Since a Tseitin formula is an unsatisfiable system of linear equations written in CNF, hence it is possible to refute a Tseitin formula in size $2^{m^{O (1 / d)}}$ and depth d, where m is the number of edges in G. However we wish to have the treewidth of G instead of m. We consider a tree-partition of a graph G, the vertices of G are split into bags and there exists a tree such that bags are nodes of this tree and if two vertices of G are connected, then they are either in one bag or in adjacent bags. It is known that there is a tree partition where the size of bags are at most $O (tw (G) Δ (G))$ [46]. Since the number of edges touching a given bag is $O (tw (G) Δ {(G)}^{2})$ we can use the compact representation to take care of the equations involving the parity of sum of adjacent bags with proofs growing in terms of the treewidth of G.

1.2. The complexity of Tseitin formulas in resolution

A recent line of research [3], [22], [31] investigates the exact relation between the treewidth of G and the proof complexity of $T (G, f)$ in resolution and its refinements. Since resolution is a special case of bounded-depth Frege, Theorem 1 is directly applicable to resolution. In Section 5 we contribute this line of research partially answering to some questions left open before. First we improve Theorem 1 for resolution. In Theorem 34 we show $2^{Ω ({tw}^{λ} (G))}$ lower bounds for resolution refutations of $T (G, f)$ , where λ is the constant from the grid-minor theorem in [13]. A stronger lower bound $2^{Ω (tw (G) / \log n)}$ was recently proved for regular resolution in [31] and it is open whether this holds for unrestricted resolution as well.

A conjecture of Urquhart asserts that the shortest resolution refutations of $T (G, f)$ are in fact regular. A consequence of our results, stated in Corollary 40, shows that the size of refutations of $T (G, f)$ in proof systems between tree-like resolution and bounded-depth Frege are quasi-polynomially correlated, i.e. if $T (G, f)$ has a refutation of size S in bounded-depth Frege, then it has a refutation of size at most $2^{poly (\log S)}$ in treelike resolution and vice versa. Since regular resolution is in between treelike resolution and bounded-depth Frege, this provides evidence (showing it for a quasi-polynomial size) to the conjecture of Urquhart.

Finally we consider the question posed in [3] of (quasi)-automatization of $T (G, f)$ formulas in resolution, i.e. whether there exists a deterministic algorithm that returns a resolution refutation of $T (G, f)$ in time which is (quasi-)polynomial in $| T (G, f) | + | τ_{T (G, f)} |$ , where $| τ_{T (G, f)} |$ is the size of the shortest refutation of $T (G, f)$ in resolution. From [3] it is known that $T (G, f)$ are (quasi)-automatizable in resolution only when G has a specific covering property known as bounded cyclicity. In Corollary 39 we extend their result proving the quasi-automatization of $T (G, f)$ for any graph G.

Organization. The paper is divided into four sections. After the Preliminary section, we have Section 3 for the lower bound (Theorem 18), and Section 4 for the upper bound (Theorem 19). Section 5 is devoted to the results on the proof complexity of $T (G, f)$ in resolution.

2. Preliminaries

Formulas and restrictions. We consider propositional formulas over binary ∨ and ∧, unary ¬ and Boolean constants $0, 1$ . We represent formulas as rooted trees such that internal vertices are labelled with connectives and leaves are labelled with propositional variables or Boolean constants. The depth of a formula is the maximal number of alternations of types of connectives over all the paths from the root to a leaf plus one.

We assume that disjunctions with unbounded fanin are represented via binary disjunctions. By default, we mean that $⋁_{i = 1}^{n} x_{i}$ is right-associative; i.e. it denotes $(\dots (x_{1} \lor x_{2}) \lor \dots) \lor x_{n - 1}) \lor x_{n}$ ; we also assume the same for ⋀.

We denote by $vars (F)$ the set of variables of a formula F. A partial assignment α for a formula F is mapping from $vars (F) \to {0, 1, ⁎}$ , where $α (x) = ⁎$ if x is unassigned. We denote by $dom (α) = α^{- 1} ({0, 1})$ the set of variables in F which α assigns a Boolean value.

Pudlák-Buss games. We use the game interpretation of Frege proofs introduced by Pudlák and Buss [36]. Let us define a game with two players Pavel and Sam. The game starts with initial conditions of the form $φ_{1} = a_{1}, \dots, φ_{k} = a_{k}$ , where $φ_{1}, φ_{2}, \dots, φ_{k}$ are propositional formulas and $a_{1}, a_{2}, \dots, a_{k} \in {0, 1}$ such that $⋀_{i = 1}^{k} (φ_{i} = a_{i})$ is identically false. Sam claims that he knows an assignment of variables that satisfies $⋀_{i = 1}^{k} (φ_{i} = a_{i})$ , the goal of Pavel is to convict Sam. On each Pavel's turn he asks Sam the value of a propositional formula and Sam gives an answer. The game stops when Pavel convicts Sam, namely Pavel finds an immediate contradiction among initial conditions and Sam's answers. An immediate contradiction with a Boolean connective ∘ of arity t is a set of $(t + 1)$ formulas $α_{1}, \dots, α_{t}$ and $\circ (α_{1}, \dots, α_{t})$ with claimed values $a_{1}, \dots, a_{t}$ and b such that $\circ (a_{1}, \dots, a_{k}) \neq b$ . In particular, 0 with claimed value 1 is an immediate contradiction.

A strategy of Pavel is a function that maps initial conditions and the history of a game to a propositional formula (request). A winning strategy is a strategy that allows Pavel to convict Sam for any behaviour of Sam. A winning strategy of Pavel can be represented as a binary tree whose nodes are labelled with Pavel's requests and edges correspond to Sam's answers. A leaf of the tree corresponds to an immediate contradiction among initial conditions and the equalities corresponding to the path from the root to this leaf.

A Pudlák-Buss game derivation of a formula ψ from formulas $φ_{1}, φ_{2}, \dots, φ_{s}$ is a tree of a Pavel's winning strategy in a game with initial conditions $φ_{1} = 1, φ_{2} = 1, \dots, φ_{s} = 1, ψ = 0$ . In that follows by derivations we always mean Pudlák-Buss game derivations. We are interested in the two complexity parameters of derivations: 1) the size of a derivation S that equals the total size of formula ψ and all formulas that are used as labels of nodes; 2) the depth of a derivation d is the maximum depth of ψ and formulas that are used as labels of nodes. We use the notation $φ_{1}, \dots, φ_{s} ⊢_{d} ψ$ for a derivation of ψ from $φ_{1}, φ_{2}, \dots, φ_{s}$ of depth at most d. A derivation of φ is a derivation of φ from the empty set of formulas.

Lemma 2

Assume that there is a derivation $φ_{1}, \dots, φ_{k} ⊢_{d_{1}} ψ_{1}$ of size $S_{1}$ and also there is a derivation $φ_{1}, \dots, φ_{k}, ψ_{1} ⊢_{d_{2}} ψ_{2}$ of size $S_{2}$ , then there is a derivation $φ_{1}, \dots, φ_{k} ⊢_{\max {d_{1}, d_{2}}} ψ_{2}$ of size $S_{1} + S_{2}$ .

Proof

Let us create the new tree with the root labelled with $ψ_{1}$ such that edge form the root labelled with 0 goes to the root of the first derivation and edge labelled with 1 goes to the root of the second derivation. □

Lemma 3

1. If a formula φ has a Frege derivation of size S and depth d, then φ has a Pudlák-Buss game derivation of size $O (S^{2})$ and depth d. 2. If φ has a Pudlák-Buss game derivation of size S and depth d, then φ has a Frege derivation of size $O (S^{3})$ and depth $d + O (1)$ .

Proof

For proof see Appendix A. □

Lemma 4

Let $ψ_{1}$ and $ψ_{2}$ be two formulas of depth at most d such that $| vars (ψ_{1}) \cup vars (ψ_{2}) | = k$ and $ψ_{1}$ semantically implies $ψ_{2}$ . Then there exists a derivation $ψ_{1} ⊢_{d} ψ_{2}$ of size at most $2^{k} (| ψ_{1} |^{2} + | ψ_{2} |^{2})$ .

Proof

Consider a game with initial conditions $ψ_{1} = 1, ψ_{2} = 0$ .

Let $| vars (ψ_{1}) \cup vars (ψ_{2}) | = {x_{1}, \dots, x_{k}}$ . In the first k rounds of the game Pavel asks Sam $x_{1}, \dots, x_{k}$ . There are $2^{k}$ possible combinations of Sam's answers. For each combination Pavel asks Sam all subformulas of $ψ_{1}$ (the value of $ψ_{1}$ is 1 from initial conditions) starting with the deeper ones and then asks all subformulas of $ψ_{2}$ starting with the deeper ones (the value of $ψ_{2}$ is 0 from initial conditions). Since all variables are known, one of possible answers to each of these questions yields an immediate contradiction. The total size of all subformulas of $ψ_{1}$ and $ψ_{2}$ is at most $| ψ_{1} |^{2} + | ψ_{2} |^{2}$ . Consider the branch of the game tree, where we still no get an immediate contradiction. In that case Sam $ψ_{1} = 1$ and $ψ_{2} = 0$ are consistent with the values of $x_{1}, \dots, x_{k}$ , but it is impossible since $ψ_{1}$ semantically implies $ψ_{2}$ . Hence, there should be an immediate contradiction. □

Corollary 5

let $ψ_{1}$ and $ψ_{2}$ be two formulas of depth $d_{1}$ such that $vars (ψ_{1}) \cup vars (ψ_{2}) = {x_{1}, x_{2}, \dots, x_{k}}$ and $ψ_{2}$ is semantically implied by $ψ_{1}$ . Let $φ_{1}, \dots, φ_{k}$ be formulas of depth $d_{2}$ . Let $ψ_{i} [x_{1} \leftarrow φ_{1}, \dots, x_{k} \leftarrow φ_{k}]$ for $i \in {1, 2}$ be the formula obtained by substitution $φ_{1}, \dots, φ_{k}$ instead of the variables of $x_{1}, x_{2}, \dots, x_{k}$ . Then there exists a derivation $ψ_{1} [x_{1} \leftarrow φ_{1}, \dots, x_{k} \leftarrow φ_{k}] ⊢_{d_{1} + d_{2}} ψ_{2} [x_{1} \leftarrow φ_{1}, \dots, x_{k} \leftarrow φ_{k}]$ of size at most $2^{k} (| ψ_{1} |^{2} + | ψ_{2} |^{2}) (\sum_{i = 1}^{k} | φ_{i} |)$

Proof

Use Lemma 4 for $ψ_{1}$ and $ψ_{2}$ and then substitute $φ_{1}, \dots, φ_{k}$ instead of the variables $x_{1}, \dots, x_{k}$ . □

A shortcut contradiction for the disjunction is a situation where Pavel asks Sam formulas $⋁_{i = 1}^{k} α_{i}$ and $α_{j}$ for $j \in [k]$ and gets the answers 0 and 1 respectively. Similarly a shortcut contradiction for the conjunction is a situation where Pavel asks Sam formulas $⋀_{i = 1}^{k} α_{i}$ and $α_{j}$ for $j \in [k]$ and gets the answers 1 and 0. We may consider shortcut games (and shortcut derivations) that has one difference from the already defined games: Pavel can convict Sam using shortcut contradictions instead of immediate contradictions. An ordinary derivation is a derivation which does not use shortcut contradictions.

Lemma 6

Consider a shortcut derivation of size S and of depth d. Then there is an ordinary derivation of size at most $S^{3}$ and of depth d.

Proof

We transform a tree with shortcut contradictions to a tree without them. Let us consider a leaf with a shortcut contradiction for the disjunction (case of conjunction is similar), which means that on the path from root to that leaf Pavel has asked Sam formulas $⋁_{i = 1}^{k} α_{i}$ and $α_{j}$ for $j \in [k]$ and got the answers 0 and 1 respectively. $⋁_{i = 1}^{k} α_{i}$ is represented as $⋁_{i = 1}^{q} α_{i} \lor ⋁_{i = q + 1}^{k} α_{i}$ for some index q, where ∨ is binary disjunction. Pavel asks Sam formulas $⋁_{i = 1}^{q} α_{i}$ and $⋁_{i = q + 1}^{k} α_{i}$ .

1.
If one of Sam's answers is 1, we get an immediate contradiction.
2.
If both Sam's answers are 0, then if $j ⩽ q$ , we continue this process with formula $⋁_{i = 1}^{q} α_{i}$ otherwise with formula $⋁_{i = q + 1}^{k} α_{i}$ .

In the end of that process we get an immediate contradiction. We repeat this for all leaves with shortcut contradictions, the size of the resulting tree is at most

S^{3}

since there are at most S leaves and the size of added formulas is at most

S^{2}

for each leaf. □

Tseitin Formulas. Let

G (V, E)

be an undirected graph and

v \in V

. We denote by

E (v)

the set of edges in E incident with v and by

N (v)

the set of neighbours

u \in V

of v, i.e. the u such that

(u, v) \in E (v)

A vertex-charging for $G (V, E)$ is a mapping $f : V ⟶ {0, 1}$ . We say that f is an odd-charging of G if $\sum_{v \in V} f (v) \equiv 1 \mod 2$ . The Tseitin formulas defined on G using variables $x_{e}, e \in E$ are the formulas: $T (G, f) : = ⋀_{v \in V} Par (v)$ , where $Par (v)$ is the canonical CNF representation of $⨁_{e \in E (v)} x_{e} = f (v)$ .

Lemma 7

[44]

$T (G, f)$ is unsatisfiable if and only if there is a connected component U of G such that the restriction of f on U is an odd-charging.

In this work we will work with the tautological form of Tseitin formulas in the form of

\neg T (G, f)

Grids, Walls, Minors, Topological Minors and Treewidth. We consider 4 structural operations on undirected graphs $G = (V, E)$ possibly with parallel edges, but without loops. We follow [8], [19].

•
edge removal of $e \in E$ . It produces the graph $[G ∖ e] = (V, E ∖ {e}$ ).
•
vertex removal of $v \in V$ . It produces the graph $[G ∖ v] = (V ∖ {v}, E ∖ E (v)$ ), where $E (v)$ is the set of edges in E incident with $v \in V$ .
•
edge contraction of $e = (u, v) \in E$ . Is the replacement of u and v with a single vertex such that edges incident to the new vertex are the edges other than e that were incident with u or v. The resulting graph $G ⋆ e$ has one edge less than G.
•
vertex suppression of a vertex v in G of degree 2. Let u and w be v's neighbours in G. The suppression of v is obtained by deleting v along with two edges $(u, v)$ and $(w, v)$ and adding a new edge $(w, u)$ (possibly parallel to an existing one). The resulting graph $[G ∖_{s} v]$ has one vertex less than G. See Fig. 1.

A graph H is a minor of G if H can be obtained from G by a sequences of edge and vertex removals and edge contractions. A graph H is a topological minor of G if H can be obtained from G by a sequence of edge removals, vertex removals and by vertex suppressions [8], [19].

The grid $H_{m, n}$ is the graph of the cellular rectangle $m \times n$ ; it has $(m + 1) (n + 1)$ vertices and $n (m + 1) + m (n + 1)$ edges, among them $n (m + 1)$ horizontal and $m (n + 1)$ vertical edges. See Fig. 2.

The wall $W_{n}$ is a subgraph of $H_{n, n}$ that is obtained by the removing of several vertical edges. Vertical edges of $H_{n, n}$ are in n rows and we enumerate them in every row from the left to the right. In the odd rows we remove all vertical edges with even numbers and in even rows we remove all vertical edges with odd numbers. See Fig. 3.

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

The width of a tree decomposition is the maximum $| X_{u} |$ for $u \in 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.

Recall the following Theorem proved in [13].

Theorem 8

[14]

If G has a treewidth t, then it has the grid $H_{r, r}$ as a minor, where $r = Ω (t^{λ})$ and $λ ⩾ \frac{1}{10}$ is a constant.

The following Corollary was mentioned in [8].

Corollary 9

If G has a treewidth t, then it has the wall $W_{r}$ as a topological minor, where $r = Ω (t^{λ})$ and λ is the constant from Theorem 8.

Proof

Since $W_{r}$ is a minor of $H_{r}$ , $W_{r}$ is a minor of G. Consider a transformation T from G to $W_{r}$ made by (1) edge removals, (2) vertex removals and (3) edge contractions that has the minimal number of edge contractions. Since operations (1), (2) and (3) commute, we may assume that in T no removal follows an edge contraction (i.e. we remove everything at first, and then contract edges). Now it is easy to understand that all edge contractions should be actually suppressions. Indeed, assume that we contract $(u, v)$ and both u and v has degrees at least 3, then we will get a vertex ${u, v}$ with degree at least 4 and this is a contradiction since $W_{r}$ does have degrees at most 3 and edge contractions can decrease degree only in one case when we contract $(u, v)$ and v has degree 1, but in this case we may just remove v and it decreases the number of edge contractions. □

3. The lower bound

3.1. Topological minors and Tseitin formulas

Le φ be a formula and let α be a partial assignment to variables of φ. Define $φ [α]$ to be the formula obtained from φ substituting each variable x in the domain of α, with the constant assigned to x by α. Notice that φ and $φ [α]$ have the same size and depth.

Lemma 10

Let $Φ_{a}$ and $Φ_{a}^{'}$ for $a \in A$ be propositional formulas of depth at most d such that $| vars (Φ_{a}) \cup vars (Φ_{a}^{'}) | ⩽ k$ . Assume that for all $a \in A$ , $Φ_{a}$ is semantically equivalent to $Φ_{a}^{'}$ . Then $\neg ⋀_{a \in A} Φ_{a}^{'} ⊢_{d + O (1)} \neg ⋀_{a \in A^{'}} Φ_{a}$ of size at most $2^{k} poly (\sum_{a \in A} (| Φ_{a} | + | Φ_{a}^{'} |))$ , where $A^{'} = {a \in A | Φ_{a} is not identically true}$ .

Proof

At first Pavel asks $⋀_{a \in A} Φ_{a}^{'}$ . The answer 1 leads to an immediate contradiction. Then Pavel proceeds to ask $Φ_{a}^{'}$ for each $a \in A$ . If all the answers are 1, Pavel asks all subformulas of the big conjunction $⋀_{a \in A} Φ_{a}^{'}$ starting with the deeper ones and at each step one of Sam's answers leads to an immediate contradiction.

If Sam claim that $Φ_{a_{0}}^{'} = 0$ for some $a_{0} \in A$ , we use Lemma 4 to construct a derivation $\neg Φ_{a_{0}}^{'} ⊢_{d} \neg Φ_{a_{0}}$ of size at most $2^{k} (| Φ_{a_{0}}^{'} |^{2} + | Φ_{a_{0}} |^{2})$ . If $a_{0} \notin A^{'}$ , then $Φ_{a_{0}}$ is identically true, thus, by Lemma 4, there is a derivation $1 ⊢_{d} Φ_{a_{0}}$ of size at most $2^{k} (| Φ_{a_{0}} |^{2} + 1)$ , using it we get an immediate contradiction.

If $a_{0} \in A^{'}$ , then Pavel asks $⋀_{a \in A^{'}} Φ_{a}$ . If Sam's answer is 0, we get a shortcut contradiction with $Φ_{a_{0}}$ and proceed with Lemma 6, otherwise we get an immediate contradiction with the initial condition $\neg ⋀_{a \in A^{'}} Φ_{a} = 0$ . □

Lemma 11

[23]

Let $G (V, E)$ be a connected graph and $H (V^{'}, E^{'})$ be a connected subgraph of G with $E^{'} \neq \emptyset$ that is obtained from G by the deletion of some vertices and edges. For every unsatisfiable Tseitin formula $T (G, f)$ there exists a partial assignment α to variables $x_{e}$ for $e \in E ∖ E^{'}$ such that α does not falsify any clause of $T (G, f)$ .

Lemma 12

Let $G (V, E)$ be a connected graph and $H (V^{'}, E^{'})$ be a connected subgraph of G. Assume that there is a derivation $⊢_{d} \neg T (G, f)$ of size S. Then for some $f^{'}$ there is a derivation $⊢_{d + O (1)} \neg T (H, f^{'})$ of size $S + poly (| T (G, f) |)$ .

Proof

Let T be the game tree of $⊢_{d} \neg T (G, f)$ . Let α be given by Lemma 11 that is defined on all variables $x_{e}$ for $e \in E ∖ E^{'}$ and does not falsify any clause of $T (G, f)$ . $T [α]$ be the tree obtained form T applying the substitution α to all the queried formulas. Size and depth do not change, hence $T [α]$ defines a derivation $⊢_{d} \neg T (G, f) [α]$ of size S. $\neg T (G, f)$ has the form $\neg ⋀_{v \in V} Par (v)$ , where $Par (v)$ is a parity condition of the vertex v. Hence, $\neg T (G, f) [α]$ is of the form $\neg ⋀_{i} Par (v) [α]$ . If $v \notin V^{'}$ , then α assigns values to all variables from $Par (v)$ , since α does not falsify $Par (v)$ , α satisfies $Par (v)$ , hence $Par (v) [α]$ is identically true. If $v \in V^{'}$ , then $Par (v) [α]$ is a parity statement depending on variables $x_{e}$ , where $e \in E^{'}$ is incident to v. Hence, for $v \in V^{'}$ , $Par (v) [α]$ is semantically equivalent to a parity condition of a Tseitin formula $T (H, φ^{'})$ for some charging $φ^{'}$ . Let Δ be the maximal degree of G. Then every parity condition of $T (H, φ^{'})$ or $T (G, φ)$ depends on at most Δ variables. Notice that since we represent parities in CNF, $| T (G, f) | ⩾ 2^{Δ}$ . By Lemma 10, there is a derivation $\neg T (G, f) [α] ⊢_{O (1)} \neg T (H, f^{'})$ of size $poly (| T (G, f) |)$ . The claim follows using the size S, depth d derivation of $\neg T (G, f) [α]$ together with Lemma 2. □

A 1-substitution for a formula φ is a partial function mapping variables of φ into literals of φ. After applying a 1-substitution σ to φ, the depth of the new formula $φ [σ]$ can increase by one. However 1-substitutions are closed under composition: if $σ_{1}$ maps $[y \mapsto \neg z]$ and $σ_{2}$ maps $[x \mapsto \neg y]$ , then $σ = σ_{1} \circ σ_{2}$ is the 1-substitution $[x \mapsto z, y \mapsto \neg z]$ . We use 1-substitutions to handle in $T (G, f)$ the operation of vertex suppression on the graph G. Let $G = (V, E)$ be a graph and $v \in V$ be a node and let $T (G, f)$ be a Tseitin formula on G. Let v be a degree-2 vertex v in G with neighbours u and w. Consider the following 1-substitution $σ_{v}$ and the charge function $f_{v}$ for $[G ∖_{s} v]$ : $σ_{v} = {\begin{matrix} [x_{(v, w)} \mapsto x_{(w, u)}, x_{(v, u)} \mapsto x_{(w, u)}] & if f (v) = 0 \\ [x_{(v, w)} \mapsto x_{(w, u)}, x_{(v, u)} \mapsto \neg x_{(w, u)}] & if f (v) = 1 \end{matrix} f_{v} (z) = {\begin{matrix} f (z) & if z \in V ∖ {u, v} \\ f (u) + f (v) & if z = u \end{matrix}$

Let $G (V, E)$ be a graph and $f : V \to {0, 1}$ be a charging. Let A be a finite set. We say that a formula Ψ is a pseudo Tseitin formula based on G and f with fake vertices in A, and we write Ψ is $T_{A}^{⁎} (G, f)$ , if Ψ has the form $⋀_{v \in V \cup A} ψ_{v}$ , where

1.
for all $v \in V$ , $ψ_{v}$ is a propositional formula depending on variables $x_{e}$ for all edges e incident to v. And $ψ_{v}$ is semantically equivalent to the parity condition $Par (v)$ of $T (G, f)$ .
2.
for all $v \in A$ , $ψ_{v}$ is a tautology.

Lemma 13

Let $G (V, E)$ be a connected constant-degree graph over n vertices. Let $[G ∖_{s} v]$ be the graph obtained after the suppression of a degree-2 vertex v in G. If Ψ is $T_{A}^{⁎} (G, f)$ , then $Ψ [σ_{v}]$ is $T_{A \cup {v}}^{⁎} ([G ∖_{s} v], f_{v})$ .

Proof

Assume that v is linked to two vertices w and u in G. Let A be the set of fake vertices of Ψ so Ψ has the form $⋀_{x \in V \cup A} ψ_{x}$ , hence $Ψ [σ_{v}]$ is $⋀_{x \in V \cup A} ψ_{x} [σ_{v}]$ . For $x \in A$ , $ψ (x)$ is a tautology, hence $ψ_{x} [σ_{v}]$ is also a tautology. By the definition of $σ_{v}$ , $ψ_{v} [σ_{v}]$ is a tautology. It is not hard to verify that for $x \in V ∖ {v}$ , $ψ_{x} [σ_{v}]$ is equivalent to parity condition of $T ([G ∖_{s} v], f_{v})$ . Hence, $Ψ [σ_{v}]$ is $T_{A \cup {v}}^{⁎} ([G ∖_{s} v], f_{v})$ □

Lemma 14

Let $G (V, E)$ be a graph and $f : V \to {0, 1}$ and $W = {v_{1}, \dots, v_{k}}$ be degree 2 nodes in V suppressed in that order from G and $[G ∖_{s} W]$ be the resulting graph. Let $σ_{i}$ be the corresponding 1-substitutions and let $σ = σ_{k} \circ \dots \circ σ_{1}$ . Then there is a charging $f_{k}$ of G such that if Ψ is $T_{A}^{⁎} (G, f)$ , then $Ψ [σ]$ is $T_{A \cup W}^{⁎} ([G ∖_{s} W], f_{k})$ .

Proof

By induction on $k ⩾ 0$ and using Lemma 13 we prove that $Ψ [σ_{1}] \dots [σ_{k}]$ is $T_{A \cup W}^{⁎} ([G ∖_{s} W], f_{k})$ , for $f_{k}$ given by repeated applications of Lemma 13.

Since the composition of 1-substitutions removes double negations, then the only difference between $Ψ [σ_{1}] \dots [σ_{k}]$ and $Ψ [σ]$ can be only in the number of negations in front of the same occurrence of a variable, though the parity of the number of negations is preserved. Hence for all $v \in V$ the semantical equivalence of the $ψ_{v}$ 's in $Ψ [σ_{1}] \dots [σ_{k}]$ and $Ψ [σ]$ is preserved. Then $Ψ [σ]$ too is $T_{A \cup W}^{⁎} ([G ∖_{s} W], f_{k})$ . □

Lemma 15

Let G be a connected graph on n vertices and with the maximal degree at most 3. Let H be obtained from G by several suppressions. Assume that there is a derivation of $\neg T (G, f)$ of size S and depth d. Then for some charging $f_{k}$ there is a derivation of $\neg T (H, f_{k})$ of size $O (S) + poly (n)$ and depth $d + O (1)$ .

Proof

Assume that, in order, to get H from G we have to apply suppressions for vertices $W = {v_{1}, \dots, v_{k}}$ . Let $σ_{i}$ be the 1-substitutions corresponding to the suppression of $v_{i}$ , and let $σ = σ_{k} \circ \dots \circ σ_{1}$ . $T (G, f)$ is $T_{\emptyset}^{⁎} (G, f)$ . Let $f_{k}$ be the charging given by Lemma 14 applied to $T (G, f)$ and $[G ∖_{s} W] = H$ . Then $T (G, f) [σ]$ is $T_{W}^{⁎} (H, f_{k})$ . We apply the 1-substitution σ to the given derivation of $\neg T (G, f)$ and we get a derivation of $\neg T (G, f) [σ]$ of size $O (S)$ and depth at most $d + 1$ . By Lemma 10, applied on $T (G, f) [σ]$ and $T (H, f_{k})$ , there is a derivation $\neg T (G, f) [σ] ⊢_{d + O (1)} \neg T (H, f_{k})$ of size $poly (n)$ . Combining the two derivations together by Lemma 2 we obtain a derivation $⊢_{d + O (1)} T (H, f_{k})$ of size $O (s) + poly (n)$ . □

3.2. From walls to grids

Lemma 16

If there exists a derivation $⊢_{d} \neg T (W_{n}, f)$ of size S, then there exists a derivation $⊢_{d + O (1)} \neg T (M_{n}, f^{'})$ of size $O (S) + poly (n)$ , where $M_{n}$ is a connected constant-degree graph that contains $H_{n, ⌊ \frac{n - 1}{2} ⌋}$ as a subgraph.

Proof

Consider a set I of all the horizontal edges of $W_{n}$ that belong to odd columns (on Fig. 4, Fig. 5 edges from I are wavy). I is a matching, i.e. no two edges from I are incident to the same vertex. If we contract all edges from I, we get the graph $M_{n}$ that for odd n coincides with $H_{n, \frac{n - 1}{2}}$ and for even n coincides with a graph that is obtained from $H_{n, ⌊ \frac{n}{2} ⌋}$ by the removal of several edges from the last vertical (see Fig. 4, Fig. 5). For every $e \in I$ we denote its left vertex by $u_{e}$ and the right vertex by $v_{e}$ . Let $E_{u_{e}}$ be the set of edges of $W_{n}$ incident to $u_{e}$ except e. Let $τ_{e}$ denote a CNF formula encoding $⨁_{f \in E_{u_{e}}} x_{f} = f (u_{e})$ .

Consider a game tree T for the derivation of the Tseitin tautology $\neg T (W_{n}, f)$ of size S and depth d. To every formula used in this tree we apply the substitution that replaces every occurrence of $x_{e}$ with $τ_{e}$ . We denote the resulting tree by $T^{'}$ .

Notice that $T^{'}$ is a correct game tree of a derivation $⊢_{d + O (1)} \neg F$ , where F is obtained from $T (W_{n}, f)$ by the same substitution. The depth of this derivation is increased by at most a constant since in several leaves we hang a formula of constant depth; here we also use that I is a matching and thus we do not add new occurrences of variables corresponding edges from I. The size of $τ_{e}$ is $O (1)$ , hence any formula from the derivation is increased in at most a constant factor, thus the size of the derivation defined by the tree $T^{'}$ is $O (S)$ .

We define a function $f^{'}$ on vertices of $M_{n}$ as follows. If a vertex w of the graph $M_{n}$ is obtained by merging the vertices $w^{'}, w^{″}$ of the graph $W_{n}$ , then $f^{'} (w) = (f (w^{'}) + f (w^{″})) \mod 2$ . If the vertex w of $H_{n, ⌊ n / 2 ⌋}$ is obtained from the vertex w of $W_{n}$ , then $f^{'} (w) = f (w)$ .

Now we show how to derive $\neg T (M_{n}, f^{'})$ from ¬F. $T (W_{n}, f)$ is a Tseitin formula and it has the following structure: $⋀_{v \in V} ψ_{v}$ , where V is the set of vertices of $W_{n}$ and $ψ_{v}$ is a CNF formula encoding a parity condition for the vertex v. F differs from $T (W_{n}, f)$ only in conditions corresponding to vertices that are incident to an edge from I (if n is even, then there are vertices in $W_{n}$ that are not incident to any edge from I). Notice that F has the form $⋀_{v \in V} ψ_{v}^{'}$ where $ψ_{v}^{'}$ is obtained by substitution from $ψ_{v}$ . Let $w = u_{e}$ for some $e \in I$ , then the formula $ψ_{w}^{'}$ is identically true. If $w = v_{e}$ , then the condition $ψ_{w}^{'}$ is equivalent to the parity condition of the merged vertex ${u_{e}, v_{e}}$ in the Tseitin formula $T (M_{n}, f^{'})$ , but $ψ_{w}^{'}$ is not written in canonical form.

Since all degrees in $M_{n}$ are at most 4, then by Lemma 10 there exists a derivation $\neg F ⊢_{d + O (1)} \neg T (M_{n}, f^{'})$ of size $poly (n)$ . The claim follows by Lemma 2. □

3.3. Putting it all together

We use Håstad's Theorem from [28].

Theorem 17

[28]

There is a constant $K > 0$ such that for $d ⩽ \frac{K \log n}{\log \log n}$ any depth d derivation of $\neg T (H_{n, n}, f))$ has size at least $2^{n^{Ω (1 / d)}}$ .

Theorem 18

There exist constants $K > 0$ and $C > 0$ such that for every connected graph G of treewidth t and every $d ⩽ \frac{K \log n}{\log \log n} - C$ , any depth d derivation of $\neg T (G, f))$ has size at least $2^{t^{Ω (1 / d)}}$ .

Proof

Suppose that $\neg T (G, f)$ have a derivation of size S and depth d. By Corollary 9 we know that G contains the wall $W_{r}$ as a topological minor, where $r = Ω (t^{λ})$ . Consider a sequence of operations (edge/vertex removals and suppressions) that transform G to $W_{r}$ . Assume that removals do not follow suppressions. And let $G^{'}$ be a subgraph of G that is obtained from G by application of all removals (hence, $W_{r}$ can be obtained from $G^{'}$ by application of several suppressions).

By Lemma 12, for some $f^{'}$ there is a derivation of $\neg T (G^{'}, f^{'})$ of size $poly (| T (G, f) |) + S$ and depth $d + O (1)$ . Since $W_{r}$ can be obtained from $G^{'}$ by application of several suppressions, $G^{'}$ is connected. Suppressions can not increase the degrees, hence all degrees in $G^{'}$ are at most 3. By Lemma 15, for some $f^{″}$ there is a derivation of $\neg T (W_{r}, f^{″})$ of size $poly (| T (G, f) |) + S$ and depth $d + O (1)$ . By Lemma 16, for some $f^{‴}$ there is a derivation of $\neg T (M_{r}, f^{‴})$ of size $poly (| T (G, f) |) + O (S)$ and depth $d + O (1)$ , where $M_{r}$ is connected constant-degree graph containing $H_{⌊ (r - 1) / 2 ⌋}$ as a subgraph. And finally by Lemma 12, for some $f^{⁗}$ there is a Frege derivation of $T (H_{⌊ (r - 1) / 2 ⌋}, f^{⁗})$ of size $poly (| T (G, f) |) + O (S)$ and depth $d + O (1)$ . Notice that S is the size of a derivation of $\neg T (G, f)$ , hence $S ⩾ | T (G, f) |$ . Thus, for some constants C and c there is a derivation of $\neg T (H_{⌊ (r - 1) / 2 ⌋}, f^{⁗})$ of size $S^{c}$ and depth $d + C$ .

By Theorem 17, there is a constant K such that if $d + C ⩽ \frac{K \log n}{\log \log n}$ , then $S^{c} ⩾ 2^{{⌊ (r - 1) / 2 ⌋}^{Ω (1 / (d + C))}}$ . Hence $S ⩾ 2^{r^{Ω (1 / d)}}$ and, thus, $S ⩾ 2^{t^{Ω (1 / d)}}$ . □

4. The upper bound

In this section we prove the following Theorem:

Theorem 19

Let $G (V, E)$ be a connected undirected graph and $T (G, f)$ be an unsatisfiable Tseitin formula. Then for all large enough d the formula $\neg T (G, f)$ has a derivation of depth d and size $2^{tw {(G)}^{O (1 / d)}} poly (| T (G, f) |)$ .

Let us give the outline of the proof:

1.
First, we define the compact representation of Parity. The main idea behind this is using associativity of the operation: we split the input on chunks of suitable size and construct the formula recursively. The first part of the section describes the technical lemmas concerning the compact representation.
2.
The next part of the section describes how to emulate summation of linear equations modulo 2 using the compact representation of Parity.
3.
In the last part of the section, we use the notion of tree-partition width of the graph. Using the small cuts of tree-partition, we construct a proof which tries to detect local contradictions of a number of variables, proportional to tree-partition width.

4.1. A compact representation of parity

Let $t_{1}, t_{2}, \dots, t_{d}$ be natural numbers, where d is a non-negative integer. Let $U_{0}, U_{1}, \dots, U_{d}$ be partitions of a finite set F; it is possible that some elements of $U_{i}$ for $i \in {0, 1, \dots, d}$ are empty. We say that a list of partitions $U = (U_{0}, U_{1}, \dots, U_{d})$ is a $(t_{1}, \dots, t_{d})$ -refinement of F if the following conditions hold:

1.
$U_{0}$ consists of the only element $U_{0, 1} = F$ .
2.
For every i, $U_{i + 1}$ is a subpartition of $U_{i}$ such that every element of $U_{i}$ is split into $t_{i + 1}$ parts. Hence, $U_{i}$ split F into $m_{i}$ parts: $U_{i, 1}, U_{i, 2}, \dots, U_{i, m_{i}}$ , where $m_{i} = \prod_{j = 1}^{i} t_{j}$ .
3.
All elements of $U_{d}$ have cardinality at most 1.

We refer to elements of

U_{i}

for

i \in {0, 1, \dots, d}

as blocks of the refinement.

Let U be a $(t_{1}, \dots, t_{d})$ -refinement of a set F and let $U_{i, j}$ be one of the blocks of this refinement. Then U induces on each of the blocks $U_{i j}$ a $(t_{i + 1}, \dots, t_{d})$ -refinement $U^{'}$ which is obtained by restricting $U_{i}, \dots, U_{d}$ to the set $U_{i j}$ . $U^{'}$ is called a sub-refinement of $U_{i j}$ in U.

Lemma 20

Let F be a set of size n and $d ⩾ 0$ be an integer. Let $t_{1}, \dots, t_{d}$ be integers such that $t_{1} \cdot t_{2} \cdot \dots \cdot t_{d} ⩾ n$ . Then there exists a $(t_{1}, \dots, t_{d})$ -refinement U of F.

Proof

We define $U_{d}$ as n singletons each containing one element of F and $t_{1} \cdot \dots \cdot t_{d} - n$ empty sets. For each $i < d$ we construct $U_{i}$ from $U_{i + 1}$ as follows. We split the $t_{i + 1} \cdot \dots \cdot t_{d}$ blocks of the partition $U_{i + 1}$ into groups of size $t_{i + 1}$ and define $U_{i, 1}$ as the union of the elements of the first group, $U_{i, 2}$ as the union of the elements of the second group and etc. □

For $a \in {0, 1}$ and natural number n we define a Boolean function ${PARITY}_{n}^{a} : {0, 1}^{n} \to {0, 1}^{n}$ such that ${PARITY}_{n}^{a} (x_{1}, \dots, x_{n}) = 1$ iff $⨁_{i = 1}^{n} x_{i} = a$ for all $x_{1}, \dots, x_{n} \in {0, 1}$ .

Lemma 21

Let n and d be positive integers and U be a $(t_{1}, t_{2}, \dots, t_{d})$ -refinement of $[n]$ . Then there exists a formula representing ${PARITY}_{n}^{b}$ of depth at most $3 d + 1$ and of size $\prod_{i = 1}^{d} 2^{t_{i} + 1} t_{i}$ .

Proof

Let us construct a formula of the needed size and depth for each of the chunks in the refinement, starting from the smallest ones. More formally, we do that by backward induction on i from d to 0. We prove that for every $j \in [\prod_{k = 1}^{i} t_{k}]$ , there is a formula representing $⨁_{k \in U_{i, j}} x_{k}$ of depth $3 (d - i)$ and of size $\prod_{q = i + 1}^{d} 2^{t_{q} + 1} t_{q}$ .

If $i = d$ , then $| U_{d, j} | ⩽ 1$ , hence $⨁_{k \in U_{i, j}} x_{k}$ is either 0 or a variable $x_{k}$ and thus has size 1 and depth 0.

Assume that $i < d$ . Let $ℓ_{1}, ℓ_{2}, \dots, ℓ_{t_{i + 1}}$ be such that $U_{i, j} = U_{i + 1, ℓ_{1}} \cup U_{i + 1, ℓ_{2}} \cup \dots \cup U_{i + 1, ℓ_{t_{i + 1}}}$ . Let for $r \in [t_{i + 1}]$ , $β_{r}$ be a representation of $⨁_{k \in U_{i + 1, ℓ_{r}}} x_{k}$ of size $\prod_{q = i + 2}^{d} 2^{t_{q} + 1} t_{q}$ and depth $3 (d - i - 1)$ that exists by the induction hypothesis. Consider a CNF-representation of $β_{1} \oplus \dots \oplus β_{t_{i + 1}}$ : $⨁_{k \in U_{i, j}} x_{k} = ⋀_{\begin{matrix} S \subseteq {1, \dots, t_{i + 1}} \\ | S | \mod 2 = 0 \end{matrix}} (⋁_{s \in S} \neg β_{s} \lor ⋁_{s \notin S} β_{s})$ . After the substitution of the representations of $β_{1}, \dots, β_{t_{i + 1}}$ we obtain a formula of size at most $2^{t_{i + 1}} t_{i + 1} \cdot \prod_{q = i + 2}^{d} 2^{t_{q} + 1} t_{q} + 2^{t_{i + 1}} t_{i + 1} ⩽ \prod_{q = i + 1}^{q} 2^{t_{q} + 1} t_{q}$ and of depth $3 (d - i - 1) + 3 = 3 (d - i)$ .

Therefore we have constructed a representation of ${PARITY}_{n}^{1}$ of the needed size and depth. The representation of ${PARITY}_{n}^{0}$ could be constructed as ¬φ where φ is the obtained representation of ${PARITY}_{n}^{1}$ . □

We call the representation of ${PARITY}_{n}^{a}$ obtained by Lemma 21 the compact representation of ${PARITY}_{n}^{a}$ with respect to a $(t_{1}, \dots, t_{d})$ -refinement U.

Let us define for $S \subseteq [n]$ and for $a \in {0, 1}$ , ${PARITY}_{n, S}^{a} (x_{1}, \dots, x_{n}) = (\neg a) \oplus ⨁_{i \in S} x_{i}$ . We define a compact representation of ${PARITY}_{n, S}^{a}$ with respect to a $(t_{1}, \dots, t_{d})$ -refinement U as the result of substitutions $x_{j} : = 0$ for all $j \notin S$ to the compact representation of ${PARITY}_{n}^{a}$ with respect to U. We denote the compact representation of ${PARITY}_{n, S}^{a} (x_{1}, x_{2}, \dots, x_{n})$ w.r.t. U by $Φ^{a} (S, U)$ .

Lemma 22

Let U be a $(t_{1}, \dots, t_{d})$ -refinement of $[n]$ and $U^{'}$ be a sub-refinement of $U_{i j}$ in U. Then for every $S \subseteq U_{i j}$ there exists a derivation $Φ^{a} (S, U^{'}) ⊢_{3 d + O (1)} Φ^{a} (S, U)$ of size at most $4 | Φ^{a} (S, U) |^{3}$ .

Proof

Let $ψ_{1} : = x$ and $ψ_{2}$ be the formula obtained from $Φ^{a} (S, U)$ by replacement of all subformulas $Φ^{a} (U^{'})$ with x. Clearly $ψ_{1}$ and $ψ_{2}$ are semantically equivalent. Then let us apply Corollary 5 to $ψ_{1}$ , $ψ_{2}$ , $k = 1$ and $φ_{1} = Φ^{a} (S, U^{'})$ . Then there exists a derivation of $ψ_{1} [x \leftarrow Φ^{a} (S, U^{'})] ⊢_{3 d + O (1)} ψ_{2} [x \leftarrow Φ^{a} (S, U^{'})]$ of size $2^{1} (| ψ_{1} |^{2} + | ψ_{2} |^{2}) | φ_{1} | = 2 (1 + | Φ^{a} (S, U) |^{2}) | Φ^{a} (S, U^{'}) | ⩽ 4 | Φ^{a} (S, U) |^{3}$ . □

4.2. Summation of linear equations

Let $S △ T$ be the symmetric difference of sets S and T i.e. $S △ T = (S \cup T) ∖ (S \cap T)$ .

Proposition 23

Let U be a $(t_{1}, \dots, t_{d})$ -refinement of $[n]$ . For any $S \subseteq [n]$ there exists a derivation $\neg Φ^{a} (S, U) ⊢_{3 d + O (1)} Φ^{1 \oplus a} (S, U)$ of size at most $2 (| Φ^{1} (S, U) | + | Φ^{0} (S, U) |)$ .

Proof

If $a = 1$ then the premise equals the conclusion, so an empty derivation is sufficient. If $a = 0$ we need to remove double negation so Pavel asks $Φ^{0} (S, U)$ . If the answer is 1 then it is an immediate contradiction with the premise and if the answer is 0 it is an immediate contradiction with the conclusion. □

Lemma 24

Let U be a $(t_{1}, \dots, t_{d})$ -refinement of $[n]$ . Then there exist a constant c and a derivation $Φ^{a} (S, U), Φ^{b} (T, U) ⊢_{3 d + O (1)} Φ^{a \oplus b} (S △ T, U)$ of size at most $c \cdot | Φ^{1} (\emptyset, U) |^{6}$ . We write ∅ here to stress that the size of $Φ^{a} (S, U)$ does not depend on S.

Proof

Let us prove this Lemma by induction on d. The base case: $d = 0$ . Since $U_{0}$ is the last layer of refinement, it contains only singletons. On the other hand by the definition $U_{0} = {[n]}$ , thus, $n = 1$ and $Φ^{a} (S, U), Φ^{b} (T, U)$ and $Φ^{a \oplus b} (S △ T, U)$ all depend on one variable $x_{1}$ . Thus by Lemma 4, there exists a derivation $Φ^{a} (S, U) \land Φ^{b} (T, U) ⊢_{2} Φ^{a \oplus b} (S △ T, U)$ of constant size. Clearly $Φ^{a} (S, U) \land Φ^{b} (T, U)$ is derivable from $Φ^{a} (S, U)$ $Φ^{b} (T, U)$ by a derivation of constant depth and size.

If $d > 0$ , let $V^{1}, \dots, V^{t_{1}}$ be the sub-refinements of $U_{1, 1}, \dots, U_{1, t_{1}}$ in U respectively where $[n] = U_{1, 1} \cup \dots \cup U_{1, t_{1}}$ . Recall that by definition $Φ^{1} (X, U) = \underset{\begin{matrix} R \subseteq [t_{1}] \\ | R | \mod 2 = 0 \end{matrix}}{⋀} (\underset{i \in R}{⋁} \neg Φ^{1} (X \cap U_{1, i}, V^{i}) \lor \underset{i \notin R}{⋁} Φ^{1} (X \cap U_{1, i}, V^{i})) .$ We view this representation as CNF in variables $Φ^{1} (X \cap U_{1, i}, V^{i})$ for $i \in [t_{1}]$ . Recall that by definition $Φ^{0} (X, U) = \neg Φ^{1} (S, U)$ .

Let us describe a strategy of Pavel in the game with initial conditions $Φ^{a} (S, U) = 1$ , $Φ^{b} (T, U) = 1$ and $Φ^{a \oplus b} (S △ T, U) = 0$ .

Pavel asks Sam the values of the following $3 t_{1}$ formulas: $Φ^{1} (S \cap U_{1, i}, V^{i})$ , $Φ^{1} (T \cap U_{1, i}, V^{i})$ , $Φ^{1} ((S △ T) \cap U_{1, i}, V^{i})$ for $i \in [t_{1}]$ . There are $2^{3 t_{1}}$ possible combinations of Sam's answers. The total size of the formulas is at most $2 \cdot 2^{3 t_{1}} \cdot | Φ^{1} (\emptyset, V^{1}) |$ . Let us show how Pavel wins in each of them. Let $α_{i}, β_{i}, γ_{i}$ denote Sam's answers to $Φ^{1} (S \cap U_{1, i}, V^{i})$ , $Φ^{1} (T \cap U_{1, i}, V^{i})$ , $Φ^{1} ((S △ T) \cap U_{1, i}, V^{i})$ respectively for $i \in [t_{1}]$ .

If $⨁_{i \in [t_{1}]} α_{i} \neq a$ , then we can get a contradiction with $Φ^{a} (S, U)$ . Indeed consider a formula $ψ : = ⋀_{i = 1}^{t_{1}} Φ^{α_{i}} (S \cap U_{1, i}, V^{i}) \land Φ^{a} (S, U)$ and let L be the size of ψ if we consider it as a formula in variables $Φ^{1} (S \cap U_{1, i}, V^{i})$ . Clearly $L ⩽ 2^{t_{1} + 1} \cdot t_{1}$ . By Corollary 5, there is a derivation of 0 from ψ of size at most $2^{t_{1}} L^{2} (\sum_{i = 1}^{t_{1}} | Φ^{1} (\emptyset, V^{i}) |) ⩽ 2^{3 t_{1} + 4} t_{1}^{3} | Φ^{1} (\emptyset, V^{1}) |$ . Pavel asks Sam the value of ψ and in both cases gets a contradiction. If the answer is 0 then it is a contradiction with the conjuncts so Pavel proceeds to ask all subformulas of ψ starting with the deeper ones until he gets an immediate contradiction. If the answer is 1 we get a contradiction by Corollary 5. The total size of all such derivation for all possible combinations of Sam's answers is at most $2^{3 t_{1}} \cdot \max {| ψ |^{2}, 2^{3 t_{1} + 4} t_{1}^{3} | Φ^{1} (\emptyset, V^{1}) |} ⩽ 2^{6 t_{1} + 4} t_{1}^{3} | Φ^{1} (\emptyset, V^{1}) |$ . Adding the size of the $3 t_{1}$ preliminary questions we get $2^{6 t_{1} + 4} t_{1}^{3} | Φ^{1} (\emptyset, V^{1}) | + 2 \cdot 2^{3 t_{1}} \cdot | Φ^{1} (\emptyset, V^{1}) | < 20 \cdot 2^{6 (t_{1} + 1)} t_{1}^{6} | Φ^{1} (\emptyset, V^{1}) |^{6} ⩽ 20 | Φ^{1} (\emptyset, U) |^{6}$ . The cases when $⨁_{i \in [t_{1}]} β_{i} \neq b$ or $⨁_{i \in [t_{1}]} γ_{i} \neq a \oplus b$ are similar.

Let us consider the case where $⨁_{i \in [t_{1}]} α_{i} = a$ , $⨁_{i \in [t_{1}]} β_{i} = b$ and $⨁_{i \in [t_{1}]} γ_{i} = 1 \oplus a \oplus b$ . In this case there exists $i_{0} \in [t_{1}]$ such that $α_{i_{0}} + β_{i_{0}} \neq γ_{i_{0}}$ . We derive a contradiction using Sam's answers $Φ^{1} (S \cap U_{1, i_{0}}, V^{i_{0}}) = α_{i}$ , $Φ^{1} (T \cap U_{1, i_{0}}, V^{i_{0}}) = β_{i}$ and $Φ^{1} ((S △ T) \cap U_{1, i_{0}}, V^{i_{0}}) = γ_{i}$ . By Proposition 23 we may assume that Sam's answers are $Φ^{α_{i_{0}}} (S \cap U_{1, i_{0}}, V^{i_{0}}) = 1$ , $Φ^{β_{i_{0}}} (T \cap U_{1, i_{0}}, V^{i_{0}}) = 1$ and $Φ^{γ_{i_{0}}} ((S △ T) \cap U_{1, i_{0}}, V^{i_{0}}) = 1$ . By the induction hypothesis there exists a derivation $Φ^{α_{i_{0}}} (S \cap U_{1, i_{0}}, V^{i_{0}}), Φ^{β_{i_{0}}} (T \cap U_{1, i_{0}}, V^{i_{0}}) ⊢_{3 d + O (1)} Φ^{1 \oplus γ_{i_{0}}} ((S △ T) \cap U_{1, i_{0}}, V^{i_{0}})$ of size at most $c | Φ^{1} (\emptyset, V^{1}) |$ so we get an immediate contradiction with $Φ^{γ_{i_{0}}} ((S △ T) \cap U_{1, i_{0}}, V^{i_{0}})$ . The total size of the derivation is at most

Since $| Φ^{1} (\emptyset, U) | = 2^{t_{1} + 1} t_{1} \cdot | Φ^{1} (\emptyset, V^{1}) |$ , for a large enough c the size of derivation does not exceed $c | Φ^{1} (\emptyset, U) |^{6}$ . □

Lemma 25

Let U be a $(t_{1}, \dots, t_{d})$ -refinement of $[n]$ . Let $S_{1}, S_{2}, \dots, S_{k} \subseteq [n]$ and $a_{1}, \dots, a_{k} \in {0, 1}$ . Then there exists a constant c such that:

1.
There exists a derivation $Φ^{a_{1}} (S_{1}, U), Φ^{a_{2}} (S_{2}, U), \dots, Φ^{a_{k}} (S_{k}, U) ⊢_{3 d + O (1)} Φ^{a_{1} \oplus \dots \oplus a_{k}} (S_{1} △ \dots △ S_{k}, U)$ of size at most $c \cdot k \cdot | Φ^{1} (\emptyset, U) |^{6}$ .
2.
If $⋀_{i \in [k]} (⨁_{j \in S_{i}} x_{j} = a_{i})$ is unsatisfiable then there exists a derivation
$Φ^{a_{1}} (S_{1}, U), Φ^{a_{2}} (S_{2}, U), \dots, Φ^{a_{k}} (S_{k}, U) ⊢_{3 d + O (1)} 0$ of size at most $c \cdot k \cdot | Φ^{1} (\emptyset, U) |^{6}$ .

Proof

The proof of (1) is simply $(k - 1)$ consecutive applications of Lemma 24 using Lemma 2. The proof of (2) is based on a well-known fact: a system of linear equations is unsatisfiable if and only if the contradiction $0 = 1$ can be obtained as a linear combination of the equations. In our case it means that there is a set $R : = {r_{1}, \dots, r_{m}} \subseteq [k]$ such that $S_{r_{1}} △ S_{r_{2}} △ \dots △ S_{r_{m}} = \emptyset$ and $⨁_{i \in R} a_{i} = 1$ .

$Φ^{a_{r_{1}} \oplus \dots a_{r_{m}}} (S_{r_{1}} △ \dots △ S_{r_{m}}) = Φ^{1} (\emptyset, U)$ . $Φ^{1} (\emptyset, U)$ is identically false, hence by Lemma 4 there is a derivation $Φ^{1} (\emptyset, U) ⊢_{3 d + 1} 0$ of size at most $4 | Φ^{1} (\emptyset, U) |^{2}$ .

Let us construct Pavel's strategy in the game with initial conditions $Φ^{a_{r_{1}}} (S_{r_{1}}, U) = 1, \dots, Φ^{a_{r_{m}}} (S_{r_{m}}, U) = 1$ and $Φ^{1} (\emptyset, U) = 0$ . Pavel asks Sam the value of $Φ^{1} (\emptyset)$ . If Sam answers 0 Pavel uses the strategy corresponding to $Φ^{a_{r_{1}}} (S_{r_{1}}), Φ^{a_{r_{2}}} (S_{r_{2}}), \dots, Φ^{a_{r_{k}}} (S_{r_{k}}) ⊢_{3 d + O (1)} Φ^{a_{r_{1}} \oplus a_{r_{2}} \oplus \dots \oplus a_{r_{k}}} (S_{r_{1}} △ S_{r_{2}} △ \dots △ S_{r_{k}})$ from (1). If Sam answers 1 Pavel uses the strategy corresponding to the derivation $Φ^{1} (\emptyset, U) ⊢_{3 d + 1} 0$ . □

4.3. Tree-partition-width

Let $G (V, E)$ be an undirected graph and $S_{1}, \dots, S_{m}$ be a partition of V. $S_{1}, \dots, S_{m}$ is a tree-partition of G if there exists a tree $T ([m], E_{T})$ such that every edge e of G connects either two vertices from the same part $S_{i}$ or connects a vertex from $S_{i}$ and a vertex from $S_{j}$ , where i and j are adjacent in T, i.e. $(i, j) \in E_{T}$ . A width of a tree-partition $S_{1}, S_{2}, \dots, S_{m}$ is the size of the largest set $S_{i}$ for $i \in [m]$ . A tree-partition width of a graph G is the smallest width among all tree-partitions of G. We denote the tree-partition width of G by $tpw (G)$ .

If we add a new vertex in the middle of every edge $(i, j)$ of the tree T and put the set $S_{i} \cup S_{j}$ on it, we will get a tree decomposition of G, hence $tw (G) ⩽ 2 tpw (G) - 1$ .

The following theorem shows an inequality in the other direction.

Theorem 26

[46]

If $tw (G) ⩾ 1$ , then $tpw (G) ⩽ 10 Δ (G) tw (G)$ , where $Δ (G)$ is the maximum degree of G.

So, $tw (G)$ and $tpw (G)$ coincide up to a multiplicative constants for constant degree graphs.

Theorem 27

Let $G (V, E)$ be a connected graph and let a Tseitin formula $T (G, f)$ be unsatisfiable. Then there exists a derivation $⊢_{3 d + O (1)} T (G, f)$ of size at most $poly (| T (G, f) |) \cdot 2^{{(tpw (G) Δ (G))}^{O (1 / d)}}$ , where $Δ (G)$ is the maximum degree of G.

Proof

Let $S_{1}, \dots, S_{m}$ be a tree-partition of G with width $tpw (G)$ and let $T ([m], E_{T})$ be the corresponding tree. Without loss of generality we assume that T is a rooted tree with the root m; for all $i \in [m - 1]$ , $p (i)$ denotes its parent and for all $i \in [m]$ , $s (i)$ denotes the set of direct successors of i. Without loss of generality we assume that $p (i) > i$ for all $i \in [m - 1]$ .

Since $T (G, f)$ is unsatisfiable and G is connected, $⨁_{v \in V} f (v) = ⨁_{i \in [m]} ⨁_{v \in S_{i}} f (v) = 1$ . We consider the sum $⨁_{i \in [m]} ⨁_{e \in E (S_{i}, V ∖ S_{i})} x_{e}$ . Since each $x_{e}$ occurs in the sum exactly twice, the sum (modulo 2) is 0 for all values of $x_{e}$ . Then for each assignment to ${x_{e}}_{e \in E}$ there exists $i_{0}$ such that $⨁_{v \in S_{i_{0}}} f (v) \neq ⨁_{e \in E (S_{i_{0}}, V ∖ S_{i_{0}})} x_{e}$ . The first part of Pavel's strategy is to find such $i_{0}$ .

Pavel will request parity of the sum of all edges between $S_{i}$ and $S_{j}$ for all $(i, j) \in E_{T}$ . In order to represent these formulas in a compact way we now define m different $(t_{1}, \dots, t_{d})$ -refinements $W^{1}, \dots, W^{m}$ ; for every i, $W^{i}$ is a refinement of the set $E (S_{i}, ⋃_{j \in s (i)} S_{j})$ of all edges connecting a vertex from $S_{i}$ with a vertex from $⋃_{j \in s (i)} S_{j}$ . We construct appropriate refinements $W^{i}$ later.

Pavel asks Sam the values of $⨁_{e \in E (S_{i}, S_{p (i)})} x_{e}$ represented as $Φ^{1} (E (S_{i}, S_{p (i)}), W^{p (i)})$ for $i \in [m - 1]$ in the increasing order until he finds $i_{0}$ such that $⨁_{e \in E (S_{i_{0}}, V ∖ S_{i_{0}})} x_{e} \neq ⨁_{v \in S_{i_{0}}} f (v)$ .

At the moment when Sam has answered the value of $Φ^{1} (E (S_{i}, S_{p (i)}), W^{p (i)})$ the values of $⨁_{e \in E (S_{i}, S_{j})} x_{e}$ for each j such that $(i, j) \in E_{T}$ are all determined, thus, the value of $⨁_{e \in E (S_{i}, V ∖ S_{i})} x_{e}$ is determined. If $⨁_{e \in E (S_{i}, V ∖ S_{i})} x_{e} \neq ⨁_{v \in S_{i}} f (v)$ Pavel proceeds to the next part of his strategy. Otherwise he continues to ask Sam similar questions corresponding to the vertices with larger indices.

Now we describe the strategy of Pavel in case if he finds $i_{0}$ . We are going to describe this case in terms of derivation using Lemma 2 multiple times. Consider a linear system that consists of the equation $⨁_{e \in E (S_{i_{0}}, V ∖ S_{i_{0}})} x_{e} = 1 \oplus ⨁_{v \in S_{i_{0}}} f (v)$ and all parity conditions of $T (G, f)$ of the vertices from $S_{i_{0}}$ . This linear system is unsatisfiable. We are going to use Lemma 25. In order to do it we need to derive the representations of these linear equations w.r.t. some refinement Q of a superset of $E (S_{i_{0}}, V)$ .

Let for $i \in [m]$ , $U^{i}$ be a $(t_{1}, t_{2}, \dots, t_{d})$ -refinement of the set $E (S_{i})$ of all edges connecting two vertices from $S_{i}$ (we construct these refinements in the end of the proof together with the refinements $W^{i}$ ). Let us define a $(3, t_{1}, \dots, t_{d})$ -refinement Q as a union of $(t_{1}, \dots, t_{d})$ -refinements $W^{i_{0}}, W^{p (i_{0})}$ and $U^{i_{0}}$ such that $Q_{1} = {E (S_{i_{0}}, ⋃_{j \in s (i_{0})} S_{j}), E (S_{p (i_{0})}, ⋃_{j \in s (p (i_{0}))} S_{j}), E (S_{i_{0}})}$ and for every $j \in {2, 3, \dots, d + 1}$ , $Q_{j}$ is the union of $W_{j - 1}^{i_{0}}, W_{j - 1}^{p (i_{0})}$ and $U_{j - 1}^{i_{0}}$ .

Let $a_{j}$ be Sam's answer to the question $⨁_{e \in E (S_{i_{0}}, S_{j})} x_{e}$ for each j that is a neighbour of $i_{0}$ in T, hence we may assume that $Φ^{a_{j}} (E (S_{i_{0}}, S_{j}), W^{i_{0}})$ for $j \in s (i_{0})$ and $Φ^{a_{p (i_{0})}} (E (S_{i_{0}}, E_{p (i_{0})}), W^{p (i_{0})})$ are already derived. By Lemma 22, we derive $Φ^{a_{j}} (E (S_{i_{0}}, S_{j}), Q)$ from $Φ^{a_{j}} (E (S_{i_{0}}, S_{j}), W^{i_{0}})$ for $j \in s (i_{0})$ and $Φ^{a_{p (i_{0})}} (E (S_{i_{0}}, S_{p (i_{0})}), Q)$ from $Φ^{a_{p (i_{0})}} (E (S_{i_{0}}, S_{p (i_{0})}), W^{p (i_{0})})$ , where $a_{j}$ are Sam's answers to the corresponding questions.

By the first part of Lemma 25 we derive $Φ^{1 \oplus (⨁_{v \in S_{i_{0}}} f (v))} (E (S_{i_{0}}, V ∖ S_{i_{0}}), Q)$ from the set of formulas ${Φ^{a_{j}} (E (S_{i_{0}}, S_{j}), Q) | (i_{0}, j) \in E_{T}}$ . We assume that the parity conditions of the vertices of G in $T (G, f)$ represented as CNF are asked at the beginning of the game i.e. for each $v \in V$ we know that the CNF representation of $⨁_{u : (u, v) \in E} x_{e}$ is true (if any clause of $T (G, f)$ is false Pavel queries all subformulas of $T (G, f)$ except subformulas of the clauses and gets an immediate contradiction, if any of the parity conditions is false it yields an immediate contradiction with the corresponding subset of clauses). Thus, by Lemma 4 we derive the representations of parity conditions of the vertices from $S_{i_{0}}$ w.r.t. Q. Since the corresponding linear system is unsatisfiable, using the second part of Lemma 25 we get a contradiction.

Claim 28

The size of the described game tree is at most $m \cdot 2^{3 Δ (G)} Δ^{2} (G) tpw (G) 2^{O (\sum_{i = 1}^{d} t_{i})}$ .

Proof

The game tree consists of m subtrees corresponding to each possible value of $i_{0}$ , $m - 1$ nodes corresponding to the questions $Φ^{1} (E (S_{i}, S_{p (i)}), W^{p (i)})$ for $i \in [m - 1]$ and $O (| V |)$ nodes corresponding to the initial questions about parity conditions of the vertices of G in CNF. The total size of formulas in these $O (| V |)$ nodes is $poly (| T (G, f) |)$ . Each of the $m - 1$ formulas corresponding to the questions $Φ^{1} (E (S_{i}, S_{p (i)}), W^{p (i)})$ has size $\prod_{i = 1}^{d} 2^{t_{i} + 1} t_{i}$ . Let us estimate the size of each of the m subtrees. It is the sum of the following values:

•
The derivation of the formulas $Φ^{1} (E (S_{i_{0}}, S_{j}), Q)$ for $j \in {p (i_{0})} \cup s (i_{0})$ . By Lemma 22 the size of each of these derivations is $O (\prod_{i = 1}^{d} 2^{3 t_{i}} t_{i}^{3})$ .
•
The derivation of the representations of parity conditions with respect to Q. By Lemma 4 the size of each of these derivations is $O (2^{Δ (G)} {(2^{Δ (G)} Δ (G) + \prod_{i = 1}^{d} 2^{t_{i}} t_{i})}^{2})$
•
The derivation of $Φ^{1 \oplus (⨁_{v \in S_{i_{0}}} f (v))} (E (S_{i_{0}}, V ∖ S_{i_{0}}), Q)$ . By the first part of Lemma 25 the size of this derivation is $Δ (G) tpw (G) 2^{O (\sum_{i = 1}^{d} t_{i})}$ .
•
The derivation of contradiction by the second part of Lemma 25 has size $(Δ (G) + 1) tpw (G) 2^{O (\sum_{i = 1}^{d} t_{i})}$ .

Each of these four summands is

2^{3 Δ (G)} Δ^{2} (G) tpw (G) 2^{O (\sum_{i = 1}^{d} t_{i})}

. □

Let us choose $t_{i} = {(Δ (G) tpw (G))}^{2 / d}$ for all $i \in [d]$ . Since $| S_{i} | ⩽ tpw (G)$ , $| E (S_{i}) | + | E (S_{i}, ⋃_{j \in s (i)} S_{j}) | ⩽ Δ (G) tpw (G)$ . Hence, the condition $\prod_{i = 1}^{d} t_{i} ⩾ Δ (G) tpw (G) ⩾ | E (S_{i}) | + | E (S_{i}, ⋃_{j \in s (i)} S_{j}) |$ holds and, thus, for all $i \in [m]$ the refinements $U^{i}, W^{i}$ exist by Lemma 20. If we substitute choosen values in the bound from Clam 28, we get the upper bound $m \cdot 2^{O (3 Δ (G) + d {(Δ (G) tpw (G))}^{2 / d})} = poly (| T (G, f) |) \cdot 2^{{(Δ (G) tpw (G))}^{O (1 / d)}}$ . □

Now we are ready to prove Theorem 19.

Proof of Theorem 19

Theorem 27 and Theorem 26 imply that there exists a constant c and a derivation $⊢_{3 d + O (1)} \neg T (G, f)$ of size at most $poly (| T (G, f) |) 2^{{(10 Δ^{2} (G) tw (G))}^{c / d}}$ . If $tw (G) > Δ (G)$ then we can rewrite our upper bound on the size as $poly (| T (G, f) |) 2^{{(10 tw (G))}^{3 c / d}}$ . If $tw (G) > 1$ then it is $poly (| T (G, f) |) 2^{{(tw (G))}^{O (1 / d)}}$ . If $tw (G) = 1$ then it is simply $poly (| T (G, f) |)$ . Otherwise if $tw (G) ⩽ Δ (G)$ we can rewrite the upper bound as $poly (| T (G, f) |) \cdot$ $2^{{(10 Δ (G))}^{3 c / d}} = poly (| T (G, f) |)$ if $3 c / d ⩽ 1$ . Thus, for $d ⩾ 3 c$ the upper bound is $poly (| T (G, f) |) \cdot$ $2^{tw {(G)}^{3 c / d}}$ . Therefore, for the both cases we have the needed upper bound. □

5. The complexity of Tseitin formulas in resolution

Resolution is a sound and complete propositional proof system suited for refuting unsatisfiable formulas in conjunctive normal form [17], [18]. A resolution refutation of a unsatisfiable CNF $F = C_{1} \land \dots \land C_{m}$ is a sequence of clauses $D_{1}, \dots, D_{t}$ such that $D_{t}$ is the empty clause □ and each clause $D_{i}$ in the sequence is either a clause $C_{j}$ of F or is obtained by the resolution rule applied to clauses $D_{j}$ and $D_{k}$ preceding $D_{i}$ in the sequence. The resolution rule is the following rule, where x is the resolved variable. $\frac{A \lor x B \lor \neg x}{A \lor B} Resolution rule$

The size of a resolution refutation is the number of clauses in the sequence. With $S (F ⊢)$ we denote the minimal size to refute F in resolution. The width of a clause is the number of literals in it; the width of a resolution refutation is the maximal width of a clause appearing in it. With $w (F ⊢)$ we denote the minimal width to refute F in resolution.

Resolution refutations can be arranged as directed acyclic graphs with leaves corresponding to clauses of F and a root corresponding to the empty clause. An important refinement of resolution is the system known as regular (or read-once) resolution. In this system refutations are constrained in such a way that in the refutation-graph in each path from the empty clause to a leaf the sequence of resolved variables is read-once, i.e. each variable appears at most once. Tree-like resolution is the restriction obtained by imposing that the refutation-graph must be a tree.

Since their introduction [43] Tseitin formulas play an important role in understanding the complexity of refutations in resolution and its restrictions [10], [44]. Since resolution is a special case of bounded-depth Frege, Theorem 18 is applicable to it as well. The lower bound that can be obtained from this theorem is $2^{Ω (tw {(G)}^{γ})}$ with $γ < \frac{1}{58} λ$ , where λ is the constant from the grid minor theorem, and $\frac{1}{58}$ comes from Håstad's lower bound (Theorem 17).

Recently in [31] Itsykson et al. proved that regular resolution refutation of $T (G, f)$ has size at least $2^{Ω (\frac{tw (G)}{\log n})}$ for every connected graph G and left open whether a similar result can be proved for unrestricted resolution. Theorem 34 improves the lower bound for general resolution comparing to the direct corollary from Theorem 18. In particular, Theorem 34 implies a lower bound $2^{Ω (tw (G))}$ for planar graphs.

5.1. Resolution lower bounds for $T (G, f)$ in terms of treewidth

Lemma 29

[31] Let $T (G, f)$ and $T (G, f^{'})$ be two unsatisfiable Tseitin formulas based on a connected graph G. Then the sizes of the shortest resolution refutations of this formulas coincide.

Let φ be a CNF and α be a partial assignment to the variables of φ. Let $φ |_{α}$ be a CNF which is obtained from $φ [α]$ by removing all satisfied clauses and removing the satisfied literals from the rest of the clauses.

Lemma 30

Let $G (V, E)$ and $G^{'} (V^{'}, E^{'})$ be connected graphs, and let $G^{'}$ is a topological minor of G, then for two unsatisfiable formulas $T (G, f)$ and $T (G^{'}, f^{'})$ , $S (T (G, f) ⊢) ⩾ S (T (G^{'}, f^{'}) ⊢)$ .

Proof

$G^{'}$ can be obtained from G by a sequence of vertex and edge deletions and edge suppressions. It is easy to see that these operations commute, so we may assume that we first delete edges and vertices and then suppress edges. Let $G^{″} (V^{″}, E^{″})$ be the graph that is obtained from G by all edge and vertex deletions. Observe that $G^{″}$ is connected since $G^{'}$ is obtained from it by vertex suppressions which do not affect connectivity. By Lemma 11 there is a partial assignment α with support ${x_{e} | e \in E ∖ E^{″}}$ that does not falsify any clause of $T (G, f)$ .

Let us show that $T (G, f) |_{α} = T (G^{″}, f^{″})$ where $f^{″} (v) = (f (v) + \sum_{e \in E^{″}; e is incident to v} α (e)) \mod 2$ . Indeed, $T (G, f) |_{α} = ⋀_{v \in V} Par (v) |_{α}$ where $Par (v)$ is the parity condition of the vertex v encoded in CNF. Observe that for $v \notin V^{″}$ $Par (v) |_{α}$ is identically true and for $v \in V^{″}$ it encodes in CNF the parity condition of v in $T (G^{″}, f^{″})$ .

Consider a resolution refutation $C_{1}, \dots, C_{k}$ of $T (G, f)$ . Observe that since α does not falsify axioms of $T (G, f)$ , $C_{1} |_{α}, \dots C_{k} |_{α}$ can be transformed into a resolution refutation of $T (G, f) |_{α}$ of size at most k. Thus $S (T (G^{″}, f^{″}) ⊢) ⩽ S (T (G, f) ⊢)$ .

Now we need to show that for a graph $G^{'} (V^{'}, E^{'})$ and for some $f^{'}$ that is obtained from $G^{″}$ by a sequence of vertex suppressions, $S (T (G^{'}, f^{'}) ⊢) ⩽ S (T (G^{″}, f^{″}) ⊢)$ . By induction it is sufficient to show this for just one suppression.

Assume that $G^{'}$ is the result of suppression of a vertex v neighbouring the vertices u and w, i.e. $G^{'} = G^{″} ∖_{s} v$ . Consider a vertex-charging of the set of vertices of $G^{'}$ , $\bar{f} (ℓ) = {\begin{matrix} f^{″} (ℓ) & if ℓ \neq w \\ f^{″} (w) + f^{″} (v) & if ℓ = w \end{matrix} .$ $\bar{f}$ is an odd-charging since it has the same parity as $f^{″}$ , which is an odd-charging since $T (G^{″}, f^{″})$ is unsatisfiable and $G^{″}$ is connected.

Consider the following procedure of obtaining $T (G^{'}, \bar{f})$ from $T (G^{″}, f^{″})$ . First substitute $x_{u v} : = x_{u w}; x_{v w} : = x_{u w}$ if $f^{″} (v) = 0$ and $x_{u v} : = \neg x_{u w}; x_{v w} : = x_{u w}$ if $f^{″} (v) = 1$ . Such substitution satisfies the clauses of $Par (v)$ in $T (G^{″}, f^{″})$ . Observe that application of the same substitution to each clause of the resolution refutation of $T (G^{″}, f^{″})$ results in a resolution refutation of $T (G^{'}, \bar{f})$ of the same or smaller length. By Lemma 29 there exists a refutation of $T (G^{'}, f^{'})$ of the same size, which completes the proof. □

The cyclicity of a graph G is the minimal ℓ for which the set of edges of G can be covered by cycles of length at most ℓ such that every edge is covered at most ℓ times.

Lemma 31

Let ${\bar{W}}_{n}$ be the result of removal all degree-1 vertices from $W_{n}$ . Then ${\bar{W}}_{n}$ has cyclicity at most 6.

Proof

We can cover all the edges by cycles corresponding to “bricks” of the wall (i.e. two cells of the grid with the edge between them removed). The length of each such cycle is 6 and since the graph $W_{n}$ is planar, each edge is covered by at most two cycles. □

Theorem 32

[3] $S (T (G, f) ⊢) = 2^{Ω (w (T (G, f) ⊢)) / ℓ {(G)}^{O (1)}}$ where $ℓ (G)$ is the cyclicity of G.

Theorem 33

[22] For a constant-degree graph $T (G, f)$ , $w (T (G, f) ⊢) = Ω (tw (G))$ .

Theorem 34

$S (T (G, f) ⊢) = 2^{Ω ({tw}^{λ} (G))}$ where λ is a constant from the grid-minor theorem.

Proof

Since $\frac{n}{2} \times n$ grid is a minor of ${\bar{W}}_{n}$ , $tw ({\bar{W}}_{n}) = Ω (n)$ . Then by Lemma 31 and Theorem 32, $S (T ({\bar{W}}_{n}, f) ⊢) = 2^{Ω (n)}$ . By Corollary 9 ${\bar{W}}_{k}$ is a topological minor of G where $k = Ω ({tw}^{λ} (G))$ . By Lemma 30 $S (T (G, f) ⊢) ⩾ S (T ({\bar{W}}_{k}, f^{'}) ⊢)$ which yields the desired result. □

5.2. Searching for resolution refutations of $T (G, f)$

A key concept in the field of automatic generation of proofs is that of automatizability of a proof system. Resolution is automatizable if there is an algorithm that, given a unsatisfiable CNF formula F of size n as input, it outputs a resolution refutation of F in time polynomial in $n + S (n)$ , where $S (n)$ is the length of a shortest refutation of F in resolution.

Given the importance of resolution in applied fields, investigation on automatizability of resolution received particular attention. Improving a result of Alekhnovich and Razborov in [2], automatizating resolution was recently found to be NP-hard [4]. These hardness results motivate the search of algorithms to generate resolution refutations for specific family of formulas like $T (G, f)$ .

Consider the next definitions from [3].

Definition 35

A class of unsatisfiable CNF formulas $F$ is (quasi-)automatizable with respect to a proof system Π if there exists a deterministic automatizing algorithm that, given an unsatisfiable formula $F \in F$ , returns its refutation in the proof system S in time which is (quasi-)polynomial in $| F | + S_{Π} (F ⊢)$ , where $S_{Π} (F ⊢)$ denotes the size of the shortest Π-refutation of F.

Definition 36

A class of unsatisfiable CNF formulas $F$ is smooth (respectively quasi-smoooth) if for all $F \in F$ , $w (F ⊢) ⩽ \log S (F ⊢)$ (resp. there is a constant C such that $w (F ⊢) ⩽ \log^{C} S (F ⊢)$ ).

Definition 37

A class $F$ of unsatisfiable CNFs is width-automatizable if there exists a deterministic algorithm that, given $F \in F$ , returns its resolution refutation of width $O (w (F ⊢))$ in time which is polynomial in $| F | + 2^{w (F ⊢)}$

Smoothness and quasi-smoothness are important properties for a class of formulas since, together with width-automatizability imply automatizability (quasi-automatizabilty) in resolution of that class of formulas.

Theorem 38

(Fact 2.7 [3]) If a class of unsatisfiable CNFs is both width-automatizable and (quasi-)smooth, then it is (quasi-)automatizable with respect to resolution.

The question whether Tseitin formulas $T (G, f)$ are (quasi-)automatizable with respect to resolution using previous theorem was investigated in [3]. There they proved that $T (G, f)$ are width-automatizable but obtained quasi-smoothess of $T (G, f)$ only for a restricted class of graphs G, namely those with constant cyclicity.

As a consequence of Theorem 1, we show that for all graphs the class of Tseitin formulas $T (G, f)$ is quasi-smooth, hence quasi-automatizable with respect to resolution answering to a question left in [3].

Corollary 39

For any graph G, $T (G, f)$ are quasi-smoooth, i.e. there is a constant C such that $w (T (G, f) ⊢) ⩽ \log^{C} S (T (G, f) ⊢)$ . Hence the class of Tseitin formulas is quasi-automatizable.

Proof

In [3], [22] it was established that $w (G) = \max {Δ (G), tw (L (G))} - 1$ , where $L (G)$ is the line graph (graph on edges) of G. It is known that $\max {Δ (G), \frac{1}{2} (tw (G) + 1)} - 1 ⩽ tw (L (G)) ⩽ (tw (G) + 1) Δ (G) - 1$ , (see, for example, [26]). By Theorem 1 and the fact that $T (G, f)$ is a CNF, we have that $S (G) ⩾ \max {2^{Δ (G)}, 2^{tw {(G)}^{ϵ}}}$ , for some $0 < ϵ < 1$ given by Theorem 1. Then $S (T G, f ⊢) ⩾ 2^{(tw {(G)}^{ϵ} + Δ (G)) / 2} ⩾ 2^{{(tw (G) Δ (G))}^{ϵ / 2}} ⩾ 2^{w {(G)}^{ϵ / 4}}$ . □

A conjecture of A. Urquhart asserts that the shortest resolution refutations of $T (G, f)$ are in fact regular. If one believes the conjecture, then devising algorithms for automatically searching for regular resolution refutations of $T (G, f)$ is important since produces the shortest resolution refutations. Alekhnovich and Razborov in [3] devised an algorithm called BWBATP which on input $T (G, f)$ , when G is of bounded cyclicity, produces a regular refutation of $T (G, f)$ in time $2^{poly (\log S_{r e g} (G))}$ , that is polylogarithmic in the length of the shortest regular refutation of $T (G, f)$ .

Using Theorem 1 and other known results we can generalize Alekhnovich and Razborov result to any graph and we can provide positive evidence (i.e. showing it for quasi-polynomial size) to the Urquhart's conjecture. We prove the more general statement that the size of refutations of $T (G, f)$ in all the proof systems between tree-like resolution and constant-depth Frege (hence in particular regular resolution) are quasi-polynomially correlated. i.e. if $T (G, f)$ has a derivation of size S in one of them of size S then it has a refutation of size at most $2^{poly (\log S)}$ in the other.

Corollary 40

Let $P$ and $Q$ be two proof systems such that both polynomially simulate tree-like resolution and both are polynomially simulated by constant-depth Frege. If there are derivations of size S in $P$ , then there are derivations of size at most $2^{poly (\log S)}$ in $Q$ .

Proof

Constant-depth Frege polynomially simulates treelike resolution hence it is sufficient to show the corollary taking $P$ as constant-depth Frege and $Q$ as treelike resolution. Assume that $\neg T (G, f)$ have proofs of size S in constant-depth Frege, we have to prove that there are derivations of size at most $2^{poly (\log S)}$ in tree-like Resolution. By Theorem 1 $S ⩾ \max {2^{Δ (G)}, 2^{tw {(G)}^{ϵ}}}$ . Hence $tw (G) ⩽ {(\log S)}^{\frac{1}{ϵ}}$ . By a result in [5], [29] there are tree-like resolution refutations of $T (G, f)$ of size $n^{O (w (G))} = 2^{O (tw (G) Δ (G) \log n)}$ , where n is the number of edges in G. Substituting the expression for the treewidth we obtain the claim. □

Declaration of Competing Interest

The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.

Acknowledgements

The authors thank Navid Talebanfard for discussions on the lower bound. Nicola also thanks Paul Wollan for introducing him to the tree-cutwidth. Dmitry is a Young Russian Mathematics award winner and would like to thank sponsors and jury of the contest.

The research was supported by Russian Science Foundation (project 16-11-10123).

Appendix A. Frege vs Pudlák-Buss games

A set of formulas Γ semantically implies a formula ψ if every assignment that satisfies all formulas from Γ also satisfies ψ.

Every particular Frege system is defined by a finite set of derivation rules. A derivation rule has form $\frac{φ_{1}, \dots, φ_{k}}{φ}$ , where $k ⩾ 0$ , $φ_{1}, \dots, φ_{k}$ and φ are propositional formulas. It is required that every rule is sound, i.e. ${φ_{1}, \dots, φ_{k}}$ semantically implies φ.

Let Γ be a list of propositional formulas. We say that φ can be derived from Γ if there exists a sequence of formulas $ψ_{1}, ψ_{2}, \dots, ψ_{s}$ such that $ψ_{s} = φ$ and each $ψ_{i}$ is either an element of Γ or can be derived from the formulas with smaller numbers by a derivation rule. It is allowed to substitute propositional formulas instead of variables into a derivation rule. A formula τ is derivable if it can be derived from an empty list of formulas.

A system of derivation rules is a Frege system if it is implicationally complete: if some set of formulas Γ semantically implies a formula φ, then φ must be derivable from Γ.

A depth of a derivation is the maximum depth of a formula that occurs in the derivation. A size of a derivation is the sum of sizes of all formulas from the derivation.

Lemma 3

Proof

1.
Let $φ_{1}, φ_{2}, \dots, φ_{s}$ be a Frege derivation of φ of size S. We construct a strategy for Pavel. Pavel asks Sam values of the formulas $φ_{1}, φ_{2}, \dots$ until he gets the answer 0. $φ_{s} = φ$ , so at least for $φ_{s}$ the answer is 0. Assume that Sam has answered 1 for the formulas $φ_{1}, φ_{2}, \dots, φ_{k}$ and 0 for $φ_{k + 1}$ where $0 ⩽ k ⩽ s - 1$ . $φ_{k + 1}$ is derived from $φ_{1}, φ_{2}, \dots, φ_{k}$ using one of the rules in Frege system. Let us consider all subformulas of this rule (there is a constant number of such subformulas). Pavel asks Sam values of the formulas corresponding to such subformulas in the application of the rule where $φ_{k + 1}$ is derived. Due to correctness of the rules, we get an immediate contradiction. Number of vertices for constructed tree is $O (S)$ . In every vertex Pavel has asked only subformulas of formulas in the Frege derivation, so size of every asked formula does not exceed S and depth does not exceed d. The total size of the game is $O (S^{2})$
2.
Let T be a tree for Pudlák-Buss game with the initial condition $φ = 0$ . Every vertex in the tree corresponds to a sequence of questions and answers on the path from the root to this vertex. For the sequence $φ_{1} = a_{1}, φ_{2} = a_{2}, \dots, φ_{j} = a_{j}$ we write a formula $\neg (\neg φ \land φ_{1}^{a_{1}} \land \dots φ_{j}^{a_{j}})$ , where $ψ^{0}$ denotes ¬ψ, and $ψ^{1}$ denotes ψ.
We assume that Frege system includes the rule $\frac{\neg (x \land y), \neg (x \land \neg y)}{\neg x}$ (it can be simulated with derivation of constant size and depth due to implicationally completeness of the system). With that rule, formulas corresponding to the inner vertices of the tree can be derived from the formulas corresponding to their descendants.
We also need to derive formulas in the leaves. Let h be the depth of T. We construct the derivation for a leaf using $O (h)$ formulas, because in every leaf we have an immediate contradiction. There exist only a constant number of ways to get an immediate contradiction, so we assume that all these axioms are present in our Frege system. In order to use these axioms we need to rearrange the formulas in the big conjunction and place the formulas needed for immediate contradiction first.
For example, if the immediate contradiction is $A = 0, B = 1, A \land B = 1$ , we need to add an axiom $\frac{}{\neg (\neg A \land B \land (A \land B) \land X)}$ .
If the tree T has N vertices then the constructed derivation has $O (N h)$ formulas, and every formula has size $O (S + h)$ . Given that $N ⩽ S$ and $h ⩽ S$ , we get a derivation with total size $O (S^{3})$ □

References

[1]
Miklós Ajtai
The complexity of the pigeonhole principle
Combinatorica, 14 (4) (1994), pp. 417-433, 10.1007/BF01302964
View at publisher
View in Scopus Google Scholar
[2]
Michael Alekhnovich, Alexander A. Razborov
Resolution is not automatizable unless W[P] is tractable
SIAM J. Comput., 38 (4) (2008), pp. 1347-1363, 10.1137/06066850X
View at publisher
View in Scopus Google Scholar
[3]
Michael Alekhnovich, Alexander A. Razborov
Satisfiability, branch-width and Tseitin tautologies
Comput. Complex., 20 (4) (2011), pp. 649-678, 10.1007/s00037-011-0033-1
View at publisher
View in Scopus Google Scholar
[4]
Albert Atserias, Moritz Müller
Automating resolution is NP-hard
J. ACM, 67 (5) (2020), pp. 31:1-31:17, 10.1145/3409472
View at publisher
Google Scholar
[5]
Paul Beame, Chris Beck, Russell Impagliazzo
Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
SIAM J. Comput., 45 (4) (2016), pp. 1612-1645, 10.1137/130914085
View at publisher
View in Scopus Google Scholar
[6]
Paul Beame, Toniann Pitassi
Simplified and improved resolution lower bounds
37th Annual Symposium on Foundations of Computer Science, FOCS'96, 14–16 October, 1996, IEEE Computer Society, Burlington, Vermont, USA (1996), pp. 274-282, 10.1109/SFCS.1996.548486
View in Scopus Google Scholar
[7]
Stephen Bellantoni, Toniann Pitassi, Alasdair Urquhart
Approximation and small-depth Frege proofs
SIAM J. Comput., 21 (6) (1992), pp. 1161-1179, 10.1137/0221068
Google Scholar
[8]
Rémy Belmonte, Archontia Giannopoulou, Daniel Lokshtanov, Dimitrios M. Thilikos
The structure of $w_{4}$ -immersion-free graphs
ICGT 2014 (2016)
arXiv:1602.02002
Google Scholar
[9]
Eli Ben-Sasson
Hard examples for the bounded depth Frege proof system
Comput. Complex., 11 (3–4) (2002), pp. 109-136, 10.1007/s00037-002-0172-5
View in Scopus Google Scholar
[10]
Eli Ben-Sasson, Avi Wigderson
Short proofs are narrow - resolution made simple
J. ACM, 48 (2) (2001), pp. 149-169, 10.1145/375827.375835
View in Scopus Google Scholar
[11]
Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
Inf. Process. Lett., 110 (23) (2010), pp. 1074-1077, 10.1016/j.ipl.2010.09.007
View PDF View article View in Scopus Google Scholar
[12]
Samuel R. Buss
Polynomial size proofs of the propositional pigeonhole principle
J. Symb. Log., 52 (4) (1987), pp. 916-927, 10.2307/2273826
View at publisher
Google Scholar
[13]
Julia Chuzhoy
Excluded grid theorem: improved and simplified
Rocco A. Servedio, Ronitt Rubinfeld (Eds.), Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, June 14–17, 2015, ACM, Portland, OR, USA (2015), pp. 645-654, 10.1145/2746539.2746551
View at publisher
View in Scopus Google Scholar
[14]
Julia Chuzhoy, Zihan Tan
Towards tight(er) bounds for the excluded grid theorem
Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial and Applied Mathematics, SODA '19, Philadelphia, PA, USA (2019), pp. 1445-1464
http://dl.acm.org/citation.cfm?id=3310435.3310523
View at publisher
CrossRef View in Scopus Google Scholar
[15]
Stephen A. Cook, Robert A. Reckhow
The relative efficiency of propositional proof systems
J. Symb. Log., 44 (1) (1979), pp. 36-50, 10.2307/2273702
View at publisher
Google Scholar
[16]
Stefan S. Dantchev, Søren Riis
Tree resolution proofs of the weak pigeon-hole principle
Proceedings of the 16th Annual IEEE Conference on Computational Complexity, June 18-21, 2001, IEEE Computer Society, Chicago, Illinois, USA (2001), pp. 69-75, 10.1109/CCC.2001.933873
View at publisher
View in Scopus Google Scholar
[17]
Martin Davis, George Logemann, Donald W. Loveland
A machine program for theorem-proving
Commun. ACM, 5 (7) (1962), pp. 394-397, 10.1145/368273.368557
View at publisher
View in Scopus Google Scholar
[18]
Martin Davis, Hilary Putnam
A computing procedure for quantification theory
J. ACM, 7 (3) (1960), pp. 201-215, 10.1145/321033.321034
http://doi.acm.org/10.1145/321033.321034
View at publisher
View in Scopus Google Scholar
[19]
Zdenek Dvorák, Paul Wollan
A structure theorem for strong immersions
J. Graph Theory, 83 (2) (2016), pp. 152-163, 10.1002/jgt.21990
View at publisher
View in Scopus Google Scholar
[20]
Merrick L. Furst, James B. Saxe, Michael Sipser
Parity, circuits, and the polynomial-time hierarchy
Math. Syst. Theory, 17 (1) (1984), pp. 13-27, 10.1007/BF01744431
View at publisher
View in Scopus Google Scholar
[21]
Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova
Bounded-depth frege complexity of tseitin formulas for all graphs
Peter Rossmanith, Pinar Heggernes, Joost-Pieter Katoen (Eds.), 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, LIPIcs, vol. 138, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019), pp. 49:1-49:15, 10.4230/LIPIcs.MFCS.2019.49
View at publisher
Google Scholar
[22]
Nicola Galesi, Navid Talebanfard, Jacobo Torán
Cops-robber games and the resolution of Tseitin formulas
ACM Trans. Comput. Theory, 12 (2) (2020), pp. 9:1-9:22, 10.1145/3378667
View at publisher
Google Scholar
[23]
Ludmila Glinskih, Dmitry Itsykson
On Tseitin formulas, read-once branching programs and treewidth
Electron. Colloq. Comput. Complex., 26 (20) (2019)
https://eccc.weizmann.ac.il/report/2019/020
Google Scholar
[24]
Qian-Ping Gu, Hisao Tamaki
Improved bounds on the planar branchwidth with respect to the largest grid minor size
Algorithmica, 64 (3) (Nov 2012), pp. 416-453, 10.1007/s00453-012-9627-5
View at publisher
View in Scopus Google Scholar
[25]
Armin Haken
The intractability of resolution
Theor. Comput. Sci., 39 (1985), pp. 297-308, 10.1016/0304-3975(85)90144-6
View PDF View article View in Scopus Google Scholar
[26]
Daniel J. Harvey, David R. Wood
The treewidth of line graphs
J. Comb. Theory, Ser. B, 132 (2018), pp. 157-179, 10.1016/j.jctb.2018.03.007
http://www.sciencedirect.com/science/article/pii/S0095895618300236
View PDF View article View in Scopus Google Scholar
[27]
Johan Hastad
Computational Limitations of Small-Depth Circuits
MIT Press (1987)
Google Scholar
[28]
Johan Håstad
On small-depth Frege proofs for Tseitin for grids
Chris Umans (Ed.), 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, October 15-17, 2017, IEEE Computer Society, Berkeley, CA, USA (2017), pp. 97-108, 10.1109/FOCS.2017.18
View at publisher
View in Scopus Google Scholar
[29]
Dmitry Itsykson, Vsevolod Oparin
Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP
Andrei A. Bulatov, Arseny M. Shur (Eds.), Computer Science - Theory and Applications - 8th International Computer Science Symposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7913, Springer (2013), pp. 162-173, 10.1007/978-3-642-38536-0_14
View at publisher
View in Scopus Google Scholar
[30]
Dmitry Itsykson, Vsevolod Oparin, Mikhail Slabodkin, Dmitry Sokolov
Tight lower bounds on the resolution complexity of perfect matching principles
Fundam. Inform., 145 (3) (2016), pp. 229-242, 10.3233/FI-2016-1358
View at publisher
View in Scopus Google Scholar
[31]
Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov
Almost tight lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
Comput. Complex., 30 (2) (2021), p. 13, 10.1007/s00037-021-00213-2
View at publisher
View in Scopus Google Scholar
[32]
Stasys Jukna
Boolean Function Complexity: Advances and Frontiers
Springer (2012)
Google Scholar
[33]
Jan Krajícek, Pavel Pudlák, Alan R. Woods
An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle
Random Struct. Algorithms, 7 (1) (1995), pp. 15-40, 10.1002/rsa.3240070103
View at publisher
View in Scopus Google Scholar
[34]
Toniann Pitassi, Paul Beame, Russell Impagliazzo
Exponential lower bounds for the pigeonhole principle
Comput. Complex., 3 (1993), pp. 97-140, 10.1007/BF01200117
View at publisher
View in Scopus Google Scholar
[35]
Toniann Pitassi, Benjamin Rossman, Rocco A. Servedio, Li-Yang Tan
Poly-logarithmic Frege depth lower bounds via an expander switching lemma
Daniel Wichs, Yishay Mansour (Eds.), Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, June 18-21, 2016, ACM, Cambridge, MA, USA (2016), pp. 644-657, 10.1145/2897518.2897637
View at publisher
View in Scopus Google Scholar
[36]
Pavel Pudlák, Samuel R. Buss
How to lie without being (easily) convicted and the lengths of proofs in propositional calculus
Leszek Pacholski, Jerzy Tiuryn (Eds.), Computer Science Logic, Springer Berlin Heidelberg, Berlin, Heidelberg (1995), pp. 151-162
View in Scopus Google Scholar
[37]
Ran Raz
Resolution lower bounds for the weak pigeonhole principle
J. ACM, 51 (2) (2004), pp. 115-138, 10.1145/972639.972640
View at publisher
View in Scopus Google Scholar
[38]
Alexander A. Razborov
Lower bounds on the size of bounded depth networks over a complete basis with logical addition
Mat. Zametki, 41 (1987), pp. 598-607
Google Scholar
[39]
Alexander A. Razborov
Resolution lower bounds for the weak functional pigeonhole principle
Theor. Comput. Sci., 303 (1) (2003), pp. 233-243, 10.1016/S0304-3975(02)00453-X
View PDF View article View in Scopus Google Scholar
[40]
Alexander A. Razborov
Resolution lower bounds for perfect matching principles
J. Comput. Syst. Sci., 69 (1) (2004), pp. 3-27, 10.1016/j.jcss.2004.01.004
View PDF View article View in Scopus Google Scholar
[41]
Neil Robertson, Paul Seymour, Robin Thomas
Quickly excluding a planar graph
J. Comb. Theory, Ser. B, 62 (2) (1994), pp. 323-348, 10.1006/jctb.1994.1073
http://www.sciencedirect.com/science/article/pii/S0095895684710732
View PDF View article View in Scopus Google Scholar
[42]
Roman Smolensky
Algebraic methods in the theory of lower bounds for Boolean circuit complexity
Alfred V. Aho (Ed.), Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, ACM, New York, New York, USA (1987), pp. 77-82, 10.1145/28395.28404
View at publisher
View in Scopus Google Scholar
[43]
Grigory S. Tseitin, On the complexity of derivation in the propositional calculus, in: A.O. Slisenko (Ed.), Studies in Constructive Mathematics and Mathematical Logic Part II, a968.
Google Scholar
[44]
Alasdair Urquhart
Hard examples for resolution
J. ACM, 34 (1) (1987), pp. 209-219, 10.1145/7531.8928
View at publisher
Google Scholar
[45]
Alasdair Urquhart, Xudong Fu
Simplified lower bounds for propositional proofs
Notre Dame J. Form. Log., 37 (4) (1996), pp. 523-544, 10.1305/ndjfl/1040046140
View at publisher
View in Scopus Google Scholar
[46]
David R. Wood
On tree-partition-width
Part Special Issue on Metric Graph Theory, Eur. J. Comb., 30 (5) (2009), pp. 1245-1253, 10.1016/j.ejc.2008.11.010
http://www.sciencedirect.com/science/article/pii/S0195669808002837
View PDF View article View in Scopus Google Scholar

Cited by (0)

^☆: A preliminary version of this paper appeared at MFCS 2019 [21].

View Abstract

[1] [1]
Miklós Ajtai
The complexity of the pigeonhole principle
Combinatorica, 14 (4) (1994), pp. 417-433, 10.1007/BF01302964
View at publisher
View in Scopus Google Scholar

[2] [2]
Michael Alekhnovich, Alexander A. Razborov
Resolution is not automatizable unless W[P] is tractable
SIAM J. Comput., 38 (4) (2008), pp. 1347-1363, 10.1137/06066850X
View at publisher
View in Scopus Google Scholar

[3] [3]
Michael Alekhnovich, Alexander A. Razborov
Satisfiability, branch-width and Tseitin tautologies
Comput. Complex., 20 (4) (2011), pp. 649-678, 10.1007/s00037-011-0033-1
View at publisher
View in Scopus Google Scholar

[4] [4]
Albert Atserias, Moritz Müller
Automating resolution is NP-hard
J. ACM, 67 (5) (2020), pp. 31:1-31:17, 10.1145/3409472
View at publisher
Google Scholar

[5] [5]
Paul Beame, Chris Beck, Russell Impagliazzo
Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
SIAM J. Comput., 45 (4) (2016), pp. 1612-1645, 10.1137/130914085
View at publisher
View in Scopus Google Scholar

[6] [6]
Paul Beame, Toniann Pitassi
Simplified and improved resolution lower bounds
37th Annual Symposium on Foundations of Computer Science, FOCS'96, 14–16 October, 1996, IEEE Computer Society, Burlington, Vermont, USA (1996), pp. 274-282, 10.1109/SFCS.1996.548486
View in Scopus Google Scholar

[7] [7]
Stephen Bellantoni, Toniann Pitassi, Alasdair Urquhart
Approximation and small-depth Frege proofs
SIAM J. Comput., 21 (6) (1992), pp. 1161-1179, 10.1137/0221068
Google Scholar

[8] [8]
Rémy Belmonte, Archontia Giannopoulou, Daniel Lokshtanov, Dimitrios M. Thilikos
The structure of $w_{4}$ -immersion-free graphs
ICGT 2014 (2016)
arXiv:1602.02002
Google Scholar

[9] [9]
Eli Ben-Sasson
Hard examples for the bounded depth Frege proof system
Comput. Complex., 11 (3–4) (2002), pp. 109-136, 10.1007/s00037-002-0172-5
View in Scopus Google Scholar

[10] [10]
Eli Ben-Sasson, Avi Wigderson
Short proofs are narrow - resolution made simple
J. ACM, 48 (2) (2001), pp. 149-169, 10.1145/375827.375835
View in Scopus Google Scholar

[11] [11]
Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
Inf. Process. Lett., 110 (23) (2010), pp. 1074-1077, 10.1016/j.ipl.2010.09.007
View PDF View article View in Scopus Google Scholar

[12] [12]
Samuel R. Buss
Polynomial size proofs of the propositional pigeonhole principle
J. Symb. Log., 52 (4) (1987), pp. 916-927, 10.2307/2273826
View at publisher
Google Scholar

[13] [13]
Julia Chuzhoy
Excluded grid theorem: improved and simplified
Rocco A. Servedio, Ronitt Rubinfeld (Eds.), Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, June 14–17, 2015, ACM, Portland, OR, USA (2015), pp. 645-654, 10.1145/2746539.2746551
View at publisher
View in Scopus Google Scholar

[14] [14]
Julia Chuzhoy, Zihan Tan
Towards tight(er) bounds for the excluded grid theorem
Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial and Applied Mathematics, SODA '19, Philadelphia, PA, USA (2019), pp. 1445-1464
http://dl.acm.org/citation.cfm?id=3310435.3310523
View at publisher
CrossRef View in Scopus Google Scholar

[15] [15]
Stephen A. Cook, Robert A. Reckhow
The relative efficiency of propositional proof systems
J. Symb. Log., 44 (1) (1979), pp. 36-50, 10.2307/2273702
View at publisher
Google Scholar

[16] [16]
Stefan S. Dantchev, Søren Riis
Tree resolution proofs of the weak pigeon-hole principle
Proceedings of the 16th Annual IEEE Conference on Computational Complexity, June 18-21, 2001, IEEE Computer Society, Chicago, Illinois, USA (2001), pp. 69-75, 10.1109/CCC.2001.933873
View at publisher
View in Scopus Google Scholar

[17] [17]
Martin Davis, George Logemann, Donald W. Loveland
A machine program for theorem-proving
Commun. ACM, 5 (7) (1962), pp. 394-397, 10.1145/368273.368557
View at publisher
View in Scopus Google Scholar

[18] [18]
Martin Davis, Hilary Putnam
A computing procedure for quantification theory
J. ACM, 7 (3) (1960), pp. 201-215, 10.1145/321033.321034
http://doi.acm.org/10.1145/321033.321034
View at publisher
View in Scopus Google Scholar

[19] [19]
Zdenek Dvorák, Paul Wollan
A structure theorem for strong immersions
J. Graph Theory, 83 (2) (2016), pp. 152-163, 10.1002/jgt.21990
View at publisher
View in Scopus Google Scholar

[20] [20]
Merrick L. Furst, James B. Saxe, Michael Sipser
Parity, circuits, and the polynomial-time hierarchy
Math. Syst. Theory, 17 (1) (1984), pp. 13-27, 10.1007/BF01744431
View at publisher
View in Scopus Google Scholar

[21] [21]
Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova
Bounded-depth frege complexity of tseitin formulas for all graphs
Peter Rossmanith, Pinar Heggernes, Joost-Pieter Katoen (Eds.), 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, LIPIcs, vol. 138, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019), pp. 49:1-49:15, 10.4230/LIPIcs.MFCS.2019.49
View at publisher
Google Scholar

[22] [22]
Nicola Galesi, Navid Talebanfard, Jacobo Torán
Cops-robber games and the resolution of Tseitin formulas
ACM Trans. Comput. Theory, 12 (2) (2020), pp. 9:1-9:22, 10.1145/3378667
View at publisher
Google Scholar

[23] [23]
Ludmila Glinskih, Dmitry Itsykson
On Tseitin formulas, read-once branching programs and treewidth
Electron. Colloq. Comput. Complex., 26 (20) (2019)
https://eccc.weizmann.ac.il/report/2019/020
Google Scholar

[24] [24]
Qian-Ping Gu, Hisao Tamaki
Improved bounds on the planar branchwidth with respect to the largest grid minor size
Algorithmica, 64 (3) (Nov 2012), pp. 416-453, 10.1007/s00453-012-9627-5
View at publisher
View in Scopus Google Scholar

[25] [25]
Armin Haken
The intractability of resolution
Theor. Comput. Sci., 39 (1985), pp. 297-308, 10.1016/0304-3975(85)90144-6
View PDF View article View in Scopus Google Scholar

[26] [26]
Daniel J. Harvey, David R. Wood
The treewidth of line graphs
J. Comb. Theory, Ser. B, 132 (2018), pp. 157-179, 10.1016/j.jctb.2018.03.007
http://www.sciencedirect.com/science/article/pii/S0095895618300236
View PDF View article View in Scopus Google Scholar

[27] [27]
Johan Hastad
Computational Limitations of Small-Depth Circuits
MIT Press (1987)
Google Scholar

[28] [28]
Johan Håstad
On small-depth Frege proofs for Tseitin for grids
Chris Umans (Ed.), 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, October 15-17, 2017, IEEE Computer Society, Berkeley, CA, USA (2017), pp. 97-108, 10.1109/FOCS.2017.18
View at publisher
View in Scopus Google Scholar

[29] [29]
Dmitry Itsykson, Vsevolod Oparin
Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP
Andrei A. Bulatov, Arseny M. Shur (Eds.), Computer Science - Theory and Applications - 8th International Computer Science Symposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7913, Springer (2013), pp. 162-173, 10.1007/978-3-642-38536-0_14
View at publisher
View in Scopus Google Scholar

[30] [30]
Dmitry Itsykson, Vsevolod Oparin, Mikhail Slabodkin, Dmitry Sokolov
Tight lower bounds on the resolution complexity of perfect matching principles
Fundam. Inform., 145 (3) (2016), pp. 229-242, 10.3233/FI-2016-1358
View at publisher
View in Scopus Google Scholar

[31] [31]
Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov
Almost tight lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
Comput. Complex., 30 (2) (2021), p. 13, 10.1007/s00037-021-00213-2
View at publisher
View in Scopus Google Scholar

[32] [32]
Stasys Jukna
Boolean Function Complexity: Advances and Frontiers
Springer (2012)
Google Scholar

[33] [33]
Jan Krajícek, Pavel Pudlák, Alan R. Woods
An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle
Random Struct. Algorithms, 7 (1) (1995), pp. 15-40, 10.1002/rsa.3240070103
View at publisher
View in Scopus Google Scholar

[34] [34]
Toniann Pitassi, Paul Beame, Russell Impagliazzo
Exponential lower bounds for the pigeonhole principle
Comput. Complex., 3 (1993), pp. 97-140, 10.1007/BF01200117
View at publisher
View in Scopus Google Scholar

[35] [35]
Toniann Pitassi, Benjamin Rossman, Rocco A. Servedio, Li-Yang Tan
Poly-logarithmic Frege depth lower bounds via an expander switching lemma
Daniel Wichs, Yishay Mansour (Eds.), Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, June 18-21, 2016, ACM, Cambridge, MA, USA (2016), pp. 644-657, 10.1145/2897518.2897637
View at publisher
View in Scopus Google Scholar

[36] [36]
Pavel Pudlák, Samuel R. Buss
How to lie without being (easily) convicted and the lengths of proofs in propositional calculus
Leszek Pacholski, Jerzy Tiuryn (Eds.), Computer Science Logic, Springer Berlin Heidelberg, Berlin, Heidelberg (1995), pp. 151-162
View in Scopus Google Scholar

[37] [37]
Ran Raz
Resolution lower bounds for the weak pigeonhole principle
J. ACM, 51 (2) (2004), pp. 115-138, 10.1145/972639.972640
View at publisher
View in Scopus Google Scholar

[38] [38]
Alexander A. Razborov
Lower bounds on the size of bounded depth networks over a complete basis with logical addition
Mat. Zametki, 41 (1987), pp. 598-607
Google Scholar

[39] [39]
Alexander A. Razborov
Resolution lower bounds for the weak functional pigeonhole principle
Theor. Comput. Sci., 303 (1) (2003), pp. 233-243, 10.1016/S0304-3975(02)00453-X
View PDF View article View in Scopus Google Scholar

[40] [40]
Alexander A. Razborov
Resolution lower bounds for perfect matching principles
J. Comput. Syst. Sci., 69 (1) (2004), pp. 3-27, 10.1016/j.jcss.2004.01.004
View PDF View article View in Scopus Google Scholar

[41] [41]
Neil Robertson, Paul Seymour, Robin Thomas
Quickly excluding a planar graph
J. Comb. Theory, Ser. B, 62 (2) (1994), pp. 323-348, 10.1006/jctb.1994.1073
http://www.sciencedirect.com/science/article/pii/S0095895684710732
View PDF View article View in Scopus Google Scholar

[42] [42]
Roman Smolensky
Algebraic methods in the theory of lower bounds for Boolean circuit complexity
Alfred V. Aho (Ed.), Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, ACM, New York, New York, USA (1987), pp. 77-82, 10.1145/28395.28404
View at publisher
View in Scopus Google Scholar

[43] [43]
Grigory S. Tseitin, On the complexity of derivation in the propositional calculus, in: A.O. Slisenko (Ed.), Studies in Constructive Mathematics and Mathematical Logic Part II, a968.
Google Scholar

[44] [44]
Alasdair Urquhart
Hard examples for resolution
J. ACM, 34 (1) (1987), pp. 209-219, 10.1145/7531.8928
View at publisher
Google Scholar

[45] [45]
Alasdair Urquhart, Xudong Fu
Simplified lower bounds for propositional proofs
Notre Dame J. Form. Log., 37 (4) (1996), pp. 523-544, 10.1305/ndjfl/1040046140
View at publisher
View in Scopus Google Scholar

[46] [46]
David R. Wood
On tree-partition-width
Part Special Issue on Metric Graph Theory, Eur. J. Comb., 30 (5) (2009), pp. 1245-1253, 10.1016/j.ejc.2008.11.010
http://www.sciencedirect.com/science/article/pii/S0195669808002837
View PDF View article View in Scopus Google Scholar

Outline

Figures (5)

Annals of Pure and Applied Logic

Abstract

MSC

Keywords

1. Introduction

1.1. Overview of the proof technique

1.2. The complexity of Tseitin formulas in resolution

2. Preliminaries

[44]

[14]

3. The lower bound

3.1. Topological minors and Tseitin formulas

[23]

3.2. From walls to grids

3.3. Putting it all together

[28]

4. The upper bound

4.1. A compact representation of parity

4.2. Summation of linear equations

4.3. Tree-partition-width

[46]

5. The complexity of Tseitin formulas in resolution

5.1. Resolution lower bounds for $T (G, f)$ in terms of treewidth

5.2. Searching for resolution refutations of $T (G, f)$

Declaration of Competing Interest

Acknowledgements

Appendix A. Frege vs Pudlák-Buss games

References

Cited by (0)

Bounded-depth Frege complexity of Tseitin formulas for all graphs☆

Abstract

MSC

Keywords

1. Introduction

1.1. Overview of the proof technique

1.2. The complexity of Tseitin formulas in resolution

2. Preliminaries

3. The lower bound

3.1. Topological minors and Tseitin formulas

3.2. From walls to grids

3.3. Putting it all together

4. The upper bound

4.1. A compact representation of parity

4.2. Summation of linear equations

4.3. Tree-partition-width

5. The complexity of Tseitin formulas in resolution

5.1. Resolution lower bounds for T(G,f)in terms of treewidth

5.2. Searching for resolution refutations of T(G,f)

Declaration of Competing Interest

Acknowledgements

Appendix A. Frege vs Pudlák-Buss games

References

5.1. Resolution lower bounds for $T (G, f)$ in terms of treewidth

5.2. Searching for resolution refutations of $T (G, f)$