/////////////////////////////////////////////////////////////////////////////// // // 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
This page was created by F1toHTML