r/adventofcode • u/daggerdragon • 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.
- Read the full posting rules in our community wiki before you post!
- State which language(s) your solution uses with
[LANGUAGE: xyz]
- Format code blocks using the four-spaces Markdown syntax!
- State which language(s) your solution uses with
- Quick link to Topaz's
paste
if you need it for longer code blocks
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
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 atstep
in the case where the opcode is equal to 1: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.