线性整数算术可满足性理论中的高效插值生成
计算机科学中的逻辑
2015-07-01 v3
摘要
在SAT和SMT中计算Craig插值的问题近来受到广泛关注，主要源于其在形式化验证中的应用。针对若干重要理论——包括等式与未解释函数、有理数上的线性算术及其组合——已提出了高效的插值生成算法，并成功应用于模型检测工具中。然而，对于整数上的线性算术理论(LA(Z))，寻找插值的问题更具挑战性，为完整LA(Z)理论开发高效插值生成器仍是当前研究的目标。本文试图弥补这一空白。我们基于先前工作，提出了一种针对SMT(LA(Z))的新型插值算法，该算法充分利用了当前最先进的SMT(LA(Z))求解器的全部能力。通过在MathSAT SMT求解器中实现所提算法并进行广泛的实验评估，我们展示了该方法的潜力。
引用
@article{arxiv.1010.4422,
title = {Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic},
author = {Alberto Griggio and Thi Thieu Hoa Le and Roberto Sebastiani},
journal= {arXiv preprint arXiv:1010.4422},
year = {2015}
}