SAT求解用于论据过滤
摘要：拟提议以依赖对为基础的词项重写系统的终结性分析中的词典路径排序的命题编码。这有助于将SAT求解器应用于基于依赖对方法的终止性分析。我们讨论了两个主要相关问题，并将它们编码为可以被SAT求解器高效处理的命题公式的可满足性问题：（1）在词典路径排序的同时搜索满足参数过滤条件的集合不等式;以及（2）参数过滤的选择如何影响必须被排序的不等式集合。我们在终止证明验证器AProVE中实现了我们的贡献。大量实验证明，通过我们的编码和应用SAT求解器，可以获得数量级的加速以及增加的终止证明能力。
作者：Michael Codish (1), Peter Schneider-Kamp (2), Vitaly Lagoon (3), Ren''e Thiemann (2), J"urgen Giesl (2) ((1) Department of Computer Science, Ben-Gurion University, Israel (2) LuFG Informatik 2, RWTH Aachen, Germany (3) Department of Computer Science and Software Engineering, University of Melbourne, Australia)
论文ID：cs/0605074
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23