Today’s problem was a quite straightforward graph traversal problem. By using memoization, a rather naïve depth-first search was sufficiently fast.
I’m afraid today’s solution is very much Haskell-in-Lean, except for the fact
that I did convince Lean that findPaths will terminate, even though it’s
calling the recursive function dfs. I did this with the same “fuel” trick
from Day 4, however.
My biggest problem today was that the answer I got for part 2 was obviously wrong. (It was a very large number.) But after scratching my head for a while, I submitted it, aaaaand it was correct all along.
Things I (re-)learned today
- Nothing, really. :|
Solution
import Batteries.Data.HashMap
import Parser
import Aoc
open Aoc
abbrev ConnMap := Std.HashMap String (List String)
def parseAttached (s : String) : ConnMap :=
match s.splitOn ": " with
| [device, attached] =>
let x := attached.words.map (λ a => (a, [device]))
Std.HashMap.ofListWith x (λ a b => a ++ b)
| _ => panic! s!"Invalid input: {s}"
abbrev Cache := Std.HashMap (String × List String) Nat
def findPaths (m : ConnMap) (req : List String) (start goal : String) : Nat :=
let rec dfs (fuel : Nat) (cache : Cache) (current : String) (reqs : List String) :=
match fuel with
| 0 => (cache, 0)
| fuel + 1 =>
let cacheKey := (current, reqs)
if current == goal then
if req.all (reqs.contains ·) then
(cache.insert cacheKey 1, 1)
else
(cache.insert cacheKey 0, 0)
else
if let some cachedCount := cache.get? cacheKey then
(cache, cachedCount)
else
match m.get? current with
| none => (cache.insert cacheKey 0, 0)
| some neighbours =>
let reqs' := if req.contains current then current :: reqs else reqs
let (cache', total) := neighbours.foldl (λ (cacheAcc, countAcc) neighbour =>
let (cache'', pathCount) := dfs fuel cacheAcc neighbour reqs'
(cache'', countAcc + pathCount)
) (cache, 0)
(cache'.insert cacheKey total, total)
let maxLength := m.keys.length
let (_, count) := dfs maxLength {} start []
count
def main : IO Unit := do
let lines <- readLines "Day11/input.txt"
let connections := lines.map parseAttached
|>.foldl (·.mergeWith (λ _ a b => a ++ b)) {}
-- part 1
let pathCount := findPaths connections [] "out" "you"
IO.println s!"Part 1: {pathCount}"
-- part 2
let pathCount := findPaths connections ["dac", "fft"] "out" "svr"
IO.println s!"Part 2: {pathCount}"