# 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.