Natural Domain SMT: A Preliminary Assessment
Natural Domain SMT: A Preliminary Assessment
复制标题
Natural Domain SMT：初步评估
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Scott Cotton
中科院分区：
文献类型：
--
作者：
Scott Cotton
SMT解算器传统上基于DPLL(T)算法，其中该过程背后的驱动力是对真值的DPLL搜索。这种传统的框架允许在处理理论解算器时具有一定程度的模块化。随着时间的推移，理论解算器越来越紧密地集成到DPLL过程中，因此模块化程度越来越低。在本文中，我们提出了一种求解SMT问题的类DPLL算法，其中的搜索是在问题中变量的自然域上进行的。作为一个实例，我们分析了它在连续域线性运算中的应用，给出了实现技术，并用差分逻辑进行了一些实验。结果表明，该方法有时可以超越领先的SMT求解器，但该方法还不是很健壮。
SMT solvers have traditionally been based on the DPLL(T) algorithm, where the driving force behind the procedure is a DPLL search over truth valuations. This traditional framework allows for a degree of modularity in the treatment of theory solvers. Over time, theory solvers have become more and more closely integrated into the DPLL process, and consequently less and less modular. In this paper, we present a DPLL-like algorithm for SMT solving in which the search takes place over the natural domain of the variables in the problem. As a case study, we analyze its application to continuous domain linear arithmetic, present implementation techniques and some experimentation with difference logic. Results indicate the method can sometimes outperform leading SMT solvers but that the method is not yet robust.