Sudoku

Sudoku is often used as a constraint programming example. Our example is 4x4 Sudoku, but the same ideas can be applied to any sudoku and solved quickly including 9x9, 16x16 etc. Transitions are unnecessary for the Sudoku problem so we do not state a Start or End and instead use Board as the object for Req Board to specify what symbols we know. ? is used for the symbols we do not know.

To make the constraint "all different" we can use AllDif. Using this as shown would require the board cells a, b, c, and d to be different symbols.

AllDif { a b c d }

We can see what the completed source for our 4x4 puzzle would look like below.

Sym{ 1 2 3 4 }

Board{

a0 a1 a2 a3;
b0 b1 b2 b3;
c0 c1 c2 c3;
d0 d1 d2 d3;

}
Req Board{

3 ? ? ?;
? ? ? 3;
? 1 ? ?;
? ? ? 2;

}

# row
AllDif{ a0 a1 a2 a3 }
AllDif{ b0 b1 b2 b3 }
AllDif{ c0 c1 c2 c3 }
AllDif{ d0 d1 d2 d3 }

# column
AllDif{ a0 b0 c0 d0 }
AllDif{ a1 b1 c1 d1 }
AllDif{ a2 b2 c2 d2 }
AllDif{ a3 b3 c3 d3 }

# block
AllDif{ a0 a1 b0 b1 }
AllDif{ a2 a3 b2 b3 }
AllDif{ c0 c1 d0 d1 }
AllDif{ c2 c3 d2 d3 }

Although SABR is designed to have a close mapping to the underlying Conjunction Normal Form (CNF), we can use code generators to express our problem more succinctly, as we will see in later examples.

source | solution