Solve 2020 day 24 and 25 and 2018 day 23 part 2

2018/d23.py

@@ -1,32 +1,45 @@
-from lib import get_data, str_to_ints
-
-def dist(a, b):
-    return sum(abs(x - y) for x, y in zip(a[:3], b[:3]))
+from lib import get_data, ints
 
 data = get_data(__file__)
-data = """pos=<10,12,12>, r=2
-pos=<12,14,12>, r=2
-pos=<16,12,12>, r=4
-pos=<14,14,14>, r=6
-pos=<50,50,50>, r=200
-pos=<10,10,10>, r=5
-"""
 
-max_bot = None
-bots = []
-for line in data.splitlines():
-    xs = str_to_ints(line)
-    if max_bot is None:
-        max_bot = xs
-    elif xs[3] > max_bot[3]:
-        max_bot = xs
-    bots.append(xs)
+X, Y, Z, RADIUS = 0, 1, 2, 3
 
-assert max_bot is not None
 
-t = 0
+def dist(a, b):
+    return sum(abs(x - y) for x, y in zip(a[:RADIUS], b[:RADIUS]))
+
+
+bots = [ints(line) for line in data.splitlines()]
+max_bot = max(bots, key=lambda b: b[RADIUS])
 r = max_bot[3]
-for bot in bots:
-    if dist(bot, max_bot) <= r:
-        t += 1
+t = sum(1 for bot in bots if dist(bot, max_bot) <= r)
 print(t)
+
+from z3 import Int, If, Abs, Sum, IntVal, Optimize, set_param
+
+
+x = Int("x")
+y = Int("y")
+z = Int("z")
+
+z3zero = IntVal(0)
+z3one = IntVal(1)
+n_out_of_range = Int("n_out_of_range")
+dist_origin = Int("dist_origin")
+
+bots_out_of_range = [
+    If(Abs(b[X] - x) + Abs(b[Y] - y) + Abs(b[Z] - z) > b[RADIUS], z3one, z3zero)
+    for b in bots
+]
+
+set_param("parallel.enable", True)
+
+opt = Optimize()
+opt.add(n_out_of_range == Sum(bots_out_of_range))
+opt.add(dist_origin == Abs(x) + Abs(y) + Abs(z))
+opt.minimize(n_out_of_range)
+opt.minimize(dist_origin)
+
+res = opt.check()
+m = opt.model()
+print(m[dist_origin])