this post was submitted on 08 Dec 2023
21 points (92.0% liked)

Advent Of Code

770 readers
67 users here now

An unofficial home for the advent of code community on programming.dev!

Advent of Code is an annual Advent calendar of small programming puzzles for a variety of skill sets and skill levels that can be solved in any programming language you like.

AoC 2023

Solution Threads

M T W T F S S
1 2 3
4 5 6 7 8 9 10
11 12 13 14 15 16 17
18 19 20 21 22 23 24
25

Rules/Guidelines

Relevant Communities

Relevant Links

Credits

Icon base by Lorc under CC BY 3.0 with modifications to add a gradient

console.log('Hello World')

founded 1 year ago
MODERATORS
 

Day 8: Haunted Wasteland

Megathread guidelines

  • Keep top level comments as only solutions, if you want to say something other than a solution put it in a new post. (replies to comments can be whatever)
  • Code block support is not fully rolled out yet but likely will be in the middle of the event. Try to share solutions as both code blocks and using something such as https://topaz.github.io/paste/ , pastebin, or github (code blocks to future proof it for when 0.19 comes out and since code blocks currently function in some apps and some instances as well if they are running a 0.19 beta)

FAQ

top 27 comments
sorted by: hot top controversial new old
[–] cvttsd2si@programming.dev 5 points 11 months ago* (last edited 11 months ago)

Scala3

this is still not 100% general, as it assumes there is only one Z-node along the path for each start. But it doesn't assume anything else, I think. If you brute force combinations of entries of the zs-arrays, this assumption can be trivially removed, but if multiple paths see lots of Z-nodes, then the runtime will grow exponentially. I don't know if it's possible to do this any faster.

def parse(a: List[String]): (List[Char], Map[String, Map[Char, String]]) =
    def parseNodes(n: List[String]) =
        n.flatMap{case s"$from = ($l, $r)" => Some(from -> Map('L'->l, 'R'->r)); case _ => None}.toMap
    a match{case instr::""::nodes => ( instr.toList, parseNodes(nodes) ); case _ => (List(), Map())}

def task1(a: List[String]): Long =
    val (instr, nodes) = parse(a)
    def go(i: Stream[Char], pos: String, n: Long): Long =
        if pos != "ZZZ" then go(i.tail, nodes(pos)(i.head), n+1) else n
    go(instr.cycle, "AAA", 0)

// ok so i originally thought this was going to be difficult, so
// we parse a lot of info we won't use
case class PathInfo(zs: List[Long], loopFrom: Long, loopTo: Long):
    def stride: Long = loopTo - loopFrom

type Cycle = Long

def getInfo(instr: List[Char], isEnd: String => Boolean, map: Map[String, Map[Char, String]], start: String): PathInfo =
    def go(i: Cycle, pos: String, is: List[Char], seen: Map[(Long, String), Cycle], acc: List[Long]): PathInfo =
        val current: (Long, String) = (is.size % instr.size, pos)
        val nis = if is.isEmpty then instr else is
        val nacc = if isEnd(pos) then i::acc else acc
        seen.get(current) match
            case Some(l) => PathInfo(acc, l, i)
            case _ => go(i + 1, map(pos)(nis.head), nis.tail, seen + (current -> i), nacc)
    go(0, start, instr, Map(), List())

// turns out we don't need to check all the different positions
// in each cycle where we are on a Z position, as a) every start
// walks into unique cycles with b) exactly one Z position,
// and c) the length of the cycle is equivalent to the steps to first
// encounter a Z (so a->b->c->Z->c->Z->... is already more complicated, 
// as the cycle length is 2 but the first encounter is after 3 steps)

// anyway let's do some math

// this is stolen code
def gcd(a: Long, b: Long): Long =
    if(b ==0) a else gcd(b, a%b)

def primePowers(x: Long): Map[Long, Long] =
    // for each prime p for which p^k divides x: p->p^k
    def go(r: Long, t: Long, acc: Map[Long, Long]): Map[Long, Long] =
        if r == 1 then acc else
            if r % t == 0 then
                go(r/t, t, acc + (t -> acc.getOrElse(t, 1L)*t))
            else
                go(r, t+1, acc)
    go(x, 2, Map())

// this algorithm is stolen, but I scalafied the impl
def vanillaCRT(congruences: Map[Long, Long]): Long = 
    val N = congruences.keys.product
    val x = congruences.map((n, y) => y*(N/n)*((N/n) % n)).sum
    if x <= 0 then x + N else x

def generalizedHardcoreCRTThatCouldHaveBeenAnLCMBecauseTheInputIsVeryConvenientlyTrivialButWeWantToDoThisRight(ys: List[Long], xs: List[Long]): Option[Long] =
    // finds the smallest k s.t. k === y_i  (mod x_i) for each i
    // even when stuff is not nice

    // pre-check if everything is sufficiently coprime
    // https://math.stackexchange.com/questions/1644677/what-to-do-if-the-modulus-is-not-coprime-in-the-chinese-remainder-theorem
    val vars = for
        ((y1, n1), i1) <- ys.zip(xs).zipWithIndex
        ((y2, n2), i2) <- ys.zip(xs).zipWithIndex
        if i2 > i1
    yield 
        val g = gcd(n1, n2)
        y1 % g == y2 % g
    
    if !vars.forall(a => a) then
        None
    else
        // we need to split k === y (mod mn) into k === y (mod m) and k === y (mod n) for m, n coprime
        val congruences = for
            (x, y) <- xs.zip(ys)
            (p, pl) <- primePowers(x)
        yield
            p -> (y % pl -> pl)
        
        // now we eliminate redundant congruences
        // since our input is trivial, this is essentially
        // the step in which we solve the task by 
        // accidentaly computing an lcm
        val r = congruences.groupMap(_._1)(_._2).mapValues(l => l.map(_._2).max -> l.head._1).values.toMap
        
        // ok now we meet the preconditions
        // for doing this
        Some(vanillaCRT(r))

def task2(a: List[String]): Long =
    val (instr, nodes) = parse(a)
    val infos = nodes.keySet.filter(_.endsWith("A")).map(s => getInfo(instr, _.endsWith("Z"), nodes, s))
    generalizedHardcoreCRTThatCouldHaveBeenAnLCMBecauseTheInputIsVeryConvenientlyTrivialButWeWantToDoThisRight(
        infos.map(_.zs.head).toList, infos.map(_.stride).toList
    ).getOrElse(0)

@main def main: Unit =
  val data = readlines("/home/tim/test/aoc23/aoc23/inputs/day8/task1.txt")
  for f <- List(
      task1,
      task2,
    ).map(_ andThen println)
  do f(data)
[–] Gobbel2000@feddit.de 4 points 11 months ago (1 children)

Rust

As others have shown, part 2 can be pretty simple if you allow one assumption: The distance from a start point to the nearest end point is always the same as cycling from that nearest end point back to itself. Under that assumption you can just take the lowest common multiple of these distances. And honestly, who can claim to understand ghost navigation and what you can and can't assume? Empirical evidence suggests that this is how ghosts travel.

[–] vole@lemmy.world 13 points 11 months ago* (last edited 11 months ago) (4 children)

Personally, I'm not a fan of requiring analysis of the individualized input to reach the correct (sufficiently efficient) solution for part 2. Or maybe I'm just resentful because I feel like I've been duped after writing an generalized-to-the-puzzle-description-but-insufficiently-efficient solution. 😔

These quantum ghosts need to come back down to reality.

[–] reboot6675@sopuli.xyz 8 points 11 months ago

Yeah I got annoyed too. Because this is not implied in the problem statement and it definitely doesn't hold up in general...

[–] hades@lemm.ee 2 points 11 months ago

For better or worse, this is to be expected for Advent of Code.

[–] bamboo@lemmy.blahaj.zone 2 points 11 months ago (3 children)

Perhaps there's a mathematical way to prove that this assumption will actually always happen despite the input? I wanted to test this assumption, and edited the map and randomly changes the destinations for keys ending in Z, and it looks like the matches are still at consistent intervals. Is it possible to have an input map which breaks the assumption?

[–] cvttsd2si@programming.dev 6 points 11 months ago* (last edited 11 months ago) (1 children)

I can prove the opposite for you. The assumption that Gobbel2000 describes is wrong in general. For example, take

L

A -> B, X
B -> C, X
C -> Z, X
Z -> C, X
X -> X, X

the first Z is reached after 3 steps, but then every cycle only takes 2 steps.

The matches are still at consistent intervals, but you can easily find a counterexample for that as well:

L

A -> 1Z, X
1Z -> 2Z, X
2Z -> A, X
X -> X, X

now the intervals will be 2, 1, 2, 1, ...

However, it is easy to prove that there will be a loop of finite length, and that the intervals will behave somewhat nicely:

Identify a "position" by a node you are at, and your current index in the LRL instruction sequence. If you ever repeat a position P, you will repeat the exact path away from the position you took the last time, and the last time you later reached P, so you will keep reaching P again and again. There are finitely many positions, so you can't keep not repeating any forever, you will run out.

Walking in circles along this loop you eventually find yourself in, the intervals between Zs you see will definitely be a repeating sequence (as you will keep seeing not just same-length intervals, but in fact the exact same paths between Zs).

So in total, you will see some finite list of prefix-intervals, and then a repeating cycle of loop-intervals. I have no idea if this can be exploited to compute the answer efficiently, but see my solution-comment for something that only assumes that only one Z will be encountered each cycle.

[–] bamboo@lemmy.blahaj.zone 2 points 11 months ago

Thank you for this, it really helped me understand this more.

[–] hades@lemm.ee 2 points 11 months ago (1 children)

This assumption doesn't hold in general, however you can construct an efficient algorithm, even if it doesn't hold.

First, let's show that a cycle always exists. Let I be the size of the instruction string, and N be the number of nodes. Since the number of states for each ghost is at most I*N, after a finite number of steps, the ghost will go into one of the previous states and cycle forever. Let's say that the cycle length is c, and after a+c steps the ghost has entered the same state it was after a steps.

Let's assume[^1] that during the first a+c steps the ghost has only once encounter an end state (a node ending with 'Z'), specifically after e states. If e >= a, this means that the ghost will encounter the end state also after e + c and e + 2c and so on, or for every number of steps s > e such that s = e (mod c). The assumption you formulated means e = 0 (mod c), or e = c.

Now, consider the K ghosts that are travelling simultaneously. If after n steps all ghosts have reached the end state, this means that n = e_i (mod c_i) for all ghosts i (1 <= i <= K). According to the Chinese remainder theorem, there is a solution if and only if e_1 = e_2 = ... = e_K (mod gcd(c_1, c_2, ... c_K)). If the assumption you formulated holds, then e_i = 0 (mod c_i), so lcm(c_1, ... c_K) works as a solution. If it doesn't, you can still find n, but it will be a bit more tricky (which is probably why the authors of the challenge made e = c always).

[^1] -- this is another assumption you've implicitly made, and that happens to hold for all the inputs. However, if this assumption doesn't hold, we can check all possible combination of end state positions.

[–] cvttsd2si@programming.dev 2 points 11 months ago (1 children)

re [^1]: yeah, but that may explode the runtime again. Do you have any idea if this is possible to solve without brute forcing the combinations?

[–] hades@lemm.ee 1 points 11 months ago

I don't think it will explode the runtime. If you have multiple feasible values for e per ghost, you just need to find a combination of e_i such that e_1 = e_2 = ... = e_K (mod gcd(c_1, c_2, ... c_K)), which is just an intersection of K sets of at most I*N elements.

[–] reboot6675@sopuli.xyz 2 points 11 months ago

I crafted a simple counter-example (single letters for brevity). The way the sequence goes totally depends on the instructions, and we don't have any guarantees on that. It could be anything. Of course, looking at the input data we could find what the instructions are, but the assumption doesn't hold in general.

A = (B, X)
B = (C, X)
C = (X, Z)
Z = (A, C)
X = (X, X)

L L R L L L R R R -> A B C Z A B C Z C Z
L L R R R L L L R -> A B C Z C Z A B C Z

Here the distance of Z cycling back into itself could be 2 or 4, depending on what the instruction string is doing.

[–] Gobbel2000@feddit.de 1 points 11 months ago

I kind of agree, props for getting a general solution. I actually realized this issue only after I got both stars and didn't feel like changing it again.

[–] cacheson@kbin.social 4 points 11 months ago (1 children)

Nim

I like how if you have an error in your calculations, you end up wandering the haunted desert for eternity. Very flavorful.

My solution for part 2 is pretty much the same as for part 1, just modified to work on a sequence of nodes instead of a single node. However, it doesn't find an answer in the time that I was willing to wait for it. I thought about trying to optimize it to run faster, but figured that if it was taking this long on Nim, then interpreted languages would have no chance, so that couldn't be the right approach.

I suspected that maybe the ghosts arrived at the Z locations at predictable intervals. I added some code to output the step count each time each ghost reached a Z (see commented code), and my suspicion was correct. Just needed to calculate the least common multiple of the 6 cycle lengths.

[–] CommunityLinkFixer@lemmings.world 1 points 11 months ago

Hi there! Looks like you linked to a Lemmy community using a URL instead of its name, which doesn't work well for people on different instances. Try fixing it like this: !nim@programming.dev

[–] corristo@programming.dev 3 points 11 months ago* (last edited 11 months ago)

APL

I'm using this year's AoC to learn (Dyalog) APL, so this is most likely a pretty terrible solutions. I would've liked to use instead of of my imitation of a while loop with a recursive function, but I couldn't figure out how to get to the number of iterations ⍣ performed to arrive at the destination. If someone here knows how to do that (or has other suggestions for improvement) I'm open for suggestions.

⎕IO ← 0       ⍝ use 0-based indexes
I←⌷⍨∘⊃⍨⍤0 99  ⍝ "sane" indexing
⎕PP←17        ⍝ print integers with up to 17 significant digits without use of scientific notation

input←⊃⎕NGET'inputs/day8.txt'1
instructions←⊃input
p←↑{0 2 4 I{6⍴⎕CSV⍠'Widths'(3 4 3 2 3 1)⊢⍵'S'1}⍵}¨ 2↓input
nodes←,1↑[1]p
L←(⍳⍴nodes) ∘.{nodes[⍺]≡⍵ 1 ⌷p} ⍳⍴nodes
R←(⍳⍴nodes) ∘.{nodes[⍺]≡⍵ 2 ⌷p} ⍳⍴nodes
S←(⊃(+.×)/{'R'≡⍵:R ⋄ ⍵≡'L':L}¨⌽instructions)
⎕←(≢instructions) × {⍺←0 ⋄ ⍵[⍸'ZZZ'∘≡¨nodes]: ⍺ ⋄ ⍺+1 ∇ S+.×⍵}'AAA'∘≡¨nodes                             ⍝ part 1
⎕←∧/(≢instructions) × {⍺←0 ⋄ 0≡+/⍵[⍸~('Z'∘=⊢/)¨nodes]: ⍺ ⋄ ⍺+1 ∇ S+.×⍵}¨{(⍳≢nodes)=⍵}¨⍸('A'∘=⊢/)¨nodes  ⍝ part 2
[–] hades@lemm.ee 2 points 11 months ago* (last edited 3 months ago)

Python

import itertools
import math
import re

from .solver import Solver

class Day08(Solver):

  def __init__(self):
    super().__init__(8)
    self.instructions: str = ''
    self.nodes: dict[str, tuple[str, str]] = {}

  def presolve(self, input: str):
    lines = input.rstrip().split('\n')
    self.instructions = lines[0]
    for line in lines[2:]:
      g = re.fullmatch(r'(\w+) = \((\w+), (\w+)\)', line)
      assert g, f"line {line} doesn't match expected format"
      target, left, right = g.groups()
      self.nodes[target] = (left, right)

  def solve_first_star(self) -> int:
    instructions = itertools.cycle(self.instructions)
    cur = 'AAA'
    counter = 0
    while cur != 'ZZZ':
      instruction = next(instructions)
      if instruction == 'L':
        cur = self.nodes[cur][0]
      elif instruction == 'R':
        cur = self.nodes[cur][1]
      else:
        raise RuntimeError(f'Unexpected instruction: {instruction}')
      counter += 1
    return counter

  def solve_second_star(self) -> int:
    start_nodes: list[str] = [node for node in self.nodes if node.endswith('A')]
    end_nodes: set[str] = set(node for node in self.nodes if node.endswith('Z'))
    loop_offsets: dict[str, int] = {}
    loop_sizes: dict[str, int] = {}
    destination_offset_in_loops: dict[str, list[int]] = {}
    for node in start_nodes:
      cur = node
      path: list[tuple[int, str]] = [(0, cur)]
      for instruction_offset, instruction in itertools.cycle(enumerate(self.instructions)):
        next_node = self.nodes[cur][0] if instruction == 'L' else self.nodes[cur][1]
        next_state = ((instruction_offset + 1) % len(self.instructions), next_node)
        if next_state in path:
          loop_offsets[node] = path.index(next_state)
          loop_sizes[node] = len(path) - loop_offsets[node]
          destination_offset_in_loops[node] = [i for i, [_, n] in enumerate(path) if n in end_nodes]
          break
        path.append(next_state)
        cur = next_node
    return math.lcm(*loop_sizes.values())
[–] snowe@programming.dev 2 points 11 months ago

Ruby

!ruby@programming.dev

Man I did not understand how to solve this one (part 2, p1 was easy). After I understood it and looked at other people's solutions I was able to extend mine quite easily...

https://github.com/snowe2010/advent-of-code/blob/master/ruby_aoc/2023/day08/day08.rb

[–] pnutzh4x0r@lemmy.ndlug.org 2 points 11 months ago* (last edited 11 months ago)

Language: Python

Part 1

First part was very straight-forward: read the input in and simulate the navigation. Taking advantage of itertools.cycle made cycling through the instructions very easy :]

Network = dict[str, dict[str, str]]

def read_instructions(stream=sys.stdin) -> Iterator[str]:
    return itertools.cycle(stream.readline().strip())

def read_network(stream=sys.stdin) -> Network:
    network = defaultdict(dict)

    for line in map(str.strip, stream):
        if not line:
            continue

        source, target_l, target_r = re.findall('[A-Z]{3}', line)
        network[source] = {
            'L': target_l,
            'R': target_r,
        }

    return network

def navigate(instructions: Iterator[str], network: Network) -> int:
    count  = 0
    source = 'AAA'
    target = 'ZZZ'

    while source != target:
        source = network[source][next(instructions)]
        count += 1

    return count

def main(stream=sys.stdin) -> None:
    instructions = read_instructions(stream)
    network      = read_network(stream)
    print(navigate(instructions, network))

Part 2

The second part was also straight-forward: locate the ghosts, and then navigate from each ghost until you hit an element that ends with a 'Z'. The trick to avoid brute-forcing is to realize that the ghosts will cycle (ie. repeat the same paths) if they all don't land on an element that ends with a 'Z' at the same time. To solve the problem, you just ened to calculate the steps for each ghost to reach an endpoint and then compute the lowest common multiple of those counts. Fortunately, Python has math.lcm, so not much code was needed!

def navigate(instructions: Iterator[str], network: Network, element: str) -> int:
    count = 0

    while not element.endswith('Z'):
        element = network[element][next(instructions)]
        count += 1

    return count

def locate_ghosts(network: Network) -> list[str]:
    return [element for element in network if element.endswith('A')]

def main(stream=sys.stdin) -> None:
    instructions = read_instructions(stream)
    network      = read_network(stream)
    ghosts       = locate_ghosts(network)
    counts       = [navigate(cycle(instructions), network, ghost) for ghost in ghosts]
    print(math.lcm(*counts))

GitHub Repo

[–] mykl@lemmy.world 2 points 11 months ago* (last edited 11 months ago)

Dart

Part 1 was easy enough. For Part 2 I took a guess that the cycles were all well behaved and I could get away with just calculating the LCM, and it paid off.

(List, Map) parse(List lines) => (
      lines.first.split(''),
      {
        for (var l in lines.skip(2).map((e) => e.split(RegExp(r'[^A-Z0-9]'))))
          l[0]: [l[4], l[6]]
      }
    );
int movesTo(pos, steps, rules) {
  var stepNo = -1;
  while (!pos.endsWith('Z')) {
    pos = rules[pos]![steps[(stepNo += 1) % steps.length] == 'L' ? 0 : 1];
  }
  return stepNo + 1;
}

part1(List lines) {
  var (steps, rules) = parse(lines);
  return movesTo('AAA', steps, rules);
}

// All cycles are independent of state of `steps`, and have
// first instance == cycle length which makes this verrry simple.
part2(List lines) {
  var (steps, rules) = parse(lines);
  return [
    for (var start in rules.keys.where((e) => e.endsWith('A')))
      movesTo(start, steps, rules)
  ].reduce((s, t) => s.lcm(t));
}
}
[–] morrowind@lemmy.ml 2 points 11 months ago* (last edited 11 months ago)

Crystal

!crystal_lang@lemmy.ml

part 1 was made way simpler after I made it a function for part 2
also I accidentally saw someone elses code, so I can't take full credit for figuring out how to do part 2

Input = File.read("input.txt").lines

Dirs = Input[0].chars.map {|c| c == 'L' ? 0 : 1}
Nodes = Hash(String, Tuple(String, String)).new
Input[2..].each {|line| Nodes[line[..2]] = {line[7..9], line[12..14]} }

# part 1
puts num_steps("AAA", &.== "ZZZ")

# part 2
currents = Nodes.keys.select(&.ends_with? 'A')
steps = currents.map {|cur| num_steps(cur, &.ends_with? 'Z')}
puts steps.reduce(1_i64) {|a, b| a.lcm b}

def num_steps(start)
	steps = 0
	Dirs.cycle do |dir|
		steps += 1
		start = Nodes[start][dir]
		break if yield start
	end
	steps
end
[–] SteveDinn@lemmy.ca 2 points 11 months ago
[–] capitalpb@programming.dev 2 points 11 months ago

First part was simple enough. Second part was easy logically, but after running the brute force solution with a parallel iterator from rayon and maxing out all 12 cores of this CPU, it was still taking forever. I always get tripped up by these ones that need fancy math, because although I was always good at math, I've never been good at looking at these problems and figuring out what kind of formula would apply. So I cheated and looked at other people's comments for their solutions, and saw the least common multiple mentioned. This made sense to me, so I implemented it and got a result almost instantly. I hate having to look at other comments to solve these things, but I never would have came to that conclusion myself.

The code still isn't the cleanest, and I'd love to tidy up the parsing, but it works and I'm happy.

https://github.com/capitalpb/advent_of_code_2023/blob/main/src/solvers/day08.rs

impl Solver for Day08 {
    fn star_one(&self, input: &str) -> String {
        let (directions, map) = input.split_once("\n\n").unwrap();

        let mut route_map = HashMap::new();

        for line in map.lines() {
            let line = line.replace(" ", "").replace("(", "").replace(")", "");
            let (position, destinations) = line.split_once('=').unwrap();
            let (left, right) = destinations.split_once(',').unwrap();
            route_map.insert(position.to_string(), (left.to_string(), right.to_string()));
        }

        let mut current_position = "AAA".to_string();
        for (step, direction) in directions.chars().cycle().enumerate() {
            current_position = match direction {
                'L' => route_map[¤t_position].0.to_string(),
                'R' => route_map[¤t_position].1.to_string(),
                _ => unreachable!(),
            };

            if current_position == "ZZZ" {
                return (step + 1).to_string();
            }
        }

        unreachable!()
    }

    fn star_two(&self, input: &str) -> String {
        let (directions, map) = input.split_once("\n\n").unwrap();

        let mut route_map = HashMap::new();

        for line in map.lines() {
            let line = line.replace(" ", "").replace("(", "").replace(")", "");
            let (position, destinations) = line.split_once('=').unwrap();
            let (left, right) = destinations.split_once(',').unwrap();
            route_map.insert(position.to_string(), (left.to_string(), right.to_string()));
        }

        let positions = route_map
            .keys()
            .filter(|pos| pos.ends_with('A'))
            .collect::>();

        let steps = positions
            .iter()
            .filter(|pos| pos.ends_with('A'))
            .map(|pos| {
                let mut current_position = pos.to_string();
                for (step, direction) in directions.chars().cycle().enumerate() {
                    current_position = match direction {
                        'L' => route_map[¤t_position].0.to_string(),
                        'R' => route_map[¤t_position].1.to_string(),
                        _ => unreachable!(),
                    };

                    if current_position.ends_with('Z') {
                        return step + 1;
                    }
                }
                unreachable!()
            })
            .collect::>();

        steps
            .into_iter()
            .reduce(|acc, steps| acc.lcm(&steps))
            .unwrap()
            .to_string()
    }
}
[–] soulsource@discuss.tchncs.de 2 points 11 months ago (1 children)

[language: Lean4]

I did not make the assumption that the distance from the start to the goal is the same as the cycle length. This made the problem a bit harder, but I'm pretty sure my solution is actually generic. As always, I'll only post the direct solution. Helper functions (like, in this case, xgcd) are in other files, you can find them together with the full solution on github.

Since my solution contains a ton of comments (that outline my thought process), I'll again split it in several posts here.

Part1

inductive Instruction
  | left
  | right

instance : ToString Instruction where
  toString a := match a with
  | Instruction.left => "Left"
  | Instruction.right => "Right"

abbrev WaypointId := String

structure Waypoint where
  id : WaypointId
  left : WaypointId
  right : WaypointId
  deriving Repr

-- Okay, the need for different representations in both parts has burnt me once too often.
-- This time it's going to be really dumb.

private def parseInstructions (input : String) : Except String $ List Instruction := do
  let mut result := []
  for character in input.toList do
    match character with
    | 'L' => result := Instruction.left :: result
    | 'R' => result := Instruction.right :: result
    | _ => throw s!"Invalid instruction {character}. Only 'L' and 'R' are valid instructions."
  pure result.reverse

private def parseWaypoint (input : String) : Except String Waypoint :=
  if let [id, targets] := input.splitOn " = " |> List.map String.trim then
    if targets.startsWith "(" && targets.endsWith ")" then
      let withoutBraces := targets.drop 1 |> flip String.dropRight 1
      match withoutBraces.splitOn "," |> List.map String.trim with
      | [a,b] => pure {id := id, left := a, right := b : Waypoint}
      | _ => throw s!"Targets need to have 2 entries, separated by ',', but were {targets}"
    else
      throw s!"Targets for waypoint need to be enclosed in (), but were {targets}"
  else
    throw s!"Waypoint could not be split in ID and targets: {input}"

private def parseWaypoints (input : List String) : Except String $ List Waypoint :=
  input.mapM parseWaypoint

open Lean in
private def validateWaypointLinks (waypoints : List Waypoint) : Bool :=
  let validLinks := HashSet.insertMany HashSet.empty $ waypoints.map Waypoint.id
  waypoints.all λw ↦ validLinks.contains w.left && validLinks.contains w.right

def target : WaypointId := "ZZZ"
def start : WaypointId := "AAA"

def parse (input : String) : Except String $ List Instruction × List Waypoint := do
  let lines := input.splitOn "\n" |> List.map String.trim |> List.filter String.notEmpty
  match lines with
  | instructions :: waypoints =>
    let instructions ← parseInstructions instructions
    let waypoints ← parseWaypoints waypoints
    if let none := waypoints.find? λx ↦ x.id == start then
      throw s!"Input must contain the waypoint \"{start}\"."
    if let none := waypoints.find? λx ↦ x.id == target then
      throw s!"Input must contain the waypoint \"{target}\""
    if not $ validateWaypointLinks waypoints then
      throw "Input contained a waypoint that is not properly linked."
    return (instructions, waypoints)
  | [] => throw "Input was empty (or only contained whitespace)."

--------------------------------------------------------------------------------------------------------
-- One of my goals for this Advent of Code is to show that the code terminates whenever that's
-- possible. In this case, it's not directly possible from the riddle input, but it's possible
-- by adding circle detection. So, instead of making the instructions just an infinite list
-- I'll treat the case that we run out of instruction in a special way, such that we detect
-- if we are lost in the desert.

private structure ConnectedWaypoints where
  left : WaypointId
  right : WaypointId

private def ConnectedWaypoints.get : ConnectedWaypoints →  Instruction → WaypointId
| {left, right := _}, Instruction.left => left
| {left := _, right}, Instruction.right => right

-- does a single pass over all instructions. Returns err if no result has been found and another pass is needed.
-- error is optional - if none, then there is an inconsistency in the input and we are stuck.
private def pass (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) (instructions : List Instruction) : Except (Option (Nat × WaypointId)) Nat := do
  if currentPosition == "ZZZ" then
    return alreadyDoneSteps
  match instructions with
  | [] => throw $ some (alreadyDoneSteps, currentPosition)
  | a :: as =>
    let currentWaypoint := waypoints.find? currentPosition
    match currentWaypoint with
    | none => throw none -- should not happen
    | some currentWaypoint => pass waypoints (alreadyDoneSteps + 1) (currentWaypoint.get a) as

private def part1_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) : Option Nat :=
  let remainingStarts := possibleStarts.filter λs ↦ s != currentPosition
  if remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy
    let passResult := pass waypoints alreadyDoneSteps currentPosition instructions
    match passResult with
    | Except.ok n => some n
    | Except.error none => none -- dead end on map. Should not be possible.
    | Except.error $ some n => part1_impl waypoints instructions remainingStarts n.fst n.snd
  else
    none -- walking in circles
  termination_by part1_impl a b c d e => c.length

open Lean in
def part1 (input : List Instruction × List Waypoint) : Option Nat :=
  let possibleStarts := input.snd.map Waypoint.id
  let waypoints : HashMap WaypointId ConnectedWaypoints := HashMap.ofList $ input.snd.map λw ↦ (w.id, {left := w.left, right := w.right : ConnectedWaypoints})
  let instructions := input.fst
  part1_impl waypoints instructions possibleStarts 0 start

[–] soulsource@discuss.tchncs.de 1 points 11 months ago* (last edited 11 months ago) (1 children)

Actually, all my comments in Part 2 make it too big for a single post. The full solution consists of two functions (that could be combined with a bit more work...).

The first function is a brute-force approach, that has a similar termination condition to the first part. It halts, once all paths are walking in circles. This function does not find a solution yet. Then there is a second function that looks for solutions that appear later, while all paths are already walking in circles. That function writes all goals as equations of the form x = start + n * period. The target condition is that all paths have the same value for x. This was then solved by looking at all permutations between two paths, and solving the Diophantine equations, creating a new, combined, path.

In the end, the closest resulting valid goal was also the final result.

Part2, the Brute Force function

--------------------------------------------------------------------------------------------------------
-- okay, part 2 is nasty.
-- what do we know?
-- o) All paths we follow simultaneously have the same path length, as they have common instructions.
--   x) This means that once we walk in circles on all of them, we are lost.
--      -> That's the way to convince the compiler this program terminates.
-- o) We could use the cycle detection to rule out short, cycled paths.
--   x) Once a path is in a cycle, the targets repeat at cycle-lenght interval.
--   x) I doubt that this would be much faster than brute-force though.

-- let's try brute force first.

private def parallelPass (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPositions : List WaypointId) (instructions : List Instruction) : Except (Option (Nat × (List WaypointId))) Nat := do
  if currentPositions.all λw ↦ w.endsWith "Z" then
    return alreadyDoneSteps
  match instructions with
  | [] => throw $ some (alreadyDoneSteps, currentPositions)
  | a :: as =>
    let currentWaypoint := currentPositions.mapM waypoints.find?
    match currentWaypoint with
    | none => throw none -- should not happen
    | some currentWaypoints =>
      let nextWaypoints := currentWaypoints.map $ flip ConnectedWaypoints.get a
      parallelPass waypoints (alreadyDoneSteps + 1) nextWaypoints as


private def totalRemainingStarts (s : List (List WaypointId)) : Nat :=
  s.foldl (·+·.length) 0

private def part2_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (alreadyDoneSteps : Nat) (possibleStarts : List (List WaypointId)) (currentPositions : List WaypointId) : Option Nat :=
  let remainingStarts := (possibleStarts.zip currentPositions).map λs ↦ s.fst.filter λt ↦ t != s.snd
  -- I _really_ don't want to prove stuff by hand... Luckily this works.
  if totalRemainingStarts remainingStarts < totalRemainingStarts possibleStarts then
    let passResult := parallelPass waypoints alreadyDoneSteps currentPositions instructions
    match passResult with
    | Except.ok n => some n
    | Except.error none => none -- dead end on map. Should not be possible.
    | Except.error $ some n => part2_impl waypoints instructions n.fst remainingStarts n.snd
  else
    none -- walking in circles
  termination_by part2_impl a b c d e => totalRemainingStarts d

[–] soulsource@discuss.tchncs.de 1 points 11 months ago

And last, but not least, here's the part that actually finds the result:

Part 2, the part for after the brute force approach fails (don't be alarmed, it's mostly comments, very few actual code lines)

-- Okay, tried Brute Force, it did NOT work. Or rather, it might work, but I won't be able to prove
-- termination for it. Not that it wouldn't be possible to prove, just I won't manage to.
-- The problem is that the termination condition in part2_impl is too soon.
-- You can actually see this in the example (for which part2_impl works, but by chance).
-- While the goals in each part repeat, they repeat at different rates.
-- Soo, we would need to continue even after each part has started walking in circles.
-- However, just doing that runs for a very long time without finding a result.
-- Sooo, let's be smarter.
--
-- Every path consist of 2 segments. The part that leads up to a cycle, and the cycle.
-- Both parts can contain goals, but once the cycle starts, the goals repeat with cycle-length.
-- A cycle is at least one pass, but can (and does...) consist of multiple passes too.

-- We can use part2_impl still - to verify that we do not reach the goals before all our paths start
-- cycling. That allows us to only care about cycling paths in the second part of the solution, which
-- we only reach if part2_impl does not yield a result (we know it doesn't, but that would be cheating).

-- Soo, how can the second part look like?

-- For simplicity let's not do this in parallel. Rather, let's find the goals for each start individually
-- So, let's just consider a single path (like the one from part1)
-- We need to write down the number of steps at which we reach a goal.
-- Whenever we remove a remaining start from the possible starts list, we need to note it down, and
--   how many steps it took us to get there.
-- Once we detect a circle, we can look up
--   how many steps we took in total till we startec cycling
--   and how many steps it took us to reach the cycle start for the first time
--   that's the period of each goal in the cycle.
-- For each goal that was found between cycle-start and cycle-end, we can write down an equation:
-- x = steps_from_start + cycle_length * n
-- n is a Natural number here, not an integer. x is the number of steps at which we pass this goal

-- Once we have that information for all goals of all starts, we can combine it:
-- That's a set of Diophantine equations.
--
-- Or, rather, several sets of Diophantine equations...
-- For each combination of goals that are reached in the cycles of the participating paths, we need to
-- solve the following system:
--
-- We can write each goal for each run in the form x = g0 + n * cg
-- Where x is the solution we are looking for, g0 is the number of steps from the start until
-- we hit the goal for the first time **in the cycle**, and cg is the cycle length
--
-- Once we have those equations, we can combine them pairwise: https://de.wikipedia.org/wiki/Lineare_diophantische_Gleichung
-- This allows us to reduce all paths to a single one, which has multiple equations that
-- describe when a goal is reached.
-- For each of those equations we need to find the first solution that is larger than
-- the point where all paths started to cycle. The smallest of those is the result.

-- a recurring goal, that starts at "start" and afterwards appears at every "interval".
private structure CyclingGoal where
  start : Nat
  interval : Nat
  deriving BEq

instance : ToString CyclingGoal where
  toString g := s!"`g = {g.start} + n * {g.interval}`"

private def CyclingGoal.nTh (goal : CyclingGoal) (n : Nat) : Nat :=
  goal.start + n * goal.interval

-- Combine two cycling goals into a new cycling goal. This might fail, if they never meet.
-- This can for instance happen if they have the same frequency, but different starts.
private def CyclingGoal.combine (a b : CyclingGoal) : Option CyclingGoal :=
  -- a.start + n * a.interval = b.start + m * b.interval
  -- n * a.interval - m * b.interval = b.start - a.start
  -- we want to do as much as possible in Nat, such that we can easily reason about which numbers are
  -- positive. Soo
  let (a, b) := if a.start > b.start then (b,a) else (a,b)
  let (g, u, _) := Euclid.xgcd a.interval b.interval
  -- there is no solution if b.start - a.start is not divisible by g
  let c := (b.start - a.start)
  let s := c / g
  if s * g != c then
    none
  else
    let deltaN := b.interval / g
    let n0 := s * u -- we can use u directly - v would need its sign swapped, but we don't use v.
    -- a.start + (n0 + t * deltaN)*a.interval
    -- a.start + n0*a.interval + t * deltaN * a.interval
    -- we need the first value of t that yields a result >= max(a.start, b.start)
    -- because that's where our cycles start.
    let x := ((max a.start b.start : Int) - a.interval * n0 - a.start)
    let interval := a.interval * deltaN
    let t0 := x / interval
    let t0 := if t0 * interval == x || x < 0 then t0 else t0 + 1 -- int division rounds towards zero, so for x < 0 it's already ceil.
    let start :=  a.start + n0 * a.interval + t0 * deltaN * a.interval
    assert! (start ≥ max a.start b.start)
    let start := start.toNat
    some {start, interval }

private def findCyclingGoalsInPathPass (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) (instructions : List Instruction) (visitedGoals : List Nat) : Option (Nat × WaypointId × (List Nat)) := do
  let visitedGoals := if currentPosition.endsWith "Z" then
    alreadyDoneSteps :: visitedGoals
  else
    visitedGoals
  match instructions with
  | [] => some (alreadyDoneSteps, currentPosition, visitedGoals)
  | a :: as =>
    let currentWaypoint := waypoints.find? currentPosition
    match currentWaypoint with
    | none => none -- should not happen
    | some currentWaypoint => findCyclingGoalsInPathPass waypoints (alreadyDoneSteps + 1) (currentWaypoint.get a) as visitedGoals

private def findCyclingGoalsInPath_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (visitedGoals : List Nat) (visitedStarts : List (WaypointId × Nat)) (currentPosition : WaypointId) (currentSteps : Nat) : List CyclingGoal :=
  let remainingStarts := possibleStarts.filter λs ↦ s != currentPosition
  if remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy
    let visitedStarts := (currentPosition, currentSteps) :: visitedStarts
    let passResult := findCyclingGoalsInPathPass waypoints currentSteps currentPosition instructions visitedGoals
    match passResult with
      | none =>  [] -- should not happen. Only possible if there's a dead end
      | some (currentSteps, currentPosition, visitedGoals) => findCyclingGoalsInPath_impl waypoints instructions remainingStarts visitedGoals visitedStarts currentPosition currentSteps
  else
    let beenHereWhen := visitedStarts.find? λs ↦ s.fst == currentPosition
    let beenHereWhen := beenHereWhen.get!.snd --cannot possibly fail
    let cycleLength := currentSteps - beenHereWhen
    visitedGoals.filterMap λ n ↦ if n ≥ beenHereWhen then
      some {start := n, interval := cycleLength : CyclingGoal}
    else
      none -- goal was reached before we started to walk in cycles, ignore.
  termination_by findCyclingGoalsInPath_impl a b c d e f g => c.length

private def findCyclingGoalsInPath (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPosition : WaypointId) : List CyclingGoal :=
  findCyclingGoalsInPath_impl waypoints instructions possibleStarts [] [] startPosition 0

-- returns the number of steps needed until the first _commmon_ goal that cycles is found.
private def findFirstCommonCyclingGoal (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPositions : List WaypointId) : Option Nat :=
  let cyclingGoals := startPositions.map $ findCyclingGoalsInPath waypoints instructions possibleStarts
  let combinedGoals : List CyclingGoal := match cyclingGoals with
    | [] => []
    | g :: gs => flip gs.foldl g λc n ↦ c.bind λ cc ↦ n.filterMap λ nn ↦ nn.combine cc
  let cyclingGoalStarts := combinedGoals.map CyclingGoal.start
  cyclingGoalStarts.minimum?

open Lean in
def part2 (input : List Instruction × List Waypoint) : Option Nat :=
  let possibleStarts := input.snd.map Waypoint.id
  let waypoints : HashMap WaypointId ConnectedWaypoints := HashMap.ofList $ input.snd.map λw ↦ (w.id, {left := w.left, right := w.right : ConnectedWaypoints})
  let instructions := input.fst
  let positions : List WaypointId := (input.snd.filter λ(w : Waypoint) ↦ w.id.endsWith "A").map Waypoint.id
  part2_impl waypoints instructions 0 (positions.map λ_ ↦ possibleStarts) positions
  <|> -- if part2_impl fails (it does), we need to dig deeper.
  findFirstCommonCyclingGoal waypoints instructions possibleStarts positions

[–] Adanisi@lemmy.zip 2 points 11 months ago

My C solutions: https://git.sr.ht/~aidenisik/aoc23/tree/master/item/day8

Yes, it'd be faster to read the file into memory and use that, but I decided to throw efficiency out the window.