[HN Gopher] Cvc5: Versatile and Industrial-Strength SMT Solver [...
___________________________________________________________________
Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
Author : ingve
Score : 34 points
Date : 2022-03-05 13:54 UTC (9 hours ago)
(HTM) web link (homepages.dcc.ufmg.br)
(TXT) w3m dump (homepages.dcc.ufmg.br)
| todayisfriday wrote:
| For SAT, a problem that is pretty much the poster child for "NP-
| Complete," the progress of SAT solvers over the past couple of
| decades has been nothing short of astounding.
| EFruit wrote:
| I wish the underlying theory to this whole class of software was
| more accessible. It seems like these logical systems can do such
| amazing things, but I'd be remiss to integrate any of them
| without some degree of understanding of what they're doing under
| the hood; what their limitations and failure modes are, etc. As
| it stands, it's all far too magical for me to trust.
| throwaway81523 wrote:
| 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.
| freemint wrote:
| What you just stated about the critical temperature is true
| for some classes of random instances. Early results on larger
| classes of random instances from this line of research do not
| survive scaling experiments. I don't have a reference one
| that but I recall that being said in one of the discussion
| rounds of the Beyond Satisfiability online seminary at the
| Simons Institute.
| mmoskal wrote:
| 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.
| freemint wrote:
| Quantified SAT is decidable. Are you aware of any theories
| where expressions with quantors over finitely many choices
| are unsatisfiable but quantor free expressions are
| satisfiable over the same theory?
| pcarbonn wrote:
| Surely you are not using neural networks ! They are quite
| magical too !
| c-cube wrote:
| 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.
| xwvvvvwx wrote:
| 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/
| amelius wrote:
| Has anyone tried machine learning techniques on these problems?
| freemint wrote:
| 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.
| zaik wrote:
| Great to see such tools growing stronger. Writing proofs in
| Isabelle/Coq/... is still hard and assistance from tools like
| this is very much welcome.
| 41b696ef1113 wrote:
| Anyone have opinions on this vs z3? I started with z3 and have
| never had reason to look elsewhere. Minor performance differences
| do not concern me as much as documentation, (Python) bindings,
| etc quality of life features.
| procedurecall wrote:
| 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.
| c-cube wrote:
| Cvc5 will likely be better if you use strings a lot, or other
| exotic theories.
___________________________________________________________________
(page generated 2022-03-05 23:01 UTC)