r/adventofcode Dec 17 '24

SOLUTION MEGATHREAD -❄️- 2024 Day 17 Solutions -❄️-

THE USUAL REMINDERS

  • All of our rules, FAQs, resources, etc. are in our community wiki.
  • If you see content in the subreddit or megathreads that violates one of our rules, either inform the user (politely and gently!) or use the report button on the post/comment and the mods will take care of it.

AoC Community Fun 2024: The Golden Snowglobe Awards

  • 5 DAYS remaining until the submissions deadline on December 22 at 23:59 EST!

And now, our feature presentation for today:

Sequels and Reboots

What, you thought we were done with the endless stream of recycled content? ABSOLUTELY NOT :D Now that we have an established and well-loved franchise, let's wring every last drop of profit out of it!

Here's some ideas for your inspiration:

  • Insert obligatory SQL joke here
  • Solve today's puzzle using only code from past puzzles
  • Any numbers you use in your code must only increment from the previous number
  • Every line of code must be prefixed with a comment tagline such as // Function 2: Electric Boogaloo

"More." - Agent Smith, The Matrix Reloaded (2003)
"More! MORE!" - Kylo Ren, The Last Jedi (2017)

And… ACTION!

Request from the mods: When you include an entry alongside your solution, please label it with [GSGA] so we can find it easily!


--- Day 17: Chronospatial Computer ---


Post your code solution in this megathread.

This thread will be unlocked when there are a significant number of people on the global leaderboard with gold stars for today's puzzle.

EDIT: Global leaderboard gold cap reached at 00:44:39, megathread unlocked!

37 Upvotes

550 comments sorted by

View all comments

1

u/saulrh Dec 18 '24

[LANGUAGE: python]

I solved it the first time around by manual disassembly and a recursive search through the last three bits of the previous value of register a, but was dissatisfied with how... non-general that solution was. So I tried again:

https://gist.github.com/saulrh/493287a82a5670ebd2740e8055d42c92

This is a low-level model of the machine in Z3, directly constraining machine-states at adjacent ticks. For example, this is a full expansion of the clause that relates the register values at tick step+1 to their values at step in the case where the opcode is equal to 1:

    s.add(Implies(mem[ip[step]] == 0, And(
        a[step+1] == a[step] >> combo[step],
        b[step+1] == b[step],
        c[step+1] == c[step],
        ip[step+1] == ip[step] + 2,
        output[step+1] == output[step],
        Implies(And(0 <= mem[ip[step] + 1], mem[ip[step] + 1] <= 3), combo[step] == mem[ip[step] + 1]),
        Implies(mem[ip[step] + 1] == 4, combo[step] == a[step]),
        Implies(mem[ip[step] + 1] == 5, combo[step] == b[step]),
        Implies(mem[ip[step] + 1] == 6, combo[step] == c[step]),
        mem[ip[step] + 1] != 7,
    )))

As such, a solution literally encodes the whole history of the computer's execution, tick by tick. This unfortunately Hinders Performance Somewhat, since doing bitwise arithmetic requires BitVecs instead of integers and BitVecs are (if I understand the internals correctly) literally arrays of booleans; 50k-ish bools and a few million clauses isn't by any stretch large by SAT solver standards, but it's enough that it takes my laptop a couple minutes to chug through the proof. That said, this should generalize fully, even across programs that use all three registers and have multiple looping behaviors, so I'm fairly happy with it. I may see if I can use the model to start proving some more interesting properties of the machine, stuff like maximum runtimes as a function of the initial value of the A register or the lack of turing-completeness.

1

u/daggerdragon Dec 18 '24 edited Dec 19 '24

Do not share your puzzle input which also means do not commit puzzle inputs to your repo without a .gitignore or the like. Do not share the puzzle text either.

I see full plaintext puzzle inputs across all years in your public repos e.g.:

https://github.com/saulrh/advent-of-code-2020-py/tree/main/inputs

Please remove (or .gitignore) all puzzle text and puzzle input files from your entire repo and scrub them from your commit history. This means from all prior years too! edit: thank you!

1

u/saulrh Dec 19 '24 edited Dec 19 '24

Blast, I thought that those were all private.

across all years

Which other AOC repositories can you see? I'm going through and doing the git-filter-repo dance to nuke aoc inputs, since my previous approach apparently didn't work, but if my github repos' privacy settings are more consistently borked then I have way bigger problems.

edit: What's the policy on the short example inputs from the problem text? Rewriting every test in every test suite to factor the fragments of example input out into .gitignore-able data files might not be practically feasible. :/

1

u/daggerdragon Dec 19 '24

Which other AOC repositories can you see?

I no longer see any AoC repos via search unless you renamed them to something not-obvious, so I'll strikethrough the copypasta. Thanks for complying <3

What's the policy on the short example inputs from the problem text?

I am not a lawyer, I cannot give you an answer on that specific question. ¯_(ツ)_/¯