Summary

Hillel Wayne shares a collection of Z3 SMT solver examples that were cut from his book Logic for Programmers. He walks through increasingly complex uses: solving systems of equations, proving no four distinct positive integers share both sum and product, optimizing financial contributions, reverse engineering RNG parameters, proving mathematical theorems, and modeling stock trading with Z3 arrays. He explains why most examples didn't make the book's final cut—they either weren't practical enough, required too much background explanation, or weren't the right tool for the job—and describes the three examples he ultimately chose.

Key Insight

Z3 is a remarkably versatile tool that can solve equations, prove theorems, and reverse engineer algorithms, but choosing good pedagogical examples requires balancing accessibility, practicality, and tool-appropriateness.

Spicy Quotes (click to share)

• 6

  You're supposed to learn how to do solve this as a system of equations, but if you want to cheat yourself out of an education you can have Z3 solve this for you.

• 2

  An SMT ("Satisfiability Modulo Theories") solver is a constraint solver that understands math and basic programming concepts.

• 2

  SMT operations must be total for all possible inputs, meaning Select(A, i) must return a value no matter what i is.

• 2

  This means Z3 can find functions that satisfy constraints!

• 5

  Z3's core engine is in C++, and yet a hand-written Python binary search finds the optimal c about a 1000x faster!

• 2

  They should be understandable to someone who is new to logic, they should look like a practical problem some readers might see in their jobs, and SMT solvers should be the right tool for solving them.

• 2

  If you can convert a programming function to a set of Z3 equations you can prove that the function has expected properties.

Tone

playful, pedagogical, self-deprecating