ABSTRACT. Solvers for Satisfiability Modulo Theories (SMT) combine the ability of fast Boolean satisfiability solvers to find solutions for complex propositional formulas with specialized theory solvers. Theory solvers for linear real and integer arithmetic reason about systems of simultaneous inequalities. These solvers either find a feasible solution or prove that no such solution exists. Linear programming (LP) solvers come from the tradition of optimization, and are designed to find feasible solutions that are optimal with respect to some optimization function. Typical LP solvers are designed to solve large systems quickly using floating point arithmetic. Because floating point arithmetic is inexact, rounding errors can lead to incorrect results, making these solvers inappropriate for direct use in theorem proving. Previous efforts to leverage such solvers in the context of SMT have concluded that in addition to being potentially unsound, such solvers are too heavyweight to compete in the context of SMT. In this paper, we describe a technique for integrating LP solvers that dramatically improves the performance of SMT solvers without compromising correctness. These techniques have been implemented using the SMT solver CVC4 and the LP solver GLPK. Experiments show that this implementation outperforms other state-of-the-art SMT solvers on the QF_LIA and QF_LRA SMT-LIB benchmarks.

ABSTRACT. This paper presents an iterative approximation refinement, called rasat loop, which solves a system of polynomial inequalities on real numbers. The approximation scheme consists of interval arithmetic (over-approximation, aiming to decide UNSAT) and testing (under-approximation, aiming to decide SAT). If both of them fail to decide, input intervals are refined by decomposition. The rasat loop is implemented as an SMT rasat with miniSAT 2.2 as a backend SAT solver. We discuss three strategy design choices: dependency to set priority among atomic polynomial constraints, sensitivity to set priority among variables, and UNSAT core for reducing learned clauses and incremental UNSAT detection. Preliminary experimental observation on comparison with Z3 4.3, dReal, and isat3 is also discussed.

ABSTRACT. We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by applications of our implementation to various examples from the literature, where it significantly improves the quality of the results.

ABSTRACT. We consider SMT-solving for linear real arithmetic. Inspired by related work for the Fourier--Motzkin method, we combine virtual substitution with learning strategies. For the first time, we present virtual substitution---including our learning strategies---as a formal calculus. We prove soundness and completeness for that calculus. Some standard linear programming benchmarks computed with an experimental implementation of our calculus show that the integration of learning techniques into virtual substitution gives rise to considerable speedups. Our implementation is open-source and freely available.