hide
Free keywords:
Computer Science, Logic in Computer Science, cs.LO
Abstract:
Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of
satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning
for corresponding constraints in SMT theory solvers is highly relevant. We
propose a new incomplete but efficient and terminating method to identify
satisfiable instances. The method is derived from the subtropical method
recently introduced in the context of symbolic computation for computing real
zeros of single very large multivariate polynomials. Our method takes as input
conjunctions of strict polynomial inequalities, which represent more than 40%
of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an
abstraction of polynomials as exponent vectors over the natural numbers tagged
with the signs of the corresponding coefficients. It then uses, in turn, SMT to
solve linear problems over the reals to heuristically find suitable points that
translate back to satisfying points for the original problem. Systematic
experiments on the SMT-LIB demonstrate that our method is not a sufficiently
strong decision procedure by itself but a valuable heuristic to use within a
portfolio of techniques.
