My Advent of Code solutions in Python.
kevinyap.ca/2019/12/going-fast-in-advent-of-code/
advent-of-code
python
Add 2025/10
+61
+61
2025/day10.py
+61
2025/day10.py
···
1
+
import fileinput
2
+
from collections import defaultdict
3
+
4
+
from z3 import Int, Optimize
5
+
6
+
7
+
def solve(goal, toggles, part_2=False):
8
+
s = Optimize()
9
+
10
+
# Create z3 variables for each "light" (light/counter).
11
+
lights = [Int('j' + str(i)) for i, g in enumerate(goal)]
12
+
13
+
# Create z3 variables to count each button press.
14
+
buttons = [Int('t' + str(i)) for i in range(len(toggles))]
15
+
16
+
# Count instances of indicator light appearing in toggle.
17
+
appearances = defaultdict(list)
18
+
for i, toggle in enumerate(toggles):
19
+
for t in toggle:
20
+
appearances[t].append(i)
21
+
22
+
# Add constraints for `counter == sum of buttons pressed`.
23
+
for i, ts in appearances.items():
24
+
s.add(lights[int(i)] == sum(buttons[x] for x in ts))
25
+
26
+
# Enforce non-negative numbers of button presses.
27
+
for b in buttons:
28
+
s.add(b >= 0)
29
+
30
+
# Add constraints depending on if we're solving part 1 or 2.
31
+
for i, g in enumerate(goal):
32
+
if part_2:
33
+
s.add(lights[i] == g)
34
+
else:
35
+
# We just care about parity in part 1.
36
+
s.add(lights[i] % 2 == g)
37
+
38
+
# Minimize the total number of button presses.
39
+
s.minimize(sum(buttons))
40
+
41
+
# Answer is the sum of button presses from the solver.
42
+
s.check()
43
+
m = s.model()
44
+
return sum(m[b].as_long() for b in buttons)
45
+
46
+
47
+
part_1 = 0
48
+
part_2 = 0
49
+
for line in fileinput.input():
50
+
parts = line.strip().split()
51
+
lights, *toggles, joltage = parts
52
+
53
+
toggles = [t[1:-1].split(',') for t in toggles]
54
+
p1_goal = [1 if c == '#' else 0 for c in lights[1:-1]]
55
+
p2_goal = [int(x) for x in joltage[1:-1].split(',')]
56
+
57
+
part_1 += solve(p1_goal, toggles)
58
+
part_2 += solve(p2_goal, toggles, part_2=True)
59
+
60
+
print("Part 1:", part_1)
61
+
print("Part 2:", part_2)