Sudoku

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

% Sudoku solver, brute force
%sort cell %.
%term 1 cell %.
%term 2 cell %.
%term 3 cell %.
%term 4 cell %.
%term 5 cell %.
%term 6 cell %.
%term 7 cell %.
%term 8 cell %.
%term 9 cell %.
%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%prec %prefix 5 s %.
%define nine s s s s s s s s s z %.
%sort cells {_ nat} %.
%term // %pi cell %-> (cells N) %-> (cells (s N)) %.
%prec %right 5 // %.
%term nil cells z %.
%sort cellss {_ nat} %.
%term /// %pi (cells nine) %-> (cellss N) %-> (cellss (s N)) %.
%prec %right 4 /// %.
%term nill cellss z %.
%sort remove {_ cells (s N)} {_ cell} {_ cells N} %.
%mode remove %in %in %out %.
%term rem-hit remove (X // C) X C %.
% okay that we can also skip this one
%term rem-miss %pi (remove (X // C) Y (X // C')) %<- (remove C Y C') %.
%worlds () (remove _ _ _) %.
%terminates D (remove D _ _) %.
%sort nodups {_ cells X} {_ cells Y} %.
%mode nodups %in %in %.
%term nd-nil nodups _ nil %.
%term nd-hit %pi (nodups OK (X // C)) %<- (remove OK X OK') %<- (nodups OK' C) %.
%worlds () (nodups _ _) %.
%terminates D (nodups _ D) %.
% valid if there are no duplicates
%define allcells 1 // 2 // 3 // 4 // 5 // 6 // 7 // 8 // 9 // nil %.
%sort unitok {_ cells nine} %.
%term uo %pi (unitok C) %<- (nodups allcells C) %.
% the nine rows
%inline board cellss nine %.
% extract three boxes from three rows
%sort boxes {_ cells nine} {_ cells nine} {_ cells nine} {_ cells nine} {_ cells nine} {_ cells nine} %.
%mode boxes %in %in %in %out %out %out %.
%term 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
%sort transpose {_ board} {_ board} %.
%mode transpose %in %out %.
%term 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 _) %.
%sort boardok {_ board} %.
%term bo
  %pi (boardok (A /// B /// C /// D /// E /// F /// G /// H /// I /// nill))
  %<- (unitok A)
  %<- (unitok B)
  %<- (unitok C)
  %<- (unitok D)
  %<- (unitok E)
  %<- (unitok F)
  %<- (unitok G)
  %<- (unitok H)
  %<- (unitok I)
  %<- (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)
  %<- (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. check="true">STELF's output from this tutorial.

Category:STELF code