solver.bend

minebender-game@1.0.0.0 · 543 lines · 71 definitions

1import Base
2import minebender-game@1.0.0.0/types.bend as T
3import minebender-game@1.0.0.0/board.bend as B
4
5# The no-guess solver: finds a provably safe hidden cell, or none.
6#
7# A hidden cell c is provably safe exactly when no layout consistent with
8# what the player knows has a mine on c. For each hidden cell (row by row),
9# the solver searches for such a layout with a mine on c; the first cell
10# with none is the answer. A layout found also shows that every other cell
11# it mines is not provably safe, which saves most searches.
12#
13# The search is a depth-first walk over the hidden cells, cells next to a
14# number first. A partial layout gives each cell Some{mine} or None
15# (unassigned). After each choice, the numbers around the cell and the
16# total mine count are checked against what can still be reached; a full
17# layout is checked for consistency before it counts.
18#
19# Speed comes from the order of the walk, the standard constraint-solving
20# approach to Minesweeper: the cells linked to c through numbers first,
21# nearest first, so a contradiction near c shows up before anything far
22# away is enumerated; then each other group of linked cells in turn, so
23# backtracking never mixes unrelated groups; then the cells next to no
24# number, rotated per search so the layouts found spread their mines and
25# rule out many cells at once. The order is a heuristic: the proofs only
26# need every cell to appear, so it runs before the plain order, whose cells
27# the walk then skips as already assigned.
28
29# A revealed cell, and for a number, the cells it counts.
30type Item is Data:
31  Item{p: T.Pos, s: T.Seen, ns: List<&2, T.Pos>}
32
33# A hidden cell to assign, and the numbers around it.
34type Todo is Data:
35  Todo{c: T.Pos, rel: List<&2, Item>}
36
37type Ctx is Data:
38  Ctx{w: Nat, h: Nat, n: Nat, rows: T.Grid(T.Seen), items: List<&2, Item>}
39
40# Checking a full layout
41# ----------------------
42
43def items.put(s: T.Seen, +p: T.Pos, w: Nat, h: Nat, rest: List<&2, Item>) -> List<&2, Item>:
44  match s:
45    case T.Hidden{}:
46      rest
47    case T.Shown{k}:
48      Item{p, T.Shown{k}, B.neighbours(w, h, p)} <> rest
49    case T.Boom{}:
50      Item{p, T.Boom{}, Nil{}} <> rest
51
52# The revealed cells of ps.
53def items(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), ps: List<&2, T.Pos>) -> List<&2, Item>:
54  match ps:
55    case Nil{}:
56      Nil{}
57    case +p <> t:
58      items.put(B.at(T.Seen, T.Hidden{}, rows, p), p, w, h, items(w, h, rows, t))
59
60def item_ok(s: T.Seen, +p: T.Pos, ns: List<&2, T.Pos>, +layout: T.Grid(Bool)) -> Bool:
61  match s:
62    case T.Hidden{}:
63      True{}
64    case T.Shown{k}:
65      Bool.not(B.mine(layout, p)) && Nat.is_eq(B.count_mines(layout, ns), k)
66    case T.Boom{}:
67      B.mine(layout, p)
68
69def items_ok(its: List<&2, Item>, +layout: T.Grid(Bool)) -> Bool:
70  match its:
71    case Nil{}:
72      True{}
73    case Item{p, s, ns} <> t:
74      item_ok(s, p, ns, layout) && items_ok(t, layout)
75
76# The layout is consistent with what the player knows.
77def check(ctx: Ctx, +layout: T.Grid(Bool)) -> Bool:
78  match ctx:
79    case Ctx{+w, +h, n, rows, items}:
80      B.shaped(Bool, w, h, layout) && B.shaped(T.Seen, w, h, rows)
81        && Nat.is_eq(B.total_mines(layout), n) && items_ok(items, layout)
82
83# Partial layouts
84# ---------------
85
86def start.cell(s: T.Seen) -> Maybe<&2, Bool>:
87  match s:
88    case T.Hidden{}:
89      None{}
90    case T.Shown{k}:
91      Some{False{}}
92    case T.Boom{}:
93      Some{True{}}
94
95def start.row(r: List<&2, T.Seen>) -> List<&2, Maybe<&2, Bool>>:
96  match r:
97    case Nil{}:
98      Nil{}
99    case s <> t:
100      start.cell(s) <> start.row(t)
101
102# What the revealed cells fix: no mine under a number, one under a Boom.
103def start(rows: T.Grid(T.Seen)) -> T.Grid(Maybe<&2, Bool>):
104  match rows:
105    case Nil{}:
106      Nil{}
107    case r <> t:
108      start.row(r) <> start(t)
109
110def fill.row(r: List<&2, Maybe<&2, Bool>>) -> List<&2, Bool>:
111  match r:
112    case Nil{}:
113      Nil{}
114    case m <> t:
115      Maybe.default(&2, Bool, m, False{}) <> fill.row(t)
116
117def fill(part: T.Grid(Maybe<&2, Bool>)) -> T.Grid(Bool):
118  match part:
119    case Nil{}:
120      Nil{}
121    case r <> t:
122      fill.row(r) <> fill(t)
123
124def look(+part: T.Grid(Maybe<&2, Bool>), p: T.Pos) -> Maybe<&2, Bool>:
125  B.at(Maybe<&2, Bool>, None{}, part, p)
126
127def is_true(m: Maybe<&2, Bool>) -> Bool:
128  match m:
129    case Some{b}:
130      b
131    case None{}:
132      False{}
133
134def is_none(m: Maybe<&2, Bool>) -> Bool:
135  match m:
136    case Some{b}:
137      False{}
138    case None{}:
139      True{}
140
141def one_if(b: Bool) -> Nat:
142  Bool.pick(Nat, b, 1n, 0n)
143
144def row_true(r: List<&2, Maybe<&2, Bool>>) -> Nat:
145  match r:
146    case Nil{}:
147      0n
148    case m <> t:
149      Nat.add(one_if(is_true(m)), row_true(t))
150
151def row_none(r: List<&2, Maybe<&2, Bool>>) -> Nat:
152  match r:
153    case Nil{}:
154      0n
155    case +m <> t:
156      Nat.add(one_if(is_none(m)), row_none(t))
157
158def part_true(part: T.Grid(Maybe<&2, Bool>)) -> Nat:
159  match part:
160    case Nil{}:
161      0n
162    case r <> t:
163      Nat.add(row_true(r), part_true(t))
164
165def part_none(part: T.Grid(Maybe<&2, Bool>)) -> Nat:
166  match part:
167    case Nil{}:
168      0n
169    case r <> t:
170      Nat.add(row_none(r), part_none(t))
171
172def true_among(+part: T.Grid(Maybe<&2, Bool>), ps: List<&2, T.Pos>) -> Nat:
173  match ps:
174    case Nil{}:
175      0n
176    case q <> t:
177      Nat.add(one_if(is_true(look(part, q))), true_among(part, t))
178
179def none_among(+part: T.Grid(Maybe<&2, Bool>), ps: List<&2, T.Pos>) -> Nat:
180  match ps:
181    case Nil{}:
182      0n
183    case q <> t:
184      Nat.add(one_if(is_none(look(part, q))), none_among(part, t))
185
186# Pruning
187# -------
188
189# k is still reachable from what is fixed: t mines, f unassigned cells.
190def between(+t: Nat, +f: Nat, +k: Nat) -> Bool:
191  Nat.is_le(t, k) && Nat.is_le(k, Nat.add(t, f))
192
193def item_open(s: T.Seen, +part: T.Grid(Maybe<&2, Bool>), +ns: List<&2, T.Pos>) -> Bool:
194  match s:
195    case T.Shown{k}:
196      between(true_among(part, ns), none_among(part, ns), k)
197    case o:
198      True{}
199
200def items_open(+part: T.Grid(Maybe<&2, Bool>), its: List<&2, Item>) -> Bool:
201  match its:
202    case Nil{}:
203      True{}
204    case Item{p, s, ns} <> t:
205      item_open(s, part, ns) && items_open(part, t)
206
207# Some completion of the partial layout may still be consistent.
208def open_ok(+part: T.Grid(Maybe<&2, Bool>), rel: List<&2, Item>, n: Nat) -> Bool:
209  between(part_true(part), part_none(part), n) && items_open(part, rel)
210
211# The search
212# ----------
213
214def ctx_n(ctx: Ctx) -> Nat:
215  match ctx:
216    case Ctx{w, h, n, rows, items}:
217      n
218
219def dfs.or(r: Maybe<&2, T.Grid(Bool)>, k: Unit -> Maybe<&2, T.Grid(Bool)>) ->
220  Maybe<&2, T.Grid(Bool)>:
221  match r:
222    case None{}:
223      k(Unit{})
224    case Some{l}:
225      Some{l}
226
227def dfs.when(ok: Bool, k: Unit -> Maybe<&2, T.Grid(Bool)>) -> Maybe<&2, T.Grid(Bool)>:
228  match ok:
229    case False{}:
230      None{}
231    case True{}:
232      k(Unit{})
233
234def dfs.free(free: Bool, skip: Unit -> Maybe<&2, T.Grid(Bool)>,
235  branch: Unit -> Maybe<&2, T.Grid(Bool)>) -> Maybe<&2, T.Grid(Bool)>:
236  match free:
237    case False{}:
238      skip(Unit{})
239    case True{}:
240      branch(Unit{})
241
242def leaf(+ctx: Ctx, +layout: T.Grid(Bool)) -> Maybe<&2, T.Grid(Bool)>:
243  Bool.pick(Maybe<&2, T.Grid(Bool)>, check(ctx, layout), Some{layout}, None{})
244
245# A consistent layout completing the partial one, assigning the cells of
246# `todo` in order (cells already assigned are skipped).
247def dfs(todo: List<&2, Todo>, +part: T.Grid(Maybe<&2, Bool>), +ctx: Ctx) ->
248  Maybe<&2, T.Grid(Bool)>:
249  match todo:
250    case Nil{}:
251      leaf(ctx, fill(part))
252    case Todo{+c, +rel} <> +rest:
253      +p0 = B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})
254      +p1 = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
255      +n = ctx_n(ctx)
256      dfs.free(is_none(look(part, c)),
257        u => dfs(rest, part, ctx),
258        v => dfs.or(dfs.when(open_ok(p0, rel, n), x => dfs(rest, p0, ctx)),
259          y => dfs.when(open_ok(p1, rel, n), z => dfs(rest, p1, ctx))))
260
261# The same search, carrying the mines t and unassigned cells f of the partial
262# layout instead of recounting the whole grid at every step. PROOF.bend
263# shows it answers exactly as dfs.
264def dfs2(todo: List<&2, Todo>, +part: T.Grid(Maybe<&2, Bool>), +t: Nat, +f: Nat, +ctx: Ctx) ->
265  Maybe<&2, T.Grid(Bool)>:
266  match todo:
267    case Nil{}:
268      leaf(ctx, fill(part))
269    case Todo{+c, +rel} <> +rest:
270      +p0 = B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})
271      +p1 = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
272      +n = ctx_n(ctx)
273      +f1 = Nat.sub(f, 1n)
274      dfs.free(is_none(look(part, c)),
275        u => dfs2(rest, part, t, f, ctx),
276        v => dfs.or(dfs.when(between(t, f1, n) && items_open(p0, rel), x => dfs2(rest, p0, t, f1, ctx)),
277          y => dfs.when(between(1n+t, f1, n) && items_open(p1, rel), z => dfs2(rest, p1, 1n+t, f1, ctx))))
278
279# The cells of a solve
280# --------------------
281
282def is_hidden(s: T.Seen) -> Bool:
283  match s:
284    case T.Hidden{}:
285      True{}
286    case o:
287      False{}
288
289def hidden_cells(+rows: T.Grid(T.Seen), ps: List<&2, T.Pos>) -> List<&2, T.Pos>:
290  match ps:
291    case Nil{}:
292      Nil{}
293    case +p <> t:
294      List.filter.put(T.Pos, p, hidden_cells(rows, t),
295        is_hidden(B.at(T.Seen, T.Hidden{}, rows, p)))
296
297def is_number(s: T.Seen) -> Bool:
298  match s:
299    case T.Shown{k}:
300      True{}
301    case o:
302      False{}
303
304def around.put(+i: Item, +c: T.Pos, rest: List<&2, Item>) -> List<&2, Item>:
305  match i:
306    case Item{p, s, ns}:
307      List.filter.put(Item, i, rest, is_number(s) && B.contains(ns, c))
308
309# The numbers of `is` that count c.
310def around(its: List<&2, Item>, +c: T.Pos) -> List<&2, Item>:
311  match its:
312    case Nil{}:
313      Nil{}
314    case +i <> t:
315      around.put(i, c, around(t, c))
316
317def todos(+its: List<&2, Item>, cs: List<&2, T.Pos>) -> List<&2, Todo>:
318  match cs:
319    case Nil{}:
320      Nil{}
321    case +c <> t:
322      Todo{c, around(its, c)} <> todos(its, t)
323
324def has_rel(t: Todo) -> Bool:
325  match t:
326    case Todo{c, rel}:
327      Bool.not(List.is_empty(&2, Item, rel))
328
329# The cells next to a number.
330def nears(ts: List<&2, Todo>) -> List<&2, Todo>:
331  match ts:
332    case Nil{}:
333      Nil{}
334    case +t <> rest:
335      List.filter.put(Todo, t, nears(rest), has_rel(t))
336
337# The other cells.
338def fars(ts: List<&2, Todo>) -> List<&2, Todo>:
339  match ts:
340    case Nil{}:
341      Nil{}
342    case +t <> rest:
343      List.filter.put(Todo, t, fars(rest), Bool.not(has_rel(t)))
344
345# The cells next to a number first, then the rest.
346def order(+ts: List<&2, Todo>) -> List<&2, Todo>:
347  List.append(&2, Todo, nears(ts), fars(ts))
348
349# The order of a search
350# ----------------------
351
352def todo_c(t: Todo) -> T.Pos:
353  match t:
354    case Todo{c, rel}:
355      c
356
357# The numbers around each cell next to one; Nil elsewhere.
358def rel_grid(+w: Nat, +h: Nat, ts: List<&2, Todo>) -> T.Grid(List<&2, Item>):
359  match ts:
360    case Nil{}:
361      B.blank(List<&2, Item>, w, h, Nil{})
362    case Todo{c, rel} <> t:
363      B.set_at(List<&2, Item>, rel_grid(w, h, t), c, rel)
364
365# A breadth-first walk over cells linked by a number: the cells to visit,
366# the cells reached (latest first) and a grid of the cells reached.
367type Reach is Data:
368  Reach{queue: List<&2, T.Pos>, order: List<&2, T.Pos>, vis: T.Grid(Bool)}
369
370def reach.add.go(fresh: Bool, +p: T.Pos, queue: List<&2, T.Pos>, order: List<&2, T.Pos>, +vis: T.Grid(Bool)) -> Reach:
371  match fresh:
372    case True{}:
373      Reach{List.append(&2, T.Pos, queue, [p]), p <> order, B.set_at(Bool, vis, p, True{})}
374    case False{}:
375      Reach{queue, order, vis}
376
377# Reach p, if it is next to a number and not reached yet.
378def reach.add(+p: T.Pos, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
379  match r:
380    case Reach{queue, order, +vis}:
381      reach.add.go(Bool.not(B.at(Bool, True{}, vis, p))
382        && Bool.not(List.is_empty(&2, Item, B.at(List<&2, Item>, Nil{}, relg, p))), p, queue, order, vis)
383
384def reach.ns(ns: List<&2, T.Pos>, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
385  match ns:
386    case Nil{}:
387      r
388    case p <> t:
389      reach.ns(t, relg, reach.add(p, relg, r))
390
391def reach.items(rel: List<&2, Item>, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
392  match rel:
393    case Nil{}:
394      r
395    case Item{p, s, ns} <> t:
396      reach.items(t, relg, reach.ns(ns, relg, r))
397
398# Visit cells until none is left to visit (fuel: more than the cells).
399def reach.run(fuel: Nat, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
400  match fuel:
401    case 0n:
402      r
403    case 1n+f:
404      match r:
405        case Reach{queue, order, vis}:
406          match queue:
407            case Nil{}:
408              Reach{Nil{}, order, vis}
409            case +q <> rest:
410              reach.run(f, relg, reach.items(B.at(List<&2, Item>, Nil{}, relg, q), relg, Reach{rest, order, vis}))
411
412def reach.order(r: Reach) -> List<&2, T.Pos>:
413  match r:
414    case Reach{queue, order, vis}:
415      List.reverse(&2, T.Pos, order)
416
417def reach.start(+w: Nat, +h: Nat) -> Reach:
418  Reach{Nil{}, Nil{}, B.blank(Bool, w, h, False{})}
419
420# The cells linked to c through numbers, nearest first (none when c is next
421# to no number).
422def linked(+c: T.Pos, +w: Nat, +h: Nat, +fuel: Nat, +relg: T.Grid(List<&2, Item>)) -> List<&2, T.Pos>:
423  reach.order(reach.run(fuel, relg, reach.add(c, relg, reach.start(w, h))))
424
425def groups.go(ts: List<&2, Todo>, +fuel: Nat, +relg: T.Grid(List<&2, Item>), r: Reach) -> Reach:
426  match ts:
427    case Nil{}:
428      r
429    case Todo{c, rel} <> t:
430      groups.go(t, fuel, relg, reach.run(fuel, relg, reach.add(c, relg, r)))
431
432# The cells next to a number, one group of linked cells at a time.
433def groups(+w: Nat, +h: Nat, ts: List<&2, Todo>, +fuel: Nat, +relg: T.Grid(List<&2, Item>)) -> List<&2, T.Pos>:
434  reach.order(groups.go(ts, fuel, relg, reach.start(w, h)))
435
436def with_c(ts: List<&2, Todo>, +q: T.Pos) -> List<&2, Todo>:
437  match ts:
438    case Nil{}:
439      Nil{}
440    case +t <> rest:
441      List.filter.put(Todo, t, with_c(rest, q), B.same(todo_c(t), q))
442
443# The todos of ts for the cells qs, in the order of qs.
444def gather(qs: List<&2, T.Pos>, +ts: List<&2, Todo>) -> List<&2, Todo>:
445  match qs:
446    case Nil{}:
447      Nil{}
448    case q <> t:
449      List.append(&2, Todo, with_c(ts, q), gather(t, ts))
450
451# ts from its k-th element on, then the first k.
452def rot(+ts: List<&2, Todo>, +k: Nat) -> List<&2, Todo>:
453  List.append(&2, Todo, List.drop(&2, Todo, ts, k), List.take(&2, Todo, ts, k))
454
455# How far to rotate the far cells for c: searches for nearby cells start
456# about n cells apart, so their layouts mine different far cells.
457def spin(c: T.Pos, +w: Nat, +n: Nat, +nf: Nat) -> Nat:
458  match c:
459    case T.Pos{x, y}:
460      Nat.mod(Nat.mul(Nat.add(Nat.mul(y, w), x), Nat.add(n, 1n)), Nat.add(nf, 1n))
461
462# What every search of a solve shares: the cells next to a number and the
463# rest, the groups, the plain order, and the numbers around each cell.
464type Plan is Data:
465  Plan{near: List<&2, Todo>, far: List<&2, Todo>, nf: Nat, gq: List<&2, T.Pos>, base: List<&2, Todo>,
466    fuel: Nat, relg: T.Grid(List<&2, Item>)}
467
468def plan(+w: Nat, +h: Nat, +ts: List<&2, Todo>) -> Plan:
469  +near = nears(ts)
470  +far = fars(ts)
471  +fuel = Nat.add(List.length(&2, Todo, near), 1n)
472  +relg = rel_grid(w, h, near)
473  Plan{near, far, List.length(&2, Todo, far), groups(w, h, near, fuel, relg), order(ts), fuel, relg}
474
475# The order of the search for c.
476def plan_todo(+c: T.Pos, pl: Plan, +ctx: Ctx) -> List<&2, Todo>:
477  match pl:
478    case Plan{+near, far, +nf, gq, base, +fuel, +relg}:
479      match ctx:
480        case Ctx{+w, +h, +n, rows, items}:
481          List.append(&2, Todo, gather(List.append(&2, T.Pos, linked(c, w, h, fuel, relg), gq), near),
482            List.append(&2, Todo, rot(far, spin(c, w, n, nf)), base))
483
484# The outer loop
485# --------------
486
487def covered(ls: List<&2, T.Grid(Bool)>, +c: T.Pos) -> Bool:
488  match ls:
489    case Nil{}:
490      False{}
491    case l <> t:
492      B.mine(l, c) || covered(t, c)
493
494# A consistent layout with a mine on c, if there is one.
495def search(+c: T.Pos, +pl: Plan, +part: T.Grid(Maybe<&2, Bool>), +ctx: Ctx) ->
496  Maybe<&2, T.Grid(Bool)>:
497  +p = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
498  dfs2(plan_todo(c, pl, ctx), p, part_true(p), part_none(p), ctx)
499
500def loop.if(b: Bool, yes: Unit -> Maybe<&2, T.Pos>, no: Unit -> Maybe<&2, T.Pos>) ->
501  Maybe<&2, T.Pos>:
502  match b:
503    case True{}:
504      yes(Unit{})
505    case False{}:
506      no(Unit{})
507
508def loop.found(r: Maybe<&2, T.Grid(Bool)>, c: T.Pos,
509  k: T.Grid(Bool) -> Maybe<&2, T.Pos>) -> Maybe<&2, T.Pos>:
510  match r:
511    case None{}:
512      Some{c}
513    case Some{l}:
514      k(l)
515
516# The first cell of hs that no consistent layout mines, given layouts
517# `found` already shown consistent.
518def loop(hs: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +pl: Plan,
519  +part: T.Grid(Maybe<&2, Bool>), +ctx: Ctx) -> Maybe<&2, T.Pos>:
520  match hs:
521    case Nil{}:
522      None{}
523    case +c <> +t:
524      loop.if(covered(found, c),
525        u => loop(t, found, pl, part, ctx),
526        v => loop.found(search(c, pl, part, ctx), c,
527          l => loop(t, l <> found, pl, part, ctx)))
528
529def solve.go(ok: Bool, +hs: List<&2, T.Pos>, +w: Nat, +h: Nat, n: Nat,
530  +rows: T.Grid(T.Seen)) -> Maybe<&2, T.Pos>:
531  match ok:
532    case False{}:
533      List.head(&2, T.Pos, hs)
534    case True{}:
535      +its = items(w, h, rows, B.cells(w, h))
536      loop(hs, Nil{}, plan(w, h, todos(its, hs)), start(rows), Ctx{w, h, n, rows, its})
537
538# A provably safe hidden cell, or None when every hidden cell might hold a
539# mine.
540def solve(k: T.Knowledge) -> Maybe<&2, T.Pos>:
541  match k:
542    case T.Knowledge{+w, +h, n, +rows}:
543      solve.go(B.shaped(T.Seen, w, h, rows), hidden_cells(rows, B.cells(w, h)), w, h, n, rows)