浮点SMT逻辑比实际SMT逻辑慢吗？

Question

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

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

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

Answer 1

与任何有关求解器性能的问题一样，不可能进行泛化。Christoph (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除法和剩余操作，即使输入是完全具体的，想象一下当它们是完全象征性的时候会发生什么！
• reals的逻辑有一个双指数复杂度的决策过程.然而，像Fourier-Motzkin消去(elimination)这样的技术，在实践中却表现得很好。
• FP求解器是相对较新的，它是一个新兴的研究领域。因此，现有的求解器倾向于非常保守和快速的比特爆炸，并将问题简化为位向量逻辑。我希望随着时间的推移，他们会有所改善，就像其他理论一样。

再一次，我想强调的是，在这两种不同的逻辑上比较求解者的表现是错误的，因为他们是完全不同的野兽。但希望以上各点说明了为什么浮点在实践中是棘手的.

关于IEEE754浮子在表面活性剂溶液中的处理的一篇很好的论文是：http://smtlib.cs.uiowa.edu/papers/BTRW14.pdf。您可以看到它所支持的无数操作，并了解到它的复杂性。