I've been trying to solve 2018; but I'm really stuck at part 2 of day 23

https://adventofcode.com/2018/day/23 -> Link for reminders

I have a written solution (in Python): It starts by checking a (3D) grid of points for bots in range of that point Then it picks the best point of that grid (the one with the most bots; and the one closest to origin after a tie) After that it shrinks the range of the grid, centers it around the previous best point, and repeats.

This repeats until the stepsize in the grid is 1. I can confirm it finds a local optimum (neighbours closer to the origin have less bots in range). I can see how this could miss a global optimum. But I really don't know how to create a solution that finds the global optimum, that will also finish in reasonable time.

If I look at the daily thread; I see only solutions that seem to work through luck (also finding local optimum; but by chance the right one), and a few using Z3. I'd like to avoid using Z3 because I've never used it so I'd just be copy-pasting something I don't really understand.

Any pointers on how to solve this?

Another solution I've been thinking about; but can't fully finish in my head: Looking at intersections of bot-ranges. It seems like a good solutions; but I feel it will spiral out of control really fast as well (with 1000 bots, there are about ~1million intersections of two bots; and ~1billion intersections of three bots. Will be less because not all are within eachothers range, but most are, so order of magnitude ~1billion). If we need to find the intersection of a few hundred bots; this will be an impossibly large number even after a few steps.