Solving Non-linear Polynomial Arithmetic
via SAT Modulo Linear Arithmetic
Authors
Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset,
Enric Rodríguez-Carbonell, and Albert Rubio.
Abstract
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.
Keywords
Constraint solving, polynomial constraints, SAT modulo theories,
termination, program analysis.