```///////////////////////////////////////////////////////////////////////////////
//
// SUDOKU
//
// The puzzle was invented in Basel, Switzerland, by 18th century matematician
// Leonhard Euler. Euler called his puzzle "Magic Squares", it became
// "Sudoku" ("single number" in Japanese) in the 1980s. The puzzle comes in
// several variants, the most common being a square grid nine by nine, consisting
// of nine sub-grids 3x3. This variant is often referred to as Sudoku 3x3.
// There are numerous Sudoku web sites dealing with history, solving strategies
// and posting new puzzles. Puzzles are often rated by their difficulty.
//
// The rules: Fill the grid with numbers so that each column, each row
// and each each tree by three grid of nine squares contains the numbers
// one to nine. No column, row or grid can have two of the same numbers.
//
// Solving:
// The code in the predicate Sudoku3x3 will solve any Sudoku problem. It is
// an ideal problem for declarative programming: all the code does is transcribe
// the rules above in the syntax of the F1 language.
// Before calling the predicate Sudoku3x3, set some of the elements of the
// Sudoku3x3 9x9 array to some initial values. This is illustrated in the
// predicate Sudoku below.
//
// To execute the program, issue the query
//
//      all Sudoku
//
// For the initial values in the predicate Sudoku, the following result will be
// generated:
//
// +-----+-----+-----+
// | 295 | 743 | 861 |
// | 431 | 865 | 927 |
// | 876 | 192 | 543 |
// +-----+-----+-----+
// | 387 | 459 | 216 |
// | 612 | 387 | 495 |
// | 549 | 216 | 738 |
// +-----+-----+-----+
// | 763 | 524 | 189 |
// | 928 | 671 | 354 |
// | 154 | 938 | 672 |
// +-----+-----+-----+
//
// Final note: The code will find all solutions, therefore can be easily used
// to generate new Sudoku puzzles: simply start with any partially filled grid,
// generate all solution, and keep filling the grid with more numbers until
// the puzzle has a single solution.
//
//
///////////////////////////////////////////////////////////////////////////////

///////////////////////////////////////////////////////////////////////////////
//
// Sudoku
//
// Set the initial Sudoku numbers and let the predicate Sudoku3x3 generate
// the rest of the grid.
//
///////////////////////////////////////////////////////////////////////////////
pred Sudoku() iff
s::[0..8]->[0..8]->>L[1..9] &

s = [ [_,9,_, 7,_,_, 8,6,_],
[_,3,1, _,_,5, _,2,_],
[8,_,6, _,_,_, _,_,_],
[_,_,7, _,5,_, _,_,6],
[_,_,_, 3,_,7, _,_,_],
[5,_,_, _,1,_, 7,_,_],
[_,_,_, _,_,_, 1,_,9],
[_,2,_, 6,_,_, 3,5,_],
[_,5,4, _,_,8, _,7,_]] &

Sudoku3x3(s) & PrettyPrint(s,0)

///////////////////////////////////////////////////////////////////////////////
//
// Sudoku3x3
//
// This is the predicate that solves the Sudoku problem. All that needs to be
// done is to set constraints (relations) between the 9x9 grid elements based on
// the Sudoku rules. In the code below, for the grid used is a logical array
// of 9x9 elements, each element being a number of 1..9.
//
// Note the logical array "s" already guarantees all elements
// of each row are different numbers 1..9, as "s" is defined as
//
//      s::[0..8]->[0..8]->>L[1..9]  (note the ->> )
//
// Had "s" been declared as an ordinary array
//
//      s::[0..8]->[0..8]->L[1..9]
//
// the constraints would have to be explicitly set guaranteeing all row elements
// are different. (The arrays with all elements different are referred to as
// "injections")
//
// So all that needs to be done is explicitly set constraints for elements of
// each column and the elements of each 3x3 sub-grid. This is done by simply
// declaring some additional "injections" composed of elements of the array "s"
//
///////////////////////////////////////////////////////////////////////////////

pred Sudoku3x3(s::[0..8]->[0..8]->>L[1..9]) iff

// Set constraints guaranteeing each column contains numbers that are all different.
c0::[0..8]->>L & c0 = [s(0,0),s(1,0),s(2,0),s(3,0),s(4,0),s(5,0),s(6,0),s(7,0),s(8,0)] &
c1::[0..8]->>L & c1 = [s(0,1),s(1,1),s(2,1),s(3,1),s(4,1),s(5,1),s(6,1),s(7,1),s(8,1)] &
c2::[0..8]->>L & c2 = [s(0,2),s(1,2),s(2,2),s(3,2),s(4,2),s(5,2),s(6,2),s(7,2),s(8,2)] &
c3::[0..8]->>L & c3 = [s(0,3),s(1,3),s(2,3),s(3,3),s(4,3),s(5,3),s(6,3),s(7,3),s(8,3)] &
c4::[0..8]->>L & c4 = [s(0,4),s(1,4),s(2,4),s(3,4),s(4,4),s(5,4),s(6,4),s(7,4),s(8,4)] &
c5::[0..8]->>L & c5 = [s(0,5),s(1,5),s(2,5),s(3,5),s(4,5),s(5,5),s(6,5),s(7,5),s(8,5)] &
c6::[0..8]->>L & c6 = [s(0,6),s(1,6),s(2,6),s(3,6),s(4,6),s(5,6),s(6,6),s(7,6),s(8,6)] &
c7::[0..8]->>L & c7 = [s(0,7),s(1,7),s(2,7),s(3,7),s(4,7),s(5,7),s(6,7),s(7,7),s(8,7)] &
c8::[0..8]->>L & c8 = [s(0,8),s(1,8),s(2,8),s(3,8),s(4,8),s(5,8),s(6,8),s(7,8),s(8,8)] &

// Set constraints guaranteeing each sub-grids 3x3 contains numbers that are all different.
s0::[0..8]->>L & s0 = [s(0,0),s(0,1),s(0,2),s(1,0),s(1,1),s(1,2),s(2,0),s(2,1),s(2,2)] &
s1::[0..8]->>L & s1 = [s(0,3),s(0,4),s(0,5),s(1,3),s(1,4),s(1,5),s(2,3),s(2,4),s(2,5)] &
s2::[0..8]->>L & s2 = [s(0,6),s(0,7),s(0,8),s(1,6),s(1,7),s(1,8),s(2,6),s(2,7),s(2,8)] &
s3::[0..8]->>L & s3 = [s(3,0),s(3,1),s(3,2),s(4,0),s(4,1),s(4,2),s(5,0),s(5,1),s(5,2)] &
s4::[0..8]->>L & s4 = [s(3,3),s(3,4),s(3,5),s(4,3),s(4,4),s(4,5),s(5,3),s(5,4),s(5,5)] &
s5::[0..8]->>L & s5 = [s(3,6),s(3,7),s(3,8),s(4,6),s(4,7),s(4,8),s(5,6),s(5,7),s(5,8)] &
s6::[0..8]->>L & s6 = [s(6,0),s(6,1),s(6,2),s(7,0),s(7,1),s(7,2),s(8,0),s(8,1),s(8,2)] &
s7::[0..8]->>L & s7 = [s(6,3),s(6,4),s(6,5),s(7,3),s(7,4),s(7,5),s(8,3),s(8,4),s(8,5)] &
s8::[0..8]->>L & s8 = [s(6,6),s(6,7),s(6,8),s(7,6),s(7,7),s(7,8),s(8,6),s(8,7),s(8,8)]

local proc PrettyPrint(x:<[0..8]->[0..8]->L[1..9],row:<I) iff
if row = 0 then Print ('\n') end &
if row mod 3 = 0 then
Print('\n +-----+-----+-----+')
end &
if row < Len(x) then
Print('\n') &
PrettyPrintColumns(x(row),0) & PrettyPrint(x,row+1)
end

local proc PrettyPrintColumns(x:<[0..8]->L,col:<I) iff
if col mod 3 = 0 then
Print(' | ')
end &
if col < Len(x) then
Print(x(col)) & PrettyPrintColumns(x,col+1)
end

```