SAT Solving for Termination Analysis with Polynomial Interpretations

SAT Solving for Termination Analysis with Polynomial Interpretations
复制标题

SAT 求解多项式解释的终止分析

DOI:
--
复制
发表时间:
2007
期刊:
International Conference on Theory and Applications of Satisfiability Testing
影响因子:
--
通讯作者:
Harald Zankl
Harald Zankl
中科院分区:
--
文献类型:
--
作者:
Carsten Fuhs;J. Giesl;A. Middeldorp;Peter Schneider;René Thiemann;Harald Zankl

文献摘要

参考文献

被引文献

相似文献

多项式解释是自动终止分析中最流行的技术之一,而寻找这样的解释是大多数终止证明者的主要瓶颈。我们表明,通过将该任务编码为SAT问题并应用现代SAT解算器,可以获得数量级的加速比。
Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination provers. We show that one can obtain speedups in orders of magnitude by encoding this task as a SAT problem and by applying modern SAT solvers.
SOFSEM 2007:计算机科学的理论与实践
DOI: 10.1007/978-3-540-69507-3_15
发表时间: 2007
期刊: --
影响因子: --
作者:
Broersma H
通讯作者: Broersma H