是浮点SMT逻辑比以假乱真慢？

Question

我写在Haskell调用Z3求解器解决制约一些复杂公式的应用程序。由于哈斯克尔我可以快速切换，我处理的数据类型。

当使用SBV的AlgReal类型计算，我得到了合理的时间的结果，但是切换到Float或Double类型使得Z3消费〜2GB的RAM，不会导致甚至在30分钟。

难道这预计生产浮点解决方案需要更多的时间，或者是在我身边的一些错误呢？

Answer 1

正如有关求解器性能的任何问题，这是不可能一概而论。克里斯托夫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除法和余数运算处理，即使在输入完全是具体的，想象一下，当他们完全有象征性的会发生什么！
• 实数的逻辑有一个双指数复杂决策程序。然而，像傅里叶Motzkin的消除（https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination）技术，而其余的指数，在实践中执行得很好。
• FP求解器是相对较新，它与新生研究中的独特领域。因此，现有的解决者往往是相当保守的，快速比特爆炸和减少问题位向量逻辑。我希望他们能够改善随着时间的推移，就像所有其他理论一样。

此外，我想强调的比较这两种不同的逻辑解算器的性能是错误的，因为它们是完全不同的野兽。但我们希望，以上几点说明，为什么浮点在实践中是非常棘手。

一个伟大的纸阅读有关IEEE754的治疗SMT求解浮是：http://smtlib.cs.uiowa.edu/papers/BTRW14.pdf。你可以看到操作的大量支持，并获得复杂的感觉。