39 lines
1 KiB
Python
39 lines
1 KiB
Python
from lib import *
|
|
|
|
input = read_input(2018, 23)
|
|
|
|
lines = input.splitlines()
|
|
|
|
|
|
bots = []
|
|
for pos, r in map(str.split, lines):
|
|
x, y, z = map(int, pos.split("<")[1].strip(">,").split(","))
|
|
r = int(r.split("=")[1])
|
|
bots.append((x, y, z, r))
|
|
sx, sy, sz, sr = max(bots, key=lambda a: a[3])
|
|
|
|
print(sum(abs(x - sx) + abs(y - sy) + abs(z - sz) <= sr for x, y, z, _ in bots))
|
|
|
|
|
|
bots = []
|
|
for pos, r in map(str.split, lines):
|
|
x, y, z = map(int, pos.split("<")[1].strip(">,").split(","))
|
|
r = int(r.split("=")[1])
|
|
bots.append((x, y, z, r))
|
|
|
|
zabs = lambda x: z3.If(x >= 0, x, -x)
|
|
x, y, z = z3.Ints("x y z")
|
|
in_ranges = [z3.Int(f"in_range_{i}") for i in range(len(bots))]
|
|
range_count = z3.Int("sum")
|
|
o = z3.Optimize()
|
|
for (nx, ny, nz, nr), ir in zip(bots, in_ranges):
|
|
o.add(ir == z3.If(zabs(x - nx) + zabs(y - ny) + zabs(z - nz) <= nr, 1, 0))
|
|
|
|
o.add(range_count == sum(in_ranges))
|
|
dist_from_zero = z3.Int("dist")
|
|
o.add(dist_from_zero == zabs(x) + zabs(y) + zabs(z))
|
|
h1 = o.maximize(range_count)
|
|
h2 = o.minimize(dist_from_zero)
|
|
o.check()
|
|
|
|
print(o.lower(h2))
|