undefined | Better HN

0 pointsjoek13016mo ago0 comments

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."

0 comments

mzl6mo ago

When 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/#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.

j / k navigate · click thread line to collapse

0 pointsjoek13016mo ago0 comments

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."

0 comments

mzl6mo ago

j / k navigate · click thread line to collapse