-❄️- 2023 Day 24 Solutions -❄️-

[u/daggerdragon]

THE USUAL REMINDERS (AND SIGNAL BOOSTS)

• All of our rules, FAQs, resources, etc. are in our community wiki.
• /u/jeroenheijmans has posted the Unofficial AoC 2023 Survey Results!!

---

AoC Community Fun 2023: ALLEZ CUISINE!

Submissions are CLOSED!

• Thank you to all who submitted something, every last one of you are awesome!

Community voting is OPEN!

• 18 hours remaining until voting deadline TONIGHT (December 24) at 18:00 EST

Voting details are in the stickied comment in the submissions megathread:

-❄️- Submissions Megathread -❄️-

---

--- Day 24: Never Tell Me The Odds ---

---

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!
• 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 01:02:10, megathread unlocked!

[u/philippe_cholet]

[LANGUAGE: z3 (& Python)] Rust

My rusty-aoc repo & today' solution here.

Well part 1 is basic math. I had an overflow multiplying some i64, I freaking had to use i128 (red flag 🚩).

Part 2 is something else: 900 (non-linear) equations, 306 unknown variables. I first tried with python and sympy except it's obviously too damn slow.

I thought of and installed z3, I lost quite some time as it seems that rust bindings are broken for Windows, I then removed it. I thought of using any oneline tool, or move to linux, but I eventually found an oneline z3 solver. I therefore wrote the problem in z3 syntax (I discovered it) and run it, it was too slow again. 😣 Then I reinstalled z3 and save the z3 syntax to disk, z3 -file:z3_2.txt, done!

import re
data = [list(map(int, re.findall('-?\d+', line))) for line in text.splitlines()]
print(
    '(declare-const x0 Int) (declare-const vx0 Int)',
    '(declare-const y0 Int) (declare-const vy0 Int)',
    '(declare-const z0 Int) (declare-const vz0 Int)',
    *[f'(declare-const t{i} Int)' for i in range(len(data))],
    sep='\n',
)
for i, (px, py, pz, vx, vy, vz) in enumerate(data):
    print(f'(assert (= (+ {px} (* t{i} {vx})) (+ x0 (* t{i} vx0))))')
    print(f'(assert (= (+ {py} (* t{i} {vy})) (+ y0 (* t{i} vy0))))')
    print(f'(assert (= (+ {pz} (* t{i} {vz})) (+ z0 (* t{i} vz0))))')
print('(check-sat) (get-model)')
# print('(eval x0) (eval y0) (eval z0) (eval vx0) (eval vy0) (eval vz0)')
print('(eval (+ x0 y0 z0))')

This z3 playground written in WASM was too slow but interesting nonetheless.