A Dumb Introduction to Z3 (2025)

This is such weird timing, for the last few weeks I’ve been messing around with Z3 and other solvers for the first time and they’re so cool. In many ways more magical than LLMs to me in some ways. Great intro!

Z3 struggles with larger problems. CVC5 or Bitwuzla do a lot better once you get into anything complex.

If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar.

Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.

Problems solved nothing learned. Poking my problems into a black box and getting numbers let me only learn how to poke numbers into black boxes

Previously: https://news.ycombinator.com/item?id=45248558. Switched domains since then.

I wonder how often interviewers object to the approach of solving their dynamic programming problem using a constraint solver?

If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++.