Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
homepages.dcc.ufmg.br
Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
1–10 of 18 posts
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#2I 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.
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#3I 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.
Decision Procedures [1] is a very good (and quite accessible) overview of the algorithms used in modern sat/smt solvers.
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#4For 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.
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#5Has anyone tried machine learning techniques on these problems?
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#6Great to see such tools growing stronger. Writing proofs in Isabelle/Coq/... is still hard and assistance from tools like this is very much welcome.
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#7I 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.
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.
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#8I 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.
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.
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#9I 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.
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, wate…
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.
Re: Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
#10Has anyone tried machine learning techniques on these problems?
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.