Proof of 1. Membership in \(\mathsf{PSPACE}\)is clear from the recursive definition of \(\mathrm{SSV}\). Given a weighted tournament \(G\) on \(N\) candidates, we can compute \(\mathrm{SSV}(G)\) using a depth-first recursion: scan the ordered pairs \((A,B)\) in decreasing order of \(w(A,B)\), recursively compute \(\mathrm{SSV}(G\setminus\{B\})\), and return the first \(A\) for which \(\mathrm{SSV}(G\setminus\{B\})=A\). Each recursive call removes one candidate, so the recursion depth is at most \(N\). At each level, it suffices to store the current subtournament, the current pair being scanned, and the returned candidate, all of which require only polynomially many bits. Thus, the recursion uses only polynomial space.

In the remainder of this proof, we show that, given a QBF formula \(\Phi\), in the tournament \(G(\Phi)\) produced by the construction in 3.1, \(\mathrm{SSV}(G(\Phi))=C\) if and only if \(\Phi\) is true. Otherwise, \(\mathrm{SSV}(G(\Phi))=D\).

The \(\mathrm{SSV}\)rule determines a winner by processing the edges in decreasing order of weight; hence, the first edges to be considered are from \(C,D\) to the literals since they are in the largest weight group (\(\mathsf g1\)). It is thus sufficient to show that the winner of the subtournament without one of those literals is \(C\) if the residual \(\mathsf{QBF}\)is true or \(D\) otherwise, and that the residual tournament respects the \(\mathsf{QBF}\)encoding.

To encode the \(\mathsf{QBF}\)formula at every step of the \(\mathrm{SSV}\)recursion, we need to maintain a valid prefix-assignment such that the winner (of the induced subtournament) correctly encodes the truth of the residual \(\mathsf{QBF}\). As we establish in [lem:guards], for each variable \(x_i\), the guard \(X_i\) prevents the deletion of both \(T_i\) and \(F_i\) before the recursion reaches a full assignment; in particular, \(X_i\) wins if both literals are removed, preventing \(C\) or \(D\) from winning.

[lem:sat-C-wins,lem:unsat-D-wins] show that when the recursion reaches a full assignment, the winner is the same as the truth value of \(\Phi\) (for that assignment).

We prove [lem:guards,lem:sat-C-wins,lem:unsat-D-wins] in [subsec:gadget-proofs,subsec:winnerofafullassignmentCD].

The proof proceeds by backward induction on prefix assignments, where the base case is a full assignment. For a prefix assignment \(\alpha_{< j}\in\{T,F\}^{j-1}\), let \(\Phi_{\alpha_{<j}}\) denote the residual QBF obtained from \(\Phi\) after fixing the first \(j-1\) variables according to \(\alpha_{<j}\). For \(j\in\{1,\ldots,n+1\}\), consider the following statement: \[P(j): \text{ for every prefix assignment } \alpha_{< j} \text{ of length } j-1,\, \mathrm{SSV}(G_{\alpha_{< j}}) = \begin{cases} C& \text{ if \Phi_{\alpha_{< j}} is true}\\ D& \text{ otherwise.} \end{cases}\] We prove \(P(j)\) for all \(j\in\{1,\ldots,n+1\}\) by backward induction.

4.0.0.1 Base Case: \((j=n+1)\)

When \(j=n+1\), the prefix assignment is a full assignment. Let \(\alpha=\alpha_{<n+1}\) and \(G_\alpha\) be the full-assignment graph. If \(\alpha\) satisfies \(\varphi\), then by [lem:sat-C-wins], \(\mathrm{SSV}(G_\alpha)=C\). If \(\alpha\) does not satisfy \(\varphi\), then by [lem:unsat-D-wins], \(\mathrm{SSV}(G_\alpha)=D\). Thus \(P(n+1)\) holds.

4.0.0.2 Induction step.

Assume \(P(j+1)\) holds for some \(0< j\le n\); we show that \(P(j)\) holds. Fix an arbitrary prefix assignment \(\alpha:=\alpha_{< j}\), and let \(G_\alpha\) be the corresponding prefix graph. The residual \(\mathsf{QBF}\)has variables \(x_1\ldots x_{j-1}\) set according to \(\alpha\) and \(Q_jx_j\) is the first quantified variable. Hence, we need to show that the winner of \(G_\alpha\) correctly encodes the truth of the residual formula \(\Phi_\alpha\) based on \(Q_j\).

To determine \(\mathrm{SSV}(G_\alpha)\), we must identify the largest critical edge of \(G_\alpha\). Recall that the \(\mathrm{SSV}\)rule processes the edges in decreasing order of weight. We show that (i) the edges \(C,D\to T_i,F_i\) are not critical edges for all \(i<j\) (these are the heaviest edges in \(G_\alpha\), since weight decreases as the index \(i\) increases), and then (ii) the largest critical edge is one of \(C\toT_j\) and \(C\toF_j\) if \(\Phi_\alpha\) is true, and the largest critical edge is one of \(D\toT_j,F_j\) if \(\Phi_\alpha\) is false, thus producing the correct winner in each case.

(i) For every \(i<j\), exactly one of \(\{T_i,F_i\}\) is present in \(G_\alpha\); let that be \(\ell_i\). Observe that none of the edges \(C\to\ell_i\) and \(D\to\ell_i\) are critical, since deleting \(\ell_i\) makes \(\mathrm{FirstX}(G_\alpha\setminus\{\ell_i\})=i\), and thus, by [lem:guards], \(\mathrm{SSV}(G_\alpha\setminus\{\ell_i\})=X_i\) (that is, the critical edge produced by deleting \(\ell_i\) is \(X_i\to\ell_i\)).

(ii) The next edges in group \(\mathsf g1\) to be considered are the four from \(C,D\) to \(F_j,T_j\), whose order depends on the quantifier \(Q_j\). Let \(\alpha^T\) and \(\alpha^F\) be the two extensions of \(\alpha\) setting \(x_j=T\) and \(x_j=F\), respectively. Then \(G_\alpha\setminus\{F_j\}\) and \(G_\alpha\setminus\{T_j\}\) are the prefix graphs corresponding to \(\alpha^T\) and \(\alpha^F\), respectively. Since these extensions have length \(j\), the induction hypothesis applies to both graphs, so each is won by either \(C\) or \(D\) according to the truth value of the corresponding residual formula. Thus, among the four edges from \(C\) and \(D\) to \(F_j\) and \(T_j\), exactly two are critical, one for each deletion. By part (i), all earlier group \(\mathsf g1\) edges have already been ruled out, so the largest critical edge of \(G_\alpha\) is the first critical edge among these four.

 - **(Case $Q_j=\exists$)** Recall that in group $\mathsf g1$, if
   the quantifier is $\exists$, then the order of the edges between
   $C,D$ and $T_j,F_j$ is
   $$C\toF_j\quad > \quadC\toT_j\quad > \quadD\toF_j\quad > \quadD\toT_j$$

   Since $Q_j=\exists$, $\Phi_\alpha$ is true exactly when at least
   one of the two graphs above is won by $C$. In that case, the
   largest critical edge among the four is a $C$-edge. If both
   graphs are won by $D$, then neither $C$-edge is critical, so the
   largest critical edge is $D\toF_j$. Thus
   $\mathrm{SSV}(G_\alpha)=C$ if and only if $\Phi_\alpha$ is true,
   and otherwise $\mathrm{SSV}(G_\alpha)=D$.

 - **(Case $Q_j=\forall$)** Recall that in group $\mathsf g1$, if
   the quantifier is $\forall$, then the order of the edges between
   $C,D$ and $T_j,F_j$ is
   $$D\toF_j\quad > \quadD\toT_j\quad > \quadC\toF_j\quad > \quadC\toT_j$$
   Since $Q_j=\forall$, $\Phi_\alpha$ is true exactly when both
   graphs above are won by $C$. If at least one of the two graphs is
   won by $D$, then the largest critical edge among the four is a
   $D$-edge. If both graphs are won by $C$, then neither $D$-edge is
   critical, so the largest critical edge is $C\toF_j$. Thus
   $\mathrm{SSV}(G_\alpha)=C$ if and only if $\Phi_\alpha$ is true,
   and otherwise $\mathrm{SSV}(G_\alpha)=D$.

This proves \(P(j)\) and completes the induction step.

Taking \(j=1\), the prefix assignment is empty, so \(G_{\alpha_{<1}}=G(\Phi)\). Therefore, by \(P(1)\), \(\mathrm{SSV}(G(\Phi))=C\) if and only if \(\Phi\) is true, and otherwise \(\mathrm{SSV}(G(\Phi))=D\). This concludes the proof of 1. ◻

Proof. We will prove the lemma by induction on \(t \mathrel{\vcenter{:}}= |V(G)|.\)

4.1.1.1 Base case (\(t=1\)).

If \(V(G)=\{X_ {i^*}\}\), for some \({i^*}\), then \(\mathrm{FirstX}(G)= {i^*}\) and \(\mathrm{SSV}(G)=X_ {i^*}\). If \(V(G)=\{u\},\) where \(u\neq X_ {i^*}\;\forall {i^*}\), \(\mathrm{SSV}(G)=u\) with \(\mathrm{FirstX}(G)=0\). Thus, the claim holds.

4.1.1.2 Induction hypothesis.

Fix \(t\ge 2\) and assume that for every induced subtournament \(H\) of \(G(\Phi)\) with \(|V(H)|< t\), \(\forall X_ {i^*}\in V(H)\) with \({i^*}>0,\)

\[\mathrm{SSV}(H)=X_ {i^*}\iff \mathrm{FirstX}(H)= {i^*}.\]

4.1.1.3 Induction step.

Let \(G\) be an induced subtournament with \(|V(G)|=t\). We prove both directions.

4.1.1.4 (\(\Leftarrow\)) \(\mathrm{FirstX}(G)= {i^*}>0 \Rightarrow \mathrm{SSV}(G)=X_ {i^*}\).

Since \(\mathrm{FirstX}(G)= {i^*}\) we have that \(X_ {i^*}\in V(G)\) and \(T_ {i^*},F_ {i^*}\notin V(G)\). We show that the largest critical edge of \(G\) is from \(X_ {i^*}\), and thus \(\mathrm{SSV}(G)=X_ {i^*}\). We break the proof into two steps. First, we show that among the critical edges produced by deleting candidates \(u\neq X_ {i^*}\), the largest one has the form \(X_ {i^*}\to u\). Then, we show that the critical edge produced by deleting \(X_ {i^*}\), namely the edge \(\mathrm{SSV}(G\setminus\{X_ {i^*}\})\rightarrowX_ {i^*}\), is smaller than the edge \(X_ {i^*}\rightarrow u\). Toward our first claim, we focus on the critical edges produced by nodes in the set \(u\in V(G\setminus\{X_ {i^*}\})\). First, observe that the residual graph \(G\setminus\{u\}\) still has \(0<\mathrm{FirstX}(G\setminus\{u\})\le {i^*},\) since \(X_ {i^*}\in V(G\setminus\{u\})\) and still \(T_ {i^*},F_ {i^*}\notin V(G\setminus\{u\}).\) However, a deletion of a node may cause a guard \(X_j\) with a smaller index to be without both of its literals. We consider the following two cases:

1. \(\mathrm{FirstX}(G\setminus\{u\})= {i^*}\). Hence, by the induction hypothesis applied to \(G\setminus\{u\}\) we get \(\mathrm{SSV}(G\setminus\{u\})=X_ {i^*},\) and thus \(X_ {i^*}\rightarrow u\) is a critical edge of \(G\). The weight of that critical edge in \(G\) is bounded below by \(\min_u\{w(X_ {i^*},u)\}\ge-\mathsf g10\), given the edges adjacent to \(X_ {i^*}\) (7). (The only incoming edges to \(X_ {i^*}\) are from \(X_j\) with \(j< {i^*}\), as \(T_ {i^*},F_ {i^*}\notin G\) is given by the assumption that \(\mathrm{FirstX}(G)= {i^*}\).)

2. \(0<\mathrm{FirstX}(G\setminus\{u\})=j< {i^*}\). This can only happen if there exists a \(j\) such that exactly one of \(F_j\) or \(T_j\) is in \(V(G)\) and \(X_j\in V(G)\). Deleting the remaining literal introduces a \(\mathrm{FirstX}\) with a smaller index. By the induction hypothesis applied to \(G\setminus\{u\}\), we get \(\mathrm{SSV}(G\setminus\{u\})=X_j.\) Then, the critical edge in \(G\) is \(X_j \rightarrow F_j/T_j\) that has weight in group \(-\mathsf g_2.\)

Therefore, all critical edges arising from Case 1 have strictly larger weight than every critical edge arising from Case 2. Moreover, if Case 2 occurs for some \(j< {i^*}\) with critical edge \(X_j\to \ell_j\) (\(-\mathsf g2\)), then deleting \(X_j\) instead falls under Case 1, the edge \(X_ {i^*}\to X_j\)(\(-\mathsf g10>-\mathsf g2\)) is also critical. Hence, the largest critical edge in \(G\) produced by removing any node \(u\neq X_ {i^*}\) is produced in Case 1, and has the form \(X_ {i^*}\rightarrow u\).

It remains to compare the largest critical edge that we just showed with the critical edge associated with deleting \(X_ {i^*}\), namely \(w\to X_ {i^*}\) where \(w=\mathrm{SSV}(G\setminus\{X_ {i^*}\})\). Since \(\mathrm{FirstX}(G)= {i^*}\), every present guard \(X_k\) with \(k< {i^*}\) has at least one of its literals in \(G\). Deleting \(X_ {i^*}\) does not change this for any \(k< {i^*}\). Therefore, \(\mathrm{FirstX}(G\setminus\{X_ {i^*}\}) \in \{0\}\cup\{j:j> {i^*}\}.\) By the induction hypothesis, \(w\neq X_k\) for every \(0<k< {i^*}\). We analyze the two possible cases for \(\mathrm{FirstX}(G\setminus\{X_ {i^*}\})\).

1. \(\mathrm{FirstX}(G\setminus\{X_ {i^*}\})=0\). Then, by the induction hypothesis, \(w\) is not a guard node . Since \(T_{i^\ast},F_{i^\ast}\notin V(G)\), the edge \(w\to X_{i^\ast}\) lies in one of the groups \(-\mathsf g5\), \(-\mathsf g6\), or \(-\mathsf g8\). Hence its weight is at most \(-\mathsf g8\). Since we already identified a critical edge of weight at least \(-\mathsf g10\) and \(-\mathsf g10>-\mathsf g8\), the edge \(w\to X_{i^\ast}\) cannot be the maximum critical edge.

2. \(\mathrm{FirstX}(G\setminus\{X_ {i^*}\})=k> {i^*}\). Then, by the induction hypothesis, \(w=X_k\), so the critical edge associated with deleting \(X_ {i^*}\) is \(X_k\to X_ {i^*}\), which lies in group \(-\mathsf g10\).

   Now consider deleting \(X_k\) instead. Since \(k> {i^*}\), the guard \(X_ {i^*}\) remains the first unguarded guard in \(G\setminus\{X_k\}\). Hence, by Case 1 above, the edge \(X_ {i^*}\to X_k\) is also critical, and this edge lies in group \(\mathsf g10\). Therefore, the critical edge produced by deleting \(X_ {i^*}\) cannot be the largest critical edge of \(G\).

Thus, in all cases, the largest critical edge of \(G\) is produced by deleting some vertex \(u\neq X_ {i^*}\) and has the form \(X_ {i^*}\to u\). Therefore \(\mathrm{SSV}(G)=X_ {i^*}\).

4.1.1.5 (\(\Rightarrow\)) \(\mathrm{SSV}(G)=X_ {i^*}\Rightarrow \mathrm{FirstX}(G)= {i^*}\).

Suppose for the sake of contradiction that \(\mathrm{FirstX}(G)=j\neq {i^*}.\)

1. \(\mathrm{FirstX}(G)=j>0\) with \(j\neq {i^*}\). By the direction just proved \((\Leftarrow)\), applied with index \(j\), we get \(\mathrm{SSV}(G)=X_j\), contradicting \(\mathrm{SSV}(G)=X_ {i^*}\). Hence, this case is impossible.

2. \(\mathrm{FirstX}(G)=0\). Since \(\mathrm{SSV}(G)=X_ {i^*}\), the largest critical edge in \(G\) must be of the form \(X_ {i^*}\rightarrow u\) for some \(u\neq X_ {i^*}\). Applying the induction hypothesis to \(G\setminus\{u\}\), we get \(\mathrm{FirstX}(G\setminus\{u\})= {i^*}\). Since \(\mathrm{FirstX}(G)=0\) but \(\mathrm{FirstX}(G\setminus\{u\})= {i^*}\), deleting \(u\) must have removed the last present literal for \(X_ {i^*}\). Hence \(u\in\{T_ {i^*},F_ {i^*}\}\), and the critical edge \(X_ {i^*}\rightarrow u\) has weight in group \(-\mathsf g2\).

Now consider the critical edge associated with deleting \(X_ {i^*}\). Since \(\mathrm{FirstX}(G)=0\), every guard present in \(G\) has at least one of its literals present. Removing \(X_ {i^*}\) preserves this property for all remaining guards, and therefore \(\mathrm{FirstX}(G\setminus\{X_ {i^*}\})=0\). By the induction hypothesis, \(\mathrm{SSV}(G\setminus\{X_ {i^*}\})\) is not a guard node. Hence, by the edges adjacent to \(X_ {i^*}\), \(\mathrm{SSV}(G\setminus\{X_ {i^*}\})\rightarrowX_ {i^*}\) has weight at least \(-\mathsf g5\), and \(-\mathsf g5>-\mathsf g2\). Therefore, the critical edge that removes \(X_ {i^*}\) is larger than \(X_ {i^*}\rightarrow u\), contradicting the assumption that \(\mathrm{SSV}(G)=X_ {i^*}\).

This completes the proof of \(\mathrm{SSV}(G)=X_ {i^*}\iff \mathrm{FirstX}(G)= {i^*}\) for \({i^*}> 0.\) ◻

Proof. By [lem:adding95lits95C95D95wins], it suffices to prove the lemma under the additional assumption that every present literal is accompanied by its guard. We prove this restricted statement by induction on the number of clauses.

Claim. Let \(I\subseteq[n]\), let \(K\subseteq[m],\, |K| > 0\), and, for every \(i\in I\), fix exactly one literal \(\ell_i\in\{T_i,F_i\}\). Let \(G(I,K)\) be the induced subtournament on \[V(G(I,K))=\{C,D\}\cup\{X_i,\ell_i:i\in I\}\cup\{L_k:k\in K\}.\] If at least one clause \(L_k\), \(k\in K\) is unsatisfied by the present literals, then \(\mathrm{SSV}(G(I,K))=D\).

4.2.1.1 Base case.

For any set \(I'\subseteq I\). If \(|K|=1\), then the unique clause in \(K\) is unsatisfied. Hence, by [lem:D-wins-with-C-and-one-unsat-clause], we get \(\mathrm{SSV}(G(I,K))=D\).

4.2.1.2 Induction hypothesis.

Fix \(t\ge 2\) and assume the statement holds for every graph \(G(I',K')\) of the above form with \(I'\subseteq I\) and \(|K'|<t\).

4.2.1.3 Inductive step.

Let \(G:=G(I,K)\) be a graph of the above form with \(|K|=t\), and fix an unsatisfied clause \(L_{r}\in K\). We show that the largest critical edge of \(G\) is of the form \(D\toL_k\) (in group \(\mathsf g7\)) for some \(L_k\in K\). We examine the critical edge produced by removing each possible type of node.

1. (Removing a clause \(L_k\).) If \(k\neq r\), then \(G\setminus\{L_k\}\) still contains the unsatisfied clause \(L_{r}\), so by the induction hypothesis \(\mathrm{SSV}(G\setminus\{L_k\})=D\). Therefore, the critical edge produced by removing \(L_k\) is \(D\toL_k\), in group \(\mathsf g7\). Such an edge always exists since the number of clauses \(t\ge 2.\)

   It remains to consider removing \(L_{r}\). If there is another unsatisfied clause in \(G\), then the same induction argument applies and the critical edge produced by removing \(L_{r}\) is again an edge out of \(D\) in group \(\mathsf g7\).

   So suppose that \(L_{r}\) is the unique unsatisfied clause. Then \(G\setminus\{L_{r}\}\) is SAT. We do not need to determine its winner exactly; we need to show that the critical edge produced has weight smaller than group \(\mathsf g7\). Now, the only edges into \(L_{r}\) with weight larger than group \(\mathsf g7\) are edges in groups \(\mathsf g3\) (\(\ell_i\toL_r\)) and \(\mathsf g6\) (\(X_i\toL_r\)), see 7. First, observe that removing a clause does not affect guards or literals; we still have \(\mathrm{FirstX}(G\setminus\{L_{r}\})=0\). By [lem:guards] no guard can win \(G\setminus\{L_{r}\}\), so no edge \(X_i\toL_r\) is critical. Additionally, we know that \(L_{r}\) is unsatisfied, so no present literal satisfies \(L_{r}\), and therefore no edge \(\ell_i\toL_{r}\) in group \(\mathsf g3\) is present. Therefore, \(w(\mathrm{SSV}(G\setminus\{L_r\}),L_r) \leq \mathsf g7\). Moreover, equality is possible only when \(\mathrm{SSV}(G\setminus\{L_r\})=D\), in which case the critical edge is \(D\to L_r\); otherwise the critical edge has weight strictly below group \(g_7\). Thus removing \(L_{r}\) produces either another group \(\mathsf g7\) edge out of \(D\), or a strictly smaller critical edge.

2. (Removing \(C\).) The graph \(G\setminus\{C\}\) is exactly of the form covered by [lem:D-wins-with-clauses-no-C-general], and it is still UNSAT. Hence \(\mathrm{SSV}(G\setminus\{C\})=D\). Therefore the critical edge produced by removing \(C\) is \(D\toC\), which lies in group \(-\mathsf g12<\mathsf g7\).

3. (Removing \(D\).) Since removing \(D\) does not affect literals or guards, we still have \(\mathrm{FirstX}(G\setminus\{D\})=0\). Moreover, \(G\setminus\{D\}\) is still UNSAT. Hence, by 1, the winner of \(G\setminus\{D\}\) is the first unsatisfied clause, say \(\mathrm{FirstUnsat}(G\setminus\{D\})={k^*}\). Therefore the critical edge produced by removing \(D\) is \(L_{{k^*}}\toD\), which lies in group \(-\mathsf g7<\mathsf g7\).

4. (Removing a literal \(\ell_i\).) Since \(X_i\) is still present and \(\ell_i\) was the unique present literal of variable \(i\), we have \(\mathrm{FirstX}(G\setminus\{\ell_i\})=i\). Hence, by [lem:guards], \(\mathrm{SSV}(G\setminus\{\ell_i\})=X_i\). Therefore the critical edge produced by removing \(\ell_i\) is \(X_i\to\ell_i\), which lies in group \(-\mathsf g2<\mathsf g7\).

5. (Removing a guard \(X_i\).) For ease of notation, let \(H:=G\setminus\{X_i\}\). We show that the critical edge \(\mathrm{SSV}(H)\toX_i\) has weight \(<\mathsf g7.\) By 7, the only incoming edge to \(X_i\) with larger weight is \(\ell_i\toX_i\) in group \(\mathsf g2.\) Hence it suffices to rule out \(\mathrm{SSV}(H)=\ell_i\).

   We are going to break the proof into two steps; first we show that \(H\) has a critical edge with weight in \(\mathsf g7.\) Then we contradict that \(\mathrm{SSV}(H)=\ell_i.\)

   Step 1: We consider the graph \(H'= H\setminus\{\ell_i,L_k\}\) (for an arbitrary fixed \(k\in K\setminus\{r\}\), such a clause always exists since \(|K|\ge2\)). This graph still contains the unsatisfied clause \(L_{r}\), and it has \(t-1\) clauses. Therefore, by the induction hypothesis, \(\mathrm{SSV}(H')=D\). By [lem:adding95lits95C95D95wins], adding any number of single non-present literals does not change a winner in \(\{C,D\}\), we get \(\mathrm{SSV}(H'\cup\{\ell_i\}) =\mathrm{SSV}(H\setminus\{L_k\})=D\). Hence \(D\toL_k\) is a critical edge of \(H\), in group \(\mathsf g7\).

   Step 2: Next we show that \(\mathrm{SSV}(H)\neq\ell_i.\) Assume for the sake of contradiction that \(\mathrm{SSV}(H)=\ell_i.\) Since we have established a critical edge of \(H\) in \(\mathsf g7,\) to get \(\mathrm{SSV}(H)=\ell_i\) the maximum critical edge of \(H\) must be of the form \(\ell_i\to u\) with weight of at least \(\mathsf g7.\) The only possibility is \(\ell_i\toL_j\) for some clause satisfied by \(\ell_i\) which is in group \(\mathsf g3,\) since \(X_i\notin V(H).\) However, we have shown in Step 1 that in \(H\), removing any clause \(L_j\neqL_r\) makes the winner \(D\), which contradicts the assumption \(\mathrm{SSV}(H)=\ell_i\).

   Thus, since \(\mathrm{SSV}(H) \neq \ell_i\), the critical edge produced by removing \(X_i\), \(\mathrm{SSV}(H)\toX_i\), has weight at most \(\mathsf g10 < \mathsf g7\), by 7.

We have now considered every possible removal. Removing any clause \(L_k\neqL_{r}\) produces a critical edge \(D\toL_k\) in group \(\mathsf g7\). Every critical edge produced by removing \(C\), \(D\), a literal, or a guard has strictly smaller weight, and removing \(L_{r}\) produces at most another group \(\mathsf g7\) edge out of \(D\). Therefore the maximum critical edge of \(G\) is of the form \(D\toL_k\) for some \(L_k\in K\), and hence \(\mathrm{SSV}(G)=D\).

This proves the restricted statement. We now deduce the lemma for an arbitrary admissible subtournament.

Let \(G\) be an arbitrary admissible subtournament satisfying the hypotheses of the lemma. Let \[B:=\{\ell_i\in V(G): X_i\notin V(G)\}\] be the set of present single literals whose guards are absent, and let \[G^\circ:=G\setminus B.\] Because \(G\) is admissible, \(G^\circ\) has the form \(G(I,K)\) for some \(I\subseteq[n]\) and \(K\subseteq[m]\). Moreover, since \(\mathrm{FirstUnsat}(G)\neq 0\), at least one clause candidate present in \(G\) is unsatisfied in \(G\). Removing literals cannot make an unsatisfied clause satisfied, so at least one clause candidate present in \(G^\circ\) is unsatisfied in \(G^\circ\). Hence the inductive claim gives \[\mathrm{SSV}(G^\circ)=D.\] By [lem:adding95lits95C95D95wins], applied to \(G^\circ\) and the set \(B\), we obtain \[\mathrm{SSV}(G)=D.\] This proves the main statement of the lemma.

The full-assignment statement follows by applying the main statement to \(G_\alpha\). ◻

Proof. We prove the following stronger statement by strong induction on \(t:=|I|+|K|\).

Induction statement. Let \(I\subseteq[n]\), let \(K\subseteq[m]\), and for every \(i\in I\) fix exactly one literal \(\ell_i\in\{T_i,F_i\}\). Let \(G(I,K)\) be the induced subtournament on \[V(G(I,K))=\{C,D\}\cup\{X_i,\ell_i:i\in I\}\cup\{L_k:k\in K\}.\] Assume that every clause \(L_k\in K\) is satisfied by at least one present literal \(\ell_i\). Then \(\mathrm{SSV}(G(I,K))=C\). The lemma follows by taking \(I=[n]\), \(K=[m]\), and choosing the literals according to \(\alpha\).

4.2.2.1 Base case.

If \(K=\emptyset\), then \(G(I,K)\) has no clause nodes for every \(I\subseteq[n]\). Hence, by [lem:c-wins-without-clauses], we get \(\mathrm{SSV}(G(I,\emptyset))=C\).

4.2.2.2 Induction hypothesis.

Fix \(t\ge 1\) and assume the statement holds for every satisfiable graph \(G(I',K')\) with \(|I'|+|K'|<t\).

4.2.2.3 Induction step.

Let \(G:=G(I,K)\) be satisfiable with \(|I|+|K|=t\). We show that the largest critical edge is \(C\toD\) with weight in \(\mathsf g12>0\). We examine the critical edge produced by removing each possible type of node and show that they are either from \(C\) or negative.

1. (Removing \(D\).) The graph \(G\setminus\{D\}\) is a SAT admissible graph with \(C\in V(G)\), \(D\notin V(G)\). By [lem:C-wins-SAT-no-D], the winner is \(C.\) Hence the edge \(C\toD\) is a critical edge with weight in group \(\mathsf g12\).

2. (Removing a clause \(L_k\).) The graph \(G\setminus\{L_k\}=G(I,K\setminus\{k\})\) is still satisfied, and \(|I|+|K\setminus\{k\}|=t-1\). Hence, by the induction hypothesis, \(\mathrm{SSV}(G\setminus\{L_k\})=C\). Therefore, the critical edge produced by removing \(L_k\) is \(C\toL_k\), which lies in group \(-\mathsf g7\).

3. (Removing \(C\).) The graph \(G\setminus\{C\}\) is an admissible graph without \(C\), with exactly one literal for every present variable and with \(\mathrm{FirstX}(G\setminus\{C\})=0\). Hence, by [lem:D-wins-with-clauses-no-C-general], we get \(\mathrm{SSV}(G\setminus\{C\})=D\). Therefore, the critical edge produced by removing \(C\) is \(D\toC\), which lies in group \(-\mathsf g12\). (\(C\toD\) is also a critical edge with positive weight.)

4. (Removing a literal \(\ell_i\).) Since \(X_i\) is still present and \(\ell_i\) was the unique present literal of variable \(i\), we have \(\mathrm{FirstX}(G\setminus\{\ell_i\})=i\). Hence, by [lem:guards], \(\mathrm{SSV}(G\setminus\{\ell_i\})=X_i\). Therefore, the critical edge produced by removing \(\ell_i\) is \(X_i\to\ell_i\), which lies in group \(-\mathsf g2\).

5. (Removing a guard \(X_i\).) We show that \(\mathrm{SSV}(G\setminus\{X_i\})\in\{C,D\}.\) Consider \(G\setminus\{X_i,\ell_i\}.\) This is a smaller graph of the same paired form, with variable set \(I\setminus\{i\}\) and the same clause set \(K\). If every clause in \(K\) remains satisfied after deleting \(\ell_i\), then by the induction hypothesis, \(\mathrm{SSV}(G\setminus\{X_i,\ell_i\})=C.\) Hence \(C\to\ell_i\) is a critical edge of \(G\setminus\{X_i\}\), in group \(\mathsf g1\). If instead some clause becomes unsatisfied after deleting \(\ell_i\), then by [lem:unsat-D-wins], \(\mathrm{SSV}(G\setminus\{X_i,\ell_i\})=D.\) Hence \(D\to\ell_i\) is a critical edge of \(G\setminus\{X_i\}\), also in group \(\mathsf g1\). Thus \(G\setminus\{X_i\}\) has a group \(\mathsf g1\) critical edge from \(C\) or \(D\) into \(\ell_i\). Since all group \(\mathsf g1\) edges originate from \(C\) or \(D\), it follows that \[\mathrm{SSV}(G\setminus\{X_i\})\in\{C,D\}.\] Therefore the critical edge produced by removing \(X_i\) is a negative edge \(\{C, D\} \to X_i\) in group \(-\mathsf g8\).

In all cases, every critical edge is either an edge out of \(C\) or has negative weight. Moreover, removing \(D\) produces the positive critical edge \(C\toD\). Hence \(\mathrm{SSV}(G)=C\). Applying the statement to the full-assignment graph \(G_\alpha\) completes the proof. ◻

Proof. By [claim:reachability], \(G\) is a prefix graph, has \(\mathrm{FirstX}(G)\neq0\), or is admissible. Every prefix graph contains all guard candidates, and every graph with \(\mathrm{FirstX}(G)= {i^*}\neq0\) contains the guard \(X_{ {i^*}}\); this proves the first part. For the second part: every prefix graph is won by \(C\) or \(D\) (statement \(P(j)\) in the proof of 1), and every graph with \(\mathrm{FirstX}(G)\neq0\) is won by a guard ([lem:guards]); so a clause or literal winner is only possible when \(G\) is admissible. ◻

Proof. Fix such a subtournament \(G\), and let \(A = \mathrm{SSV}(G)\) be its winner; by assumption, \(A\) is one of the designated candidates \(C\) or \(D\), a guard \(X_{ {i^*}}\), or a clause \(L_{{k^*}}\). We treat each case separately, showing that for every candidate \(B\) that beats \(A\) head-to-head, there is a does-not-defeat path \(A \rightsquigarrow B\) all of whose edges have strictly larger weight than \(B \to A\). In each case, we also show that the candidates of the path are present in \(G\); 8 shows all such paths. Throughout, note that whenever the winner is not a guard, [lem:guards] gives \(\mathrm{FirstX}(G) = 0\), so every present guard \(X_i\) has one of its literals present; we denote such a literal by \(\ell_i\).

1. (\(\mathrm{SSV}(G) = C\).) The only in-edges to \(C\) are from clauses \(L_k\) (group \(\mathsf g7\)) and from guards \(X_i\) (group \(\mathsf g8\)). For a guard \(X_i\), the path is \(C\to \ell_i \to X_i\) (\(\mathsf g1,\mathsf g2\)); \(\ell_i\) must be present for \(X_i\) to not win. For a clause \(L_k\), we distinguish two subcases.

   • If some guard \(X_i\) is present in \(G\), the path is \(C\to \ell_i \to X_i \to L_k\) (\(\mathsf g1,\mathsf g2,\mathsf g6\)).

   • If no guard is present in \(G\), then \(G\) is admissible by 1, and by [claim:admissible-winners](b) the clause \(L_k\) is satisfied by some present literal \(\ell_j\); the path is \(C\to \ell_j \to L_k\) (\(\mathsf g1,\mathsf g3\)).

   All path edges lie in groups of smaller index than the edges into \(C\), so \(C\) is undefeated.

2. (\(\mathrm{SSV}(G) = D\).) The only in-edges to \(D\) are from \(C\) (group \(\mathsf g{12}\)) and from guards \(X_i\) (group \(\mathsf g8\)). For a guard \(X_i\), the path is \(D\to \ell_i \to X_i\) (\(\mathsf g1,\mathsf g2\)); \(\ell_i\) must be present for \(X_i\) to not win. Now suppose \(C\in V(G)\); we show that \(C\) does not defeat \(D\), in two subcases.

   • If some guard \(X_i\) is present in \(G\), the path is \(D\to \ell_i \to X_i \to C\) (\(\mathsf g1,\mathsf g2,\mathsf g8\)), and all three groups have index smaller than \(12\).

   • If no guard is present in \(G\), then \(G\) is admissible by 1. For \(D\) to win in \(G\), a clause candidate must then be present; otherwise, by [lem:c-wins-without-clauses] we would get \(\mathrm{SSV}(G) = C\neq D\) for an admissible graph with \(C, D\in V(G)\) and \(L_k\notin V(G).\) The path \(D\to L_k \to C\) (\(\mathsf g7,\mathsf g7\)) then shows that \(C\) does not defeat \(D\).

   All path edges lie in groups of smaller index than the edges into \(D\), so \(D\) is undefeated.

3. (\(\mathrm{SSV}(G) = X_{ {i^*}}\).) By [lem:guards], \(\mathrm{FirstX}(G) = {i^*}\), so the literals \(T_{ {i^*}}, F_{ {i^*}}\) are absent, and the edges \(\{T_{ {i^*}}, F_{ {i^*}}\}\toX_{ {i^*}}\) (group \(\mathsf g2\)) are gone. The only remaining in-edges to \(X_{ {i^*}}\) are from guards \(X_j\) with \(j < {i^*}\) (group \(\mathsf g{10}\)). For each such \(X_j\), one of its literals \(\ell_j\) is present, since \(j < {i^*}= \mathrm{FirstX}(G)\). Hence, the path \(X_{ {i^*}} \to \ell_j \to X_j\) has edges in groups \(\mathsf g5\) and \(\mathsf g2\), both of index smaller than \(10\). Hence \(X_j\) does not defeat \(X_{ {i^*}}\), and \(X_{ {i^*}}\) is undefeated in \(G\).

4. (\(\mathrm{SSV}(G) = L_{{k^*}}\).) By 1, \(G\) is admissible, and by [claim:admissible-winners](c), \(D\notin V(G)\) and \(\mathrm{FirstUnsat}(G) = {k^*}\). Since \(L_{{k^*}}\) is unsatisfied, there is no edge \(\ell_i\to L_{k^*}\) in group \(\mathsf g3\). So the only candidates beating \(L_{{k^*}}\) are the guards \(X_i\) (group \(\mathsf g6\)) and the earlier clauses \(L_{k'}\) with \(k' < {k^*}\) (group \(\mathsf g{11}\)). Since \(L_{{k^*}}\) is unsatisfied, the edge \(L_{{k^*}} \to \ell_i\) is positive (group \(\mathsf g4\)) for every present literal \(\ell_i\); and \(\mathrm{FirstX}(G) = 0\), so every present guard has its literal present. Hence, for a guard \(X_i\), the path is \(L_{{k^*}} \to \ell_i \to X_i\) (\(\mathsf g4,\mathsf g2\)). For an earlier clause \(L_{k'}\), it is satisfied (as \(k' < {k^*}= \mathrm{FirstUnsat}(G)\)), so a satisfying literal \(\ell_j\) gives the path \(L_{{k^*}} \to \ell_j \to L_{k'}\) (\(\mathsf g4,\mathsf g3\)). All path edges lie in groups of smaller index than the edges into \(L_{{k^*}}\), so \(L_{{k^*}}\) is undefeated.

 ◻

Proof. (a) Let \(A = \mathrm{SSV}(G)\) and let \(\ell_i \in V(G)\) be any literal candidate for some \(i\in [n]\). In each case below, every incoming edge to \(A\) lies in a group of strictly larger index (hence smaller weight) than the edge \(A \to \ell_i\), so \(A\) defeats \(\ell_i\) by 2.

• \(A = C\): the edge \(C\to \ell_i\) lies in group \(\mathsf g1\); the in-edges of \(C\) lie in groups \(\mathsf g7\) and \(\mathsf g8\).

• \(A = D\): the edge \(D\to \ell_i\) lies in group \(\mathsf g1\); the in-edges of \(D\) lie in groups \(\mathsf g{12}\) and \(\mathsf g8\).

• \(A = X_{ {i^*}}\): by [lem:guards], \(\mathrm{FirstX}(G) = {i^*}\), so \(T_{ {i^*}},F_{ {i^*}} \notin V(G)\), and every present literal belongs to another variable; hence the edge \(X_{ {i^*}} \to \ell_i\) lies in group \(\mathsf g5\). The in-edges of \(X_{ {i^*}}\) from its own literals (group \(\mathsf g2\)) are absent, leaving only the edges from guards \(X_j\) with \(j< {i^*}\), in group \(\mathsf g{10}\).

• \(A = L_{{k^*}}\): by 1, \(G\) is admissible, and by [claim:admissible-winners](c), \(L_{{k^*}}\) is unsatisfied and \(D\notin V(G)\); hence the edge \(L_{{k^*}} \to \ell\) lies in group \(\mathsf g4\) for every present literal \(\ell\). The in-edges of \(L_{{k^*}}\) from satisfying literals (group \(\mathsf g3\)) and from \(D\) (group \(\mathsf g7\)) are absent, leaving only the edges from guards (group \(\mathsf g6\)) and earlier clauses (group \(\mathsf g{11}\)).

(b) Let \(\mathrm{SSV}(G)=\ell_i\) for some \(i\in[n]\). By 1, \(G\) is admissible, and by [claim:admissible-winners](d), \(C, D\notin V(G)\) and every present clause is satisfied by a present literal (\(\mathrm{FirstUnsat}(G)=0\)); moreover \(\mathrm{FirstX}(G) = 0\) since \(G\) is an admissible graph. We show that every guard and every clause of \(G\) is defeated (which only requires one candidate to defeat them, as opposed to being undefeated by any other candidate); since \(C\) and \(D\) are absent, only literal candidates can then be undefeated.

• Let \(X_j \in V(G)\). Its literal \(\ell_j\) is present, and the edge \(\ell_j\to X_j\) is in group \(\mathsf g2\). Every positive edge leaving \(X_j\) lies in group \(\mathsf g5\) (other literals), \(\mathsf g6\) (clauses), or \(\mathsf g{10}\) (later guards) all strictly smaller than \(\mathsf g2\). By 2, \(\ell_j\) defeats \(X_j\).

• Let \(L_k \in V(G)\), and let \(\ell_j\) be a present literal satisfying it; the edge \(\ell_j \to L_k\) lies in group \(\mathsf g3\). Every positive edge leaving \(L_k\) lies in group \(\mathsf g4\) (non-satisfying literals) or \(\mathsf g{11}\) (later clauses) all strictly smaller than \(\mathsf g3\). By 2, \(\ell_j\) defeats \(L_k\).

Finally, by 3 and the definition of \(\mathrm{SV}\), the candidate \(\mathrm{SV}(G)\) is undefeated in \(G\); since literals are the only undefeated candidates, \(\mathrm{SV}(G)\) is a literal candidate. ◻

Proof. The second assertion is 3(b). We prove the first by strong induction on \(|V(G)|\).

5.0.0.6 Base case

(\(|V(G)| = 1\)). Both rules return the unique candidate, so \(\mathrm{SV}(G) = \mathrm{SSV}(G)\).

5.0.0.7 Induction hypothesis.

Assume the statement holds for every induced subtournament \(G'\) arising in the recursive evaluation of \(\mathrm{SSV}(G(\Phi))\) with \(|V(G')| < |V(G)|\).

5.0.0.8 Induction step.

Let \(A= \mathrm{SSV}(G)\) be a non-literal winner, determined by the maximum-weight critical edge \(A\to B\); that is, \(\mathrm{SSV}(G\setminus\{B\}) = A\). By 2, \(A\) is undefeated in \(G\).

If \(G\) has a unique undefeated candidate \(U\), then \(A= U\), and \(\mathrm{SV}\)returns \(U = A\) directly, so \(\mathrm{SV}(G) = \mathrm{SSV}(G)\). Otherwise, recall that \(\mathrm{SV}\)scans the ordered pairs \((U,V)\) with \(U\) undefeated in \(G\) in decreasing \(w(U,V)\), returning the first with \(\mathrm{SV}(G\setminus\{V\}) = U\). We make two observations. First, since \(\mathrm{SSV}\)scans all ordered pairs in decreasing weight down to \((A,B)\), every pair with weight at least \(w(A,B)\) was scanned by \(\mathrm{SSV}\), so for every such pair \((U,V)\) the subtournament \(G\setminus\{V\}\) arises in the recursive evaluation of \(\mathrm{SSV}(G(\Phi))\) and the induction hypothesis applies to it. Second, by 3(a), no literal candidate is undefeated in \(G\), so every tail \(U\) that \(\mathrm{SV}\)scans is a non-literal candidate.

The pair \((A, B)\) is critical for \(\mathrm{SV}\), since the winner \(A\) is undefeated in \(G\), and \(\mathrm{SSV}(G\setminus\{B\}) = A\) is not a literal, the induction hypothesis gives \(\mathrm{SV}(G\setminus\{B\}) = \mathrm{SSV}(G\setminus\{B\}) = A\).

It remains to show that \(\mathrm{SV}\)does not stop at any earlier pair. Suppose, for contradiction, that \(\mathrm{SV}\)stops at a pair \((U,V)\) with \(w(U,V) > w(A,B)\); then \(U\) is undefeated in \(G\) (hence not a literal) and \(\mathrm{SV}(G\setminus\{V\}) = U\). The subtournament \(G\setminus\{V\}\) arises in the evaluation of \(\mathrm{SSV}(G(\Phi))\), so the induction hypothesis applies to it, and we consider two cases. If \(\mathrm{SSV}(G\setminus\{V\})\) is a literal candidate, then \(\mathrm{SV}(G\setminus\{V\})\) is also a literal candidate, contradicting \(\mathrm{SV}(G\setminus\{V\}) = U\) with \(U\) not a literal. If \(\mathrm{SSV}(G\setminus\{V\})\) is not a literal, then \(\mathrm{SSV}(G\setminus\{V\}) = \mathrm{SV}(G\setminus\{V\}) = U\), so \((U,V)\) is a critical edge of \(G\) for \(\mathrm{SSV}\)with weight larger than \(w(A,B)\), contradicting the maximality of \((A,B)\).

Hence \(\mathrm{SV}\)stops exactly at \((A,B)\), giving \(\mathrm{SV}(G) = A= \mathrm{SSV}(G)\). ◻

Proof. Membership in \(\mathsf{PSPACE}\)follows as in 1: \(\mathrm{SV}\)admits the same depth-first recursion, and the additional test of whether a candidate is undefeated is a reachability computation that requires only polynomial space. For hardness, let \(\Phi\) be a TQBF instance and let \(G(\Phi)\) be the tournament of [margin_groups]. The tournament \(G(\Phi)\) trivially arises in the recursive evaluation of \(\mathrm{SSV}(G(\Phi))\), and by 1 its winner \(\mathrm{SSV}(G(\Phi))\) is \(C\) or \(D\) (in particular, not a literal candidate). Hence, by 4, \(\mathrm{SV}(G(\Phi)) = \mathrm{SSV}(G(\Phi))\), and so \(\mathrm{SV}(G(\Phi)) = C\) if and only if \(\Phi\) is true. The same polynomial-time reduction therefore establishes \(\mathsf{PSPACE}\)-hardness for \(\mathrm{SV}\). ◻

Proof. We proceed by induction on \(t\mathrel{\vcenter{:}}=|B|\) for some \(B\) as defined above.

10.1.0.1 Base case

(\(t=0\)) This is trivially true.

10.1.0.2 Inductive Hypothesis

Fix \(t \ge 1\) and assume the claim holds for \(t-1\). That is, given any \(B\) of size \(t\) (as defined above), \[\mathrm{SSV}(G \cup ( B \setminus \{\ell_i\} )) = \mathrm{SSV}(G) \quad \forall \, \ell_i \in B\]

10.1.0.3 Inductive Step

Fix any arbitrary \(B\) of size \(t\) and define \(H \mathrel{\vcenter{:}}= G \cup B\). Let \(M \in \{C, D\}\) be the designated winner, \(\mathrm{SSV}(G) = M\).

By the inductive hypothesis, we know that the edges \(M \rightarrow \ell_i\) (in group \(\mathsf g1\)) are critical edges of \(H\) for all \(\ell_i \in B\), since \(\mathrm{SSV}(H\setminus\{\ell_i\}) = M\). Let \(M \rightarrow \ell_{i^*}\) be the largest among those (\({i^*}= \mathop{\mathrm{arg\,min}}_i \{\ell_i\in B\}\)). Note that the only other possible critical edge of larger weight is \(M \rightarrow \ell_j\) for \(j< {i^*},\;\ell_j \in V(G)\), i.e., the designated winner to some other literal already present in \(G\) with a smaller index. However, the critical edge produced by removing \(\ell_j\) is \(X_j \rightarrow \ell_j\) by [lem:guards] since \(\mathrm{FirstX}(H\setminus\{\ell_j\})=j\), therefore the largest set of critical edges in \(H\) is \(M \rightarrow \ell_ {i^*},\, \ell_ {i^*}\in B\) and \(\mathrm{SSV}(H)=M\). ◻

Proof. Using 4, we are going to decompose into the different types of nodes. Let \(S_I\) be the paired core of literals and guards and \(B\) the set of extra single literals. And let \(K\subseteq[m]\) be the present clauses. By [lem:adding95lits95C95D95wins], it suffices to prove the claim for the paired core. Let \(G_{I,K}\) be the induced subtournament on \(V(G_{I,K})=\{D\}\cup\{L_k:k\in K\}\cup S_I\). We will show that \(\mathrm{SSV}(G_{I,K})=D\) and thus \(\mathrm{SSV}(G)=D\).

We prove the statement by induction on the number of clauses. For each integer \(t\ge 0\), define the statement \(P(t)\) as follows:

\(P(t)\): \(\forall \, J\subseteq I, \forall \, K'\subseteq K\) with \(|K'|=t\), the \(\mathrm{SSV}(H_{J,K'})=D\) where \(H_{J,K'}\) is the induced subtournament on \[V(H_{J,K'})=\{D\}\cup \{\ell_j,X_j:j\in J\} \cup \{L_k:k\in K'\}.\]

10.1.2.1 Base case: \((t=0)\).

Let \(J\subseteq I\) and let \(K'=\emptyset\). Then \(V(H_{J,K'})=\{D\}\cup \{\ell_j,X_j:j\in J\}\), so \(\mathrm{SSV}(H_{J,K'})=D\) by 5. Hence \(P(0)\) holds.

10.1.2.2 Induction hypothesis.

Fix \(t\ge 1\) and assume that \(P(r)\) holds for every \(r<t\).

10.1.2.3 Induction step.

We prove \(P(t)\). Fix \(J\subseteq I\), \(K'\subseteq K\) with \(|K'|=t\), and \(H\mathrel{\vcenter{:}}= H_{J,K'}\). We assume \(|J|>0\), since \(|J|=0\) implies that \(D\) is a Condorcet winner of the corresponding graph. By definition, since every present guard in \(H\) has its corresponding literal also present, we have \(\mathrm{FirstX}(H)=0\). We will show that the largest critical edge of \(H\) is of the form \(D\to L_k\) for some \(k\in K'\), which implies \(\mathrm{SSV}(H)=D\).

We consider the critical edge produced by removing each type of node.

1. (Removing a clause \(L_k\) .) The graph \(H\setminus \{L_k\}\) is exactly of the form covered by \(P(t-1)\), with the same set \(J\) and clause set \(K'\setminus\{k\}\). Since \(|K'\setminus\{k\}|=t-1\), the induction hypothesis gives \(\mathrm{SSV}(H\setminus\{ L_k\})=D\). Therefore, \(D\to L_k\) is a critical edge of \(H\), and it lies in group \(\mathsf g7\).

2. (Removing a literal \(\ell_i\) .) By assumption \(|J|>0.\) Since \(X_i\) is still present and \(\ell_i\) was the unique present literal of variable \(i\), we have \(\mathrm{FirstX}(H\setminus \{\ell_i\})=i\). By [lem:guards], \(\mathrm{SSV}(H\setminus \{\ell_i\})=X_i\). Hence the critical edge produced by removing \(\ell_i\) is \(X_i\to \ell_i\), which lies in group \(-\mathsf g2\). Hence, this critical edge is smaller than \(D\to L_k\) in \(\mathsf g_7.\)

3. (Removing \(D\) .) Since removing \(D\) does not affect literals or guards, we still have \(\mathrm{FirstX}(H\setminus \{D\})=0\). Hence, by [lem:guards], no guard can win \(H\setminus \{D\}\). We distinguish two cases.

   1. If \(H\setminus \{D\}\) is UNSAT, then by 1, \(\mathrm{SSV}(H\setminus \{D\})=L_{k^*}\), where \(L_{k^*}=\mathrm{FirstUnsat}(H\setminus \{D\})\) is the first unsatisfied clause. Thus the critical edge produced by removing \(D\) is \(L_{k^*}\to D\), which lies in group \(-\mathsf g7\).

   2. If \(H\setminus \{D\}\) is SAT, then \(\mathrm{FirstUnsat}(H\setminus \{D\})=0\), so by 1 no clause can win \(H\setminus \{D\}\). As no guard can win \(H\setminus \{D\}\), the winner must be some literal \(\ell_j\), and the critical edge produced by removing \(D\) is \(\ell_j\to D\), which lies in group \(-\mathsf g1\).

   In either case, the critical edge produced by removing \(D\) is negative, hence strictly smaller than every positive group \(\mathsf g7\) edge.

4. (Removing a guard \(X_i\).) Let \(H_i:=H\setminus\{X_i\}\). We show that the critical edge produced by removing \(X_i\) has weight \(<\mathsf g7\). First, \(\mathrm{FirstX}(H_i)=0\), so by [lem:guards], no guard can win \(H_i\).

   We claim that, for every \(k\in K'\), \(\mathrm{SSV}(H_i\setminus\{L_k\})=D.\) Indeed, \(H_i\setminus\{L_k,\ell_i\} = H_{J\setminus\{i\},K'\setminus\{k\}},\) so by the induction hypothesis it is won by \(D\). Since \(X_i\notin V(H_i\setminus\{L_k\})\), adding back the single literal \(\ell_i\) does not change a designated winner, by [lem:adding95lits95C95D95wins]. Hence \[\mathrm{SSV}(H_i\setminus\{L_k\})=D.\] Thus every edge \(D\toL_k\), \(k\in K'\), is a critical edge of \(H_i\), in group \(\mathsf g7\).

   It remains to rule out \(\mathrm{SSV}(H_i)=\ell_i\). If \(\ell_i\) won \(H_i\), then its winning critical edge would have to beat the group \(\mathsf g7\) edge \(D\toL_k\). Since \(X_i\notin V(H_i)\), the group \(\mathsf g2\) edge \(\ell_i\toX_i\) is absent. The only remaining edges out of \(\ell_i\) that can beat group \(\mathsf g7\) are edges \(\ell_i\toL_k\) in group \(\mathsf g3\). But for every \(L_k\in K'\), we just proved that \(\mathrm{SSV}(H_i\setminus\{L_k\})=D,\) so the critical edge produced by deleting \(L_k\) is \(D\toL_k\), not \(\ell_i\toL_k\). Therefore \(\ell_i\) cannot win \(H_i\).

   Thus neither a guard nor \(\ell_i\) can win \(H_i\). Hence the critical edge into \(X_i\) is not the positive edge \(\ell_i\toX_i\); all remaining possible edges into \(X_i\) have weight \(<\mathsf g7\).

We have now examined all possible removals from \(H\). Removing any clause \(L_k\) produces a critical edge \(D\to L_k\) in group \(\mathsf g7\), while every critical edge produced by removing a literal, a guard, or \(D\) has weight strictly smaller than \(\mathsf g7\). Therefore, the largest critical edge of \(H\) is of the form \(D\to L_k\), and consequently \(\mathrm{SSV}(H)=D\). This concludes the proof of \(P(t)\).

Applying \(P(|K'|)\) to \(J=I\) and \(K'=K\), we get \(\mathrm{SSV}(G_{J,K})=D\). We can apply [lem:adding95lits95C95D95wins] to add the literals in \(B\), to get \(\mathrm{SSV}(G)=D\). ◻

Proof. Using 4, we write \(S=S_I\cup B\), where \(S_I\) is the paired core and \(B\) is the set of extra single literals. Let \(G_I\) be the induced subtournament on \(V(G_I)=\{C,D\}\cup S_I\). We will show that \(\mathrm{SSV}(G_I)=C\). By [lem:adding95lits95C95D95wins], it follows that \(\mathrm{SSV}(G)=C\).

We do this by proving that the maximum critical edge of \(G_I\) is \(C\toD\), and comparing it to the critical edges produced by removing every other node of \(G_I\).

1. (Removing \(D\).) \(\mathrm{SSV}(G_I\setminus \{D\}) = C\) by 6, producing a critical edge in group \(\mathsf g12\).

2. (Removing \(C\).) \(\mathrm{SSV}(G_I\setminus C) = D\) by 5, producing a critical edge in group \(-\mathsf g12\).

3. (Removing \(\ell_i\).) Since in \(G_I\) all the literals are paired with their guards, we get \(\mathrm{FirstX}(G_I\setminus\{\ell_i\}) = i\), implying \(X_i \rightarrow \ell_i\) is the critical edge produced by removing \(\ell_i\), in group \(-\mathsf g2\).

4. (Removing \(X_i\).) It suffices to show that the critical edge produced by removing \(X_i\) has weight \(< \mathsf g12\). That is, the edge \(w \rightarrow X_i\) has weight less than \(\mathsf g12,\) where \(w=\mathrm{SSV}(G_I\setminus \{X_i\})\) Suppose, for contradiction, that the critical edge has weight \(>\mathsf g12\). The only two candidate sets for the critical edges are thus \(X_{j<i} \rightarrow X_i\) (\(\mathsf g10\)) and \(\ell_i \rightarrow X_i\) (\(\mathsf g2\)). We show that \(w\neqX_j\) and \(w\neq\ell_i.\)

   1. By [lem:guards], \(X_j\) can only win if its corresponding literal is removed, and by assumption, \(\mathrm{FirstX}(G_I)=0\), hence \(\mathrm{FirstX}(G_I\setminus\{X_i\})=0.\)

   2. Since the winner is \(w=\ell_i,\) the largest critical edge of \(G_I\setminus \{X_i\}\) must be of the form \(\ell_i \rightarrow u\), for some \(u\in G_I\setminus\{X_i\}\). We proceed by case analysis:

      1. By [lem:guards], the winner would be in \(X_j\), since \(\mathrm{FirstX}(G\setminus\{X_i,\ell_j\})=j.\)

      2. Then the critical edge of \(G\setminus\{X_i\}\) would be in group \(-\mathsf g5.\)

      3. By 5, \(D\) wins. Hence, a critical edge of \(G\setminus\{X_i\}\) is \(D\toC\) that is in group \(-\mathsf g12 > -\mathsf g5.\)

      4. By 6, \(C\) wins. Hence, a critical edge of \(G\setminus\{X_i\}\) is \(C\toD\) which is in group \(\mathsf g12>-\mathsf g5.\)

      Thus, \(\ell_i\) cannot win in \(G_I\setminus \{X_i\}\) since there exists a critical edge (\(C\toD\)) in \(G_I\setminusX_i\) with a larger weight than the largest critical edge of the form \(\ell_i\to u.\)

   Thus, the critical edge produced by removing \(X_i\) has weight \(<0<\mathsf g12\).

Thus, the highest critical edge in \(G_I\) is \(C\rightarrow D\), and \(C\) wins. ◻

Proof. We will show that the largest critical edge is \(D\rightarrowC\), by comparing it to all other critical edges produced by removing any node in \(V(G)\setminus\{D\}.\) We begin by removing all unpaired literals \(\ell_i\): literals for whom no guard \(X_i\) is present. A simple argument uses [lem:adding95lits95C95D95wins] to add these back at the end.

1. (Removing \(C\).) \(\mathrm{SSV}(G\setminus C) = D\) by [lem:D-wins-with-clauses-no-C-general], producing a critical edge in group \(-\mathsf g12\).

2. (Removing \(D\).) \(\mathrm{SSV}(G\setminus \{D\}) = L_k\) by 1 since \(L_k\) is unsatisfied and \(D\) is not in the graph. Hence, the critical edge produced is in group \(-\mathsf g7\).

3. (Removing \(L_k\).) \(\mathrm{SSV}(G\setminus\{L_k\})=C\) by [lem:c-wins-without-clauses], hence the critical edge produced is \(C\toL_k\) with weight in \(-\mathsf g7.\)

4. (Removing \(\ell_i\).) \(\mathrm{FirstX}(G\setminus\{\ell_i\}) = i \implies \mathrm{SSV}(G\setminus\{\ell_i\}) = X_i\), by [lem:guards]. Hence, \(X_i \rightarrow \ell_i\) is the critical edge produced, which is in group \(-\mathsf g2\).

5. (Removing \(X_i\).) It suffices to show that the critical edge produced by removing \(X_i\) has weight \(<- \mathsf g12\). That is, the edge \(\mathrm{SSV}(G\setminus \{X_i\}) \rightarrow X_i\) has weight less than \(-\mathsf g12.\) Suppose, for contradiction, that the critical edge has weight \(>-\mathsf g12\). The only two candidate sets for the critical edges are thus \(X_{j<i} \rightarrow X_i\) (\(\mathsf g10\)) and \(\ell_i \rightarrow X_i\) (\(\mathsf g2\)).

   1. By [lem:guards], \(X_j\) can only win if its corresponding literal is removed, and by assumption, \(\mathrm{FirstX}(G)=0\).

   2. Assume, for the sake of contradiction, that \(SSV(G\setminus \{X_i\}) = \ell_i\). Then the largest critical edge of \(G\setminus \{X_i\}\) must be of the form \(\ell_i \rightarrow u\), for some \(u\in V(G\setminusX_i)\). We proceed by case analysis:

      1. By [lem:guards], the winner would be in \(X_j\).

      2. Then the critical edge of \(G\setminusX_i\) would be in group \(-\mathsf g5.\)

      3. By [lem:D-wins-with-clauses-no-C-general], \(D\) wins. Hence, a critical edge of \(G\setminusX_i\) is \(D\toC\) that is in group \(-\mathsf g12 > -\mathsf g5.\)

      4. By 1, \(L_k\) wins. Hence, a critical edge of \(G\setminusX_i\) is \(L_k\toD\), which is in group \(-\mathsf g7<-\mathsf g12,\) which is smaller than the critical edge \(D\toC\) in group \(-\mathsf g12\).

      5. by [lem:c-wins-without-clauses] \(C\) wins. Hence, a critical edge of \(G\setminusX_i\) is \(C\toL_k\), which is in group \(-\mathsf g7<-\mathsf g12,\) which is smaller than the critical edge \(D\toC\) in group \(-\mathsf g12\).

      Thus, \(\ell_i\) cannot win in \(G\setminus \{X_i\}\) since there exists a critical edge (\(D\toC\)) in \(G\setminusX_i\) with a larger weight than any critical edge of the form \(\ell_i\to u.\)

   Thus, the critical edge produced by removing \(X_i\) has weight \(<-\mathsf g12\).

As mentioned at the start, we use the simple argument implied by [lem:adding95lits95C95D95wins] to add back the unpaired literals and prove the claim.

Thus, the highest critical edge in \(G\) is \(D\rightarrow C\), and \(D\) wins. ◻

Proof. We proceed by induction on \(t := |V(G)|\).

10.1.5.1 Base case

(\(t = 1\)). \(V(G) = \{C\}\), so \(\mathrm{SSV}(G) = C\).

10.1.5.2 Inductive hypothesis.

Fix \(t \ge 2\) and assume the claim holds for every admissible graph \(G'\) with \(C\in V(G')\), \(D\notin V(G')\), \(\mathrm{FirstUnsat}(G') = 0\), and \(|V(G')| < t\).

10.1.5.3 Inductive step.

Let \(G\) be such a graph with \(|V(G)| = t\). Since \(G\) is an admissible graph, \(\mathrm{FirstX}(G) = 0\). We consider all possible critical edges produced by removing each type of node.

1. (Removing \(X_i\).) Since \(\mathrm{FirstX}(G) = 0\), the literal \(\ell_i\) is present in \(G\). Removing \(X_i\) does not expose any other guard, hence \(\mathrm{FirstX}(G \setminus \{X_i\}) = 0\). Removing a guard does not affect clause satisfaction, so \(\mathrm{FirstUnsat}(G \setminus \{X_i\}) = 0\). Thus \(G \setminus \{X_i\}\) is a strictly smaller admissible graph with \(C\) present, \(D\) absent, and \(\mathrm{FirstUnsat}= 0\). By the inductive hypothesis, \(\mathrm{SSV}(G \setminus \{X_i\}) = C\). Therefore, \(C\to X_i\) is a critical edge of \(G\) with weight in group \(-\mathsf g8\).

2. (Removing \(L_k\).) Removing a clause does not affect guards or literals, so \(\mathrm{FirstX}(G \setminus \{L_k\}) = 0\) and \(\mathrm{FirstUnsat}(G \setminus \{L_k\}) = 0\). By the inductive hypothesis, \(\mathrm{SSV}(G \setminus \{L_k\}) = C\). Therefore, \(C\to L_k\) is a critical edge of \(G\) with weight in group \(-\mathsf g7\).

3. (Removing \(\ell_i\) with \(X_i \in V(G)\).) We have \(\mathrm{FirstX}(G \setminus \{\ell_i\}) = i > 0\). By [lem:guards], \(\mathrm{SSV}(G \setminus \{\ell_i\}) = X_i\). The critical edge is \(X_i \to \ell_i\) with weight in group \(-\mathsf g2\). However, \(C\toX_i\) is also a critical edge with a larger weight.

4. (Removing a literal \(\ell_i\) with \(X_i \notin V(G)\).) Since \(X_i\) is absent, \(\mathrm{FirstX}(G \setminus \{\ell_i\}) = 0\), so \(G \setminus \{\ell_i\}\) is an admissible graph with \(C\) present and \(D\) absent.

   • Case 1: \(\mathrm{FirstUnsat}(G \setminus \{\ell_i\}) = 0\). By the inductive hypothesis, \(\mathrm{SSV}(G \setminus \{\ell_i\}) = C\). The critical edge is \(C\to \ell_i\) with weight in group \(\mathsf g1\).

   • Case 2: \(\mathrm{FirstUnsat}(G \setminus \{\ell_i\}) = r > 0\). The literal \(\ell_i\) was the unique satisfying literal for clause \(L_r\), and \(D\notin V(G \setminus \{\ell_i\})\). By 1, \(\mathrm{SSV}(G \setminus \{\ell_i\}) = L_r\). Since \(\ell_i\) satisfied \(L_r\), the edge \(\ell_i \to L_r\) lies in group \(\mathsf g3\), so the critical edge \(L_r \to \ell_i\) has weight in group \(-\mathsf g3\). But the edge \(C\toL_r\) is also critical with a larger weight.

5. (Removing \(C\).) Removing \(C\) does not affect guards or literals, so \(\mathrm{FirstX}(G \setminus \{C\}) = 0\). By [lem:guards], no guard wins \(G \setminus \{C\}\). Since \(\mathrm{FirstUnsat}(G \setminus \{C\}) = 0\) and \(D\notin V(G \setminus \{C\})\), 1 implies no clause wins \(G \setminus \{C\}\) either. Hence, \(\mathrm{SSV}(G \setminus \{C\}) = \ell_j\) for some literal, and the critical edge \(\ell_j \to C\) has weight in group \(-\mathsf g1\). But, as we showed in the previous cases, there is always a critical edge from \(C\) with a larger weight.

By the case analysis above, every critical edge that is not from \(C\) is dominated by a critical edge from \(C\). Therefore, the maximum critical edge is from \(C\), and hence \(\mathrm{SSV}(G)=C\). ◻

Proof of [claim:reachability]. The evaluation starts at \(G(\Phi) = G_{\alpha_{<1}}\), which is a prefix graph. We show that whenever the rule is evaluated on a graph \(G\) in \((\mathcal{P})\cup(\mathcal{A})\cup(\mathcal{F})\), every subtournament \(G\setminus\{B\}\) on which it recurses also lies in \((\mathcal{P})\cup(\mathcal{A})\cup(\mathcal{F})\); the claim then follows by induction on the depth of the recursion.

• \(G = G_{\alpha_{<j}}\) is a prefix graph. If \(j = n+1\) then \(G\) is a full-assignment graph, hence admissible, and the admissible case applies. So let \(j \le n\). The proof of 1 shows that the scan on \(G\) is resolved within the group \(\mathsf g1\) edges of variables \(1,\ldots,j\): for \(i<j\) the pairs \((C,\ell_i)\) and \((D,\ell_i)\) are not critical, since \(\mathrm{FirstX}(G\setminus\{\ell_i\}) = i\) and so \(\mathrm{SSV}(G\setminus\{\ell_i\}) = X_i\) by [lem:guards]; and among the four pairs of variable \(j\), one is critical, because \(G\setminus\{F_j\}\) and \(G\setminus\{T_j\}\) are the prefix graphs of the two extensions of \(\alpha_{<j}\) and each is won by \(C\) or \(D\) by \(P(j{+}1)\). Hence the evaluated subtournaments are \(G\setminus\{\ell_i\} \in (\mathcal{F})\) for \(i<j\), and \(G\setminus\{F_j\}, G\setminus\{T_j\} \in (\mathcal{P})\).

• \(G\) is admissible. Let \(B \in V(G)\) be arbitrary; we show \(G\setminus\{B\}\in(\mathcal{F})\cup(\mathcal{A})\) regardless of whether the pair is scanned. Deleting a candidate cannot make both literals of a variable present, so \(G\setminus\{B\}\) contains at most one literal per variable. Since \(\mathrm{FirstX}(G)=0\), every present guard has its literal present. If \(B = \ell_i\) is a literal with \(X_i \in V(G)\), then deleting \(B\) uncovers exactly the guard \(X_i\), so \(\mathrm{FirstX}(G\setminus\{B\}) = i \neq 0\) and \(G\setminus\{B\}\in(\mathcal{F})\). For every other \(B\) (a designated candidate, a clause, a guard, or a literal whose guard is absent), every remaining guard keeps its literal, so \(\mathrm{FirstX}(G\setminus\{B\}) = 0\) and \(G\setminus\{B\}\) is admissible.

• Graphs with \(\mathrm{FirstX}(G) = {i^*}\neq 0\). By [lem:guards], \(\mathrm{SSV}(G) = X_{ {i^*}}\), so the maximum critical edge of \(G\) has the form \(X_{ {i^*}} \to u\). For every \(B \neq X_{ {i^*}}\), the guard \(X_{ {i^*}}\) remains present in \(G\setminus\{B\}\) with both of its literals absent, so \(\mathrm{FirstX}(G\setminus\{B\}) \in \{1,\ldots, {i^*}\}\), and \(G\setminus\{B\}\in(\mathcal{F})\). It remains to consider \(B = X_{ {i^*}}\), and we distinguish two cases.

  • If \(G\) contains at most one literal per variable: deleting \(X_{ {i^*}}\) cannot uncover a guard with a smaller index (those were covered in \(G\) and keep their literals), so \(\mathrm{FirstX}(G\setminus\{X_{ {i^*}}\})\) is either \(0\), in which case \(G\setminus\{X_{ {i^*}}\}\) is admissible, or some \(j > {i^*}\), in which case \(G\setminus\{X_{ {i^*}}\}\in(\mathcal{F})\).

  • If \(G\) contains both literals \(T_m, F_m\) of some variable \(m\) (note \(m \neq {i^*}\), as \(T_{ {i^*}},F_{ {i^*}}\notin V(G)\)), we show that the pair \((Z, X_{ {i^*}})\) is never scanned, for any \(Z\), so \(G\setminus\{X_{ {i^*}}\}\) never arises. Deleting \(T_m\) leaves \(F_m\) present, so no guard becomes uncovered and \(\mathrm{FirstX}(G\setminus\{T_m\}) = {i^*}\); by [lem:guards], \(\mathrm{SSV}(G\setminus\{T_m\}) = X_{ {i^*}}\), and the edge \(X_{ {i^*}}\toT_m\), which lies in group \(\mathsf g5\), is critical. Hence the maximum critical edge of \(G\) has weight at least that of a group \(\mathsf g5\) edge. On the other hand, since \(T_{ {i^*}},F_{ {i^*}}\notin V(G)\), the only positive edges entering \(X_{ {i^*}}\) come from guards \(X_j\) with \(j< {i^*}\), in group \(\mathsf g{10}\). Since \(\mathsf g5 > \mathsf g{10}\), every pair \((Z, X_{ {i^*}})\) has weight strictly below the maximum critical edge, so the scan stops before reaching it.

 ◻

Proof of [claim:admissible-winners]. As in 4, write \(B := \{\ell_j \in V(G) : X_j \notin V(G)\}\) for the single literals whose guards are absent, and let the core of \(G\) be the induced subtournament on \(V(G)\setminus B\). The core is admissible, contains no literal of any variable \(j\) with \(\ell_j \in B\), and consists of the designated candidates \(\{C, D\}\) present in \(G\), the paired guards and literals \(\{X_i, \ell_i : i \in I\}\), and the clause candidates of \(G\). By [lem:adding95lits95C95D95wins], if the winner of the core is \(C\) or \(D\), then it is also the winner of \(G\).

1. Suppose \(C, D\in V(G)\). The core then has exactly the form \(G(I,K)\) appearing in the induction statements established in the proofs of [lem:sat-C-wins,lem:unsat-D-wins]. If every clause of the core is satisfied by a present (paired) literal, the statement in the proof of [lem:sat-C-wins] gives \(\mathrm{SSV}(\mathrm{core}) = C\) (when no clause is present, this is [lem:c-wins-without-clauses]); if some clause of the core is unsatisfied, the statement in the proof of [lem:unsat-D-wins] gives \(\mathrm{SSV}(\mathrm{core}) = D\). In both cases [lem:adding95lits95C95D95wins] lifts the winner to \(G\), so \(A \in \{C,D\}\).

2. Suppose \(A = C\). If \(D\in V(G)\): by the dichotomy in (a), \(A = C\) forces every clause of the core to be satisfied by a paired literal; since paired literals are present in \(G\) and \(G\) has the same clauses as its core, \(\mathrm{FirstUnsat}(G) = 0\).

   If \(D\notin V(G)\): by 1, the winner is a clause candidate if and only if \(\mathrm{FirstUnsat}(G) \neq 0\); since \(A = C\), \(\mathrm{FirstUnsat}(G) = 0\).

3. Suppose \(A = L_{{k^*}}\). First, we show \(D\notin V(G)\). If \(D\in V(G)\) and \(C\notin V(G)\), then [lem:D-wins-with-clauses-no-C-general] gives \(A = D\), a contradiction; and if \(C, D\in V(G)\), then (a) gives \(A \in \{C,D\}\), again a contradiction. Now that \(D\notin V(G)\), 1 applies and gives \(\mathrm{FirstUnsat}(G) = {k^*}\).

4. Suppose \(A\) is a literal. As in (c), \(D\in V(G)\) leads to \(A \in \{C,D\}\) or \(A = D\), a contradiction; so \(D\notin V(G)\). If \(C\in V(G)\): were \(\mathrm{FirstUnsat}(G) = 0\), [lem:C-wins-SAT-no-D] would give \(A = C\); were \(\mathrm{FirstUnsat}(G) \neq 0\), 1 would give a clause winner; either way a contradiction, so \(C\notin V(G)\). Finally, by 1 (with \(D\notin V(G)\)), the winner is a clause candidate if and only if \(\mathrm{FirstUnsat}(G) \neq 0\); since \(A\) is a literal, \(\mathrm{FirstUnsat}(G) = 0\).

 ◻