SudokuGrid.xtl

1⍝# Sudoku's rules and a solver, a library: sudoku.xtl (scripted),
2⍝# play.xtl (at the terminal) and the web page all use these. (Named
3⍝# SudokuGrid because a disk that ignores case cannot hold both
4⍝# Sudoku.xtl and sudoku.xtl.) A grid is a vector of 81 digits, row by
5⍝# row, 0 an empty cell. A game's state is the puzzle's givens (81),
6⍝# then the grid as filled so far (81).
7
8j ← (r̲ange 9) − 1
9cell ← (r̲ange 81) − 1
10
11⍝ :: Unit -> Int
12⍝# The 27 units (9 rows, 9 columns, 9 boxes) as a 27 by 9 table of the
13⍝# cells (from 1) in each.
14ˡ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 }
15⍝ :: Unit -> Int
16⍝# The other way round: each cell's three units (from 1), its row's,
17⍝# its column's and its box's, as a 3 by 81 table.
18ˡ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 }
19
20⍝ :: (Num a, Truthy a) => Int -> a
21⍝# The digits placed, one-hot: 81 by 9, a 1 at each filled cell's digit.
22ˡo̲nehot ← { g → 0 + g '= t̲able r̲ange 9 }
23⍝ :: Num a => a -> a
24⍝# How many times each digit appears in each unit, all 27 at once: the
25⍝# unit table selects its cells' rows of m (27 by 9 by 9), summed over
26⍝# the 9 cells.
27ˡp̲erUnit ← { m → '+ r̲/₂ (ˡu̲nits @) s̲elect m }
28⍝ :: Num a => a -> a
29⍝# Back to the cells: each cell's sum of its three units' rows of t
30⍝# (27 by 9 in, 81 by 9 out).
31ˡp̲erCell ← { t →
32  h ← ˡh̲omes @
33  ((1 s̲elect h) s̲elect t) + ((2 s̲elect h) s̲elect t) + (3 s̲elect h) s̲elect t
34}
35⍝ :: (Num a, Truthy a) => Int -> a
36⍝# The candidates, 81 by 9: a digit is open in an empty cell when none
37⍝# of the cell's units holds it yet; a filled cell keeps its digit.
38ˡc̲andidates ← { g →
39  f ← ˡo̲nehot g
40  open ← (g = 0) '× t̲able 9 r̲eshape 1
41  0 + (0 < f) ∨ (0 < open) ∧ 0 = ˡp̲erCell ˡp̲erUnit f
42}
43⍝ :: (Num a, Num b, Num c, Truthy c) => a -> b -> c
44⍝# The singles of grid g with candidates c, one-hot (81 by 9): a naked
45⍝# single is an empty cell with one candidate left; a hidden single a
46⍝# digit with only one place left in one of the cell's units.
47ˡs̲ingles ← { g c →
48  empty ← 0 < (g = 0) '× t̲able 9 r̲eshape 1
49  naked ← (0 < c) ∧ (1 = '+ r̲/₂ c) '× t̲able 9 r̲eshape 1
50  hidden ← (0 < c) ∧ 0 < ˡp̲erCell 0 + 1 = ˡp̲erUnit c
51  0 + empty ∧ naked ∨ hidden
52}
53⍝ :: Int -> Int
54⍝# One round: every single filled at once. A cell given two digits at
55⍝# once means the grid has no solution: -1 in every cell.
56ˡr̲ound ← { g →
57  s ← g ˡs̲ingles ˡc̲andidates g
58  1 < 'm̲ax r̲/ '+ r̲/₂ s ? 81 r̲eshape -1
59  g + '+ r̲/₂ s × 81 9 r̲eshape r̲ange 9
60}
61⍝ :: Int -> Int
62⍝# Rounds until nothing changes (or a contradiction).
63ˡp̲ropagate ← { g →
64  h ← ˡr̲ound g
65  h m̲atch g ? g
66  0 > 'm̲in r̲/ h ? h
67  ˡp̲ropagate h
68}
69⍝ :: (Num a, Num b, Truthy b) => Int -> a -> b
70⍝# 1 when grid g (candidates c) cannot be completed: a contradiction
71⍝# marked, a digit twice in a unit, or an empty cell with no candidate.
72ˡb̲roken ← { g c →
73  0 > 'm̲in r̲/ g ? 1
74  1 < 'm̲ax r̲/ r̲avel ˡp̲erUnit ˡo̲nehot g ? 1
75  0 < '+ r̲/ 0 + (g = 0) ∧ 0 = '+ r̲/₂ c
76}
77⍝ :: Int -> Int
78⍝# The solution of grid g (-1 in every cell when there is none):
79⍝# propagation, then a guess in the cell with the fewest candidates,
80⍝# each candidate in turn, each guess propagated again.
81ˡs̲olve ← { g →
82  h ← ˡp̲ropagate g
83  c ← ˡc̲andidates h
84  h ˡb̲roken c ? 81 r̲eshape -1
85  0 = '+ r̲/ 0 + h = 0 ? h
86  k ← f̲irst g̲rade ('+ r̲/₂ c) + 10 × h ≠ 0
87  h ˡt̲ry k c̲at w̲here k s̲elect c
88}
89⍝ :: Int -> Int -> Int
90⍝# Guessing: kd is the cell and the digits still to try there.
91ˡt̲ry ← { g kd →
92  2 > t̲ally kd ? 81 r̲eshape -1
93  r ← ˡs̲olve g + (2 s̲elect kd) × (f̲irst kd) = r̲ange 81
94  0 > 'm̲in r̲/ r ? g ˡt̲ry (f̲irst kd) c̲at 2 d̲rop kd◆ r
95}
96⍝ :: Num a => Int -> a
97⍝# How many rounds propagation takes on grid g.
98ˡr̲ounds ← { g →
99  h ← ˡr̲ound g
100  (h m̲atch g) ∨ 0 > 'm̲in r̲/ h ? 0
101  1 + ˡr̲ounds h
102}
103
104⍝## The game
105
106⍝# The puzzles: Wikipedia's example; one with 17 givens, the fewest a
107⍝# sudoku with one solution can have; two that singles alone cannot
108⍝# finish (Peter Norvig's first hard one, and Arto Inkala's, called the
109⍝# hardest in 2012).
110wikipedia ← 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
111seventeen ← 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
112norvig ← 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
113inkala ← 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
114⍝ :: Unit -> Int
115⍝# The puzzles, easiest first, one per row (81 digits).
116ˡp̲uzzles ← { @ → 4 81 r̲eshape wikipedia c̲at seventeen c̲at norvig c̲at inkala }
117⍝ :: Int -> Int
118⍝# A new game on puzzle n (1 to 4): the givens, and the grid so far.
119ˡn̲ew ← { n →
120  g ← n s̲elect ˡp̲uzzles @
121  g c̲at g
122}
123⍝ :: a -> a
124⍝# The puzzle's givens (81 digits, 0 an empty cell).
125ˡg̲ivens ← { s → 81 t̲ake s }
126⍝ :: a -> a
127⍝# The grid as filled so far (81 digits).
128ˡg̲rid ← { s → 81 d̲rop s }
129⍝ :: Num a => Int -> Int -> a
130⍝# Why digit d cannot go at row r, column c (rcd is r c d; d 0 clears
131⍝# the cell): 0 it can, 1 off the board, 2 a given, 3 a peer holds d.
132ˡw̲hy ← { s rcd →
133  (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
134}
135⍝ :: Num a => Int -> Int -> a
136⍝# 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.
137ˡc̲lash ← { s rcd →
138  k ← 1 + (9 × (f̲irst rcd) − 1) + (2 s̲elect rcd) − 1
139  0 < k s̲elect ˡg̲ivens s ? 2
140  d ← 3 s̲elect rcd
141  g ← (ˡg̲rid s) × k ≠ r̲ange 81
142  (d = 0) ∨ d m̲ember? w̲here k s̲elect ˡc̲andidates g ? 0◆ 3
143}
144⍝ :: Int -> Int -> Int
145⍝# Digit d at row r, column c (d 0 clears it), when it may go there.
146ˡm̲ove ← { s rcd →
147  0 < s ˡw̲hy rcd ? s
148  k ← 1 + (9 × (f̲irst rcd) − 1) + (2 s̲elect rcd) − 1
149  (ˡg̲ivens s) c̲at ((ˡg̲rid s) × k ≠ r̲ange 81) + (3 s̲elect rcd) × k = r̲ange 81
150}
151⍝ :: (Num a, Truthy a) => Int -> a
152⍝# The candidates of the grid so far, 81 by 9.
153ˡl̲egal ← { s → ˡc̲andidates ˡg̲rid s }
154⍝ :: (Num a, Truthy a) => Int -> a
155⍝# 1 solved, else 0 (playing).
156ˡs̲tatus ← { s → 0 + (0 = '+ r̲/ 0 + 0 = ˡg̲rid s) ∧ n̲ot (ˡg̲rid s) ˡb̲roken ˡl̲egal s }
157⍝ :: Int -> Int
158⍝# A hint, as row, column and digit: the first single of the grid so
159⍝# far, else the first empty cell's digit in the solution; 0 0 0 when
160⍝# the grid so far has no solution (a digit placed wrong).
161ˡh̲int ← { s →
162  g ← ˡg̲rid s
163  x ← ˡs̲olve g
164  0 > 'm̲in r̲/ x ? 0 0 0
165  one ← w̲here 0 < '+ r̲/₂ g ˡs̲ingles ˡc̲andidates g
166  k ← f̲irst one c̲at w̲here g = 0
167  (1 + (k − 1) d̲iv 9) c̲at (1 + (k − 1) m̲od 9) c̲at k s̲elect x
168}
169⍝ :: Int -> Char
170⍝# A grid as text: digits, . for an empty cell, the boxes ruled off.
171ˡs̲hown ← { g →
172  m ← (9 9 r̲eshape (1 + g) s̲elect ".123456789") c̲at₂ 9 2 r̲eshape " |"
173  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
174  1 2 3 10 4 5 6 10 7 8 9 s̲elect r c̲at 1 21 r̲eshape "------+-------+------"
175}
176⍝ :: Int -> Char
177⍝# The game's grid so far.
178ˡv̲iew ← { s → ˡs̲hown ˡg̲rid s }