So I started building a solver for satisfactory for someone. Code is on GitHub if you are bored. It can do similar things, as well as finding optimal recipes and such (like some websites do) but I did it to speed up their app where their current solving of graphical models can be quite slow (20 minutes to solve a model)
I've tried a lot of approaches as a result, including going down the same paths.
The balancer issue is different in particular but in my experience, for this kind of problem, using z3 and cvc5 give much faster result than mnilp solvers or cp-sat. On smaller models they are all quite fast. But as it gets larger it's actually much faster for me to binary search an optimal objective through sat with z3 or cvc5 than it is to ask most nlp solvers to optimize it. I haven't tried gurobi or cplex of course.
But I expect this is because of their ability to do really effective incremental solving so that binary searching the objective is very efficient (z3 has an optimizer and soft constraints but they do not advertise it as supporting non linear logic and I can get it to hang on some models)
Especially for this type of problem, I would consider using an SMT solver and seeing how it does
If you stick with Clos networks, a homegrown solver using bdds is probably quite fast and wildly memory efficient.
How did you learn to work with Z3? I dipped my toes in recently having no prior experience. ChatGPT got me started but once the problem got complex enough I was stumped. I also don’t really have any mathematics ability.
The balancer issue is different in particular but in my experience, for this kind of problem, using z3 and cvc5 give much faster result than mnilp solvers or cp-sat. On smaller models they are all quite fast. But as it gets larger it's actually much faster for me to binary search an optimal objective through sat with z3 or cvc5 than it is to ask most nlp solvers to optimize it. I haven't tried gurobi or cplex of course.
But I expect this is because of their ability to do really effective incremental solving so that binary searching the objective is very efficient (z3 has an optimizer and soft constraints but they do not advertise it as supporting non linear logic and I can get it to hang on some models)
Especially for this type of problem, I would consider using an SMT solver and seeing how it does
If you stick with Clos networks, a homegrown solver using bdds is probably quite fast and wildly memory efficient.