对编程任务的定理证明者进行基准测试：YICES与Z3

大多数程序员应该知道的一个巧妙的工具家族是“定理证明器”。如果你读的是计算机专业的大学，你可能已经接触到了…。但在编程时，您可能不会考虑使用它们。

虽然我确信它们可以用来证明定理，但我从来没有用过它们来证明定理。它们对于快速检验一些假设和找到有用的常数很有用。让我举一个简单的例子。

我们知道软件中的无符号奇数有乘法逆数。也就是说，如果给你一个数字3，你可以找到另一个数字，这样当你把它与3相乘时，你就会得到1。有一些高效的算法可以找到这样的乘法逆，但定理证明者可以在没有任何麻烦或领域知识的情况下做到这一点。您可以编写以下Python程序：

它的回报率将达到12297829382473034411。作为64位无符号整数，如果你用12297829382473034411乘以3，你会得到1。如果没有可能的解，定理证明者也会告诉你。所以它可以找到有用的常量，或者证明找不到常量。

对于一些相关的任务，我一直在使用流行的Z3定理证明器，它对我非常有用。但它有时可能会很慢。所以我向Geoff Langdale请教，他推荐了yices，另一种定理证明器，对于程序员所做的那种工作来说可能更快，例如，使用固定位整数值。

虽然我信任杰夫，但我想得出一些衡量标准。因此，我构建了以下基准。对于0到1000之间的所有整数，我尝试找一个乘法逆数。它并不总是有效的(即使数字没有倒数)，但定理证明者将会弄清楚这一点。

所以，至少在这一次测试中，yices的速度是z3的15倍。我的Python脚本可用。您可以使用标准的pip工具安装z3和yices。请注意，您的系统上应该有yices，但作者提供了简单的说明。

我发现与Z3相比，yices的Python接口相当麻烦。因此，如果性能不是问题，Z3可能会为您提供很好的服务。

但为什么要提到业绩呢？回到上面的数字。要在15秒内解决1000个反问题，按每个数字计算真的是相当慢的。它大约是每个数字6000万个CPU周期。这是一个很容易解决的问题。当你开始提出更复杂的问题时，定理证明者可能很快就会变得无法使用。能够只快10倍的速度在实践中会产生很大的不同。

警告：这只是一次测试，它不能以任何方式确定YICS相对于Z3的优势(总体上)。