aoc/2018/23_teleport.py

#!/usr/bin/env python3
import sys
import re
import z3
from functools import reduce
from operator import itemgetter, add

bots = [tuple(map(int, re.findall(r'-?[0-9]+', line))) for line in sys.stdin]

# part 1
x, y, z, r = max(bots, key=itemgetter(3))
print(sum(int(abs(bx - x) + abs(by - y) + abs(bz - z) <= r)
          for bx, by, bz, br in bots))

# part 2
def zabs(x):
    return z3.If(x >= 0, x, -x)

def dist(xa, ya, za, xb, yb, zb):
    return zabs(xb - xa) + zabs(yb - ya) + zabs(zb - za)

# build an optimizing model with the solution and its intersections as variables
x, y, z = z3.Ints('x y z')
opt = z3.Optimize()

# maximize: number of intersecting bots
nisect = reduce(add, (z3.If(dist(bx, by, bz, x, y, z) <= br, 1, 0)
                      for bx, by, bz, br in bots))
bestisect = opt.maximize(nisect)

# minimize: manhattan distance of solution to (0, 0, 0)
bestdist = opt.minimize(dist(x, y, z, 0, 0, 0))

assert opt.check() == z3.sat
#print(opt.model())
print('best teleportation point at %s from origin (%s nanobots in range)' %
      (bestdist.value(), bestisect.value()))