# Exact Method for Generating Strategy-Solvable Sudoku Clues
## 3 Formulation
For such strategies, suppose that \(q_{2}\) is obtained from \(q_{1}\) by applying all strategies applicable to \(q_{1}\). Then, if \(g_{1}=g_{2}\), no strategy applicable to \(q_{2}\) remains, and \(q_{2}\) cannot be changed any more, i.e., \(q_{2}=q_{3}\). A state \(q=\left(f,g\right)\in Q\) is an _initial state_ if it satisfies the following: \(f\left(i,j\right)\
eq 0\) for all clue cells; \(f\left(i,j\right)=0\) for the other cells; and \(n\
ot\in g\left(i,j\right)\) if and only if the antecedent of \(S_{2}\) holds. The last condition ensures that for each clue cell, all digits but the determined one are ruled out; all digits that appear as candidates in a common group to some determined digit are ruled out; and--the only-if part--no other digits are ruled out. Notice that the only-if part is the most essential because the if part can be omitted thanks to \(S_{2}\). It is worth noting, that for non-initial states, this must not be assumed in general because of strategies for number removals such as locked candidates. For example, in the-left most grid of Figure 5, we can observe that all digits not designated to be ruled out by the antecedent of \(S_{2}\) remain as candidates. We denote by \(I\) the set of all initial states. A _final state_ is a state such that digits are determined for all cells, that is, \(f\left(i,j\right)\
eq 0\) for all \(\left(i,j\right)\). We denote by \(F\) the set of all final states. **Definition 1**. : _Let \(\left(Q,R,I,F\right)\) be a state transition model of Sudoku. A state \(q_{0}\) is strategy-solvable if there is a sequence of states \(q_{0},\ldots,q_{k}\in Q\) such that \(q_{0}\in I\), \(q_{k}\in F\), and \(q_{i}Rq_{i+1}\) for all \(i\in\left\{0,\ldots,k-1\right\}\)._  
**Definition 2**. : _Let \(\left(Q,R,I,F\right)\) be a state transition model of Sudoku. The strategy-solvable Sudoku clues problem (or SSC in short) is to determine whether there is a strategy-solvable state of \(\left(Q,R,I,F\right)\)._  
Figure 5: Sequence of grids in a \(4\times 4\) Sudoku, evolving from the left-most initial state to the right-most final state. Larger digits are determined ones and smaller digits are candidates. Suppose that \(R\) is given as a logical formula that represents strategies and a set \(S\) of clue cells is also given. Consider \(Q\), \(I\), and \(F\) as the ones defined as described above. Sudoku clues are _strategy-solvable_ if the initial state corresponding to the Sudoku clues is strategy-solvable with respect to \((Q,R,I,F)\). The strategy-solvable Sudoku clues problem is defined accordingly. If the output of the problem is yes, in practice we will also ask for generating strategy-solvable Sudoku clues. **Proposition 1**. : _Let \(q=(f,g)\) be a state of grid. For any cells \((i,j)\), \((i^{\prime},f^{\prime})\) in a common group, \(f\left(i,j\right)=f\left(i^{\prime},j^{\prime}\right)\) implies \((i,j)=(i^{\prime},j^{\prime})\) or \(f\left(i,j\right)=0\)._  
Proof. : Suppose that \(f\left(i,j\right)=f\left(i^{\prime},j^{\prime}\right)\), \((i,j)\
eq(i^{\prime},j^{\prime})\), and \(f\left(i,j\right)\
eq 0\). Let \(n=f\left(i^{\prime},j^{\prime}\right)\). Applying \(S_{2}\), we obtain \(n\
ot\in g\left(i,j\right)\). Since \(n=f\left(i,j\right)\), applying \(S_{2}\), we obtain \(n^{\prime}\
ot\in g\left(i,j\right)\) for all \(n^{\prime}\
eq n\). From both, \(g\left(i,j\right)=\emptyset\) follows, and this is contradictory to \(S_{1}\). **Corollary 1**. : _Every final state represents a Sudoku solution._  
Proof. : Let \(q=(f,g)\) be a final state. Since \(f\) is a function, each cell must have a single digit. From Proposition 1 and \(f\left(i,j\right)>0\), it follows that each digit appears once in every group. Notice that this corollary holds no matter what state transition relation is given. **Proposition 2**. : _Let \(R\) be a state transition relation. Let \(q_{0}=(f_{0},g_{0})\,,\ldots,q_{k}=(f_{k},g_{k})\) be a sequence of states such that \(q_{s}Rq_{s+1}\) for all \(s\in\{0,\ldots,k-1\}\).