Year 2015 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.

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.

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.

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.

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.

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.

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.

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.

shortestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
  (paths : List (List Location, Integer)) -> Eff fs (List Location, Integer)
shortestPath paths = do
  shortest paths 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)

Calculate the longest path from a list of paths by recursively comparing lengths.

longestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
  (paths : List (List Location, Integer)) -> Eff fs (List Location, Integer)
longestPath paths = do
  longest paths Nothing
  where
    longest : List (a, Integer) -> (acc : Maybe (a, Integer)) 
      -> Eff fs (a, Integer)
    longest [] acc = note "No paths" acc
    longest (x :: xs) acc = 
      case acc of
        Nothing => longest xs (Just x)
        Just y => 
          if (snd x) > (snd y)
            then longest xs (Just x)
            else longest 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.

part1 : 
  Eff (PartEff String) (Integer, (DistanceMap, List (List Location, 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"
  distances <- traverse pathLen paths
  let pairs = zip paths distances
  (path, len) <- shortestPath pairs
  info "Shortest Path: \{show path} \{show len}"
  pure (len, (distance_map, pairs))

Part 2

Feed the locations back into a longest path function

part2 : (DistanceMap, List (List Location, Integer))
  -> Eff (PartEff String) Integer
part2 (distance_map, pairs) = do
  runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do
  (path, len) <- longestPath pairs
  info "Longest Path: \{show path} \{show len}"
  pure len