Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]

In my limited experience trying both on a couple CTF problems this last year (although having used Z3 a plenty for years before that), they're not even in the same ballpark. CVC5 is ridiculously good.

I do recall that for real number theory, CVC4 and Z3 have very different models though. I don't recall which one uses which model though, and I'm not sure if CVC5 uses the same model. I don't use either of them for real number arithmetic anyway.

Cvc5 will likely be better if you use strings a lot, or other exotic theories.

The paper had a comparison table gainst the prev. version CVC4 and Z3. cvc5 found more solutions than the other 2. Their python API is the same, it's a drop-in replacement against Z3, its C++ Api is better, its solver is better.

I just miss the comparison against lingeling and others. will have to wait for next competition. most cvc4 users, like Isabelle and Ada Spark will upgrade soon.

Decision Procedures [1] is a very good (and quite accessible) overview of the algorithms used in modern sat/smt solvers.

[1]: https://www.decision-procedures.org/

It is indeed magical with largely unpredictable run times, especially once you venture into undecidable fragments (quantified formulas). There is a million heuristics that you can tune (and indeed there have been attempts of using ML for that; ML is mostly useless for the actual reasoning). Using quantifiers with SMT is a bit like programming in Prolog though much more non-deterministic.

However, for the simpler (just NP-complete) problems the run times are more predictable. If your problem has a streight-forward encoding into SMT, you should definitely try it. The common format also makes it relatively easy to swap tools like CVC and Z3.

The basic algorithm is DPLL and the other stuff is mostly clever hacks added on. There is a critical-systems analogy for SAT that supposedly really does go pretty far. SAT problems are like water: below a certain temperature, water is frozen and understandable. By analogy, SAT problems with too many clauses per variable are generally unsatisfiable and it's not too hard to figure that out. Above that temperature, water is liquid and understandable: the corresponding SAT problems tend to be satisfiable. It's only right around the critical temperature that stuff is chaotic and unpredictable, and that's where the hard SAT instances are. When I say that the analogy goes pretty far, I mean that the phenomenon really does get studied using tools of statistical physics. But I don't know anything more about that at the moment.

https://yurichev.com/writings/SAT_SMT_by_example.pdf is a very good tutorial about using SAT solvers, though it doesn't say much about the theory.

The so-far-released portions of Knuth TAOCP vol 4 do discuss SAT solver theory.

Surely you are not using neural networks ! They are quite magical too !

It'd be great if it were less opaque, yes. SMT is a young field (early oughts) with a lot of extremely complicated algorithms jamed together, and there's not a lot of explanations beyond scientific papers. Even then, lots of topic required to implement a solver are not published at all, you need to know experts and ask them directly.

The best way is of course to write a solver, but it's a tremendous amount of work to obtain a system that will most likely have bad performance, and where a single bug can invalidate the correctness of the whole program. Ask me how I know :-). People are working towards proof checking though, so that's at least going to help with trustability.

It's unfortunately a very rapidly evolving field and is difficult to "break into" as far as understanding internals. Though just understanding DLPP is a good start, but ultimately you need a lot of practice and experimenting on your own to get a good intuition for it.

For the record these are problems many "solver-aided" communities struggle with; I'd say the #1 problem that people have with this class of tools is prospective, interested users struggle with the issue of "how can I encode my problem into a SAT instance with reasonable efficiency." I know this because it's my #1 problem!

On the other hand, there are a lot of "straightforward" NP problems you can run into and get good solutions for with little effort though. Binpacking comes up surprisingly often and being able to just throw it at a solver and get a good, generic solution quickly is always nice (not that this is exclusive to SMT solvers, but it's an easy way to get your feet wet at least.)

Yes for SAT atleast. The best results I have seen used graph neural networks which were trained on different classes of problems (ones amendable to local neighborhood search, ones with a small unsatisfiable cores) and neural networks trained on these classes were able to learn some kind of algorithm that works on these but they were not competitive in terms of performance if one uses a traditional solver. Generalization inside a problem class was shown but there was no meaningful generalisation between problem classes.