-
Notifications
You must be signed in to change notification settings - Fork 0
/
day23.py
executable file
·94 lines (64 loc) · 2.5 KB
/
day23.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
#!/usr/bin/env python3
from collections import namedtuple
import re
import z3
import aoc
Coord3 = namedtuple('Coord3', ['x_val', 'y_val', 'z_val'])
NanoBot = namedtuple('NanoBot', ['coord', 'radius'])
def parse_input(input_list):
parser = re.compile(r'^pos=<(.+),(.+),(.+)>, r=(.+)$')
nanobots = set()
for line in input_list:
match = parser.fullmatch(line)
assert match
x_val = int(match.group(1))
y_val = int(match.group(2))
z_val = int(match.group(3))
r_val = int(match.group(4))
nanobots.add(NanoBot(Coord3(x_val, y_val, z_val), r_val))
return nanobots
def part1(input_list):
nanobots = parse_input(input_list)
largest_nanobot = NanoBot(Coord3(0,0,0), 0)
for nanobot in nanobots:
if nanobot.radius > largest_nanobot.radius:
largest_nanobot = nanobot
num_nanobots = 0
for nanobot in nanobots:
distance = abs(nanobot.coord.x_val - largest_nanobot.coord.x_val) + \
abs(nanobot.coord.y_val - largest_nanobot.coord.y_val) + \
abs(nanobot.coord.z_val - largest_nanobot.coord.z_val)
if distance <= largest_nanobot.radius:
num_nanobots += 1
return num_nanobots
def z3_abs(value):
return z3.If(value >= 0, value, -value)
def z3_dist(coord1, coord2):
return z3_abs(coord1[0] - coord2[0]) + \
z3_abs(coord1[1] - coord2[1]) + \
z3_abs(coord1[2] - coord2[2])
def part2(input_list):
# Use z3 to find x,y,z that maximizes number_of_nearby_bots(x,y,z).
# Based on https://github.com/msullivan's solution.
nanobots = parse_input(input_list)
z3_x_val = z3.Int('x')
z3_y_val = z3.Int('y')
z3_z_val = z3.Int('z')
best_location = (z3_x_val, z3_y_val, z3_z_val)
z3_number_of_bots = z3.Int('number_of_bots')
z3_number_of_nearby_bots = z3_x_val * 0
for nanobot in nanobots:
z3_number_of_nearby_bots += z3.If(z3_dist(best_location, nanobot[0]) <= nanobot[1], 1, 0)
optimize = z3.Optimize()
optimize.add(z3_number_of_bots == z3_number_of_nearby_bots)
optimize.maximize(z3_number_of_bots)
optimize.minimize(z3_dist((0,0,0), (z3_x_val, z3_y_val, z3_z_val)))
optimize.check()
model = optimize.model()
position = (model[z3_x_val].as_long(),
model[z3_y_val].as_long(),
model[z3_z_val].as_long())
distance = abs(position[0]) + abs(position[1]) + abs(position[2])
return distance
if __name__ == "__main__":
aoc.main(part1, part2)