Cops-Robber Games and the Resolution of Tseitin Formulas

Abstract

We characterize several complexity measures for the resolution of Tseitin formulas in terms of a two person cop-robber game. Our game is a slight variation of the one Seymour and Thomas used in order to characterize the tree-width parameter. For any undirected graph, by counting the number of cops needed in our game in order to catch a robber in it, we are able to exactly characterize the width, variable space and depth measures for the resolution of the Tseitin formula corresponding to that graph. We also give an exact game characterization of resolution variable space for any formula.

We show that our game can be played in a monotone way. This implies that the corresponding resolution measures on Tseitin formulas correspond exactly to those under the restriction of regular resolution.

Using our characterizations we improve the existing complexity bounds for Tseitin formulas showing that resolution width, depth and variable space coincide up to a logarithmic factor, and that variable space is bounded by the clause space times a logarithmic factor.

N. Talebanfard—Supported by ERC grant FEALORA 339691.

1 Introduction

Tseitin propositional formulas for a graph $G=(V,E)$ encode the combinatorial statement that the sum of the degrees of the vertices of G is even. Such formulas provide a great tool for transforming in a uniform way a graph into a propositional formula that inherits some of the properties of the graph. Tseitin formulas have been extensively used to provide hard examples for resolution or as benchmarks for testing SAT-solvers. To name just a few examples, they were used for proving exponential lower bounds on the minimal size required in tree-like and regular resolution [17], in general resolution [18] and for proving lower bounds on resolution proof measures as the width [7] and the space [9], or more recently for proving time-space trade-offs in resolution [5, 6]. Due to the importance of these formulas, it is of great interest to find ways to understand how different parameters on the underlying graphs are translated as some complexity measures of the corresponding Tseitin formula. This was the key of the mentioned resolution results. For example the expansion of the graph translated into resolution lower bounds for the corresponding formula in all mentioned lower bounds, while the carving-width or the cut-width of the graph were used to provide upper bounds for the resolution width and size in [2, 5].

In this paper we obtain an exact characterization of the complexity measures of resolution width, variable space and depth for any Tseitin formula in terms of a cops-robber game played on its underlying graph. There exists a vast literature on such graph searching games (see eg. [10]). Probably the best known game of this kind is the one used by Seymour and Thomas [15] in order to characterize exactly the graph tree-width parameter. In the original game, a team of cops has to catch a robber that moves arbitrarily fast in a graph. Cops and robber are placed on vertices, and have perfect information of the positions of the other player. The robber can move any time from one vertex to any other reachable one but cannot go through vertices occupied by a cop. Cops are placed or removed from vertices and do not move. The robber is caught when a cop is placed on the vertex where she is standing. The value of the game for a graph G is the minimum number of cops needed to catch the robber on G. In [15] Seymour and Thomas also showed that this game is monotone in the sense that there is always an optimal strategy for the cops in which they never occupy the same vertex again after a cop has been removed from it. In a previous version of the game [13] the robber is invisible and the cops have to search the whole graph to be sure to catch her. The minimum number of cops needed to catch the robber in this game on G, characterizes exactly the path-width of G [8]. The invisible cop game is also monotone [13].

Our game is just a slight variation from the original game from [15]. The only differences are that the cops are placed on the graph edges instead of on vertices, and that the robber is caught when she is completely surrounded by cops. We show that the minimum number of cops needed to catch a robber on a graph G in this game, exactly characterizes the resolution width of the corresponding Tseitin formula. We also show that the number of times some cop is placed on an edge of G exactly coincides with the resolution depth of the Tseitin formula on G. Also, if we consider the version of the game with an invisible robber instead, we exactly obtain the resolution variable space of the Tseitin formula on G.

We also show that the ideas behind the characterization of variable space in terms of a game with an invisible robber, can in fact be extended to define a new combinatorial game to exactly characterize the resolution variable space of any formula (not necessarily a Tseitin formula). Our game is a non-interactive version of the Atserias and Dalmau game for characterizing resolution width [4].

An interesting consequence of the cops-robber game characterizations is that the property of the games being monotone can be used to show that for the corresponding complexity measures, the resolution proof can be regular without changing the bounds. As mentioned, the vertex-cops games are known to be monotone. This did not need to be true for our game. In fact, the robber-marshals game [11], another version of the game in which the cops are placed on the (hyper)edges, is know to be non-monotone [1]. We are able to show that the edge-cops game (for both cases of visible and invisible robber) is also monotone. This is done by reducing our edge game to the Seymour and Thomas vertex game. This fact immediately implies that in the context of Tseitin formulas, the width and variable space in regular resolution proofs is not worse that in general resolution¹. A long standing open question from Urquhart [18] asks whether regular resolution can simulate general resolution on Tseitin formulas (in size). Our results show that this is true for the measures of width and variable space.

Finally we use the game characterization to improve the known relationships between different complexity measures on Tseitin formulas. In particular we show that for any graph G with n vertices, the resolution depth of the corresponding formula is at most its resolution width times $\log n$. From this follows that all the three measures width, depth and variable space are within a logarithmic factor in Tseitin formulas. Our results provide a family of a uniform class of propositional formulas where clause space is polynomially bounded in the variable space. No such result was known before as recently pointed to by Razborov in [14].

The paper is organized as follows. In Sect. 2, we have all the necessary preliminaries on resolution and its complexity measures. In Sect. 3 we present the characterization of variable space in resolution. In Sect. 4 we introduce our variants of the Cops-Robber games on graphs and we show the characterizations of width, variable space and depth of the Tseitin formula on G in terms of Cops-Robber games played on G. In Sect. 5 we focus on the monotone version of the games and we prove that all our characterizations can be made monotone. In the last Sect. 6 we use all our previous results to prove the new relationships between width, depth, variable space and clause space for Tseitin formulas. We finish with some conclusions and open questions.

2 Preliminaries

Let $[n] = \{1, 2, . . . , n\}$. A literal is either a Boolean variable x or its negation $\bar{x}$. A clause is a disjunction (possibly empty) of literals. The empty clause will be denoted by $\square$. The set of variables occurring in a clause C, will be denoted by ${{\mathrm{\mathsf {Vars}}}}(C)$. The width of a clause C is defined as ${{\mathrm{\mathsf {W}}}}(C):= |{{\mathrm{\mathsf {Vars}}}}(C)|$.

A CNF $F_n$ over n variables $x_1,\ldots , x_n$ is a conjunction of clauses defined over $x_1,\ldots , x_n$. We often consider a CNF as a set of clauses and to simplify the notation in this section we omit the index n expressing the dependencies of $F_n$ from the n variables. The width of a CNF F is ${{\mathrm{\mathsf {W}}}}(F):= \max _{c\in F} {{\mathrm{\mathsf {W}}}}(C)$. A CNF is a k-CNF if all clauses in it have width at most k.

The resolution proof system is a refutational propositional system for CNF formulas handling with clauses, and consisting of the only resolution rule:

$$ \frac{C \vee x \quad \quad \quad D \vee \bar{x}}{C \vee D} $$

A proof $\pi$ of a clause C from a CNF F (denoted by $F\vdash _\pi C$) is a sequence of clauses $\pi :=C_1,\ldots , C_m$, $m\ge 1$ such that $C_m=C$ and each $C_i$ in $\pi$ is either a clause of F or obtained by the resolution rule applied to two previous clauses (called premises) in the sequence. When C is the empty clause $\square$, $\pi$ is said to be a refutation of F. Resolution is a sound a complete system for unsatisfiable formulas in CNF.

Let $\pi :=C_1,\ldots , C_m$ be a resolution proof from a CNF F. The width of $\pi$ is defined as ${{\mathrm{\mathsf {W}}}}(\pi ) := \max _{i\in [m]} {{\mathrm{\mathsf {W}}}}(C_i)$. The width needed to refute an unsatisfiable CNF F in resolution is ${{\mathrm{\mathsf {W}}}}(F \vdash ):=\min _{F \vdash _\pi \square }{{\mathrm{\mathsf {W}}}}(\pi )$. The size of $\pi$ is defined as ${{\mathrm{\mathsf {S}}}}(\pi ):=m$. The size needed to refute an unsatisfiable CNF F in resolution is ${{\mathrm{\mathsf {S}}}}(F \vdash ):=\min _{F \vdash _\pi \square }{{\mathrm{\mathsf {S}}}}(\pi )$.

Resolution proofs $F \vdash _\pi C$, can be represented also in two other notations: as directed acyclic graphs (DAG) or as sequences of set of clauses $\mathbb M$, called (memory) configurations. As a DAG, $\pi$ is represented as follows: source nodes are labeled by clauses of F, the (unique) target node is labeled by C and each non-source node, labeled by a clause D, has two incoming edges from the (unique) nodes labeled by the premises of D in $\pi$. Using this notation the size of a proof $\pi$, is the number of nodes in the DAG representing $\pi$. The DAG notation allow to define other proof measures for resolution proofs. The depth of a proof $\pi$, ${{\mathrm{\mathsf {D}}}}(\pi )$ is the length of the longest path in the DAG representing $\pi$. The depth for refuting an unsatisfiable CNF F is ${{\mathrm{\mathsf {D}}}}(F\vdash ) := \min _{F \vdash _\pi \square }{{\mathrm{\mathsf {D}}}}(\pi )$.

The representation of resolution proofs as configurations was introduced in [3, 9] in order to define space complexity measures for resolution proofs. A proof $\pi$, $F \vdash _\pi C$, is a sequence $\mathbb M_1, \ldots , \mathbb M_s$ such that: $\mathbb M_1=\emptyset$, $C \in \mathbb M_s$ and for each $t\in [s-1]$, $\mathbb M_{t+1}$ is obtained from $\mathbb M_{t}$, by one of the following rules:

• [Axiom Download]: $\mathbb M_{t+1} = \mathbb M_{t} \cup \{D\}$, for D a clause in F;

• [Erasure]: $\mathbb M_{t+1} \subset \mathbb M_{t}$ ;

• [Inference]: $\mathbb M_{t+1} = \mathbb M_{t} \cup \{D\}$, if $A,B \in \mathbb M_{t}$ and $\frac{A \quad B}{D}$ is a valid resolution rule.

$\pi$ is a refutation if C is $\square$.

The clause space of a configuration $\mathbb M$ is ${{\mathrm{\mathsf {Cs}}}}(\mathbb M):=|\mathbb M|$. The clause space of a refutation $\pi := \mathbb M_1, \ldots , \mathbb M_s$ is ${{\mathrm{\mathsf {Cs}}}}(\pi ): = \max _{i\in [s]} {{\mathrm{\mathsf {Cs}}}}(\mathbb M_i)$. Finally the clause space to refute an unsatisfiable F is ${{\mathrm{\mathsf {Cs}}}}(F\vdash ) := \min _{F\vdash _\pi \square }{{\mathrm{\mathsf {Cs}}}}(\pi )$. Analogously, we define the variable space and the total space of a configuration $\mathbb M$ as ${{\mathrm{\mathsf {Vs}}}}(\mathbb M):= |\bigcup _{C\in \mathbb M} {{\mathrm{\mathsf {Vars}}}}(C)|$ and ${{\mathrm{\mathsf {Ts}}}}(\mathbb M):= \sum _{C\in \mathbb M} {{\mathrm{\mathsf {W}}}}(C)$. Variable space and total space needed to refute an unsatisfiable F, are respectively ${{\mathrm{\mathsf {Vs}}}}(F\vdash ) := \min _{F\vdash _\pi \square }{{\mathrm{\mathsf {Vs}}}}(\pi )$ and ${{\mathrm{\mathsf {Ts}}}}(F\vdash ) := \min _{F\vdash _\pi \square }{{\mathrm{\mathsf {Ts}}}}(\pi )$.

An assignment for a set of variables X, specifies a truth-value ($\{0,1\}$ value) for all variables in X. Variables, literals, clauses and CNFs are simplified under partial assignments (i.e. assignment to a subset of their defining variables) in the standard way.

2.1 Tseitin Formulas

Let $G=(V,E)$ be a connected undirected graph with n vertices, and let $\varphi :V\rightarrow \{0,1\}$ be an odd marking of the vertices of G, i.e. satisfying the property

$$\sum _{x\in V} \varphi (x)=1(\mathrm{mod}\ 2).$$

For such a graph we can define an unsatisfiable formula in conjunctive normal form ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ in the following way: The formula has E as set of variables, and is a conjunction of the CNF translation of the formulas $F_x$ for $x\in V$, where $F_x$ expresses that $e_1(x)\oplus \dots \oplus e_d(x)=\varphi (x)$ and $e_1(x)\dots e_d(x)$ are the edges (variables) incident with vertex x.

${{\mathrm{\mathsf {T}}}}(G,\varphi )$ encodes the combinatorial principle that for all graphs the sum of the degrees of the vertices is even. ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ is unsatisfiable if and only if the marking $\varphi$ is odd. For an undirected graph $G=(V,E)$, let $\varDelta (G)$ denote its maximal degree. It is easy to see that ${{\mathrm{\mathsf {W}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi ))=\varDelta (G)$.

The following fact was proved several times (see for instance [9, 18]).

Fact 1

For an odd marking $\varphi$, for every $x\in V$ there exists an assignment $\alpha _\varphi$ such that $\alpha _\varphi (F_x)=0$, and $\alpha _\varphi (F_y)=1$ for all $y\not =x$. Moreover if $\varphi$ is an even marking, then ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ is satisfiable.

Consider a partial truth assignment $\alpha$ of some of the variables of ${{\mathrm{\mathsf {T}}}}(G,\varphi )$. We refer to the following process as applying $\alpha$ to $(G,\varphi )$: Setting a variable $e=(x,y)$ in $\alpha$ to 0 corresponds to deleting the edge e in the graph G, and setting it to 1 corresponds to deleting the edge from the graph and toggling the values of $\varphi (x)$ and $\varphi (y)$ in G. Observe that the formula ${{\mathrm{\mathsf {T}}}}(G',\varphi ')$ resulting after applying $\alpha$ to (G, m) is still unsatisfiable.

3 A Game Characterization of Resolution Variable Space

We start by giving a new characterization of resolution variable space. This result holds for any CNF formula and is therefore quite independent of the rest of the paper. We include it at the beginning since it will be used to show that the invisible robber game characterizes variable space in Tseitin formulas.

The game is a non-interactive version of the Spoiler-Duplicator width game from Atserias and Dalmau [4]:

Given an unsatisfiable formula F in CNF with variable set V, Player 1 constructs step by step a finite list $L=L_0,L_1,\dots ,L_k$ of sets of variables, $L_i\subseteq V.$ Starting by the empty set, $L_0=\emptyset$, in each step he can either add variables to the previous set, or delete variables from it. The cost of the game is the size of the largest set in the list.

Once the Player 1 finishes his list, Player 2 has to construct dynamically a partial assignment for the set of variables in the list. In each step i, the domain of the assignment is the set of variables $L_i$ in the list at this step. She starts giving some value to the first set of variables in the list, $L_1$, in a way that no clause of F is falsified. If variables are added to the set at any step, she has to extend the previous partial assignment to the new domain in any way, but again, no initial clause can be falsified. If a variable is kept from one set to the next one in the list, its value in the assignment remains. If variables are removed from the set at any step, the new partial assignment is the restriction of the previous one to the new domain.

If Player 2 manages to come to the end of the list without having falsified any clause of F at any point, she wins. Otherwise Player 1 wins.

Define ${{\mathrm{\mathsf {nisd}}}}(F)$ to be the minimum cost of a winning game for Player 1 on F. We prove that for any unsatisfiable formula F the variable space of F coincides exactly with ${{\mathrm{\mathsf {nisd}}}}(F)$.

Theorem 1

Let F be an unsatisfiable formula, then ${{\mathrm{\mathsf {nisd}}}}(F)\le {{\mathrm{\mathsf {Vs}}}}(F\vdash ).$

Proof

(sketch) Consider a resolution proof $\varPi$ of F as a list of configurations. The strategy of Player 1 consists in constructing a list L of sets of variables, that in each step i contains the variables present in the i-th configuration. The cost for this list is exactly ${{\mathrm{\mathsf {Vs}}}}(\varPi ).$

We claim that any correct list of partial assignments of Player 2 that does not falsify any clause in F, has to satisfy simultaneously all the clauses at the configurations in each step. The argument is completed by observing that there must be a step in $\varPi$ in which the clauses in the configuration are not simultaneously satisfiable.

Theorem 2

Let F be an unsatisfiable formula, then ${{\mathrm{\mathsf {Vs}}}}(F \vdash )\le {{\mathrm{\mathsf {nisd}}}}(F).$

Proof

(sketch) Let L be the list of sets of variables constructed by Player 1, containing at each step i a set $L_i$ of at most ${{\mathrm{\mathsf {nisd}}}}(F)$ variables. We consider for each step i a set of clauses $\mathcal{C}_i$ containing only the variables in $L_i$. Initially $L_1$ is some set of variables and $\mathcal{C}_1$ is the set of all clauses that can be derived by resolution (in any number of steps) from the clauses in F containing only variables in $L_1$. At any step i, if $L_i$ is constructed by adding some new variables to $L_{i-1}$, $\mathcal{C}_i$ is defined to be the set of clauses that can be derived from the clauses in $\mathcal{C}_{i-1}$ and the clauses in F containing only variables in $L_i$. If $L_i$ is constructed by subtracting some new variables from $L_{i-1}$, $\mathcal{C}_i$ is defined to be the set of clauses in $\mathcal{C}_{i-1}$ that only have variables in the set $L_i$. By definition $\mathcal{C}_{i}$ can be always be constructed from $\mathcal{C}_{i-1}$ by using only resolution steps, deletion or inclusion of clauses in F, and therefore this list of sets of clauses can be written as a resolution proof. At every step in this proof at most ${{\mathrm{\mathsf {nisd}}}}(F)$ variables are present.

We claim that if L is a winning strategy for Player 1, then at some point i, $\mathcal{C}_i$ must contain the empty clause. This implies the result. To sketch a proof of this claim let us define at each step i the set $A_i$ of partial assignments for the variables in ${L}_{i}$ that satisfy all the clauses in $\mathcal{C}_{i},$ and the set $B_i$ to be the set of partial assignments for the variables in $L_i$ that do not falsify any initial clause and can be constructed by Player 2 following the rules of the game. It can be seen by induction on i that at each step, $A_i=B_i.$ Since at some point i, Player 2 does not have any correct assignment that does not falsify a clause in F, it follows that $A_i=B_i=\emptyset$, which means that $\mathcal{C}_i$ in unsatisfiable and must contain the empty clause by the definition of $\mathcal{C}_i$ and the completeness of resolution.

4 Cops and Robber Games

We consider a slight variation of the Cops and Robber game from Seymour and Thomas [15] which they used to characterize exactly the tree-width of a graph. We call our version the Edge (Cops and Robber) Game.

Initially a robber is placed on a vertex of a connected graph G. She can move arbitrarily fast to any other vertex along the edges. The team of cops, directed by one person, want to capture her, and can always see where she is. They are placed on edges and do not move.

Definition 3

(Edge Cops-Robber Game) Player 1 takes the role of the cops. At any stage he can place a cop on any unoccupied edge or remove a cop from and edge. The robber (Player 2) can then move to any vertex that is reachable from his actual position over a path without cops. Both teams have at any moment perfect information of the position of the other team. Initially no cop is on the graph. The game finishes when the robber is captured. This happens when the vertex she occupies is completely surrounded by cops.

The value of the game is the maximum number of edge-cops present on the edges at any point in the game. We define ${{\mathrm{\mathsf {ec}}}}(G)$ as the minimum value in a finishing Edge Game on G.

The only difference between our Edge Cops-Robber Game and the Cops-Robber game from Seymour and Thomas in that here the cops are placed on the edges, while in [15] they were placed on the vertices and that our game ends with the robber surrounded while in the Seymour-Thomas game a cop must occupy the same vertex as the robber.

4.1 The Cops-Robber Game Characterizes Width on Tseitin Formulas

The edge-cops game played on a connected graph G characterizes exactly the minimum width of a resolution refutation of ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ for any odd marking $\varphi$. In order to show this, we use the Atserias-Dalmau game [4] introduced to characterize resolution width. We prove that ${{\mathrm{\mathsf {ec}}}}(G)={{\mathrm{\mathsf {sd}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi ))$ where ${{\mathrm{\mathsf {sd}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi ))$ denotes the value of the Atserias-Dalmau game played on ${{\mathrm{\mathsf {T}}}}(G,\varphi ).$ We use the simplified explanation of the game from [16].

Spoiler and Duplicator play on a CNF formula F. Spoiler wants to falsify a clause of the formula, while Duplicator tries to prevent this from happening. During the game they construct a partial assignment $\alpha$ of the variables in F and the game ends when $\alpha$ falsifies a clause from F. Initially $\alpha$ is empty. At each step, Spoiler can select an unassigned variable x or forget (unassign) a variable from $\alpha$. In the first case the Duplicator assigns a value to x, in the second case she does not do anything. The value of a game is the maximum number of variables that are assigned in $\alpha$ at some point during the game. ${{\mathrm{\mathsf {sd}}}}(F)$ is the minimum value of a finishing game on F.

Atserias and Dalmau [4] proved that this measure characterizes the width of a resolution refutation of any unsatisfiable F, ${{\mathrm{\mathsf {W}}}}(F\vdash )=\max \{{{\mathrm{\mathsf {W}}}}(F), {{\mathrm{\mathsf {sd}}}}(F)-1\}$². Let us observe how the game goes when played on the formula ${{\mathrm{\mathsf {T}}}}(G,\varphi ).$ In a finishing game on ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ Spoiler and Duplicator construct a partial assignment $\alpha$ of the edges. Applying $\alpha$ to the variables of ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ a new graph $G'$ and marking $\varphi '$ are produced. Consider a partial truth assignment $\alpha$ of some of the variables. Assigning a variable $e=\{x,y\}$ in $\alpha$ to 0 corresponds to deleting the edge e in the graph, and setting it to 1 corresponds to deleting the edge from the graph and toggling the values of $\varphi (x)$ and $\varphi (y).$ The formula ${{\mathrm{\mathsf {T}}}}(G',\varphi ')$ resulting after applying $\alpha$ to $(G,\varphi )$ is still unsatisfiable. We will call a connected component of $G'$ for which the sum of the markings of its vertices is odd, an odd component. Initially G is an odd component under $\varphi$. By assigning an edge, an odd component can be divided in at most two smaller components, an odd one and an even one. The only way for Spoiler to end the game is to construct an assignment $\alpha$ that assigns values to all the edges of a vertex, contradicting its marking under $\alpha$. This falsifies one of the clauses corresponding to the vertex.

Theorem 4

For any connected graph G and any odd marking $\varphi$, ${{\mathrm{\mathsf {ec}}}}(G)={{\mathrm{\mathsf {sd}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )).$

Proof

In order to compare both games, the team of cops will be identified with the Spoiler and the robber will be identified with the Duplicator. Since the variables in ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ are the edges of G, the action of Spoiler selecting (forgetting) a variable in the Atserias-Dalmau game will be identified with placing (removing) a cop on that edge.

We show first that ${{\mathrm{\mathsf {ec}}}}(G)\le {{\mathrm{\mathsf {sd}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )).$ No matter what the strategy of Duplicator is, Spoiler has a way to play in which he spends at most ${{\mathrm{\mathsf {sd}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi ))$ points at the Spoiler-Duplicator game on ${{\mathrm{\mathsf {T}}}}(G,\varphi ).$ In order to obtain a value smaller or equal than ${{\mathrm{\mathsf {sd}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi ))$ in the Edge Game, the cops just have to imitate Spoiler’s strategy on ${{\mathrm{\mathsf {T}}}}(G,\varphi ).$ At the same time, they compute a strategy for Duplicator that simulates the position of the robber. This is done by considering a Duplicator assigning values in such a way that there is always a unique odd component which corresponds to the subgraph of G isolated by cops where the robber is. At any step in the Edge Game, we the following invariant is kept:

The partial assignment produced in the Spoiler-Duplicator game on ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ defines a unique odd component corresponding to the component of the robber.

If in a step of the Spoiler-Duplicator game the edge selected by Spoiler does not cut the component where the robber is, Player 1 can simulate Duplicator’s assignment for this variable in a way in which a unique odd component is kept and continue with the next decision of Spoiler. At a step right after the component of the robber is cut by the cops, Player 1 can compute an assignment of Duplicator for the last occupied edge, which would create a labeling that identifies the component where the robber as the unique odd component of the graph. This is always possible. Then Player 1 just needs to continue the imitation of Spoiler’s strategy for the assignment produced by Duplicator.

At the end of the game Spoiler falsifies an initial clause, and the vertex corresponding to this clause is the unique odd component under the partial assignment. Therefore the cops will be on the edges of a falsified clause, thus catching the robber on the corresponding vertex.

The proof of ${{\mathrm{\mathsf {ec}}}}(G)\ge {{\mathrm{\mathsf {sd}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi ))$ is very similar. Now we consider that there is a strategy for Player 1 in the Edge Game using at most ${{\mathrm{\mathsf {ec}}}}(G)$ cops, and we want to extract from it a strategy for the Spoiler. He just needs to select (remove) variables is the same way as the cops are being placed (removed). This time, all through the game we have the following invariant:

The component isolated by cops in which the robber is, is an odd component in the Spoiler-Duplicator game.

When the variable (edge) selected does not cut the component where the robber is, he does not need to do anything. When the last selected variable cuts the component of the robber, by choosing a value for this variable Duplicator decides which one of the two new components is the odd one. Spoiler figures that the robber has gone to the new odd component and asks the cops what to do next in this situation. When the robber is caught, this will be in an odd component of size 1 which all its edges assigned. This partial assignment falsifies the corresponding clause in ${{\mathrm{\mathsf {T}}}}(G,\varphi ).$

Corollary 5

For any connected graph G and any odd marking $\varphi$,

$${{\mathrm{\mathsf {W}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash )=\max \{\varDelta (G),{{\mathrm{\mathsf {ec}}}}(G)-1\}.$$

4.2 An Invisible Robber Characterizes Variable Space on Tseitin Formulas

Consider now the cops game in which the robber is invisible. That means that the cops strategy cannot depend on the robber and the cops have to explore the whole graph to catch her. As in the visible version of the game, the robber is caught if all the edges around the vertex in which she is, are occupied by cops. For a graph G let ${{\mathrm{\mathsf {iec}}}}(G)$ be the minimum number of edge-cops needed to catch an invisible robber in G. Let ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ be the Tseitin formula corresponding to G. We show that ${{\mathrm{\mathsf {iec}}}}(G)$ corresponds exactly with Vs$({{\mathrm{\mathsf {T}}}}(G,\varphi )).$

Theorem 6

${{\mathrm{\mathsf {Vs}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )) = {{\mathrm{\mathsf {iec}}}}(G).$

Proof

(sketch)

• (i) ${{\mathrm{\mathsf {Vs}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash ) \le {{\mathrm{\mathsf {iec}}}}(G).$ We use the game characterization of variable space. Consider the strategy of the cops. At each step the set of variables constructed by Spoiler corresponds to the set of edges (variables) where the cops are. Now consider any list of partial assignments that Player 2 might construct. Any such assignment can be interpreted as deleting some edges and moving the robber to an odd component in the graph. But the invisible robber is caught at some point, no matter what she does, and this corresponds to a falsified initial clause.

• (ii) ${{\mathrm{\mathsf {iec}}}}(G)\le {{\mathrm{\mathsf {Vs}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash ).$ Now we have a strategy for Spoiler, and the cops just need to be placed on the edges corresponding to the variables selected by Player 1. If the robber could escape, by constructing a list of partial assignments mimicking the robber moves (that is, each time the cops produce a new cut in the component where the robber is, she sets the value of the last assigned variable to make odd the new component where the robber has moved to), Player 2 never falsifies a clause in ${{\mathrm{\mathsf {T}}}}(G,\varphi ).$

4.3 A Game Characterization of Depth on Tseitin Formulas

We consider now a version of the game in which the cops have to remain on their edges until the end of the game and cannot be reused.

Definition 7

For a graph G let ${{\mathrm{\mathsf {iec}}}}(G)$ be the minimum number of edge-cops needed in order to catch a visible robber on G, in the cops-robber game, with the additional condition that the cops once placed, cannot be removed from the edges until the end of the game.

Theorem 8

For any connected undirected graph G and any odd marking $\varphi$ of G, ${{\mathrm{\mathsf {D}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash )={{\mathrm{\mathsf {iec}}}}(G)$.

Proof

(sketch)

• (i) ${{\mathrm{\mathsf {D}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash ) \le {{\mathrm{\mathsf {iec}}}}(G)$. Based on the strategy of the cops, we construct a regular resolution proof tree of ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ in which the variables are resolved in the order (from the empty clause) as the cops are being placed on the edges. Starting at the node in the tree corresponding to the empty clause, in each step when a cop is placed on edge e we construct two parent edges, one labeled by e and the other one by $\overline{e}$. A node in the tree is identified by the partial assignment defined by the path going from the empty clause to this node. Each time the cops produce a cut in G, such an assignment defines two different connected components in G, one with odd marking and one with even marking. We consider at this point the resolution of the component with the odd marking, following the cop strategy for the case in which the robber did go to this component.

• (ii) ${{\mathrm{\mathsf {iec}}}}(G)\le {{\mathrm{\mathsf {D}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash )$. Consider a resolution proof $\varPi$ of ${{\mathrm{\mathsf {T}}}}(G,\varphi )$. Starting by the empty clause, the cops are placed on the edges corresponding to the variables being resolved. At the same time a partial assignment is being constructed (by the robber) that defines a path in the resolution that goes through the clauses that are negated by the partial assignment. If removing these edges where the cops are produces a cut in G, the cops continue from a node in the resolution proof corresponding to an assignment for the last chosen variable that gives odd value to the component where the robber has moved. At the end a clause in ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ is falsified, which corresponds to the cops being placed in the edges around the robber. The number of cops needed is at most the resolution depth.

5 Regular Resolution and Monotone Games

We show in this section that the fact that the games can be played in a monotone way, implies that width and variable space in regular resolution are as good as in general resolution in the context for Tseitin formulas.

We need some further notation. For a set S and $k > 0$, we denote the set of subsets of S of size at most k by $S^k$.

5.1 The Visible Robber

We recall the game of [15]. Let $G = (V, E)$ be a simple graph and let $Y \subseteq V$. A Y-flap is the vertex set of a connected component in $G \setminus Y$. A position in this game is a pair (Y, Q) where $Y \subseteq V$ and Q is an Y-flap. The game starts in position $(\emptyset , V)$. Assume that position $(Y_i, Q_i)$ is reached. The cops-player chooses $Y_{i + 1}$ such that either $Y_i \subseteq Y_{i + 1}$ or $Y_{i + 1} \subseteq Y_i$. Then the robber-player chooses a $Y_{i + 1}$-flap $Q_{i + 1}$ such that $Q_i \subseteq Q_{i + 1}$ or $Q_{i + 1} \subseteq Q_i$. The cops-player wins when $Q_i \subseteq Y_{i + 1}$. We say that a sequence of positions $(Y_0, Q_0), \ldots , (Y_t, Q_t)$ is monotone if for all $0 \le i \le j \le k \le t$, $Y_i \cap Y_k \subseteq Y_j$. The main result of Seymour and Thomas is that if k cops can win the game, they can also win monotonically. We will use this result to prove an analogous statement about our games where we put the cops on edges.

We extend the framework of Seymour and Thomas to talk about edges. Now we have $X \subseteq E$. An X-flap is the edge set of a connected component in $G\setminus X$. A position is a pair (X, R) with $X \subseteq E$ and R an X-flap. Assume that a position $(X_i, R_i)$ is reached. The cops-player chooses $X_{i + 1}$ such that either $X_i \subseteq X_{i + 1}$ or $X_{i + 1} \subseteq X_i$. Then the robber-player chooses an $X_{i + 1}$-flap $R_{i + 1}$ such that either $R_i \subseteq R_{i + 1}$ or $R_{i + 1} \subseteq R_i$. The cops win when $R_i \subseteq X_{i + 1}$. Note that under this definition if some X isolates more than one vertex, then we will have multiple empty sets as X-flaps. However if the robber moves to such an X-flap she will immediately lose as in the next round the cops remain where they are and $\emptyset \subseteq X$.

Similarly a sequence of positions $(X_0, R_0), \ldots , (X_t, R_t)$ is monotone if for all $0 \le i \le j \le k \le t$, $X_i\cap X_k\subseteq X_j$.

Given a graph $G = (V, E)$ the line graph of G is $L(G) = (V', E')$ defined as follows: for every edge $e \in E$ we put a vertex $w_e \in V'$. We then set

$$E' = \{\{w_{e_1}, w_{e_2}\} : e_1, e_2 \in E, e_1 \cap e_2 \ne \emptyset \}.$$

For $X \subseteq E$ define $L(X) := \{w_e : e \in X\}$ and for $Y \subseteq V'$ define $L^{-1}(Y) = \{e : w_e \in Y\}$.

Proposition 9

Let $G = (V, E)$ be a graph and let $X \subseteq E$. It follows that $R \subseteq E$ is an X-flap if and only L(R) is an L(X)-flap.

Proof

It is enough to show that any $e_1, e_2 \in E \setminus X$ are reachable from each other in $G \setminus X$ if and only if $w_{e_1}$ and $w_{e_2}$ are reachable from each other in $L(G) \setminus L(X)$. Let $P = e_1, f_1, \ldots , f_t, e_2$ be a path in $G\setminus X$ connecting $e_1$ and $e_2$. By construction we have a path $w_{e_1}, w_{f_1}, \ldots , w_{f_t}, w_{e_2}$ in $L(G) \setminus L(X)$.

Conversely let $w_{e_1}, w_{f_1}, \ldots , w_{f_t}, w_{e_2}$ be a path of minimum length between $w_{e_1}$ and $w_{e_2}$ in $L(G) \setminus L(X)$. It is easy to see that $e_1, f_1, \ldots , f_t, e_2$ is a path between $e_1$ and $e_2$ in $G \setminus X$.

Theorem 10

Assume that there is a strategy for the edge-cops game on G with k cops. Then there exists a strategy for the vertex-cops game in L(G) with k cops.

Proof

Fix a strategy $\sigma$ for the edge-cops on G, i.e., for every $X \in E^k$ and every X-flap R, $\sigma (X, R) \in E^k$ which guarantees that the robber will eventually be captured. We will inductively construct a sequence $\{(Y_i, Q_i)\}$ of positions in the vertex game on L(G), where $Q_i$s are the responses of the robber, while keeping a corresponding sequence $\{(X_i, R_i)\}$ for the edge game on G. The vertex game starts in position $(Y_0, Q_0) = (\emptyset , V')$ and the edge game starts in $(X_0, R_0) = (\emptyset , E)$. We have $X_1 = \sigma (X_0, R_0)$. In general we set $Y_i = L(X_i)$ and after the robber has responded with $Q_i$ we define $R_i = L^{-1}(Q_i)$, from which we construct $X_{i + 1} = \sigma (X_i, R_i)$ and so on. That $R_i$ is an $X_i$-flap follows immediately from Proposition 9. To see that this is indeed a winning strategy, note that at some point we reach a position with $R_i \subseteq X_{i + 1}$. This happens only when $Q_i \subseteq Y_{i + 1}$.

Theorem 11

Assume that there is a monotone strategy for the vertex-cops game in L(G) with k cops. Then there exists a monotone strategy with k cops for the edge-cops game in G.

Proof

We will construct a sequence $\{(X_i, R_i)\}$ of positions in the edge game on G while keeping a corresponding sequence $\{(Y_i, Q_i)\}$ of positions in the vertex game on L(G). Note that $R_i$ will be the response of the robber on G. Let $\sigma$ be a monotone strategy with k vertex-cops on L(G). We will inductively construct $X_i = \{e : w_e \in Y_i\}$ and after the robber has responded with $R_i$ we define $Q_i = L(R_i)$. Proposition 9 implies that $Q_i$ is a $Y_i$-flap. Since $\sigma$ is a winning strategy at some point we reach a position with $Q_i \subseteq Y_{i + 1}$. This happens only when $R_i \subseteq X_{i + 1}$. The monotonicity of the strategy follows immediately.

5.2 The Invisible Robber

In a similar way as we did with the visible robber game, we can reduce the edge-game with an invisible robber to the invisible robber vertex-game of Kirousis and Papadimitriou [12] (we will call this game KP). In their game cops are placed on vertices. An edge is cleared if both its endpoints have cops. An edge can be recontaminated if it is connected to an uncleared edge passing through no cops. It is shown in [12] that the cops can optimally clear all the edges without occupying any vertex twice.

Theorem 12

Assume that k cops can win the edge-game capturing an invisible robber on G. Then k cops can capture the robber in KP game on L(G).

Theorem 13

Assume that k cops can monotonically capture the robber in KP game on L(G). Then k cops can monotonically capture the invisible robber in the edge-game on G.

Corollary 14

Let $G = (V, E)$ be a simple connected graph and let $\varphi$ be any odd marking of G. Assume that there exist a resolution refutation of ${{\mathrm{\mathsf {T}}}}(G, \varphi )$ of variable space at most k. Then there exists a regular resolution refutation of ${{\mathrm{\mathsf {T}}}}(G, \varphi )$ of variable space at most k.

6 New Relations Between Complexity Measures for Tseitin Formulas

For any unsatisfiable formula F the following inequalities hold:

$$\begin{aligned} {{\mathrm{\mathsf {W}}}}(F\vdash ) \le {{\mathrm{\mathsf {Vs}}}}(F\vdash ) \end{aligned}$$

(1)

$$\begin{aligned} {{\mathrm{\mathsf {Vs}}}}(F\vdash ) \le {{\mathrm{\mathsf {D}}}}(F\vdash ) \end{aligned}$$

(2)

$$\begin{aligned} {{\mathrm{\mathsf {Cs}}}}(F\vdash )\le {{\mathrm{\mathsf {D}}}}(F\vdash )+1 \end{aligned}$$

(3)

$$\begin{aligned} {{\mathrm{\mathsf {Cs}}}}(F\vdash )\ge {{\mathrm{\mathsf {W}}}}(F\vdash ) -{{\mathrm{\mathsf {W}}}}(F)+1 \end{aligned}$$

(4)

Here Eq. 1 follows by definition, Eq. 2 is proved in [19], Eq. 4 is the Atserias-Dalmau [4] width-space inequality and Eq. 3 follows from the following two observations:

• 1. Any resolution refutation $\pi$ can be transformed, doubling subproofs, in a tree-like refutation with the same depth of the original proof $\pi$.

• 2. The clause space of a treelike refutation is at most as large as its depth$+1$ [9].

In general the relationship between variable space and clause space is not clear. It is also an open problem to know whether variable space and depth are polynomially related (see [14, 19]) and if clause space is polynomially bounded in variable space (see Razborov in [14], Open problems). In this section we answer this questions in the context of Tseitin formulas. We show in Corollary 17 below that for any Tseitin formula ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ corresponding to a graph G with n vertices,

$$\begin{aligned} {{\mathrm{\mathsf {D}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi ) \vdash )\le {{\mathrm{\mathsf {W}}}}( {{\mathrm{\mathsf {T}}}}(G,\varphi ) \vdash )\log n \end{aligned}$$

(5)

From this and the inequalities above it follow the following new relations:

$$\begin{aligned} {{\mathrm{\mathsf {D}}}}( {{\mathrm{\mathsf {T}}}}(G,\varphi ) \vdash )\le {{\mathrm{\mathsf {Vs}}}}( {{\mathrm{\mathsf {T}}}}(G,\varphi ) \vdash )\log n \end{aligned}$$

(6)

$$\begin{aligned} {{\mathrm{\mathsf {Cs}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi ) \vdash )\le {{\mathrm{\mathsf {Vs}}}}( {{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash )\log n+1 \end{aligned}$$

(7)

$$\begin{aligned} {{\mathrm{\mathsf {Vs}}}}( {{\mathrm{\mathsf {T}}}}(G,\varphi ) \vdash )\le ({{\mathrm{\mathsf {Cs}}}}( {{\mathrm{\mathsf {T}}}}(G,\varphi ) \vdash )+\varDelta (G)-1)\log n. \end{aligned}$$

(8)

Where the last equation follow since ${{\mathrm{\mathsf {W}}}}( {{\mathrm{\mathsf {T}}}}(G,\varphi ))= \varDelta (G)$.

That is, in the context of Tseitin formulas ${{\mathrm{\mathsf {T}}}}(G,\varphi )$:

• 1. If G is a graph of bounded degree, the width, depth, variable space and clause space for refuting ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ differ by at most a $\log n$ factor.

• 2. For any graph G the clause space of refuting ${{\mathrm{\mathsf {T}}}}(G, \varphi )$ is bounded above by the a $\log n$ factor of the variable space of refuting ${{\mathrm{\mathsf {T}}}}(G, \varphi )$.

To prove our results, we need two preliminary lemmas.

Lemma 15

Let ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ be a Tseitin formula and $\varPi$ be a width k resolution refutation of ${{\mathrm{\mathsf {T}}}}(G,\varphi ).$ From $\varPi$ it is possible to find in linear time in $|\varPi |$ a set W of at most $k+1$ variables such that any assignment of these variables when applied to G in the usual way, defines a graph $G'$ and a labeling $\varphi '$ in which there is some odd connected component with at most $\lceil \frac{|V|}{2}\rceil$ vertices.

Proof

We use again the Spoiler and Duplicator game from [4]. A way for Spoiler to pay at most $k+1$ points on the game on ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ is to use the structure of $\varPi$ starting at the empty clause and query each time the variable that is being resolved at the parent clauses. When Duplicator assigns a value to this variable, Spoiler moves to the parent clause falsified by the partial assignment and deletes from this assignment any variables that do not appear in the parent clause. In this way he always reaches at some point an initial clause, falsifying it and thus winning the game. At any point at most $k+1$ variables have to be assigned. To this strategy of Spoiler, Duplicator can oppose the following strategy: She applies the partial assignment being constructed to the initial graph G producing a subgraph $G'$ and a new labeling $\varphi '$. Every time a variable e has to be assigned, if e does not produce a new cut in $G'$ she gives to e an arbitrary value. If e cuts an odd component in $G'$ she assigns e with the value that makes the largest of the two new components an odd component. In case e cuts an even component in two, Duplicator gives to e the value which keeps both components even. Observe that with this strategy there is always a unique odd component. Even when Spoiler releases the value of some assigned variable he cannot create more components, he either keeps the same number of components or connects two of them.

While playing the game on ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ with these two strategies, both players define a path from the empty clause to an initial one. There must be a first clause K along this path in which the constructed partial assignment constructed in the game at the point t in which K is reached, when applied to G, defines a unique odd component of size at most $\lceil \frac{|V|}{2}\rceil .$ This is so because the unique odd component initially has size |V| while at the end has size 1. This partial assignment has size at most $k+1$. Not only the odd component, but any component produced by the partial assignment has size at most $\lceil \frac{|V|}{2}\rceil .$ This is because at the point before t the odd component was larger than $\lceil \frac{|V|}{2}\rceil$ and therefore any other component had to be smaller than this. At time t Spoiler chooses a variable that when assigned cuts the odd component in two pieces. Duplicator assigns it in such a way that the largest of these two components is odd and has size at most $\lceil \frac{|V|}{2}\rceil$. Therefore the other new component must have at most this size.

Any other assignment of these variables also produces an odd component of size at most $\lceil \frac{|V|}{2}\rceil$. They correspond to other strategies and they all produce the same cuts and components in the graph, just different labellings of the components. Since the initial formula was unsatisfiable there must always be at least one odd component. In order to find the set W of variables, one just has to move on refutation $\varPi$ simulating Spoiler and Duplicator strategies. This can be done in linear time in the size of $\varPi .$

Theorem 16

There is an algorithm that on input a connected graph $G=(V,E)$ with an odd labeling $\varphi$ and a resolution refutation $\varPi$ of ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ with width k, produces a tree-like resolution refutation $\varPi '$ of ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ of depth ${k\log (|V|)}.$

Proof

Let $W=\{e_1,\dots e_{|W|}\}$ be a set of variables producing an odd connected component of size at most $\lceil \frac{|V|}{2}\rceil$, as guaranteed by Lemma 15. We can construct a tree-like resolution of depth |W| of the complete formula $F_W$ with $2^{|W|}$ clauses, each containing all variables in W but with a different sign combination.

By the Lemma, each assignment of the variables, when applied to G produces a subgraph $G_i$ and a labeling $\varphi _i$ with an odd component with at most $\lceil \frac{|V|}{2}\rceil$ vertices. The problem of finding a tree-like refutation for ${{\mathrm{\mathsf {T}}}}(G,\varphi )$ has been reduced to finding a tree-like resolution refutation for each of the formulas ${{\mathrm{\mathsf {T}}}}(G_i,\varphi _i)$. But each of the graphs $G_i$ have an odd component with at most $\lceil \frac{|V|}{2}\rceil$ vertices and the problem is to refute the Tseitin formulas corresponding to these components. After at most $\log (|V|)$ iterations we reach Tseitin formulas with just two vertices that can be refuted by trees of depth one. Since W has width at most $k+1$ literals, in each iteration the refutation trees have depth at most k. Putting everything together we get a tree-like refutation of depth at most $k\log (|V|).$

Corollary 17

For any graph $G=(V,E)$ and any odd labeling $\varphi$,

${{\mathrm{\mathsf {D}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash )\le {{\mathrm{\mathsf {W}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash )\log (|V|).$

Corollary 18

For any graph $G=(V,E)$ and any odd labeling $\varphi$

${{\mathrm{\mathsf {Cs}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash )\le {{\mathrm{\mathsf {Vs}}}}({{\mathrm{\mathsf {T}}}}(G,\varphi )\vdash )\log (|V|).$

7 Conclusions and Open Problems

We have shown that the measures of width, depth and variable space in the resolution of Tseitin formulas can be exactly characterized in terms of a graph searching game played on the underlying graph. Our game is a slight modification of the well known cops-robber game from Seymour and Thomas. The main motivation for this characterization is the fact that some results in graph searching can be used to solve questions in proof complexity. Using the monotonicity properties of the Seymour and Thomas game, we have proven that the measures of width and variable space in regular resolution coincide exactly with those of general resolution in the context of Tseitin formulas. Previously it was only known that for Tseitin formulas, regular width was within a constant factor of the width in general resolution [2]. The game characterization also inspired new relations between the three resolution measures on Tseitin formulas and we proved that they are all within a logarithmic factor.

We have also obtained a game characterization of variable space for the resolution of general CNF formulas, as a non-interactive version of the Atserias and Dalmau game [4] for resolution width.

Still open is whether for Tseitin formulas, regular resolution can also simulate general resolution in terms of size, as asked by Urquhart [18]. Also game characterizations for other resolution measures like size or space, either for Tseitin or general formulas, would be a very useful tool in proof complexity.