My Advent of Code solutions in Python.
kevinyap.ca/2019/12/going-fast-in-advent-of-code/
advent-of-code
python
Add solution for 2024/13
Yep, it's a z3 day.
+43
+43
2024/day13.py
+43
2024/day13.py
···
1
+
import fileinput
2
+
from utils import parse_nums
3
+
4
+
from z3 import Optimize, Int, And, sat
5
+
6
+
7
+
PART_2_FACTOR = 10000000000000
8
+
9
+
part_1 = 0
10
+
part_2 = 0
11
+
12
+
13
+
INPUT = ''.join(fileinput.input())
14
+
for block in INPUT.split('\n\n'):
15
+
lines = block.split('\n')
16
+
ax, ay = parse_nums(lines[0])
17
+
bx, by = parse_nums(lines[1])
18
+
px, py = parse_nums(lines[2])
19
+
20
+
a = Int('a')
21
+
b = Int('b')
22
+
23
+
for part in range(1, 3):
24
+
o = Optimize()
25
+
o.add(And(
26
+
a >= 0,
27
+
b >= 0,
28
+
a * ax + b * bx == px + (PART_2_FACTOR if part == 2 else 0),
29
+
a * ay + b * by == py + (PART_2_FACTOR if part == 2 else 0),
30
+
))
31
+
32
+
o.minimize(a * 3 + b)
33
+
34
+
if o.check() == sat:
35
+
m = o.model()
36
+
result = m[a].as_long() * 3 + m[b].as_long()
37
+
if part == 1:
38
+
part_1 += result
39
+
else:
40
+
part_2 += result
41
+
42
+
print("Part 1:", part_1)
43
+
print("Part 2:", part_2)