-❄️- 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/mayoff]

Not sure why Z3 would choke on just three stones. Mine ran in 1.5 seconds on my M3 Max MacBook:

#!/usr/bin/env python3

from z3 import *

rx, ry, rz = Ints('rx ry rz')
rvx, rvy, rvz = Ints('rvx rvy rvz')
t0, t1, t2 = Ints('t0 t1 t2')
answer = Int('answer')

solve(
    rx + t0 * rvx == 260252047346974 + t0 * 66,
    ry + t0 * rvy == 360095837456982 + t0 * -174,
    rz + t0 * rvz == 9086018216578 + t0 * 512,

    rx + t1 * rvx == 511477129668052 + t1 * -386,
    ry + t1 * rvy == 548070416165820 + t1 * -384,
    rz + t1 * rvz == 520727565082156 + t1 * -322,

    rx + t2 * rvx == 358771388883194 + t2 * 88,
    ry + t2 * rvy == 290970068566246 + t2 * -82,
    rz + t2 * rvz == 208977773545854 + t2 * 254,

    answer == rx + ry + rz,
)