ali*_*ias 12
与任何有关求解器性能的问题一样,不可能进行概括.Christoph Wintersteiger(/sf/users/60897651/)将成为此专家,但我不确定他是如何密切关注这一群体的.克里斯:如果你正在读这篇文章,我很想听听你的想法!
这里也存在比较苹果到橙子的风险:Reals和Floats是两种完全不同的逻辑,具有不同的决策程序,启发式算法,算法等.我相信你可以找到一个比另一个更优秀的问题,没有明确的"表演"获胜者.
说了这么多,这里有一些使浮点(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.您可以看到它支持的无数操作,并了解复杂性.