Sudoku
From The Twelf Project
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.