SAT Modulo Linear Arithmetic for Solving Polynomial Constraints |
| |
Authors: | Cristina Borralleras Salvador Lucas Albert Oliveras Enric Rodríguez-Carbonell Albert Rubio |
| |
Affiliation: | 1. Universitat de Vic, Vic, Spain 2. Universitat Polit??cnica de Val??ncia, Val??ncia, Spain 3. Universitat Polit??cnica de Catalunya, Barcelona, Spain
|
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|