Sudoku

From The Twelf Project
Jump to: navigation, search
Example Sudoku puzzle

In the Sudoku puzzle, a 9x9 board must be filled with the numbers such that no row, column, or box contains the same digit twice.

This article or section needs to be completed.

% Sudoku solver, brute force

cell : type.
1 : cell.
2 : cell.
3 : cell.
4 : cell.
5 : cell.
6 : cell.
7 : cell.
8 : cell.
9 : cell.

nat : type.
z : nat.
s : nat -> nat. %prefix 5 s.
nine = s s s  s s s  s s s z.

cells : nat -> type.
//  : cell -> cells N -> cells (s N).
%infix right 5 //.
nil : cells z.

cellss : nat -> type.
///  : cells nine -> cellss N -> cellss (s N).
%infix right 4 ///.
nill : cellss z.

remove : cells (s N) -> cell -> cells N -> type.
%mode remove +L +C -L'.

rem-hit  : remove (X // C) X C.
% okay that we can also skip this one
rem-miss : remove (X // C) Y (X // C')
        <- remove C Y C'.

%worlds () (remove _ _ _).
%terminates D (remove D _ _).

nodups : cells X -> cells Y -> type.
%mode nodups +OK +L.

nd-nil  : nodups _ nil.
nd-hit  : nodups OK (X // C)
       <- remove OK X OK'
       <- nodups OK' C.

%worlds () (nodups _ _).
%terminates D (nodups _ D).

% valid if there are no duplicates
allcells = 1 // 2 // 3 //
           4 // 5 // 6 //
           7 // 8 // 9 // nil.

unitok : cells nine -> type.

uo : unitok C
  <- nodups allcells C.

% the nine rows
%abbrev board = cellss nine.

% extract three boxes from three rows
boxes : cells nine -> cells nine -> cells nine ->
        cells nine -> cells nine -> cells nine -> type.
%mode boxes +A +B +C -A' -B' -C'.

b : boxes
      (A1 // B1 // C1  //  D1 // E1 // F1  //  G1 // H1 // I1  //  nil)
      (A2 // B2 // C2  //  D2 // E2 // F2  //  G2 // H2 // I2  //  nil)
      (A3 // B3 // C3  //  D3 // E3 // F3  //  G3 // H3 // I3  //  nil)
%
      (A1 // B1 // C1 //
       A2 // B2 // C2 //
       A3 // B3 // C3 // nil)
%
      (D1 // E1 // F1 //
       D2 // E2 // F2 //
       D3 // E3 // F3 // nil)
%
      (G1 // H1 // I1 //
       G2 // H2 // I2 //
       G3 // H3 // I3 // nil).

%worlds () (boxes _ _ _  _ _ _).
%total {} (boxes _ _ _  _ _ _).

% transpose a whole board
transpose : board -> board -> type.
%mode transpose +B -B'.

tr : transpose ((A1 // B1 // C1 // D1 // E1 // F1 // G1 // H1 // I1 // nil) ///
                (A2 // B2 // C2 // D2 // E2 // F2 // G2 // H2 // I2 // nil) ///
                (A3 // B3 // C3 // D3 // E3 // F3 // G3 // H3 // I3 // nil) ///
                (A4 // B4 // C4 // D4 // E4 // F4 // G4 // H4 // I4 // nil) ///
                (A5 // B5 // C5 // D5 // E5 // F5 // G5 // H5 // I5 // nil) ///
                (A6 // B6 // C6 // D6 // E6 // F6 // G6 // H6 // I6 // nil) ///
                (A7 // B7 // C7 // D7 // E7 // F7 // G7 // H7 // I7 // nil) ///
                (A8 // B8 // C8 // D8 // E8 // F8 // G8 // H8 // I8 // nil) ///
                (A9 // B9 // C9 // D9 // E9 // F9 // G9 // H9 // I9 // nil) /// nill)
%
               ((A1 // A2 // A3 // A4 // A5 // A6 // A7 // A8 // A9 // nil) ///
                (B1 // B2 // B3 // B4 // B5 // B6 // B7 // B8 // B9 // nil) ///
                (C1 // C2 // C3 // C4 // C5 // C6 // C7 // C8 // C9 // nil) ///
                (D1 // D2 // D3 // D4 // D5 // D6 // D7 // D8 // D9 // nil) ///
                (E1 // E2 // E3 // E4 // E5 // E6 // E7 // E8 // E9 // nil) ///
                (F1 // F2 // F3 // F4 // F5 // F6 // F7 // F8 // F9 // nil) ///
                (G1 // G2 // G3 // G4 // G5 // G6 // G7 // G8 // G9 // nil) ///
                (H1 // H2 // H3 // H4 // H5 // H6 // H7 // H8 // H9 // nil) ///
                (I1 // I2 // I3 // I4 // I5 // I6 // I7 // I8 // I9 // nil) /// nill).
%worlds () (transpose _ _).
%total {} (transpose C _).

boardok : board -> type.

bo : boardok
     (A /// B /// C /// D /// E /// F /// G /// H /// I /// nill)
% rows
  <- unitok A <- unitok B <- unitok C
  <- unitok D <- unitok E <- unitok F
  <- unitok G <- unitok H <- unitok I
% boxes
  <- boxes A B C  Ab Bb Cb
  <- unitok Ab <- unitok Bb <- unitok Cb
  <- boxes D E F  Db Eb Fb
  <- unitok Da <- unitok Ea <- unitok Fa
  <- boxes G H I  Gb Hb Ib
  <- unitok Gb <- unitok Hb <- unitok Ib
% cols
  <- transpose (A  /// B  /// C  /// D  /// E  /// F  /// G  /// H  /// I  /// nill)
               (At /// Bt /// Ct /// Dt /// Et /// Ft /// Gt /// Ht /// It /// nill)
  <- unitok At <- unitok Bt <- unitok Ct
  <- unitok Dt <- unitok Et <- unitok Ft
  <- unitok Gt <- unitok Ht <- unitok It.

%solve _ : boardok
(
(8 // 2 // 6  //  7 // 1 // 4  //  9 // 5 // 3  // nil) ///
(3 // 4 // 5  //  8 // 6 // 9  //  2 // 1 // 7  // nil) ///
(9 // 7 // 1  //  2 // 5 // 3  //  4 // 8 // 6  // nil) ///

(1 // 6 // 3  //  9 // 2 // 5  //  7 // 4 // 8  // nil) ///
(5 // 9 // 4  //  6 // 7 // 8  //  1 // 3 // 2  // nil) ///
(2 // 8 // 7  //  3 // 4 // 1  //  5 // 6 // 9  // nil) ///

(7 // 5 // 9  //  4 // 3 // 6  //  8 // 2 // 1  // nil) ///
(4 // 3 // 2  //  1 // 8 // 7  //  6 // 9 // 5  // nil) ///
(6 // 1 // 8  //  5 // 9 // 2  //  3 // 7 // 4  // nil) /// nill).

%solve _ : boardok
(
(8 // 2 // 6  //  7 // 1 // 4  //  9 // 5 // 3 // nil) ///
(3 // 4 // 5  //  8 // 6 // 9  //  2 // 1 // 7  // nil) ///
(9 // 7 // 1  //  2 // 5 // 3  //  4 // 8 // 6  // nil) ///

(1 // 6 // 3  //  _ // 2 // 5  //  7 // 4 // 8  // nil) ///
(5 // 9 // 4  //  _ // 7 // 8  //  1 // 3 // 2  // nil) ///
(2 // 8 // 7  //  _ // _ // 1  //  5 // 6 // 9  // nil) ///

(7 // 5 // 9  //  4 // 3 // 6  //  8 // 2 // 1  // nil) ///
(4 // 3 // 2  //  1 // 8 // 7  //  6 // 9 // 5  // nil) ///
(6 // 1 // 8  //  5 // 9 // 2  //  3 // 7 // 4  // nil) /// nill).

All code from this tutorial. Twelf's output from this tutorial.



Read more Twelf case studies and other Twelf documentation.