Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

homepages.dcc.ufmg.br

Post reply on HN
Print view View original

11–18 of 18 posts

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

#11

Post by freemint »

mmoskal wrote: post #7
EFruit wrote: post #2

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.

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 (jus…

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?

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

#13

Post by procedurecall »

41b696ef1113 wrote: post #12

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.

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.

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

#14

Post by pcarbonn »

EFruit wrote: post #2

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.

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

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

#15

Post by c-cube »

41b696ef1113 wrote: post #12

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.

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

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

#16

Post by c-cube »

EFruit wrote: post #2

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.

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.

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

#17

Post by aseipp »

EFruit wrote: post #2

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.

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.)

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

#18

Post by rurban »

41b696ef1113 wrote: post #12

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.

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.

Post reply on HN