Solving Logic Puzzles with Microsoft's z3 SAT Soler | Blogmarks

This post walks through how to formulate a logic puzzle as the declarative elements that a SAT solver like z3 knows how to take in. It can then determine if the given elements are satisfiable (SAT) or not (UNSAT). It can also produce the set of values that make it SAT which is then a solution to the puzzle.

Here is the GitHub project for z3: https://github.com/Z3Prover/z3