Deciding floating-point logic with abstract conflict driven clause learning
Deciding floating-point logic with abstract conflict driven clause learning
复制标题
DOI：
10.1007/s10703-013-0203-7
复制
发表时间：
2014-10-01
影响因子：
0.8
通讯作者：
Kroening, Daniel
中科院分区：
文献类型：
--
作者：
Brain, Martin;D'Silva, Vijay;Kroening, Daniel
我们为浮点算术理论提供了一个精确的决策程序。我们方法的核心是对现代SAT求解器中的冲突驱动子句学习算法对基于晶格的抽象的非平凡的晶格理论概括。我们使用浮点间隔来推理变量范围，这使我们能够直接处理算术，并且比将公式作为比特矢量更有效，就像当前的浮点求解器一样。仅间隔推理是不完整的，我们通过开发一种在间隔内的冲突分析算法来获得完整性。我们已经在MathSAT5 SMT求解器中实现了此方法，并根据绑定程序变量值的断言检查问题进行了评估。我们的新技术比80％的基准测试的比特矢量编码方法要快，并且在60％的基准测试的基准下，按一个数量级或更高的速度更快。我们提出的CDCL的概括非常适用，可用于为其他理论得出基于抽象的SMT求解器。
We present a bit-precise decision procedure for the theory of floating-point arithmetic. The core of our approach is a non-trivial, lattice-theoretic generalisation of the conflict-driven clause learning algorithm in modern SAT solvers to lattice-based abstractions. We use floating-point intervals to reason about the ranges of variables, which allows us to directly handle arithmetic and is more efficient than encoding a formula as a bit-vector as in current floating-point solvers. Interval reasoning alone is incomplete, and we obtain completeness by developing a conflict analysis algorithm that reasons natively about intervals. We have implemented this method in the MATHSAT5 SMT solver and evaluated it on assertion checking problems that bound the values of program variables. Our new technique is faster than a bit-vector encoding approach on 80 % of the benchmarks, and is faster by one order of magnitude or more on 60 % of the benchmarks. The generalisation of CDCL we propose is widely applicable and can be used to derive abstraction-based SMT solvers for other theories.