I actually did try ILP, see https://stackoverflow.com/questions/79422270/why-is-my-z3-an...
I tried Z3 and OR Tools. I didn't try Gurobi. But this was enough to make me think ILP was a dead end. (There were a lot of dead ends in this project.)
I don't know much about integer programming, though, and I'd love to be proven wrong.
I saw that! In my experience, problems that seem completely intractable using open source tools often get solved in seconds using state of the art commercial approaches.