Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
复制标题
通过 SAT 模线性算术求解非线性多项式算术
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
A. Rubio
中科院分区：
文献类型：
--
作者：
C. Borralleras;Salvador Lucas;Rafael Navarro;Enric Rodríguez;A. Rubio
多项式约束求解在工程和软件验证的几个领域中扮演着重要的角色。具体地说，多项式约束求解在证明程序终止性的工具开发方面有着悠久而成功的历史。最近提出了众所周知的非常有效的技术，如SAT算法和工具，并用于通过适当的编码来实现多项式约束求解算法。然而，像SMT(SAT模理论)方法提供的用于线性算术约束(超过有理数)的强大技术到目前为止还没有得到充分的探索。在本文中，我们证明了使用这些技术开发多项式约束求解器的性能优于现有的最好的求解器，并为为终止证明器实现更好和更通用的求解器提供了一种新的强有力的方法。
Polynomial constraint-solving plays a prominent role in several areas of engineering and software verification. In particular, polynomial constraint solving has a long and successful history in the development of tools for proving termination of programs. Well-known and very efficient techniques, like SAT algorithms and tools, have been recently proposed and used for implementing polynomial constraint solving algorithms through appropriate encodings. However, powerful techniques like the ones provided by the SMT (SAT modulo theories) approach for linear arithmetic constraints (over the rationals) are underexplored to date. In this paper we show that the use of these techniques for developing polynomial constraint solvers outperforms the best existing solvers and provides a new and powerful approach for implementing better and more general solvers for termination provers.