aesop can solve mazes!

Stream: general

[David Renshaw]

I wanted to learn a bit more about how to use aesop, so I tried getting it to solve my maze game (previously discussed here).

After adding a few attributes and configuration options ... it works! See the main file on Github here or try playing with it in your browser here.

We can can even read off a solution from the aesop? output.

def maze2 := ┌────────┐
             │▓▓▓▓▓▓▓▓│
             │▓░▓░▓░▓▓│
             │▓░▓░░░▓▓│
             │▓░░▓░▓▓▓│
             │▓▓░▓░▓░░│
             │▓░░░░▓░▓│
             │▓░▓▓▓▓░▓│
             │▓░░░@░░▓│
             │▓▓▓▓▓▓▓▓│
             └────────┘

set_option maxRecDepth 2000 in
example : can_escape maze2 :=
 by aesop? (add norm maze2)
           (options := {maxRuleApplications := 10000})
           (simp_options := {decide := true})

/-
Try this:
  simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only [maze2, game_state_from_cells,
      game_state_from_cells_aux, update_state_with_row, update_state_with_row_aux, Nat.zero_add]
    apply step_east
    · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
    · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
    · apply step_east
      · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
      · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
      · apply step_north
        · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
        · apply step_north
          · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
          · apply step_north
            · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
            · apply step_east
              · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
              · simp_all (config := ({ decide := true } : Aesop.SimpConfig✝).toConfigCtx✝) only
              · apply escape_east
-/

[David Renshaw]

It is, however, very inefficient. My understanding is that it does no deduplication of goal nodes (i.e. no detecting transpositions), so the search tree gets big quite quickly.

[David Renshaw]

(And the GameState representation is not very efficient to begin with.)

[Kim Morrison]

There is a test file doing best first search of mazes in (Mathlib's) test/search/BestFirst.lean, and a somewhat idiosyncratic implementation of A* search in #3973.