3 ms·
I also was inspired to play around with Z3 after reading a Hillel Wayne article. I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips
by joek1301 1y ago
I also was inspired to play around with Z3 after reading a Hillel Wayne article.
I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips https://kerrigan.dev/blog/nyt-pips
- QuadmasterXLII 1y agoI guess z3 is fine with it, but it confuses me that they decided pips wouldn't have unique solutions
- joek1301 1y agoI 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.
- hwayne 1y agoI love how you create dataclasses to abstract over constraints!