浮点 SMT 逻辑是否比真实逻辑慢？
Are floating point SMT logics slower than real ones?
我在 Haskell 中编写了一个应用程序，它调用 Z3 解算器来解决一些复杂公式的约束。感谢 Haskell 我可以快速切换我正在使用的数据类型。
当使用 SBV 的 AlgReal 类型进行计算时，我在合理的时间内得到了结果，但是切换到 Float 或 Double 类型会使 Z3 消耗 ~2Gb 的 RAM 而不会即使在 30 分钟内也能得到结果。
这是预期生成浮点解决方案需要更多时间，还是我这边的一些错误？
与有关求解器性能的任何问题一样，无法一概而论。 Christoph Wintersteiger (https://whosebug.com/users/869966/christoph-wintersteiger) 是对此发表意见的专家，但我不确定他对这个小组的关注程度。克里斯：如果你正在读这篇文章，我很想听听你的想法！
这里也有比较苹果和橘子的风险：实数和浮点数是两种完全不同的逻辑，具有不同的决策程序、启发式算法、算法等。我相信您会发现其中一个优于其他，没有明确的 "performance" 获胜者。
说了这么多，这里有一些让浮点 (FP) 变得棘手的事情：
用 FP 重写几乎是不可能的，因为像关联性这样的规则很简单
不支持 FP addition/multiplication。所以机会比较少
位爆破前的简化。
同样，a * 1/a == 1 不适用于浮点数。 x + 1 /= x 或 (x + a == x) -> (a == 0) 以及您希望能够进行的许多其他 "obvious" 简化也没有。所有这些都使推理复杂化。
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。您可以看到它支持的无数操作并了解其复杂性。
我在 Haskell 中编写了一个应用程序，它调用 Z3 解算器来解决一些复杂公式的约束。感谢 Haskell 我可以快速切换我正在使用的数据类型。
当使用 SBV 的 AlgReal 类型进行计算时，我在合理的时间内得到了结果，但是切换到 Float 或 Double 类型会使 Z3 消耗 ~2Gb 的 RAM 而不会即使在 30 分钟内也能得到结果。
这是预期生成浮点解决方案需要更多时间，还是我这边的一些错误？
与有关求解器性能的任何问题一样，无法一概而论。 Christoph Wintersteiger (https://whosebug.com/users/869966/christoph-wintersteiger) 是对此发表意见的专家，但我不确定他对这个小组的关注程度。克里斯：如果你正在读这篇文章，我很想听听你的想法！
这里也有比较苹果和橘子的风险：实数和浮点数是两种完全不同的逻辑，具有不同的决策程序、启发式算法、算法等。我相信您会发现其中一个优于其他，没有明确的 "performance" 获胜者。
说了这么多，这里有一些让浮点 (FP) 变得棘手的事情：
用 FP 重写几乎是不可能的，因为像关联性这样的规则很简单 不支持 FP addition/multiplication。所以机会比较少 位爆破前的简化。
同样，
a * 1/a == 1不适用于浮点数。x + 1 /= x或(x + a == x) -> (a == 0)以及您希望能够进行的许多其他 "obvious" 简化也没有。所有这些都使推理复杂化。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。您可以看到它支持的无数操作并了解其复杂性。