I've used Z3 to create some logic puzzles, but I was using the SAT solver features rather than the proof features. One effective, if naive, approach to determi

I've used Z3 to create some logic puzzles, but I was using the SAT solver features rather than the proof features. One effective, if naive, approach to determining whether a logic puzzle has a unique solution is checking: * is my current constraint set satisfiable? * if so, exhibit a satisfying assignment ("foo") * add a new constraint that explicitly excludes the solution "foo" * is the resulting constraint set satisfiable? * if not, great! (the solution "foo" is unique)