|
Title:
|
SAT Modulo Linear Arithmetic for Solving Polynomial
|
|
Author:
|
Borralleras Andreu, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert
|
|
Other authors:
|
Universitat de Vic. Escola Politècnica Superior; Universitat de Vic. Grup de Recerca en Tecnologies Digitals |
|
Notes:
|
Polynomial constraint solving plays a prominent role in several areas of
hardware and software analysis and verification, e.g., termination proving, program
invariant generation and hybrid system verification, to name a few. In this paper we
propose a new method for solving non-linear constraints based on encoding the problem
into an SMT problem considering only linear arithmetic. Unlike other existing methods,
our method focuses on proving satisfiability of the constraints rather than on proving
unsatisfiability, which is more relevant in several applications as we illustrate with
several examples. Nevertheless, we also present new techniques based on the analysis
of unsatisfiable cores that allow one to efficiently prove unsatisfiability too for a broad
class of problems. The power of our approach is demonstrated by means of extensive
experiments comparing our prototype with state-of-the-art tools on benchmarks taken
both from the academic and the industrial world. |
|
Subject(s):
|
-Aritmètica |
|
Rights:
|
(c) Springer (The original publication is available at www.springerlink.com)
Tots els drets reservats
|
|
Document type:
|
Article
Article - Accepted version |
|
Share:
|
|
