不同的SMT解算器之间有比较吗？

Question

我在Python中有一个利用定理证明的实现。我想知道是否有可能加快SMT的解决部分，目前正在使用Z3。

我试图发现不同的求解者，并发现cvc5 4/cvc5 5和y是多元理论(算术，等式，位向量.)解决者。我还找到了dReal和MetiTarski (这一项似乎已经过时了)用于实际算术的具体情况。

我的目的是用这些工具的API测试我的实现，看看我是否可以使用一个或其他的解决程序，这取决于我想要解决的类型。

然而，我想事先知道，这些求解者之间是否有某种比较，以便为我的发现提供一个更有用的基础。我对GitHub或Stack中的标准基准测试或用户测试都感兴趣。

我只找到了cvc5 (https://www-cs.stanford.edu/~preiner/publications/2022/BarbosaBBKLMMMN-TACAS22.pdf)的这篇文章，很明显，它是最好的选择。我还发现了这个极小的比较(https://lemire.me/blog/2020/11/08/benchmarking-theorem-provers-for-programming-tasks-yices-vs-z3/)，它告诉我们Yices比具体示例的Z3快15倍。

有什么建议吗？

https://yices.csl.sri.com/

• cvc5：https://cvc5.github.io/

• dReal：http://dreal.github.io/

• MetiTarski：https://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html

：

• Yice

Answer 1

您可以随时查看SMT竞赛的结果：https://smt-comp.github.io

话虽如此，我认为寻找“最好的”是傻瓜的差事。用一种有意义的方式来比较所有的求解者，没有一个好的院子:这都取决于您的特定应用程序。

如果您的系统允许使用多个后端解决程序，那么为什么不利用现代机器上的许多核心:生成所有这些核心并利用第一个完成的结果。任何先验选择的解决者将遭受的情况下，另一个将表现得更好。在这一点上，运行所有可用的，并取得最快的结果是最好的选择，利用您的硬件。