[Club2] Mi. 26.8., 14h im Turing (00.09.055): Carsten Fuhs

[Alexander Krauss]

Title:
     SAT Modulo Non-Linear Arithmetic for Termination Analysis


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.