- 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.
- I do software verification. In my experience, Z3 is consistently but noticeably better than CVC5 at the kinds of problems we generate, though the two tools are close enough that you definitely want to architect your verification tool to be able to use either one (or both at once, in case you hit a problem which is pathological in one but not the other).
One place where Z3 exposes a superior interface to CVC5 is when you want to do term simplification. CVC5 does not have any real analogue to Z3's simplification tactics (like ctx-solver-simplify), so if you want to take a term and simplify it with respect to a set of assumptions, Z3 is your only choice. I think CVC5 has all the machinery you need to implement that stuff inside of it, but as a user you can't access it.
The place where CVC5 really pulls ahead of Z3 is when you want to produce proofs (eg, to integrate SMT solving into a proof assistant like Lean, HOL, or Rocq). Both tools have support for generating proofs, but CVC5's are noticeably less buggy, to the point that Lean's SMT integration uses CVC5, even though Leo de Moura (Lean's designer) was also the original designer of Z3.
- I'm curious as to why Z3 is so much more popular than CVC5 if CVC5 is better for solving complex problems. Is it because Z3 is older?
- That’s interesting. I’m a logic designer too. How do you make use of it?
- One of two cases: pushing Verilog through yosys-smtbmc to check design assertions/properties, or writing a lil Python model of some optimisation trick and checking it's equivalent to a more direct implementation.
For the former it's useful when there's already a well-defined contract at some interface, like "this bus interface follows these basic AHB5 manager rules" or "if x_valid is asserted, it remains asserted until x_ready is asserted, and the other x_foobar are stable during that time" or "a FIFO is never both empty and full".
Simple properties + exhaustive checking is good bang-for-buck because it often teases out subtle tangential issues without having to write checks for implementation details. This isn't "formal verification" per se but using formal checks in a lightweight way to help find bugs and inconsistencies in your design.
- What would u recommend for freight/trucking optimiser? not real time.
(scaling to 100s-1000s of units)
- 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
- You learn how to use tools to solve problems and what kind of problems those tools can solve.
Using a database or 3D Printer isn't bad because you don't learn anything about the internals.
- It's still better than using AI, where even the authors of the black box don't really know what they're doing.
- to be fair that's the general experience with such solvers
step 1: insert the problem
step 2: ???
step 3: profit
- 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?
- Like any interview, randomly. Some of them will think it's amazing, clever person, chose the best tool for the job. Other will think it's weird, person is too clever, chose the worst tool for the job.
It totally depends for WHAT you're interviewing, but unlikely the company will want Z3-backed code, so most reactions would be the later.
- If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++.
- I'm not sure I understand your argument. Z3's API is canonically C. There's a C++ wrapper that works pretty well. I don't have experience with the Rust wrapper, but I'd imagine that works pretty well too.
- What solver would you have them use? Z3 is very mature and the Rust bindings are pretty good in my (limited) experience.
- I would write the tutorial in C++, for a more direct experience.
- There's nothing "more direct" - the different APIs for different languages call into the same underlying library, and most of them are more accessible and easier to work with than C++.
Z3 is presumably written in C++ for performance, but without data I am very confident the vast majority of programs that use Z3 consume it via one of the other APIs.
- I personally like to avoid the “writing in C++” experience. :/
- The authors of a powerful solver package thought differently.
- It might have more to do with the first release of Z3 being in 2012, with the first stable Rust release being in 2015. Rather than the authors of Z3 passing some kind of judgment on Rust…
- Z3 uses a sophisticated and fast garbage collection scheme internally that doesn't mesh well with Rust idioms.
- It's reference-counted at the boundaries. See https://github.com/Z3Prover/z3/blob/daf2506b6002149d531cb6c9...
- The authors of a powerful solver package were solving a different problem than the users of a powerful solver package, and so different tools may be appropriate.
- The author might not know C++ and you don't need to use C++ to effectively use z3.
