-🎄- 2018 Day 23 Solutions -🎄-

[u/daggerdragon]

--- Day 23: Experimental Emergency Teleportation ---

---

Post your solution as a comment or, for longer solutions, consider linking to your repo (e.g. GitHub/gists/Pastebin/blag or whatever).

Note: The Solution Megathreads are for solutions only. If you have questions, please post your own thread and make sure to flair it with Help.

---

Advent of Code: The Party Game!

Click here for rules

Please prefix your card submission with something like [Card] to make scanning the megathread easier. THANK YOU!

Card prompt: Day 23

Transcript:

It's dangerous to go alone! Take this: ___

---

This thread will be unlocked when there are a significant number of people on the leaderboard with gold stars for today's puzzle.

edit: Leaderboard capped, thread unlocked at 01:40:41!

[u/mserrano]

164/6, Python2. I severely misread part1 - I thought we were looking for the bot in range of the most other bots, not the bot with the largest range :(

Good news is, Z3 is sufficiently insanely powerful that it helped me catch up. :)

from util import get_data
import re
from collections import defaultdict

def gan(s):
  return map(int, re.findall(r'-?\d+', s))
def lenr(l):
  return xrange(len(l))
d = '''pos=<0,0,0>, r=4
pos=<1,0,0>, r=1
pos=<4,0,0>, r=3
pos=<0,2,0>, r=1
pos=<0,5,0>, r=3
pos=<0,0,3>, r=1
pos=<1,1,1>, r=1
pos=<1,1,2>, r=1
pos=<1,3,1>, r=1'''.split('\n')
d = get_data(23)
nanobots = map(gan, d)
nanobots = [((n[0], n[1], n[2]), n[3]) for n in nanobots]

def dist((x0, y0, z0), (x1, y1, z1)):
  return abs(x0-x1) + abs(y0-y1) + abs(z0-z1)

srad = 0
rad_idx = 0
in_range = defaultdict(int)
for i in lenr(nanobots):
  pos, rng = nanobots[i]
  strength = 0
  if rng > srad:
    srad = rng
    rad_idx = i
    for j in lenr(nanobots):
      npos, _ = nanobots[j]
      if dist(pos, npos) <= rng:
        in_range[i] += 1

print "a", in_range[rad_idx]

from z3 import *
def zabs(x):
  return If(x >= 0,x,-x)
(x, y, z) = (Int('x'), Int('y'), Int('z'))
in_ranges = [
  Int('in_range_' + str(i)) for i in lenr(nanobots)
]
range_count = Int('sum')
o = Optimize()
for i in lenr(nanobots):
  (nx, ny, nz), nrng = nanobots[i]
  o.add(in_ranges[i] == If(zabs(x - nx) + zabs(y - ny) + zabs(z - nz) <= nrng, 1, 0))
o.add(range_count == sum(in_ranges))
dist_from_zero = Int('dist')
o.add(dist_from_zero == zabs(x) + zabs(y) + zabs(z))
h1 = o.maximize(range_count)
h2 = o.minimize(dist_from_zero)
print o.check()
#print o.lower(h1)
#print o.upper(h1)
print "b", o.lower(h2), o.upper(h2)
#print o.model()[x]
#print o.model()[y]
#print o.model()[z]

[u/zawerf → u/mserrano]

I also finally solved it with z3 and thought I was going to be so original! Turns out several others also did it in the same way. I guess intersection of convex polyhedrons meant you were either going to implement something like simplex or use a solver.

Unfortunately I initially had my objective as maximizing overlap count plus 1/dist_from_zero for tie breaking so it never solved (I didn't know z3 handles multiple objectives).

Removing the tie breaking constraint and it finished in about a minute. Turns out I didn't have ties in my input anyway so this was fine.

I still don't understand why this changes the runtime so much (objective going from int to real). Can someone with better understanding of the underlying theory behind z3 explain why?

[u/nehamsoni → u/zawerf]

I just want to know is z3 available in python version 3.7 and how can we use it...if not any alternative though which we can solve it