3 ms·
I actually wasn't aware of this either. Z3 is fine with it--its job is to find any satisfying model. The possible outcomes are "the puzzle is solvable and here
by joek1301 1y ago
I actually wasn't aware of this either.
Z3 is fine with it--its job is to find any satisfying model. The possible outcomes are "the puzzle is solvable and here's a solution" or "the puzzle isn't solvable."
- mzl 1y agoWhen using minizinc or other constraint programming tools to solve puzzles that require a single solution, I typically run them asking for 2 solutions. If I get 1 solution only, I know the puzzle is well formed, if I get more than one solution I know the puzzle is mal-formed. For example, in https://zayenz.se/blog/post/benchmarking-linkedin-queens/#test-instances https://zayenz.se/blog/post/benchmarking-linkedin-queens/#te... I took a large number of LinkedIn Queens puzzles, and I filtered out the ones that were not well-formed so that they wouldn't mess up the benchmarking and statistics.