13 The \((k, \ell )\)-pebble game
Lee and Streinu [ LS08 ] decide whether a graph is \((k, \ell )\)-sparse by an algorithm, the \((k, \ell )\)-pebble game. It generalizes the pebble game of Jacobs and Hendrickson [ JH97 ] for rigidity in the plane, which in Lee and Streinu’s terms is the \((2, 3)\)-pebble game [ LS08 , p. 1426 ] . The game considers the edges of the input graph one at a time. It keeps the accepted edges oriented, with pebbles on the vertices, and it accepts an edge when at least \(\ell + 1\) free pebbles can be gathered on its two endpoints. We formalize Lee and Streinu’s basic pebble game [ LS08 , § 3 ] on simple graphs, for \(\ell {\lt} 2k\), the range they consider. We prove that it accepts every edge of a graph \(G\) if and only if \(G\) is \((k, \ell )\)-sparse. When it rejects an edge, it returns a set of vertices that shows that \(G\) is not \((k, \ell )\)-sparse.
In section 13.1 we describe the state of the game, a partial orientation from which the free pebbles are counted, and its two moves, which reverse a directed path and insert an arc. In section 13.2 we prove Lee and Streinu’s four invariants for the orientations that these moves reach. In section 13.3 we define the algorithm; it finds pebbles with the depth-first search of section 12. We prove the two directions of correctness in section 13.4 and section 13.5, and combine them in section 13.6. The first direction follows from the fourth invariant. For the second, we show that when the game rejects an edge, the set \(V'\) of vertices reachable from its endpoints spans more than \(k|V'| - \ell \) edges of \(G\). In the formalization, the game returns its answer together with these proofs, as a verdict (section 13.7). In section 13.8 we return to the \((k, \ell )\)-count matroid of section 11: the game decides whether the edge set of a graph is independent in it, and so, at \((k, \ell ) = (2, 3)\), in the planar rigidity matroid.
Lee and Streinu play the game on multigraphs, which may have loops and parallel edges. On simple graphs their invariants simplify (formalization note 13.8). We do not formalize their component pebble game (§5). It maintains the components of the accepted graph (section 11), rejects an edge at once when both its endpoints lie in one component, and runs in time \(O(n^2)\) on \(n\) vertices [ LS08 , p. 1436 ] . For the details of its implementation, Lee and Streinu refer to Lee, Streinu and Theran [ LST05 ] , who introduce for them a data structure problem, union pair-find. Nor do we formalize the Henneberg sequences of Lee and Streinu’s §6, which extend the Henneberg construction (section 5) from Laman graphs to tight graphs.
Lee and Streinu bound the running time of their basic game by \(O(m_a n)\), where \(m_a\) is the number of accepted edges, counting at most \(\ell + 1\) depth-first searches for each edge [ LS08 , p. 1430 ] . Our pebble search enters each vertex at most once (section 12), but we prove no bound on the running time of our game.
13.1 State and moves
Lee and Streinu play the pebble game on a directed graph \(D\) on \(V\), which starts with no edges and with \(k\) pebbles on each vertex [ LS08 , § 3 ] . An edge is inserted into \(D\) oriented away from an endpoint that holds a pebble, and that pebble is removed. On a simple graph, \(D\) has no loops and at most one arc between two vertices, so it is a partial orientation (definition 13.1). By Lee and Streinu’s Invariant (1) [ LS08 , Lemma 10 ] , the number of free pebbles at a vertex is then \(k\) minus its out-degree. So we do not keep the pebbles separately, and define them from \(D\) (definition 13.2). The game changes \(D\) by two moves. It reverses a directed path, which moves a pebble from the end of the path to its start (definition 13.4). It also inserts arcs (definition 13.5).
Let \(V\) be a set. A partial orientation on \(V\) is a finite set \(D \subseteq V \times V\) such that:
(no loops) \((v, v) \notin D\) for every \(v \in V\);
(no antiparallel pairs) if \((u, v) \in D\), then \((v, u) \notin D\).
The elements of \(D\) are its arcs, and an arc \((u, v)\) has tail \(u\) and head \(v\). An edge \(uv\) of the complete graph \(K_V\) is oriented in \(D\) if \((u, v) \in D\) or \((v, u) \in D\). The underlying edge set \(\underline{D} \subseteq E(K_V)\) is the set of edges oriented in \(D\). The empty orientation has no arcs.
Let \(D\) be a partial orientation on \(V\), and let \(k\) be a non-negative integer. For a vertex \(v\), the out-degree \(\mathrm{out}_D(v)\) is the number of arcs of \(D\) with tail \(v\), and the number of free pebbles at \(v\) is
For a finite set \(V' \subseteq V\), let
\(\mathrm{peb}_{D,k}(V') = \sum _{v \in V'} \mathrm{peb}_{D,k}(v)\);
\(\mathrm{span}_D(V')\) be the number of arcs of \(D\) with both ends in \(V'\);
\(\mathrm{out}_D(V')\) be the number of arcs of \(D\) with tail in \(V'\) and head outside \(V'\).
These are Lee and Streinu’s functions \(\mathrm{peb}\), \(\mathrm{span}\) and \(\mathrm{out}\) [ LS08 , § 4 ] , for a graph without loops. The maximum with \(0\) matters only when \(\mathrm{out}_D(v) {\gt} k\). This does not happen at the orientations the game reaches, the \((k, \ell )\)-reachable ones of definition 13.6, as Invariant (1) of lemma 13.7 shows.
In order, the five pins define \(\mathrm{out}_D(v)\), \(\mathrm{peb}_{D,k}(v)\), \(\mathrm{span}_D(V')\), \(\mathrm{out}_D(V')\) and \(\mathrm{peb}_{D,k}(V')\).
Let \(D\) be a partial orientation on \(V\). A directed path in \(D\) from \(u_0\) to \(u_m\) is a simple directed walk \(u_0, u_1, \ldots , u_m\) along the arcs of \(D\) (definition 12.1): the vertices \(u_i\) are distinct, and \((u_{i-1}, u_i) \in D\) for \(1 \le i \le m\). Reversing the path replaces \(D\) by the partial orientation
The underlying edge sets of \(D'\) and \(D\) are equal.
The set \(D'\) is a partial orientation. It has no loops, since the vertices of the path are distinct. Each arc of \(D'\) is either an arc of \(D\) off the path or the reverse \((u_i, u_{i-1})\) of an arc of the path. Two arcs of \(D\) off the path are not antiparallel, since \(D\) has no antiparallel pairs. The arc \((u_i, u_{i-1})\) is not antiparallel to an arc of \(D\) off the path, since \((u_{i-1}, u_i)\) is on the path. Nor is it antiparallel to the reverse of another arc of the path, since a path with distinct vertices does not use the edge \(u_{i-1} u_i\) twice.
Let \(m \ge 1\). Reversing the path lowers \(\mathrm{out}_D(u_0)\) by \(1\), raises \(\mathrm{out}_D(u_m)\) by \(1\), and leaves every other out-degree unchanged: an inner vertex \(u_i\) loses the arc \((u_i, u_{i+1})\) and gains the arc \((u_i, u_{i-1})\). Suppose that \(\mathrm{out}_D(u_0) \le k\) and \(\mathrm{out}_D(u_m) {\lt} k\). Then \(u_0\) gains a free pebble and \(u_m\) loses one, so the move takes a pebble from \(u_m\) to \(u_0\). This is the move by which Lee and Streinu collect a pebble [ LS08 , § 3, Fig. 4 ] .
Let \(D\) be a partial orientation on \(V\), and let \(u \ne v\) be vertices with \((v, u) \notin D\). Inserting the arc \((u, v)\) replaces \(D\) by the partial orientation \(D \cup \{ (u, v)\} \). Its underlying edge set is \(\underline{D} \cup \{ uv\} \).
The set \(D \cup \{ (u, v)\} \) is a partial orientation, since \(u \ne v\) rules out a loop and \((v, u) \notin D\) rules out an antiparallel pair. If the arc is new, that is, if \((u, v) \notin D\), the insertion raises \(\mathrm{out}_D(u)\) by \(1\) and leaves every other out-degree unchanged. If moreover \(\mathrm{out}_D(u) {\lt} k\), then \(u\) loses a free pebble. This is Lee and Streinu’s edge insertion [ LS08 , § 3, Fig. 4 ] .
13.2 Invariants
Lee and Streinu [ LS08 , Lemma 10 ] prove four invariants of their game. We prove them for the orientations obtained from the empty one by the two moves, each made under the conditions the game imposes on it (definition 13.6). Invariant (4) bounds the number of underlying edges inside a set of vertices by the sparsity count, and the soundness of the game (section 13.4) follows from it.
Let \(k\) and \(\ell \) be non-negative integers. The \((k, \ell )\)-reachable partial orientations on \(V\) form the smallest set of partial orientations that contains the empty orientation and is closed under the following two moves, applied to a member \(D\):
reversing a directed path in \(D\) from \(u_0\) to \(u_m\) with \(\mathrm{out}_D(u_m) {\lt} k\) (definition 13.4);
inserting an arc \((u, v)\) with \(u \ne v\), \((u, v) \notin D\), \((v, u) \notin D\), \(\mathrm{out}_D(u) {\lt} k\) and \(\mathrm{peb}_{D, k}(u) + \mathrm{peb}_{D, k}(v) \ge \ell + 1\) (definition 13.5).
Let \(V\) be a set, let \(k\) and \(\ell \) be non-negative integers, and let \(D\) be a \((k, \ell )\)-reachable partial orientation on \(V\). Let \(v \in V\), and let \(V' \subseteq V\) be a finite set. Then:
\(\mathrm{peb}_{D, k}(v) + \mathrm{out}_D(v) = k\);
\(\mathrm{peb}_{D, k}(V') + \mathrm{span}_D(V') + \mathrm{out}_D(V') = k|V'|\);
if \(\ell \le k|V'|\), then \(\mathrm{peb}_{D, k}(V') + \mathrm{out}_D(V') \ge \ell \);
if \(\ell \le k|V'|\), then \(\mathrm{span}_D(V') \le k|V'| - \ell \).
We argue by induction on the moves that produce \(D\) from the empty orientation (definition 13.6).
For (1) it suffices to show that \(\mathrm{out}_D(v) \le k\), by the definition of \(\mathrm{peb}_{D, k}(v)\). All out-degrees are \(0\) at the empty orientation. Reversing a path raises no out-degree other than that of its last vertex \(u_m\), which it raises by at most \(1\), and the move requires \(\mathrm{out}_D(u_m) {\lt} k\). Inserting an arc raises no out-degree other than that of its tail \(u\), which it raises by \(1\), and the move requires \(\mathrm{out}_D(u) {\lt} k\).
For (2) we need no induction. Summing (1) over \(V'\) gives
An arc with tail in \(V'\) has its head either in \(V'\) or outside it. So the sum of the out-degrees over \(V'\) is \(\mathrm{span}_D(V') + \mathrm{out}_D(V')\).
For (3), let \(\ell \le k|V'|\). At the empty orientation the left-hand side is \(k|V'| \ge \ell \). Reversing a path does not change \(\mathrm{span}_D(V')\), since it replaces each arc of the path by an arc with the same ends. By (2), before and after the move, it does not change \(\mathrm{peb}_{D, k}(V') + \mathrm{out}_D(V')\) either. Inserting a new arc \((u, v)\) with \(\mathrm{out}_D(u) {\lt} k\) lowers \(\mathrm{peb}_{D, k}(V')\) by \(1\) if \(u \in V'\), and leaves it unchanged otherwise. It raises \(\mathrm{out}_D(V')\) by \(1\) if \(u \in V'\) and \(v \notin V'\), and leaves it unchanged otherwise. So the insertion lowers the left-hand side of (3) by \(1\) if \(u, v \in V'\), and leaves it unchanged otherwise. If \(u, v \in V'\), then before the move
so the left-hand side is at least \(\ell \) after it.
Part (4) follows from (2) and (3).
Lee and Streinu state their Lemma 10 for multigraphs, and the setting here simplifies it in two ways. First, a simple graph has no loops. Their invariant \(\mathrm{peb}(v) + \mathrm{span}(v) + \mathrm{out}(v) = k\), in which \(\mathrm{span}(v)\) counts the loops at \(v\), therefore becomes (1). Second, they assume \(|V'| \ge 1\) when \(\ell \le k\) and \(|V'| \ge 2\) when \(k {\lt} \ell {\lt} 2k\). Both give \(\ell \le k|V'|\), which is the hypothesis of (3) and (4) here; no part needs \(\ell {\lt} 2k\). The formal statement of (4) is \(\mathrm{span}_D(V') + \ell \le k|V'|\), which avoids the truncated subtraction of natural numbers. Under \(\ell \le k|V'|\) the two forms agree. The first two pins are (1), in the equivalent form \(\mathrm{out}_D(v) \le k\) and as stated, and the other three are (2) to (4).
13.3 The basic algorithm
Lee and Streinu’s basic pebble game [ LS08 , § 3, Fig. 4 ] considers the edges of the input graph one at a time. An edge \(uv\) is accepted, and inserted as an arc, when \(u\) and \(v\) together hold at least \(\ell + 1\) free pebbles. While they hold fewer, the game searches \(D\) for a free pebble on another vertex, reachable from \(u\) or from \(v\), and brings it to \(u\) or \(v\) by reversing a directed path. If there is no such pebble, the edge is rejected. Lee and Streinu go on after a rejected edge, in order to classify the input graph. Our game stops at the first rejected edge, and returns a set of vertices which shows that the graph is not \((k, \ell )\)-sparse.
We define the algorithm in three levels. The pebble search (definition 13.9) looks for a vertex with a given property, here a free pebble, and reverses the path to it. Processing an edge (definition 13.12) repeats pebble searches until it can insert the edge or must reject it. The pebble game (definition 13.14) processes a list of edges in turn.
The search of section 12 visits the out-neighbours of a vertex in the order of a list. In this subsection, each partial orientation \(D\) on \(V\) comes with a list \(N^+_D(a)\) for each vertex \(a\), whose entries are the out-neighbours of \(a\) in \(D\), that is, the vertices \(b\) with \((a, b) \in D\). Every result below holds for every choice of these lists.
Let \(D\) be a partial orientation on a finite set \(V\), and let each vertex \(a\) have a list \(N^+_D(a)\) whose entries are the out-neighbours of \(a\) in \(D\). Let \(P\) be a predicate on \(V\), and let \(v \in V\). The pebble search for \(P\) from \(v\) in \(D\) runs the search for \(P\) from \(v\) (definition 12.2) with these lists, so that the search follows the arcs of \(D\).
If the search returns a vertex \(w\) and a walk \(p\), then \(p\) is a directed path in \(D\) from \(v\) to \(w\), and \(P(w)\) holds (theorem 12.4). The pebble search returns \(w\), \(p\), and the partial orientation obtained from \(D\) by reversing \(p\) (definition 13.4).
If the search fails, the pebble search fails.
The first two pins are the pebble search, with the lists \(N^+_D(a)\) as an argument and with mathlib’s lists (formalization note 13.15). The third computes the partial orientation obtained from \(D\) by reversing \(p\), from the data that the search returns.
When the processing of an edge \(uv\) cannot gather \(\ell + 1\) free pebbles on \(u\) and \(v\), it rejects \(uv\) and returns the following data.
Let \(V\) be a set, and let \(k\) and \(\ell \) be non-negative integers. A failure witness consists of a partial orientation \(D\) on \(V\), a finite set \(V' \subseteq V\), and a pair \((u, v)\) of distinct vertices in \(V'\), such that:
\(D\) is \((k, \ell )\)-reachable (definition 13.6);
the edge \(uv\) is not oriented in \(D\);
no arc of \(D\) has its tail in \(V'\) and its head outside \(V'\), that is, \(\mathrm{out}_D(V') = 0\);
\(\mathrm{peb}_{D, k}(V') \le \ell \).
A failure witness does not mention a graph. Let \(\ell {\lt} 2k\), and let \(G\) be a simple graph on \(V\) with finitely many edges, whose edges include \(uv\) and the edges in \(\underline{D}\). Then \(\ell \le k|V'|\), and \(V'\) spans more than \(k|V'| - \ell \) edges of \(G\) (lemma 13.22).
Let \(V\) be a finite set, and let \(k\) and \(\ell \) be non-negative integers. Let each partial orientation on \(V\) come with lists \(N^+_D(a)\) as in definition 13.9. Let \(D\) be a \((k, \ell )\)-reachable partial orientation on \(V\), and let \(u \ne v\) be vertices such that the edge \(uv\) is not oriented in \(D\). Let \(P_D\) be the predicate that holds at a vertex \(w\) when \(w \ne u\), \(w \ne v\) and \(\mathrm{peb}_{D, k}(w) {\gt} 0\). Processing \(uv\) at \(D\) runs as follows.
If \(\mathrm{peb}_{D, k}(u) + \mathrm{peb}_{D, k}(v) \ge \ell + 1\), it accepts \(uv\). It inserts the arc \((u, v)\) if \(\mathrm{peb}_{D, k}(u) {\gt} 0\), and the arc \((v, u)\) otherwise (definition 13.5), and returns the result.
Otherwise, it runs the pebble search for \(P_D\) from \(u\) in \(D\). If this search does not fail, it processes \(uv\) at the partial orientation \(D'\) that the search returns.
Otherwise, it runs the pebble search for \(P_D\) from \(v\) in \(D\). If this search does not fail, it processes \(uv\) at the partial orientation \(D'\) that the search returns.
Otherwise it rejects \(uv\). It returns the failure witness made of \(D\), the set \(\mathrm{Reach}_D(u) \cup \mathrm{Reach}_D(v)\) and the pair \((u, v)\). Here \(\mathrm{Reach}_D(x)\) is the reachability region of \(x\) in \(D\), the set of vertices reachable from \(x\) along the arcs of \(D\) (definition 12.5).
We check that each step is defined and that the processing stops. In step 1 the inserted arc is new, and its tail has a free pebble, since \(\mathrm{peb}_{D, k}(v) \ge \ell + 1 \ge 1\) when \(\mathrm{peb}_{D, k}(u) = 0\). So the insertion is a move of definition 13.6, and the result is \((k, \ell )\)-reachable.
In step 2, the pebble search returns a directed path from \(u\) to a vertex \(w\) with \(w \ne u, v\) and \(\mathrm{peb}_{D, k}(w) {\gt} 0\). So the path has at least one arc, and \(\mathrm{out}_D(w) {\lt} k\). Hence \(D'\) is \((k, \ell )\)-reachable, and \(uv\) is not oriented in \(D'\), since the reversal keeps the underlying edge set. Since \(D\) is \((k, \ell )\)-reachable, \(\mathrm{out}_D(u) \le k\) by Invariant (1) of lemma 13.7. So the reversal raises \(\mathrm{peb}_{D, k}(u)\) by \(1\). It leaves \(\mathrm{peb}_{D, k}(v)\) unchanged, since \(v\) is not an end of the path. Step 3 is the same with \(u\) and \(v\) exchanged. Hence \(\ell + 1 - \mathrm{peb}_{D, k}(u) - \mathrm{peb}_{D, k}(v)\) drops by \(1\) each time the processing starts again, so step 1 or step 4 is reached.
Lee and Streinu mark \(u\) and \(v\) before the search, so that it neither passes through them nor moves their pebbles [ LS08 , § 3, Fig. 4 ] . Here the predicate \(P_D\) only excludes \(u\) and \(v\) as ends of the path. A search may pass through \(u\) or \(v\), but reversing a path does not change the out-degrees of its inner vertices.
The data returned in step 4 form a failure witness. By hypothesis, \(D\) is \((k, \ell )\)-reachable and \(uv\) is not oriented in \(D\). The set \(V' = \mathrm{Reach}_D(u) \cup \mathrm{Reach}_D(v)\) contains \(u\) and \(v\). No arc of \(D\) leaves \(V'\), since the head of an arc whose tail is reachable from \(u\) is reachable from \(u\), and likewise for \(v\). Both pebble searches failed, so no vertex reachable from \(u\) or from \(v\) satisfies \(P_D\) (theorem 12.4, part (2)). Hence every vertex of \(V'\) other than \(u\) and \(v\) has no free pebble, and
The set \(V'\), and the argument that no arc leaves it, are from Lee and Streinu’s proof of their Lemma 13 [ LS08 ] .
When the game rejects a graph, it returns a set of vertices of the following kind.
Let \(G\) be a simple graph on \(V\), and let \(k\) and \(\ell \) be non-negative integers. A blocking witness for \(G\) is a finite set \(V' \subseteq V\) with \(\ell \le k|V'|\) that spans more than \(k|V'| - \ell \) edges of \(G\), that is, \(|E_{G}[V']| + \ell {\gt} k|V'|\).
A blocking witness shows that \(G\) is not \((k, \ell )\)-sparse (definition 3.1).
Let \(V\), \(k\), \(\ell \) and the lists \(N^+_D(a)\) be as in definition 13.12. Let \(D_0\) be a \((k, \ell )\)-reachable partial orientation on \(V\), and let \((u_1, v_1), \ldots , (u_m, v_m)\) be a list of pairs of vertices. The pebble game on this list from \(D_0\) starts with \(D = D_0\), and for \(i = 1, \ldots , m\) in turn runs as follows.
If \(u_i = v_i\), or \((u_i, v_i) \in D\), or \((v_i, u_i) \in D\), it skips the pair.
Otherwise it processes \(u_i v_i\) at \(D\). If this rejects \(u_i v_i\), the game stops and returns the failure witness. If it accepts \(u_i v_i\) and returns \(D'\), the game sets \(D = D'\).
If no pair is rejected, the game returns the final orientation \(D\).
Now let \(G\) be a simple graph on \(V\), and let \(\ell {\lt} 2k\). The pebble game on \(G\) is the pebble game from the empty orientation on a list of the edges of \(G\) in which each edge \(uv\) appears once, as \((u, v)\) or as \((v, u)\). It accepts \(G\) if this game returns a partial orientation \(D\). It rejects \(G\), with the set \(V'\), if the game returns a failure witness whose set is \(V'\).
The game is defined at every step, since processing an edge returns a \((k, \ell )\)-reachable orientation when it accepts. It stops, since the list is finite. In section 13.4 we show that if the game accepts \(G\) with \(D\), then \(\underline{D} = E(G)\), and \(G\) is \((k, \ell )\)-sparse. In section 13.6 we show that if it rejects \(G\) with \(V'\), then \(V'\) is a blocking witness for \(G\). The formal pebble game on \(G\) (definition 13.26) returns its answer together with proofs. With \(D\) it returns proofs that \(\underline{D} = E(G)\) and that \(D\) is \((k, \ell )\)-reachable. With \(V'\) it returns a proof that \(V'\) is a blocking witness for \(G\), for which it uses \(\ell {\lt} 2k\).
The pebble search, the processing of an edge and the pebble game on a list are formalized with the lists \(N^+_D(a)\) as an argument, one for each partial orientation \(D\) and vertex \(a\), together with a proof that the entries of \(N^+_D(a)\) are the out-neighbours of \(a\) in \(D\). These forms (the declarations whose names end in “With”) can be computed whenever the lists can, and the results below are proved for them. A second form of each procedure takes for \(N^+_D(a)\) mathlib’s list of the elements of the finite set of out-neighbours, so it is the first form with particular lists. For the pebble game, the second form is the formal pebble game on \(G\). It also lists the edges of \(G\) in this way, and writes each edge as an ordered pair by a choice. As in section 12, mathlib lists the elements of a finite set by a choice that cannot be computed, so the second forms cannot be computed. In section 14 we use lists sorted by a linear order on \(V\) instead, which can be computed.
13.4 Soundness
We show that if the pebble game on \(G\) accepts \(G\), then \(G\) is \((k, \ell )\)-sparse. Lee and Streinu prove this direction of their Theorem 8 first, as part of their Corollary 12 [ LS08 ] . Like theirs, our proof rests on Invariant (4) of lemma 13.7. Suppose that the game accepts \(G\) with \(D\). It runs on a list in which each edge of \(G\) appears once, so it skips no edge, and since it returns \(D\), it accepts every edge. Hence \(\underline{D} = E(G)\) (lemma 13.17). For a set \(V'\) of vertices, \(\mathrm{span}_D(V')\) is then the number of edges of \(G\) inside \(V'\) (lemma 13.18), and Invariant (4) becomes the count that defines sparsity.
Let \(V\), \(k\), \(\ell \) and the lists \(N^+_D(a)\) be as in definition 13.12, and let \(D\) be a \((k, \ell )\)-reachable partial orientation on \(V\).
Let \(u \ne v\) be vertices such that the edge \(uv\) is not oriented in \(D\). If processing \(uv\) at \(D\) accepts \(uv\) and returns \(D'\), then \(\underline{D'} = \underline{D} \cup \{ uv\} \).
Let \((u_1, v_1), \ldots , (u_m, v_m)\) be a list of pairs of vertices. If the pebble game on this list from \(D\) returns a partial orientation \(D'\), then \(\underline{D} \subseteq \underline{D'}\), and every edge in \(\underline{D'} \setminus \underline{D}\) is \(u_i v_i\) for some \(i\).
For (1), processing \(uv\) at \(D\) stops in step 1 or step 4 of definition 13.12. Otherwise, in step 2 or step 3, it processes \(uv\) again at a partial orientation \(D''\) obtained from \(D\) by reversing a directed path. We argue by induction along this recursion, which stops, as shown after definition 13.12. Step 4 rejects \(uv\), so it is not reached. Step 1 inserts the arc \((u, v)\) or the arc \((v, u)\), and either way the underlying edge set becomes \(\underline{D} \cup \{ uv\} \) (definition 13.5). In steps 2 and 3, \(\underline{D''} = \underline{D}\) (definition 13.4), and processing \(uv\) at \(D''\) accepts \(uv\) and returns \(D'\). By induction, \(\underline{D'} = \underline{D''} \cup \{ uv\} = \underline{D} \cup \{ uv\} \).
For (2) we argue by induction on \(m\). If \(m = 0\), then \(D' = D\). Let \(m \ge 1\). If the game skips \((u_1, v_1)\), it plays the rest of the list from \(D\), and the claim follows by induction. Otherwise it processes \(u_1 v_1\) at \(D\). Since the game returns a partial orientation, the processing accepts \(u_1 v_1\) and returns a \((k, \ell )\)-reachable partial orientation \(D_1\), with \(\underline{D_1} = \underline{D} \cup \{ u_1 v_1\} \) by (1). The game then plays \((u_2, v_2), \ldots , (u_m, v_m)\) from \(D_1\) and returns \(D'\). The induction hypothesis at \(D_1\) gives both claims.
Let \(V\), \(k\), \(\ell \) and the lists \(N^+_D(a)\) be as in definition 13.12, and let \(D\) be a \((k, \ell )\)-reachable partial orientation on \(V\). Let \((u_1, v_1), \ldots , (u_m, v_m)\) be a list of pairs of vertices with \(u_i \ne v_i\) and \(u_i v_i \notin \underline{D}\) for every \(i\), such that the edges \(u_1 v_1, \ldots , u_m v_m\) are distinct. If the pebble game on this list from \(D\) returns a partial orientation \(D'\), then \(u_i v_i \in \underline{D'}\) for every \(i\).
Moreover, let \(G\) be a simple graph on \(V\), and let the pairs \((u_i, v_i)\) list the edges of \(G\), each once, as \((u, v)\) or as \((v, u)\). If the pebble game on this list from the empty orientation returns \(D'\), then \(\underline{D'} = E(G)\).
We argue by induction on \(m\); for \(m = 0\) there is nothing to prove. Let \(m \ge 1\). Since \(u_1 \ne v_1\) and \(u_1 v_1 \notin \underline{D}\), neither \((u_1, v_1)\) nor \((v_1, u_1)\) is an arc of \(D\), so the game does not skip \((u_1, v_1)\). As in the proof of lemma 13.16 (2), processing \(u_1 v_1\) at \(D\) accepts it and returns a \((k, \ell )\)-reachable partial orientation \(D_1\) with \(\underline{D_1} = \underline{D} \cup \{ u_1 v_1\} \). For \(i \ge 2\), the edge \(u_i v_i\) is neither in \(\underline{D}\) nor equal to \(u_1 v_1\), so the rest of the list satisfies the hypotheses at \(D_1\). By induction, \(u_i v_i \in \underline{D'}\) for \(i \ge 2\). Also \(u_1 v_1 \in \underline{D_1}\), and \(\underline{D_1} \subseteq \underline{D'}\) by lemma 13.16 (2).
For the second part, the edges of \(G\) are not loops, none of them is oriented in the empty orientation, and each is listed once. So the first part gives \(E(G) \subseteq \underline{D'}\). Conversely, by lemma 13.16 (2), every edge in \(\underline{D'}\) is one of the \(u_i v_i\), and so an edge of \(G\).
The pebble game on \(G\) (definition 13.14) runs on a list of this kind, since a list of the elements of a finite set has no repetitions (formalization note 13.15). So if it accepts \(G\) with \(D\), then \(\underline{D} = E(G)\).
Let \(D\) be a partial orientation on \(V\), and let \(G\) be a simple graph on \(V\) with \(\underline{D} = E(G)\). Then every finite set \(V' \subseteq V\) satisfies
Map each arc \((a, b)\) of \(D\) with both ends in \(V'\) to the edge \(ab\). This edge lies in \(\underline{D} = E(G)\) and inside \(V'\), so it is in \(E_{G}[V']\). The map is injective: two arcs with the same underlying edge are equal or antiparallel, and \(D\) has no antiparallel pairs. It is surjective: an edge \(ab\) of \(G\) inside \(V'\) lies in \(\underline{D}\), so \((a, b)\) or \((b, a)\) is an arc of \(D\), and both its ends are in \(V'\).
Let \(V\) be a finite set, let \(G\) be a simple graph on \(V\), and let \(k\) and \(\ell \) be non-negative integers. Let the lists \(N^+_D(a)\) be as in definition 13.12, and let the pairs \((u_1, v_1), \ldots , (u_m, v_m)\) list the edges of \(G\), each once, as \((u, v)\) or as \((v, u)\). If the pebble game on this list from the empty orientation returns a partial orientation, then \(G\) is \((k, \ell )\)-sparse. In particular, if \(\ell {\lt} 2k\) and the pebble game on \(G\) accepts \(G\), then \(G\) is \((k, \ell )\)-sparse.
Let \(D\) be the partial orientation returned. It is \((k, \ell )\)-reachable, since processing an edge returns a \((k, \ell )\)-reachable partial orientation when it accepts (definition 13.12). By lemma 13.17, \(\underline{D} = E(G)\). Let \(V' \subseteq V\) with \(\ell \le k|V'|\). Invariant (4) of lemma 13.7 gives \(\mathrm{span}_D(V') \le k|V'| - \ell \). By lemma 13.18, the left-hand side is \(|E_{G}[V']|\). Hence \(G\) is \((k, \ell )\)-sparse. The pebble game on \(G\) runs on a list of the kind above (lemma 13.17), which gives the last claim.
Only the last claim assumes \(\ell {\lt} 2k\), the range in which the pebble game on \(G\) is defined (definition 13.14).
13.5 Completeness
We now prepare the converse, which section 13.6 completes: if the pebble game on \(G\) rejects \(G\) with \(V'\), then \(V'\) is a blocking witness for \(G\), so \(G\) is not \((k, \ell )\)-sparse.
Following Lee and Streinu [ LS08 , § 2 ] , we call an edge \(uv\) that is not oriented in a partial orientation \(D\) independent in \(D\) if the graph on \(V\) with edge set \(\underline{D} \cup \{ uv\} \) is \((k, \ell )\)-sparse. Their Lemma 14 states that the game inserts \(uv\) if and only if \(uv\) is independent in \(D\). One direction follows from Invariant (4): if processing \(uv\) at \(D\) accepts \(uv\), then \(uv\) is independent in \(D\) (lemma 13.23). For the other, Lee and Streinu apply their Lemma 13 repeatedly. While \(u\) and \(v\) hold at most \(\ell \) free pebbles, their Lemma 13 gives a free pebble on another vertex reachable from \(u\) or from \(v\), and reversing a directed path brings it to \(u\) or to \(v\). They remark that the vertices reachable from \(u\) and from \(v\) may change after such a move, and that each application of their Lemma 13 needs \(uv\) to be independent [ LS08 , p. 1433 ] . It is, since reversing a path does not change \(\underline{D}\).
We prove Lee and Streinu’s Lemma 13 as lemma 13.21, from a form that does not mention a graph (lemma 13.20). For the correctness of the game, however, we argue at the rejection. Processing \(uv\) at \(D\) rejects \(uv\) only in step 4 of definition 13.12. The failure witness that it returns there shows that \(uv\) is not independent in \(D\) (lemma 13.22). The inequalities are those of Lee and Streinu’s Lemma 13, read in the contrapositive.
Let \(V\) be a set, let \(k\) and \(\ell \) be non-negative integers, and let \(D\) be a \((k, \ell )\)-reachable partial orientation on \(V\). Let \(u \ne v\) be vertices, and let \(V' \subseteq V\) be a finite set that contains \(u\) and \(v\) and that no arc of \(D\) leaves, that is, \(\mathrm{out}_D(V') = 0\). Suppose that
Then \(\mathrm{peb}_{D, k}(w) \ge 1\) for some vertex \(w \in V'\) other than \(u\) and \(v\).
By Invariant (2) of lemma 13.7,
Since \(\mathrm{out}_D(V') = 0\), the first inequality gives \(\mathrm{peb}_{D, k}(V') \ge \ell + 1\). By the second, \(u\) and \(v\) hold at most \(\ell \) of these pebbles, so another vertex of \(V'\) holds one.
In Lee and Streinu’s proof of their Lemma 13 [ LS08 ] , \(V'\) is the set of vertices reachable from \(u\) or from \(v\), and the first inequality follows from the independence of \(uv\), as in the proof of lemma 13.21.
Let \(V\) be a finite set, let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\), and let \(D\) be a \((k, \ell )\)-reachable partial orientation on \(V\). Let \(u \ne v\) be vertices such that the edge \(uv\) is not oriented in \(D\) and the graph on \(V\) with edge set \(\underline{D} \cup \{ uv\} \) is \((k, \ell )\)-sparse. If \(\mathrm{peb}_{D, k}(u) + \mathrm{peb}_{D, k}(v) \le \ell \), then \(\mathrm{peb}_{D, k}(w) \ge 1\) for some vertex \(w \ne u, v\) that is reachable from \(u\) or from \(v\) along the arcs of \(D\).
Let \(G\) be the graph on \(V\) with edge set \(\underline{D} \cup \{ uv\} \), and let \(V' = \mathrm{Reach}_D(u) \cup \mathrm{Reach}_D(v)\) be the set of vertices reachable from \(u\) or from \(v\) along the arcs of \(D\). Then \(V'\) contains \(u\) and \(v\), and no arc of \(D\) leaves \(V'\), as shown after definition 13.12. Since \(|V'| \ge 2\) and \(\ell {\lt} 2k\), we have \(\ell \le k|V'|\). As \(G\) is \((k, \ell )\)-sparse, \(V'\) spans at most \(k|V'| - \ell \) edges of \(G\).
As in the proof of lemma 13.18, the arcs of \(D\) inside \(V'\) have distinct underlying edges, and these are edges of \(G\) inside \(V'\). The edge \(uv\) is one more, since it is not oriented in \(D\). Hence
and lemma 13.20 gives the vertex \(w\).
Let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\), and let \((D, V', (u, v))\) be a failure witness (definition 13.11). Let \(G\) be a simple graph on \(V\) with finitely many edges, whose edges include \(uv\) and the edges in \(\underline{D}\). Then \(\ell \le k|V'|\) and
The distinct vertices \(u\) and \(v\) lie in \(V'\), so \(|V'| \ge 2\) and \(\ell {\lt} 2k \le k|V'|\). Since \(D\) is \((k, \ell )\)-reachable, Invariant (2) of lemma 13.7 gives
By the definition of a failure witness, \(\mathrm{out}_D(V') = 0\) and \(\mathrm{peb}_{D, k}(V') \le \ell \). So \(k|V'| \le \mathrm{span}_D(V') + \ell \).
As in the proof of lemma 13.18, the arcs of \(D\) inside \(V'\) have distinct underlying edges, and these are edges of \(G\) inside \(V'\). The edge \(uv\) is one more, since it lies inside \(V'\) and is not oriented in \(D\). Hence \(\mathrm{span}_D(V') + 1 \le |E_{G}[V']|\), and so \(k|V'| {\lt} |E_{G}[V']| + \ell \). Thus \(V'\) is a blocking witness for \(G\) (definition 13.13).
Let \(V\), \(k\), \(\ell \) and the lists \(N^+_D(a)\) be as in definition 13.12. Let \(D\) be a \((k, \ell )\)-reachable partial orientation on \(V\), and let \(u \ne v\) be vertices such that the edge \(uv\) is not oriented in \(D\). If processing \(uv\) at \(D\) accepts \(uv\), then the graph on \(V\) with edge set \(\underline{D} \cup \{ uv\} \) is \((k, \ell )\)-sparse.
Let \(G\) be this graph, and let \(D'\) be the partial orientation that the processing returns. It is \((k, \ell )\)-reachable (definition 13.12). By lemma 13.16 (1), \(\underline{D'} = \underline{D} \cup \{ uv\} = E(G)\). Let \(V' \subseteq V\) with \(\ell \le k|V'|\). By Invariant (4) of lemma 13.7, \(\mathrm{span}_{D'}(V') \le k|V'| - \ell \). By lemma 13.18, the left-hand side is \(|E_{G}[V']|\). Hence \(G\) is \((k, \ell )\)-sparse.
13.6 Correctness
We now prove the part of Lee and Streinu’s Theorem 8 [ LS08 , p. 1431 ] that concerns sparse graphs: the game accepts every edge of \(G\), an outcome they call well-constrained or under-constrained (§3), if and only if \(G\) is \((k, \ell )\)-sparse. One direction is theorem 13.19. Lee and Streinu prove the other from their Lemma 15 (p. 1433); here it follows from part (2) of the theorem below. We state the theorem for every list of the edges of \(G\) and every choice of the lists \(N^+_D(a)\), so that it applies to each formal form of the game (formalization note 13.15).
Let \(V\) be a finite set, let \(G\) be a simple graph on \(V\), and let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\). Let the lists \(N^+_D(a)\) be as in definition 13.12, and let the pairs \((u_1, v_1), \ldots , (u_m, v_m)\) list the edges of \(G\), each once, as \((u, v)\) or as \((v, u)\). Then \(G\) is \((k, \ell )\)-sparse if and only if the pebble game on this list from the empty orientation returns a partial orientation. More precisely:
if the game returns a partial orientation \(D\), then \(\underline{D} = E(G)\), and \(G\) is \((k, \ell )\)-sparse;
if the game returns a failure witness \((D, V', (u, v))\), then \(V'\) is a blocking witness for \(G\) (definition 13.13).
In particular, \(G\) is \((k, \ell )\)-sparse if and only if the pebble game on \(G\) accepts \(G\), and if it rejects \(G\) with \(V'\), then \(V'\) is a blocking witness for \(G\).
Part (1) is lemma 13.17 and theorem 13.19.
For part (2), we first show that every partial orientation that the game reaches orients only edges of \(G\). We argue by induction on the list, as in the proof of lemma 13.16 (2). The empty orientation orients no edge. When the game accepts \(u_i v_i\), the underlying edge set gains only the edge \(u_i v_i\) (lemma 13.16 (1)), and \(u_i v_i\) is an edge of \(G\).
Now suppose that the game returns a failure witness \((D, V', (u, v))\). Then for some \(i\), processing \(u_i v_i\) at a partial orientation \(D_{i-1}\) that the game has reached rejects \(u_i v_i\). By step 4 of definition 13.12, \((u, v) = (u_i, v_i)\), so \(uv\) is an edge of \(G\). The processing reaches \(D\) from \(D_{i-1}\) by reversing directed paths in steps 2 and 3. So \(\underline{D} = \underline{D_{i-1}}\) (definition 13.4), and every edge in \(\underline{D}\) is an edge of \(G\) (runPebbleGameWith_witness_bridges). Since \(G\) is finite, lemma 13.22 shows that \(V'\) is a blocking witness for \(G\). This is the only step of the proof that uses \(\ell {\lt} 2k\).
The game returns either a partial orientation or a failure witness. If \(G\) is \((k, \ell )\)-sparse, then no set of vertices is a blocking witness for \(G\), by definition 3.1. So by (2), the game returns a partial orientation. The converse is (1). The pebble game on \(G\) (definition 13.14) runs on a list of the kind above, which gives the last claim.
13.7 The verdict
We now define the verdicts and the formal pebble game on \(G\), which returns one, and restate theorem 13.24 for them. The formal pebble game on \(G\) uses mathlib’s lists (formalization note 13.15). The computable pebble game on \(G\) of section 14 differs from it only in its lists, which are sorted by a linear order on \(V\). It also returns a verdict, for which the restated theorem holds as well (theorem 14.7).
Let \(G\) be a simple graph on \(V\) with finitely many edges, and let \(k\) and \(\ell \) be non-negative integers. A verdict on \(G\) is one of the following:
an acceptance, given by a \((k, \ell )\)-reachable partial orientation \(D\) on \(V\) with \(\underline{D} = E(G)\) (definition 13.6);
a rejection, given by a blocking witness \(V'\) for \(G\) (definition 13.13).
A verdict accepts \(G\) if it is an acceptance.
A verdict on \(G\) shows whether \(G\) is \((k, \ell )\)-sparse. An acceptance given by \(D\) shows that \(G\) is \((k, \ell )\)-sparse, as in the proof of theorem 13.19. A rejection shows that \(G\) is not \((k, \ell )\)-sparse (the paragraph after definition 13.13).
Let \(V\) be a finite set, let \(G\) be a simple graph on \(V\), and let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\). The formal pebble game on \(G\) runs the pebble game from the empty orientation on mathlib’s list of the edges of \(G\), with mathlib’s lists of out-neighbours as the lists \(N^+_D(a)\) (formalization note 13.15). It returns the verdict on \(G\) (definition 13.25) that is an acceptance, given by \(D\), if the game returns a partial orientation \(D\), and a rejection, given by \(V'\), if the game returns a failure witness whose set is \(V'\).
The verdict is well defined. Mathlib’s list of the edges of \(G\) lists each edge once, as \((u, v)\) or as \((v, u)\) (lemma 13.17). So the game is the pebble game on \(G\) (definition 13.14). If it returns \(D\), then \(\underline{D} = E(G)\) by the same lemma, and \(D\) is \((k, \ell )\)-reachable, since processing an edge returns a \((k, \ell )\)-reachable orientation when it accepts. If it returns a failure witness, then the witness’s pair is an edge of \(G\), and every edge oriented by its partial orientation is an edge of \(G\), as in the proof of theorem 13.24 (2). Since \(\ell {\lt} 2k\), the witness’s set \(V'\) is then a blocking witness for \(G\) (lemma 13.22).
Let \(V\) be a finite set, let \(G\) be a simple graph on \(V\), and let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\). Then \(G\) is \((k, \ell )\)-sparse if and only if the verdict that the formal pebble game on \(G\) returns accepts \(G\).
The formal pebble game on \(G\) runs the pebble game from the empty orientation on a list of the edges of \(G\) that contains each edge once (lemma 13.17). It returns an acceptance when this game returns a partial orientation, and a rejection when it returns a failure witness (definition 13.26). So its verdict accepts \(G\) if and only if the game returns a partial orientation. By theorem 13.24, this holds if and only if \(G\) is \((k, \ell )\)-sparse.
13.8 Independence in the count matroid
We restate theorem 13.27 for the \((k, \ell )\)-count matroid of section 11, whose independent sets are the \((k, \ell )\)-sparse subsets of \(E(K_V)\): the pebble game decides whether the edge set of a graph is independent in it.
Let \(V\) be a finite set, let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\), and let \(G\) be a simple graph on \(V\). Then \(E(G)\) is independent in the \((k, \ell )\)-count matroid on \(V\) (definition 11.7) if and only if the verdict that the formal pebble game on \(G\) returns accepts \(G\).
Since \(G\) is simple, \(E(G) \subseteq E(K_V)\), and the graph on \(V\) with edge set \(E(G)\) is \(G\). So \(E(G)\) is independent in the count matroid if and only if \(G\) is \((k, \ell )\)-sparse (theorem 11.9). By theorem 13.27, this holds if and only if the verdict accepts \(G\).
At \((k, \ell ) = (2, 3)\), the count matroid is the planar rigidity matroid \(\mathcal{R}(V)\) (definition 10.12). So the pebble game decides whether \(E(G)\) is independent in \(\mathcal{R}(V)\), that is, whether \(E(G)\) is row-independent at some framework on \(V\) in \({\mathbb {R}}^{2}\) (theorem 10.13). A Laman graph is a \((2, 3)\)-sparse graph with \(2|V| - 3\) edges (definition 4.1). So the game, together with a count of the edges, decides whether \(G\) is Laman, and section 14 makes this decision computable. This is the setting of Jacobs and Hendrickson’s pebble game for rigidity in the plane [ JH97 ] .