Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)

It's worth noting these notes are 11 years old. The first give-away was the comment that in Python 3/2 is an integer, which is indeed true in Python 2 but not in Py3.

For modern users of Z3, you'd want to do `pip install z3-solver` rather than use `Z3Py` mentioned at the very bottom of this doc.

We care about Z3 because it is a Satisfiability Modulo Theories (SMT) solver.

Satisfiability: In 1971, Stephen A. Cook established that Boolean satisfiability, given an arbitrary Boolean formula whether an assignment to its variables exists that evaluates true, is NP-complete.

https://dl.acm.org/doi/10.1145/800157.805047

Translating between NP-complete problems is at most a polynomial (“fast”) amount of work, so every improvement gained on satisfiability (whose worst case is exponential rather than polynomial time complexity) benefits all other NP-complete problems, and thus the rest of NP.

Modulo Theories: We can think of SMT as a high-level language that automates encoding of other problems into raw Boolean formulas. Applications built on Z3 outsource search by encoding problems via one or more theories and then decoding results back to the problem domain at hand.

The benefits of doing this are (1) using an existing robust, well-tested suite of algorithms where (2) lots of research effort is concentrated and (3) improvements to Z3 improve your problem’s results more-or-less for free. According to Microsoft, “Z3 is used in a wide range of software engineering applications, ranging from program verification, compiler validation, testing, fuzzing using dynamic symbolic execution, model-based software development, network verification, and optimization.”

https://www.microsoft.com/en-us/research/project/z3-3/

See also:

https://github.com/Z3Prover/z3

"SAT/SMT by Example" also contains many Z3 examples (and has a new URL): https://smt.st/

I'm a fan. I've been building a proof assistant directly on the z3py api. https://pypi.org/project/knuckledragger/0.1.3/

Solvers are something that still kind of feel like magic to me. I have done a fair amount of Isabelle, and the "sledgehammer" tool in there (which uses solvers to see if an existing proof can be made to work to solve your subgoal) is something that impresses me every single time I use it.

I have created a Python library called "z4-solver" that adds some nice utility functions on top of z3: https://github.com/Tyilo/z4

I always use that instead of the z3-solver directly.

https://www.hakank.org/z3/

That’s a very clean API.

Very good to see all this in one short page!