I have used Codex (Sol 5.6 or whatever) to solve this problem. It turns the problem into Z3, then iteratively work through the problems until it figured out the solution.
Personally, I did not learn that much from that experience. So I am glad that there's other people working on it as well. I am mostly interested in the techniques used to solve this.
Personally, I did not learn that much from that experience. So I am glad that there's other people working on it as well. I am mostly interested in the techniques used to solve this.