On: The Little Prover

[schoen]

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)