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 &amp;&amp; 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.