Day 24 p2 - Z3 linear programming can't solve it
Until today, I had a certainty in life, that if you can model your problem as a Linear Programming problem any solver like z3 would solve it in an instant.
I did so for the day 24 part 2, but the solver never came back with an answer.
For people who know LP, do you think is there something with this type of problem that makes it hard to solve by the solver? Or do I just have a bug in my code?
The idea of my solution is that you add all the circuits as constraints, plus the input x,y and the output z.
Then, we add a layer after every output, that allow to swap the "original" output with another "original" output. The inputs, always use the "non-original" version after a potential swap, the swap are decided by z3 solver, that will try allow only 4 swaps.