SAT Modulo Non-Linear Arithmetic for Termination Analysis

 

 

Carsten Fuhs

 

 

Abstract:
Efficiently solving non-linear polynomial constraints plays an important
role for many techniques in automated termination analysis, such as
polynomial interpretations. We present both the classical setting,
where polynomials with coefficients from the natural numbers are used,
and several recent extensions to max-polynomials and to polynomials
over the reals.

In these settings, the current state of the art for solving constraints
from SAT modulo non-linear arithmetic is represented by an eager
encoding: Not only is the Boolean structure of the constraints
represented on logical level, but also the atomic arithmetical
constraints themselves are encoded to SAT. Then the actual search is
performed by a modern SAT solver like MiniSAT, which does not employ
dedicated domain knowledge for arithmetic. This way, we have achieved
speed improvements by orders of magnitude over earlier dedicated
techniques for solving such constraints.

An interesting challenge now is to combine the efficiency of modern SAT
solvers with dedicated techniques that operate directly on non-linear
arithmetic. This way, one could obtain a technique that combines the
best of both worlds and potentially outperforms the current methods
based on eager encodings.