A beginner-friendly walkthrough of using the z3 constraint solver via its Rust bindings. Covers core concepts like free constants, sorts, and the SMT-LIB2 language, then progresses through practical examples: solving simple equations, handling multiple solutions, the coin change optimization problem (using the Optimize API with push/pop for multiple totals), Sudoku solving, and a basic page layout problem. The author is candid about their limited experience and focuses on making the API approachable for developers without a formal theorem-proving background.
Table of contents
What are Solvers?A Note on TerminologyA Simple EquationA Jump in ComplexityMultiple SolutionsCoin Change Problempush and popSudokuPage LayoutEpilogueSort: