# How can I complete my derivation of an algorithm to solve Sudoku puzzles from my formalisation of the rules?

I'm hoping to design and implement an intuitive algorithm that solves 9x9 Sudoku puzzles. I want to do this by first formalising the basic rules of the puzzle, and then deriving principles from these that when followed should be sufficient for solving the problem. I have reproduced my (very rough) work below.

Rule 1: Each box must contain one instance of each of the numbers 1 to 9:
----- At least one instance: If (i, j) is only possible location of v in box b, then val(i, j) = v
----- At most one instance: If val(i, j) = v in box b, then for all (i2, j2) in box b, if (i != i2 || j != j2) then val(i2, j2) != v

Rule 2: Each row must contain one instance of each of the numbers 1 to 9:
----- At least one instance: If (i, j) is only possible location of v in row r, then val(i, j) = v
----- At most one instance: If val(i, j) = v in row r, then for all (i2, j2) in row r, if (i != i2 || j != j2) then val(i2, j2) != v

Rule 3: Each column must contain one instance of each of the numbers 1 to 9:
----- At least one instance: If (i, j) is only possible location of v in column c, then val(i, j) = v
----- At most one instance: If val(i, j) = v in column c, then for all (i2, j2) in column c, if (i != i2 || j != j2) then val(i2, j2) != v

Rule 4: Each cell must contain exactly one number:
----- At least one number: If (i, j) cannot contain any value except v, then val(i, j) = v
----- At most one number: If val(i, j) = v1 && val(i, j) = v2, then v1 = v2


However, I have run into a problem. Having solved Sudoku puzzles of various difficulties myself, I am aware of other principles that may need to be followed to solve a given puzzle. For instance:

----- If v must occur in one of two or three cells in box b, and these cells fall in the same row r, v cannot occur anywhere else in r.
----- If v must occur in one of two or three cells in box b, and these cells fall in the same column c, v cannot occur anywhere else in c.


These examples look like weaker versions of principles I have already written above, but I am having a hard time trying to derive them from the rules, since I want to be rigorous rather than simply adding principles ad hoc.

If anyone could give me a hand by showing me how I can go about deriving these more complex principles rigorously from the rules (ensuring that nothing is missed), I would be grateful. Thanks.

One method of dealing with these, somewhat, emergent rules is constraint solving. You can iterate through each cell and place constraints on other squares based on that cell.

For example, if a square is 3, you can place a "cannot be 3" constraint on all other squares in its row, column, and 3x3 box. The two examples you provided can be solved once you place all the constraints, and look at what options are available.

This sort of method is very similar to what you would do when solving a sudoku puzzle when you write down the possible numbers in each square, and fill a box in when there is only one possibility.

• Thanks for the reply. The approach that you have outlined is very much in line with how I have designed my algorithm. But my real question is how one can determine all possible constraints on other squares that could potentially arise during a puzzle. In particular, I am attempting to derive these from the basic rules. It is necessary to be rigorous in this activity in order to guarantee that my algorithm will be able to solve every 9x9 sudoku, rather than discovering and adding rules in an ad hoc manner. Jul 10 '18 at 15:45
• What do you mean by "all possible constraints"? In higher difficulty Sudoku puzzles, it is required to guess some squares, then backtrack if it was wrong, so incorporating backtracking in your algorithm is a must if you want to be able to solve every sudoku puzzle. Jul 10 '18 at 15:55
• If what you mean by "deriving from basic rules" means just entering the basic rules and solving the puzzle, you could look into Z3, a constraint solver. However, this also uses bruteforcing/backtracking to solve the constraints it is given, so backtracking is still a must. Jul 10 '18 at 16:02
• You are saying that there exists a 9x9 sudoku which cannot be solved without backtracking. Can you give an example? I am postulating that if the algorithm is restricted to operate on 9x9 sudokus only, that a finite number of 'reasonably' simple principles can be repeatedly applied to solve any 9x9 sudoku with a unique solution - without the need for any brute force/guesswork/backtracking. Jul 10 '18 at 22:38
• The Sudoku puzzles intended for humans to solve require no guessing. In principle, it is possible to design a puzzle that requires guessing.
– Juho
Jul 11 '18 at 6:12