SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
复制标题
SAT 求解具有递归路径顺序和依赖对的终止证明
DOI：
10.1007/s10817-010-9211-0
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
R. Thiemann
中科院分区：
文献类型：
--
作者：
M. Codish;J. Giesl;P. Schneider-Kamp;R. Thiemann
本文介绍了一种与依赖对有关的递归路径序（RPO）的命题编码。因此，我们在统一的设置中捕获RPO的所有常见实例，即，词典路径顺序（LPO）、多集路径顺序（MPO）和具有状态的词典路径顺序（LPOS）。这有利于SAT求解器的终止分析的长期重写系统（TRS）的应用。我们解决了四个主要的相互关联的问题，并展示了如何将它们编码为命题公式的可满足性问题，可以有效地处理SAT解决：（A）字典比较w.r.t.变元;（B）基序的多集扩展;（C）结合路径序和参数过滤器来定向不等式集;（D）参数过滤器的选择如何影响必须定向的不等式集（所谓的可用规则）。我们已经在终止证明程序AProVE中实现了我们的贡献。大量的实验表明，通过我们的编码和SAT求解器的应用程序，获得了数量级的加速，以及增加终止证明功率。
This paper introduces a propositional encoding for recursive path orders (RPO), in connection with dependency pairs. Hence, we capture in a uniform setting all common instances of RPO, i.e., lexicographic path orders (LPO), multiset path orders (MPO), and lexicographic path orders with status (LPOS). This facilitates the application of SAT solvers for termination analysis of term rewrite systems (TRSs). We address four main inter-related issues and show how to encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (A) the lexicographic comparison w.r.t. apermutationof the arguments; (B) themultiset extensionof a base order; (C) the combined search for a path order together with anargument filterto orient a set of inequalities; and (D) how the choice of the argument filter influences the set of inequalities that have to be oriented (so-calledusable rules). We have implemented our contributions in the termination prover AProVE. Extensive experiments show that by our encoding and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.
登录
查看更多内容
DOI：
10.1145/1599410.1599442
发表时间：
2009-09
期刊：
--
影响因子：
--
作者：
M. Codish;S. Genaim;Peter James Stuckey
通讯作者：
M. Codish;S. Genaim;Peter James Stuckey
多项式解释的重写系统终止及其实现
影响因子：
1.3
作者：
Ahlem Ben Cherifa;P. Lescanne
通讯作者：
P. Lescanne
通过 SAT 模线性算术求解非线性多项式算术
DOI：
--
发表时间：
2009
期刊：
CADE
影响因子：
--
作者：
C. Borralleras;Salvador Lucas;Rafael Navarro;Enric Rodríguez;A. Rubio
通讯作者：
A. Rubio
使用惰性 CNF 转换方案改进 Coq 命题推理
影响因子：
2.9
作者：
Stéphane Lescuyer;S. Conchon
通讯作者：
S. Conchon
关于递归路径排序
影响因子：
1.1
作者：
M. Krishnamoorthy;P. Narendran
通讯作者：
P. Narendran