librarygames/sudoku/SudokuGrid.xtl
Sudoku's rules and a solver, a library: sudoku.xtl (scripted), play.xtl (at the terminal) and the web page all use these. (Named SudokuGrid because a disk that ignores case cannot hold both Sudoku.xtl and sudoku.xtl.) A grid is a vector of 81 digits, row by row, 0 an empty cell. A game's state is the puzzle's givens (81), then the grid as filled so far (81).
ˡu̲nits : Unit -> Int
The 27 units (9 rows, 9 columns, 9 boxes) as a 27 by 9 table of the cells (from 1) in each.
ˡu̲nits ← { @ → 1 + ((9 × j) '+ t̲able j) c̲at (j '+ t̲able 9 × j) c̲at ((27 × j d̲iv 3) + 3 × j m̲od 3) '+ t̲able (9 × j d̲iv 3) + j m̲od 3 }
ˡh̲omes : Unit -> Int
The other way round: each cell's three units (from 1), its row's, its column's and its box's, as a 3 by 81 table.
ˡh̲omes ← { @ → 3 81 r̲eshape 1 + (cell d̲iv 9) c̲at (9 + cell m̲od 9) c̲at 18 + (3 × cell d̲iv 27) + (cell m̲od 9) d̲iv 3 }
ˡo̲nehot : (Num a, Truthy a) => Int -> a
The digits placed, one-hot: 81 by 9, a 1 at each filled cell's digit.
ˡo̲nehot ← { g → 0 + g '= t̲able r̲ange 9 }
ˡp̲erUnit : Num a => a -> a
How many times each digit appears in each unit, all 27 at once: the unit table selects its cells' rows of m (27 by 9 by 9), summed over the 9 cells.
ˡp̲erUnit ← { m → '+ r̲/₂ (ˡu̲nits @) s̲elect m }
ˡp̲erCell : Num a => a -> a
Back to the cells: each cell's sum of its three units' rows of t (27 by 9 in, 81 by 9 out).
ˡp̲erCell ← { t → h ← ˡh̲omes @ ((1 s̲elect h) s̲elect t) + ((2 s̲elect h) s̲elect t) + (3 s̲elect h) s̲elect t }
ˡc̲andidates : (Num a, Truthy a) => Int -> a
The candidates, 81 by 9: a digit is open in an empty cell when none of the cell's units holds it yet; a filled cell keeps its digit.
ˡc̲andidates ← { g → f ← ˡo̲nehot g open ← (g = 0) '× t̲able 9 r̲eshape 1 0 + (0 < f) ∨ (0 < open) ∧ 0 = ˡp̲erCell ˡp̲erUnit f }
ˡs̲ingles : (Num a, Num b, Num c, Truthy c) => a -> b -> c
The singles of grid g with candidates c, one-hot (81 by 9): a naked single is an empty cell with one candidate left; a hidden single a digit with only one place left in one of the cell's units.
ˡs̲ingles ← { g c → empty ← 0 < (g = 0) '× t̲able 9 r̲eshape 1 naked ← (0 < c) ∧ (1 = '+ r̲/₂ c) '× t̲able 9 r̲eshape 1 hidden ← (0 < c) ∧ 0 < ˡp̲erCell 0 + 1 = ˡp̲erUnit c 0 + empty ∧ naked ∨ hidden }
ˡr̲ound : Int -> Int
One round: every single filled at once. A cell given two digits at once means the grid has no solution: -1 in every cell.
ˡr̲ound ← { g → s ← g ˡs̲ingles ˡc̲andidates g 1 < 'm̲ax r̲/ '+ r̲/₂ s ? 81 r̲eshape -1 g + '+ r̲/₂ s × 81 9 r̲eshape r̲ange 9 }
ˡp̲ropagate : Int -> Int
Rounds until nothing changes (or a contradiction).
ˡp̲ropagate ← { g → h ← ˡr̲ound g h m̲atch g ? g 0 > 'm̲in r̲/ h ? h ˡp̲ropagate h }
ˡb̲roken : (Num a, Num b, Truthy b) => Int -> a -> b
1 when grid g (candidates c) cannot be completed: a contradiction marked, a digit twice in a unit, or an empty cell with no candidate.
ˡb̲roken ← { g c → 0 > 'm̲in r̲/ g ? 1 1 < 'm̲ax r̲/ r̲avel ˡp̲erUnit ˡo̲nehot g ? 1 0 < '+ r̲/ 0 + (g = 0) ∧ 0 = '+ r̲/₂ c }
ˡs̲olve : Int -> Int
The solution of grid g (-1 in every cell when there is none): propagation, then a guess in the cell with the fewest candidates, each candidate in turn, each guess propagated again.
ˡs̲olve ← { g → h ← ˡp̲ropagate g c ← ˡc̲andidates h h ˡb̲roken c ? 81 r̲eshape -1 0 = '+ r̲/ 0 + h = 0 ? h k ← f̲irst g̲rade ('+ r̲/₂ c) + 10 × h ≠ 0 h ˡt̲ry k c̲at w̲here k s̲elect c }
ˡt̲ry : Int -> Int -> Int
Guessing: kd is the cell and the digits still to try there.
ˡt̲ry ← { g kd → 2 > t̲ally kd ? 81 r̲eshape -1 r ← ˡs̲olve g + (2 s̲elect kd) × (f̲irst kd) = r̲ange 81 0 > 'm̲in r̲/ r ? g ˡt̲ry (f̲irst kd) c̲at 2 d̲rop kd◆ r }
ˡr̲ounds : Num a => Int -> a
How many rounds propagation takes on grid g.
ˡr̲ounds ← { g → h ← ˡr̲ound g (h m̲atch g) ∨ 0 > 'm̲in r̲/ h ? 0 1 + ˡr̲ounds h }
The game
wikipedia : Int
The puzzles: Wikipedia's example; one with 17 givens, the fewest a sudoku with one solution can have; two that singles alone cannot finish (Peter Norvig's first hard one, and Arto Inkala's, called the hardest in 2012).
wikipedia ← 5 3 0 0 7 0 0 0 0 6 0 0 1 9 5 0 0 0 0 9 8 0 0 0 0 6 0 8 0 0 0 6 0 0 0 3 4 0 0 8 0 3 0 0 1 7 0 0 0 2 0 0 0 6 0 6 0 0 0 0 2 8 0 0 0 0 4 1 9 0 0 5 0 0 0 0 8 0 0 7 9
seventeen : Int
seventeen ← 0 0 0 0 0 0 0 1 0 4 0 0 0 0 0 0 0 0 0 2 0 0 0 0 0 0 0 0 0 0 0 5 0 4 0 7 0 0 8 0 0 0 3 0 0 0 0 1 0 9 0 0 0 0 3 0 0 4 0 0 2 0 0 0 5 0 1 0 0 0 0 0 0 0 0 8 0 6 0 0 0
norvig : Int
norvig ← 4 0 0 0 0 0 8 0 5 0 3 0 0 0 0 0 0 0 0 0 0 7 0 0 0 0 0 0 2 0 0 0 0 0 6 0 0 0 0 0 8 0 4 0 0 0 0 0 0 1 0 0 0 0 0 0 0 6 0 3 0 7 0 5 0 0 2 0 0 0 0 0 1 0 4 0 0 0 0 0 0
inkala : Int
inkala ← 8 0 0 0 0 0 0 0 0 0 0 3 6 0 0 0 0 0 0 7 0 0 9 0 2 0 0 0 5 0 0 0 7 0 0 0 0 0 0 0 4 5 7 0 0 0 0 0 1 0 0 0 3 0 0 0 1 0 0 0 0 6 8 0 0 8 5 0 0 0 1 0 0 9 0 0 0 0 4 0 0
ˡp̲uzzles : Unit -> Int
The puzzles, easiest first, one per row (81 digits).
ˡp̲uzzles ← { @ → 4 81 r̲eshape wikipedia c̲at seventeen c̲at norvig c̲at inkala }
ˡn̲ew : Int -> Int
A new game on puzzle n (1 to 4): the givens, and the grid so far.
ˡn̲ew ← { n → g ← n s̲elect ˡp̲uzzles @ g c̲at g }
ˡw̲hy : Num a => Int -> Int -> a
Why digit d cannot go at row r, column c (rcd is r c d; d 0 clears the cell): 0 it can, 1 off the board, 2 a given, 3 a peer holds d.
ˡw̲hy ← { s rcd → (0 < 'm̲in r̲/ 2 t̲ake rcd) ∧ (9 ≥ 'm̲ax r̲/ 2 t̲ake rcd) ∧ (0 ≤ 3 s̲elect rcd) ∧ 9 ≥ 3 s̲elect rcd ? s ˡc̲lash rcd◆ 1 }
ˡc̲lash : Num a => Int -> Int -> a
Why digit d cannot go at row r, column c, given that rcd is on the board: 0 it can, 2 a given, 3 a peer holds d.
ˡc̲lash ← { s rcd → k ← 1 + (9 × (f̲irst rcd) − 1) + (2 s̲elect rcd) − 1 0 < k s̲elect ˡg̲ivens s ? 2 d ← 3 s̲elect rcd g ← (ˡg̲rid s) × k ≠ r̲ange 81 (d = 0) ∨ d m̲ember? w̲here k s̲elect ˡc̲andidates g ? 0◆ 3 }
ˡm̲ove : Int -> Int -> Int
Digit d at row r, column c (d 0 clears it), when it may go there.
ˡm̲ove ← { s rcd → 0 < s ˡw̲hy rcd ? s k ← 1 + (9 × (f̲irst rcd) − 1) + (2 s̲elect rcd) − 1 (ˡg̲ivens s) c̲at ((ˡg̲rid s) × k ≠ r̲ange 81) + (3 s̲elect rcd) × k = r̲ange 81 }
ˡl̲egal : (Num a, Truthy a) => Int -> a
The candidates of the grid so far, 81 by 9.
ˡl̲egal ← { s → ˡc̲andidates ˡg̲rid s }
ˡs̲tatus : (Num a, Truthy a) => Int -> a
1 solved, else 0 (playing).
ˡs̲tatus ← { s → 0 + (0 = '+ r̲/ 0 + 0 = ˡg̲rid s) ∧ n̲ot (ˡg̲rid s) ˡb̲roken ˡl̲egal s }
ˡh̲int : Int -> Int
A hint, as row, column and digit: the first single of the grid so far, else the first empty cell's digit in the solution; 0 0 0 when the grid so far has no solution (a digit placed wrong).
ˡh̲int ← { s → g ← ˡg̲rid s x ← ˡs̲olve g 0 > 'm̲in r̲/ x ? 0 0 0 one ← w̲here 0 < '+ r̲/₂ g ˡs̲ingles ˡc̲andidates g k ← f̲irst one c̲at w̲here g = 0 (1 + (k − 1) d̲iv 9) c̲at (1 + (k − 1) m̲od 9) c̲at k s̲elect x }
ˡs̲hown : Int -> Char
A grid as text: digits, . for an empty cell, the boxes ruled off.
ˡs̲hown ← { g → m ← (9 9 r̲eshape (1 + g) s̲elect ".123456789") c̲at₂ 9 2 r̲eshape " |" r ← 1 10 2 10 3 10 11 10 4 10 5 10 6 10 11 10 7 10 8 10 9 s̲elect₂ m 1 2 3 10 4 5 6 10 7 8 9 s̲elect r c̲at 1 21 r̲eshape "------+-------+------" }