More Samples
///////////////////////////////////////////////////////////////////////////////
//
// 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

">2)*9+col+1),s((row+2)*9+col+2)] // Set constraints a column: all elements are different local pred DiffCols(s::SUDOKUTYPE, col:<I) iff sg::ATYPE & sg = [ s(col), s(col+9), s(col+2*9), s(col+3*9), s(col+4*9),s(col+5*9),s(col+6*9), s(col+7*9), s(col+8*9)] // Set constraints for a row: all elements are different local pred DiffRows(s::SUDOKUTYPE, row:<I) iff sg::ATYPE & sg = [ s(row*9), s(row*9+1),s(row*9+2), s(row*9+3), s(row*9+4),s(row*9+5),s(row*9+6), s(row*9+7), s(row*9+8)] /////////////////////////////////////////////////////////////////////////////// // // Formatted printout of the results. // /////////////////////////////////////////////////////////////////////////////// local proc PrettyPrint(x:<SUDOKUTYPE,elem:<I,row:<I) iff if row = 0 then Print ('\n') end & if row mod 3 = 0 then Print('\n +-----+-----+-----+') end & if row < 9 then Print('\n') & PrettyPrintColumns(x,elem,0) & PrettyPrint(x,elem+9,row+1) end local proc PrettyPrintColumns(x:<SUDOKUTYPE,elem:<I,col:<I) iff if col mod 3 = 0 then Print(' | ') end & if col < 9 then Print(x(elem+col)) & PrettyPrintColumns(x,elem,col+1) end

This page was created by F1toHTML