haskell - 浮点 SMT 逻辑是否比真实逻辑慢？

Question

我在 Haskell 中编写了一个应用程序，它调用 Z3 求解器来解决具有一些复杂公式的约束。感谢 Haskell，我可以快速切换我正在使用的数据类型。

当使用 SBV 的AlgReal类型进行计算时，我会在合理的时间内得到结果，但是切换到FloatorDouble类型会使 Z3 消耗约 2Gb 的 RAM，甚至在 30 分钟内也不会产生结果。

这是预期产生浮点解决方案需要更多时间，还是我这边的一些错误？

标签： haskellz3smtsbv

Answer 1

与任何关于求解器性能的问题一样，不可能进行概括。Christoph Wintersteiger ( https://stackoverflow.com/users/869966/christoph-wintersteiger ) 将是这方面的专家，但我不确定他对这个群体的关注程度。克里斯：如果你正在读这篇文章，我很想听听你的想法！

在这里比较苹果和橙子也有风险：实数和浮点数是两种完全不同的逻辑，具有不同的决策程序、启发式、算法等。我相信你会发现一个优于另一个的问题，没有明确的“性能”赢家。

说了这么多，这里有一些使浮点（FP）变得棘手的事情：

• 使用 FP 重写几乎是不可能的，因为像关联性这样的规则根本不适用于 FP 加法/乘法。因此，在位爆破之前进行简化的机会较少。

• 同样a * 1/a == 1不适用于浮动。您希望能够进行的许多其他“明显”简化也x + 1 /= x没有。(x + a == x) -> (a == 0)所有这些都使推理复杂化。

• 价值观的存在NaN使平等不具有反身性：没有什么比NaN包括自身更平等。因此，用等号代替等号也是有问题的，并且需要附带条件。

• 同样， 和 的存在+0，-0它们比较相等但由于四舍五入而表现不同，这使事情变得复杂。典型的例子是x == 0 -> fma(a, b, x) == a * b不成立的（其中fma是融合乘加），因为根据零的符号，这两个表达式可以为不同的舍入模式产生不同的值。

• 浮点数与整数和实数的组合引入了非线性，这始终是求解器的软肋。因此，如果您使用 FP，建议不要将其与其他理论混合，因为组合本身会产生额外的复杂性。

• 诸如乘法、除法和余数之类的运算（是的，有一个浮点余数运算！）本质上是非常复杂的，并且会导致非常大的 SAT 公式。特别是，由于缺乏任何良好的变量排序和拆分启发式算法，乘法是一种挑战大多数 SAT/BDD 引擎的已知操作。求解器很快就完成了位爆破，从而产生了非常大的状态空间。我观察到，即使输入完全具体，求解器也很难处理 FP 除法和余数运算，想象一下当它们完全是符号时会发生什么！

• 实数逻辑有一个具有双指数复杂度的决策过程。然而，像 Fourier-Motzkin 消除 ( https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination ) 这样的技术虽然保持指数级，但在实践中表现得非常好。

• FP 求解器相对较新，它是一个新兴研究的利基领域。因此，现有的求解器往往非常保守，并且会快速进行位爆破，并将问题简化为位向量逻辑。我希望它们会随着时间的推移而改进，就像所有其他理论一样。

再次强调，比较求解器在这两种不同逻辑上的性能是被误导的，因为它们是完全不同的野兽。但希望以上几点说明了为什么浮点在实践中很棘手。

一篇关于 SMT 求解器中 IEEE754 浮点数处理的好论文是：http ://smtlib.cs.uiowa.edu/papers/BTRW14.pdf 。您可以看到它支持的无数操作并了解其复杂性。