This commit is contained in:
akp 2023-12-25 11:38:31 +00:00
parent 1802fb5df6
commit 5b2c191cf7
No known key found for this signature in database
GPG key ID: CF8D58F3DEB20755
6 changed files with 136 additions and 0 deletions

View file

@ -0,0 +1,7 @@
# [Day 24: Never Tell Me The Odds](https://adventofcode.com/2023/day/24)
Part 1 is not:
* 1344 (too low)
* 48384 (too high)
Running this solution requires `z3-solver` to be installed.

View file

@ -0,0 +1,112 @@
import sys
from collections import namedtuple
from numbers import Number
import gridutil.coord as cu
from functools import reduce
import math
import z3
Hailstone = namedtuple("Hailstone", ["position", "velocity"])
def parse(instr: str) -> list[Hailstone]:
return [
Hailstone(
*map(lambda x: cu.Coordinate3(*map(int, x.split(", "))), line.split(" @ "))
)
for line in instr.splitlines()
]
def get_2d_line(stone: Hailstone) -> tuple[Number, Number]:
m = stone.velocity.y / stone.velocity.x
c = stone.position.y - (m * stone.position.x)
return m, c
def get_2d_intersection(a: Hailstone, b: Hailstone) -> cu.Coordinate | None:
m1, c1 = get_2d_line(a)
m2, c2 = get_2d_line(b)
if math.isclose(m1, m2):
return None
x = (c2 - c1) / (m1 - m2)
y = (m1 * x) + c1
return cu.Coordinate(x, y)
def one(instr: str):
hailstones = parse(instr)
MIN, MAX = (7, 27) if len(hailstones) == 5 else (200000000000000, 400000000000000)
acc = 0
for i, stone1 in enumerate(hailstones[:-1]):
for stone2 in hailstones[i + 1 :]:
if stone1 == stone2:
continue
p = get_2d_intersection(stone1, stone2)
if p is None or not reduce(lambda acc, x: acc and MIN <= x <= MAX, p, True):
continue
if not (
(p.x > stone1.position.x) == (stone1.velocity.x > 0)
and (p.x > stone2.position.x) == (stone2.velocity.x > 0)
):
continue
acc += 1
return acc
def two(instr: str):
hailstones = parse(instr)
# for our thrown rock
# initial position: x, y, z
# velocity: vx, vy, vz
# for each of 3 hailstones
# time of collision with that hailstone: t_i
# intial position: hx, hy, hz
# velocity: hvx, hvy, hvz
x, y, z = (z3.Int(x) for x in ["x", "y", "z"])
vx, vy, vz = (z3.Int(x) for x in ["vx", "vy", "vz"])
solver = z3.Solver()
for i in range(3):
hailstone = hailstones[i]
t = z3.Int(f"t_{i}")
solver.add(
t >= 0,
x + (vx * t) == hailstone.position.x + (hailstone.velocity.x * t),
y + (vy * t) == hailstone.position.y + (hailstone.velocity.y * t),
z + (vz * t) == hailstone.position.z + (hailstone.velocity.z * t),
)
_debug("Solving...", end="", flush=True)
assert solver.check() == z3.sat
model = solver.model()
_debug("\r \r" + str(model))
return sum(model[var].as_long() for var in [x, y, z])
def _debug(*args, **kwargs):
kwargs["file"] = sys.stderr
print(*args, **kwargs)
if __name__ == "__main__":
if len(sys.argv) < 2 or sys.argv[1] not in ["1", "2"]:
print("Missing day argument", file=sys.stderr)
sys.exit(1)
inp = sys.stdin.read().strip()
if sys.argv[1] == "1":
print(one(inp))
else:
print(two(inp))

View file

@ -0,0 +1,14 @@
{
"1": [
{
"is": "2",
"input": "19, 13, 30 @ -2, 1, -2\n18, 19, 22 @ -1, -1, -2\n20, 25, 34 @ -2, -2, -4\n12, 31, 28 @ -1, -2, -1\n20, 19, 15 @ 1, -5, -3\n\n"
}
],
"2": [
{
"is": "47",
"input": "19, 13, 30 @ -2, 1, -2\n18, 19, 22 @ -1, -1, -2\n20, 25, 34 @ -2, -2, -4\n12, 31, 28 @ -1, -2, -1\n20, 19, 15 @ 1, -5, -3\n\n"
}
]
}

View file

@ -35,3 +35,4 @@ A day denoted with a star means it has a visualisation.
| 21 - Step Counter | ★ ☆ | Python | ??? |
| 22 - Sand Slabs | ★ ★ | Python | I maintain that OpenSCAD is the best AoC 3D debugging tool |
| 23 - A Long Walk | ★ ★ | Python | Both parts here could theorietcially be done with the same implementation but I couldn't be bothered to rework the part 2 solution to work for part 1 as well. |
| 24 - Never Tell Me The Odds | ★ ★ | Python | Z3 seems like an *incredible* useful tool but also not a satisfying puzzle at all :( |

Binary file not shown.

Before

Width:  |  Height:  |  Size: 50 KiB

After

Width:  |  Height:  |  Size: 51 KiB

Before After
Before After

View file

@ -41,3 +41,5 @@
{"day": 22, "part": 2, "runner": "py", "min": 30.386138439178467, "max": 30.386138439178467, "avg": 30.386138439178467, "n": 1}
{"day": 23, "part": 1, "runner": "py", "min": 2.006169557571411, "max": 2.006169557571411, "avg": 2.006169557571411, "n": 1}
{"day": 23, "part": 2, "runner": "py", "min": 33.72923398017883, "max": 33.72923398017883, "avg": 33.72923398017883, "n": 1}
{"day": 24, "part": 1, "runner": "py", "min": 0.12593984603881836, "max": 0.1335890293121338, "avg": 0.13133821487426758, "n": 5}
{"day": 24, "part": 2, "runner": "py", "min": 4.988582134246826, "max": 6.0756916999816895, "avg": 5.414014768600464, "n": 5}