diff --git a/README.md b/README.md index f40d0a7..3ca6197 100644 --- a/README.md +++ b/README.md @@ -37,3 +37,4 @@ solution. - [Day 6](src/Years/Y2015/Day6.md) - [Day 7](src/Years/Y2015/Day7.md) - [Day 8](src/Years/Y2015/Day8.md) + - [Day 9](src/Years/Y2015/Day9.md) diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index d3be367..0225c82 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -15,6 +15,7 @@ import Years.Y2015.Day5 import Years.Y2015.Day6 import Years.Y2015.Day7 import Years.Y2015.Day8 +import Years.Y2015.Day9 --> # Days @@ -73,6 +74,12 @@ y2015 = MkYear 2015 [ , day8 ``` +## [Day 9](Y2015/Day9.md) + +```idris + , day9 +``` + ```idris ] ``` diff --git a/src/Years/Y2015/Day9.md b/src/Years/Y2015/Day9.md new file mode 100644 index 0000000..acb702c --- /dev/null +++ b/src/Years/Y2015/Day9.md @@ -0,0 +1,258 @@ +# Year 2016 Day 9 + +This day provides our first example of a graph traversal problem. We'll use a +`Choose` based effectful breath first search to identify all the possible paths +meeting the problem criteria, and then figure out the length in a separate step. +This isn't a particularly efficient solution, but its good enough for this small +problem size. + + + +```idris +import Data.String +import Data.List1 +import Data.Vect +import Data.List.Lazy +import Data.SortedMap +import Data.SortedSet + +import Util +``` + +## Parsing and data structures + +### Parsing + +Define a location pair as a collection of two locations and a distance between +them (as this graph is undirected), as well as some type aliases, a `contains` +method to test if a pair covers a given location, and implement `Foldable` for +the type to get access to the standard library utility methods. + +`DistanceMap` serves as a slightly fancy adjacency list for our graph +representation. We'll load this into a `Reader` effect to avoid having to pass +it around as an explicit argument to every function later on once it's been +computed. + +```idris +Location : Type +Location = String + +Distance : Type +Distance = Integer + +record LocationPair (l : Type) where + constructor MkLP + locations : Vect 2 l + distance : Integer +%name LocationPair lp, mp, np, op + +contains : Eq l => l -> LocationPair l -> Bool +contains x lp = + case find (== x) lp.locations of + Nothing => False + Just _ => True + +Foldable LocationPair where + foldl f acc lp = foldl f acc lp.locations + foldr f acc lp = foldr f acc lp.locations + toList lp = toList lp.locations + +LP : Type +LP = LocationPair Location + +DistanceMap : Type +DistanceMap = SortedMap Location (List LP) +``` + + + +Perform simple, pattern matching based parsing of a location pair. + +```idris +parseLocationPair : Has (Except String) fs => + String -> Eff fs LP +parseLocationPair str = do + from ::: ["to", to, "=", dist] <- pure $ split (== ' ') str + | _ => throw "Badly formatted input string: \{str}" + dist <- note "Bad distance: \{dist}" $ parsePositive dist + pure $ MkLP [from, to] dist +``` + +Convert a list of pairs to a `DistanceMap`, a mapping from a location to all the +location pairs that cover it. To keep this function readable, we do this inside +an inner function with the `State DistanceMap` effect. + +Since the inner function is recursive, instead of extracting the result after +running the state effect, we lift it into an unconstrained `fs` so we can borrow +the stack-saftey from our runner's top level `runEff`. + +```idris +pairsToMap : List LP -> Eff fs DistanceMap +pairsToMap lps = do + (_, out) <- lift . runState empty $ insertPairs lps + pure out + where + insertLoc : LP -> (loc : Fin 2) -> Eff [State DistanceMap] () + insertLoc lp loc = do + let loc = (index loc lp.locations) + list <- map (lookup loc) get + case list of + Nothing => modify $ insert loc [lp] + Just xs => modify $ insert loc (lp :: xs) + insertPair : LP -> Eff [State DistanceMap] () + insertPair lp = traverse_ (insertLoc lp) (the (List _) [0, 1]) + insertPairs : List LP -> Eff [State DistanceMap] () + insertPairs lps = traverse_ insertPair lps +``` + +## Solver functions + +Generate all the possible paths originating from `current` with length `depth`, +which is set to the number of locations in the calling function to provide the +"visits each node once" property. + +The `path` argument accumulates the path taken by this particular branch of the +breadth first search. It is accumulated in reverse order, but this doesn't +really matter as this graph is undirected. + +We use the `Choose` effect to explore every possible link connecting to the +current node, after filtering the possible links for ones that satisfy the +problem constraints. + +```idris +paths : Has (Reader DistanceMap) fs => Has Choose fs => Has Logger fs => + (path : List Location) + -> (depth : Nat) + -> (current : Location) + -> Eff fs (List Location) +paths path 0 current = empty +paths path 1 current = + if contains current path + then empty + else pure $ current :: path +paths path (S depth') current = do + debug "Paths from \{current} at \{show (S depth')} having visited \{show path}" + -- If we are in the path list, we have revisited this node, bail + False <- pure $ contains current path + | _ => empty + -- Update our path list to contain ourself + let path = current :: path + -- Find our next possible steps, bailing out if there are none + Just nexts <- map (lookup current) ask + | _ => do empty + -- Convert it to a list of locations + let nexts = concat . map toList $ nexts + -- Filter out any that are already in the path, this would be covered by the + -- check at the start of this function, but this cleans up the logs + let nexts = filter (not . (flip contains) path) nexts + -- Select our next node + next <- oneOf nexts + paths path depth' next +``` + +Calculate all the possible paths that satisfy the problem constraints. + +As a minor optimization, we only explore the paths leading out of a single +arbitrary location to start with, and then take advantage of a symmetry of the +problem, collecting all the "rotations" of each output path to cheaply calculate +all the paths that take all the same steps as our "seed" path, but have +different starting and ending locations. + +```idris +allPaths : + Has (Reader DistanceMap) fs => Has Logger fs => Has (Except String) fs => + Eff fs $ SortedSet (List Location) +allPaths = do + locs <- map keys ask + first <- note "No locations" $ head' locs + paths <- lift . runChoose {f = LazyList} $ + paths [] (length locs) first {fs = [Choose, Reader _, Logger]} + pure $ buildSet paths empty + where + insertPaths : List (List Location) -> (acc : SortedSet (List Location)) + -> SortedSet (List Location) + insertPaths [] acc = acc + insertPaths (x :: xs) acc = insertPaths xs (insert x acc) + buildSet : LazyList (List Location) -> (acc : SortedSet (List Location)) + -> SortedSet (List Location) + buildSet [] acc = acc + buildSet (x :: xs) acc = + let rots = rotations x + in buildSet xs (insertPaths rots acc) +``` + +Calculate the length of a path by recursively destructuring the list and looking +up each pair of locations in our `DistanceMap`. + +```idris +pathLen : Has (Reader DistanceMap) fs => Has (Except String) fs => + (path : List Location) -> Eff fs Integer +pathLen [] = pure 0 +pathLen (x :: []) = pure 0 +pathLen (x :: (y :: xs)) = do + lps <- map (lookup x) ask >>= note "Not found in distance map: \{x}" + lp <- note "Pair not found \{x} \{y}" $ + find (\l => contains x l && contains y l) lps + map (lp.distance +) $ pathLen (y :: xs) +``` + +Calculate the shortest path from a list of paths by recursively comparing +lengths. + +```idris +shortestPath : Has (Reader DistanceMap) fs => Has (Except String) fs => + (paths : List (List Location)) -> Eff fs (List Location, Integer) +shortestPath paths = do + lens <- traverse pathLen paths + let pairs = zip paths lens + shortest pairs Nothing + where + shortest : List (a, Integer) -> (acc : Maybe (a, Integer)) + -> Eff fs (a, Integer) + shortest [] acc = note "No paths" acc + shortest (x :: xs) acc = + case acc of + Nothing => shortest xs (Just x) + Just y => + if (snd x) < (snd y) + then shortest xs (Just x) + else shortest xs (Just y) +``` + +## Part Functions + +### Part 1 + +Parse our locations, turn them into a `DistanceMap`, load that into our reader, +generate our paths, then find the one with the shortest length. + +```idris +part1 : Eff (PartEff String) (Integer, ()) +part1 = do + locations <- map lines (askAt "input") >>= traverse parseLocationPair + info "Locations: \{show locations}" + distance_map <- pairsToMap locations + info "Distance map: \{show distance_map}" + runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do + paths <- map Prelude.toList allPaths + trace "Paths: \{show paths}" + info "Found \{show $ length paths} paths" + (path, len) <- shortestPath paths + info "Shortest Path: \{show path} \{show len}" + pure (len, ()) +``` + +