top | item 45269422 (no title) joek1301 | 5 months 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 discuss order hn newest QuadmasterXLII|5 months ago I guess z3 is fine with it, but it confuses me that they decided pips wouldn't have unique solutions joek1301|5 months 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." load replies (1) hwayne|5 months ago I love how you create dataclasses to abstract over constraints!
QuadmasterXLII|5 months ago I guess z3 is fine with it, but it confuses me that they decided pips wouldn't have unique solutions joek1301|5 months 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." load replies (1)
joek1301|5 months 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." load replies (1)
QuadmasterXLII|5 months ago
joek1301|5 months ago
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."
hwayne|5 months ago