4 comments
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.<p>Using a database or 3D Printer isn't bad because you don't learn anything about the internals.
to be fair that's the general experience with such solvers<p>step 1: insert the problem<p>step 2: ???<p>step 3: profit
It's still better than using AI, where even the authors of the black box don't really know what they're doing.
I wonder how often interviewers object to the approach of solving their dynamic programming problem using a constraint solver?
Z3 struggles with larger problems. CVC5 or Bitwuzla do a lot better once you get into anything complex.<p>If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar.<p>Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.
If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++.