2

I have an implementation in Python that makes use of theorem proving. I would like to know if there is a possibility to speed up the SMT solving part, which is currently using Z3.

I am trying to discover different solvers, and have found cvc4/cvc5 and Yices as multiple-theory (arithmetics, equality, bitvectors...) solvers. I also found dReal and MetiTarski (this one seems to be out to date) for the concrete case of real arithmetics.

My intention is to test my implementation with those tools' APIs to see whether I can use one or other solver depending on the sort I want to solve.

However, I would like to know in advance if there is some kind of comparison between these solvers in order to have a more useful foundation for my findings. I am interested in both standard benchmarks or user-tests out there in GitHub or Stack.

I only found this paper of cvc5 (https://www-cs.stanford.edu/~preiner/publications/2022/BarbosaBBKLMMMN-TACAS22.pdf), which, obviously suggests it as the best option. I also found this minimal comparison (https://lemire.me/blog/2020/11/08/benchmarking-theorem-provers-for-programming-tasks-yices-vs-z3/) that tells us Yices is 15 times faster than Z3 for a concrete example.

Any advise?

Theo Deep
  • 666
  • 4
  • 15
  • Requests for external resources are [off-topic](https://stackoverflow.com/help/on-topic) on Stack Overflow. I understand that you are not asking us to recommend a *solver*, but you are requesting us to find some sort of existing research or analysis which compares solvers. – kaya3 Sep 15 '22 at 14:36
  • 1
    I think this is a perfectly fine question to ask as it is seeking info on how to take advantage of multiple existing solvers in its essence. And that’s exactly what the SMT competition is for, even though one has to be careful in making overly generalized assumptions. Each problem is unique when it comes to performance. – alias Sep 15 '22 at 14:45
  • 1
    STP has been a favorite of mine for years.. small, fast and easy to learn IMO. Better and faster than Z3 in my experience. – Morten Jensen May 27 '23 at 08:07

1 Answers1

4

You can always look at the results of SMT competition: https://smt-comp.github.io

Having said that, I think it’s a fool’s errand to look for the “best.” There isn’t a good yard stick to compare all solvers in a meaningful way: it all depends on your particular application.

If your system allows for using multiple backend solvers, why not take advantage of the many cores on modern machines: spawn all of them and take the result of first to complete. Any a priori selection of the solver will suffer from a case where another will perform better. At this point, running all available and taking the fastest result is the best option to utilize your hardware.

alias
  • 28,120
  • 2
  • 23
  • 40
  • *"why not take advantage of the many cores on modern machines"* - I suggest taking advantage of this by using a solver which is not single-threaded; no decent solver is. *"At this point, running all available and taking the fastest result is the best option to utilize your hardware."* Highly doubtful - there are lots of available solvers, and on many problems they will have similar performance to each other, so by running all of them you are just increasing your computational costs by some constant factor. In other cases it is surely possible to estimate which solver will perform best. – kaya3 Sep 15 '22 at 14:33
  • 1
    This isn’t my experience. Even different versions of the same solver vary vastly in performance for the same solver. Estimating performance across multiple solvers which you claim is “surely possible” hasn’t been my experience at all, not even for seemingly simple problems across solver versions. – alias Sep 15 '22 at 14:44
  • Thanks a lot! I will play with multi-cores and ask here in case I find problems. – Theo Deep Sep 15 '22 at 14:48