浮点 SMT 逻辑是否比真实逻辑慢？答案

【问题标题】：Are floating point SMT logics slower than real ones?浮点 SMT 逻辑是否比真实逻辑慢？
【发布时间】：2019-06-27 09:46:45
【问题描述】：

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

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

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

【问题讨论】：

我只是半个专家，但我相信，是的，IEEE754 的理论比任意代数实数理论显着复杂，因为每个运算都包含一个舍入很难推理的操作。（不写这个作为答案，因为我只有一半的专家，只有大约 80% 相信我自己的陈述。）
@ThomasM.DuBuisson 哈哈，老实说，如果允许抄送具体用户，我会在问题中添加@LeventErkok。

标签： haskell z3 smt sbv

【解决方案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 除法和余数运算，即使输入完全具体，想象一下当它们完全是符号时会发生什么！
实数逻辑具有双指数复杂度的决策过程。然而，傅里叶-莫茨金消除 (https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination) 等技术虽然保持指数级，但在实践中表现得非常好。
FP 求解器相对较新，是一个新兴研究领域。因此，现有的求解器往往非常保守，并且会快速进行位爆破，并将问题简化为位向量逻辑。我希望它们会随着时间的推移而改进，就像所有其他理论一样。

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

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

【讨论】：

是的，@levent-erkok 所说的一切。请注意，用浮点数/双精度数替换实数不会保留问题或属性的任何语义，即，这是不合理的。关于性能：想象在我们用浮点数替换实数的实数上转换一个微不足道的、完全线性的问题。结果是一个高度非线性和不连续的问题，对于这个问题，没有一个“好的”实数方法可以工作，即使有类似的方法，它们也具有更高的复杂性。