A Survey of Satisfiability Modulo Theory <s> Linear Real Arithmetic <s> Encompassing all the major topics students will encounter in courses on the subject, the authors teach both the underlying mathematical foundations and how these ideas are implemented in practice. They illustrate all the concepts with both worked examples and plenty of exercises, and, in addition, provide software so that students can try out numerical methods and so hone their skills in interpreting the results. As a result, this will make an ideal textbook for all those coming to the subject for the first time. Authors' note: A problem recently found with the software is due to a bug in Formula One, the third party commercial software package that was used for the development of the interface. It occurs when the date, currency, etc. format is set to a non-United States version. Please try setting your computer date/currency option to the United States option . The new version of Formula One, when ready, will be posted on Www. <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> Linear Real Arithmetic <s> Introduction and Preliminaries. Problems, Algorithms, and Complexity. LINEAR ALGEBRA. Linear Algebra and Complexity. LATTICES AND LINEAR DIOPHANTINE EQUATIONS. Theory of Lattices and Linear Diophantine Equations. Algorithms for Linear Diophantine Equations. Diophantine Approximation and Basis Reduction. POLYHEDRA, LINEAR INEQUALITIES, AND LINEAR PROGRAMMING. Fundamental Concepts and Results on Polyhedra, Linear Inequalities, and Linear Programming. The Structure of Polyhedra. Polarity, and Blocking and Anti--Blocking Polyhedra. Sizes and the Theoretical Complexity of Linear Inequalities and Linear Programming. The Simplex Method. Primal--Dual, Elimination, and Relaxation Methods. Khachiyana s Method for Linear Programming. The Ellipsoid Method for Polyhedra More Generally. Further Polynomiality Results in Linear Programming. INTEGER LINEAR PROGRAMMING. Introduction to Integer Linear Programming. Estimates in Integer Linear Programming. The Complexity of Integer Linear Programming. Totally Unimodular Matrices: Fundamental Properties and Examples. Recognizing Total Unimodularity. Further Theory Related to Total Unimodularity. Integral Polyhedra and Total Dual Integrality. Cutting Planes. Further Methods in Integer Linear Programming. References. Indexes. <s> BIB002 </s> A Survey of Satisfiability Modulo Theory <s> Linear Real Arithmetic <s> Algebraically Closed Fields.- Real Closed Fields.- Semi-Algebraic Sets.- Algebra.- Decomposition of Semi-Algebraic Sets.- Elements of Topology.- Quantitative Semi-algebraic Geometry.- Complexity of Basic Algorithms.- Cauchy Index and Applications.- Real Roots.- Cylindrical Decomposition Algorithm.- Polynomial System Solving.- Existential Theory of the Reals.- Quantifier Elimination.- Computing Roadmaps and Connected Components of Algebraic Sets.- Computing Roadmaps and Connected Components of Semi-algebraic Sets. <s> BIB003 </s> A Survey of Satisfiability Modulo Theory <s> Linear Real Arithmetic <s> We present a new Simplex-based linear arithmetic solver that can be integrated efficiently in the DPLL(T) framework. The new solver improves over existing approaches by enabling fast backtracking, supporting a priori simplification to reduce the problem size, and providing an efficient form of theory propagation. We also present a new and simple approach for solving strict inequalities. Experimental results show substantial performance improvements over existing tools that use other Simplex-based solvers in DPLL(T) decision procedures. The new solver is even competitive with state-of-the-art tools specialized for the difference logic fragment. <s> BIB004 </s> A Survey of Satisfiability Modulo Theory <s> Linear Real Arithmetic <s> Many highly sophisticated tools exist for solving linear arithmetic optimization and feasibility problems. Here we analyze why it is difficult to use these tools inside systems for SAT Modulo Theories (SMT) for linear arithmetic: one needs support for disequalities, strict inequalities and,more importantly, for dealingwith incorrect results due to the internal use of imprecise floating-point arithmetic.We explain how these problems can be overcome by means of result checking and error recovery policies. ::: ::: Second, by means of carefully designed experiments with, among other tools, the newest version of ILOG CPLEX and our own new Barcelogic T-solver for arithmetic, we show that, interestingly, the cost of result checking is only a small fraction of the total T-solver time. ::: ::: Third, we report on extensive experiments running exactly the same SMT search using CPLEX and Barcelogic as T-solvers, where CPLEX tends to be slower than Barcelogic. We analyze these at first sight surprising results, explaining why tools such as CPLEX are not very adequate (nor designed) for this kind of relatively small incremental problems. ::: ::: Finally, we show how our result checking techniques can still be very useful in combination with inexact floating-point-based T-solvers designed for incremental SMT problems. <s> BIB005 </s> A Survey of Satisfiability Modulo Theory <s> Linear Real Arithmetic <s> We consider the decision problem for quantifier-free formulas whose atoms are linear inequalities interpreted over the reals or rationals. This problem may be decided using satisfiability modulo theory (SMT), using a mixture of a SAT solver and a simplex-based decision procedure for conjunctions. State-of-the-art SMT solvers use simplex implementations over rational numbers, which perform well for typical problems arising from model-checking and program analysis (sparse inequalities, small coefficients) but are slow for other applications (denser problems, larger coefficients). We propose a simple preprocessing phase that can be adapted on existing SMT solvers and that may be optionally triggered. Despite using floating-point computations, our method is sound and complete - it merely affects efficiency. We implemented the method and provide benchmarks showing that this change brings a naive and slow decision procedure ("textbook simplex" with rational numbers) up to the efficiency of recent SMT solvers, over test cases arising from model-checking, and makes it definitely faster than state-of-the-art SMT solvers on dense examples. <s> BIB006 </s> A Survey of Satisfiability Modulo Theory <s> Linear Real Arithmetic <s> SMT solvers combine SAT reasoning with specialized theory solvers either to find a feasible solution to a set of constraints or to 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 inexact 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 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_LRA SMT-LIB benchmarks and is competitive on the QF_LIA benchmarks. <s> BIB007 </s> A Survey of Satisfiability Modulo Theory <s> Linear Real Arithmetic <s> Convex polyhedra are commonly used in the static analysis of programs to represent over-approximations of sets of reachable states of numerical program variables. When the analyzed programs contain nonlinear instructions, they do not directly map to standard polyhedral operations: some kind of linearization is needed. Convex polyhedra are also used in satisfiability modulo theory solvers which combine a propositional satisfiability solver with a fast emptiness check for polyhedra. Existing decision procedures become expensive when nonlinear constraints are involved: a fast procedure to ensure emptiness of systems of nonlinear constraints is needed. We present a new linearization algorithm based on Handelman's representation of positive polynomials. Given a polyhedron and a polynomial inequality, we compute a polyhedron enclosing their intersection as the solution of a parametric linear programming problem. To get a scalable algorithm, we provide several heuristics that guide the construction of the Handelman's representation. To ensure the correctness of our polyhedral approximation, our ocaml implementation generates certificates verified by a checker certified ini¾?coq. <s> BIB008
In the case of linear rational, or equivalently real, arithmetic (LRA), the theory solver is typically implemented using a variant BIB004  of the simplex algorithm BIB001 BIB002 . The atomic (in)equalities from the formula, put in canonical form, are collected; new variables are introduced for the linear combinations of variables that are not of the form ±x where x is a variable. For instance, (11) is rewritten as (x ≥ 0 ∨ α ≥ 1) ∧ (y ≥ 0) ∧ (β ≤ −1), together with the system of linear equalities α = 2x + y and β = x + y. The simplex algorithm both maintains a tableau and, for each variable, a current valuation and optional lower and upper bounds. At all times, the simplex tableau contains a system of linear equalities equivalent to this system, such that the variables are partitioned into those (basic variables) occurring (each alone) on the left side and those occurring on the right side. The nonbasic variables are assigned one of their bounds, or at least a value between these bounds. The simplex algorithm tries to fit each basic variable within its bounds; if one does not fit, it makes it non-basic and assigns to it the bound that was exceeded, and selects a formerly non-basic variable to make it basic, through a pivoting operation maintaining the equivalence of the system of equalities. The algorithm stops when either a candidate solution fitting all bounds is found, either one equation in the simplex tableau can be shown to have no solution using interval arithmetic from the bounds of the variables (the interval obtained from the right hand side does not intersect that of the basic variable on the left hand side). A pivot selection ordering is used to ensure that the algorithm always terminates. Theory propagation may be performed by noticing that the current tableau implies that some literals are satisfied. This system is turned into a system of equations ("tableau") and a system of inequalities on the variables: The variables on the left of the equal signs are deemed "nonbasic" and those on the right are "basic". The simplex algorithm performs pivoting steps on the tableau, akin to those of Gaussian eliminations, until a tableau such as this one is reached: Now consider the first equation (e =). By interval analysis, knowing c ≤ 18 and d ≥ −2, −7/16c − 1/16d ≤ 8. Yet e ≥ 20, thus the system has no solution. These coefficients 7/16 and 1/16 can be applied to the original inequalities constraining c and d, with coefficient 1 for that defining e, and the resulting inequalities are summed into a trivially false one: By reading nonzero coefficients off the conflicting line of the simplex tableau, one gets a minimal set of contradictory constraints: d + 1 constraints, corresponding to the nonbasic variable and the basic variables with nonzero multipliers, where d is the dimension of the space. These multipliers may be presented as an unsatisfiability witness to an independent proof checker. Most SMT solvers implement the simplex algorithm using rational arithmetic. In most cases arising from verification problems, rational arithmetic can be performed using machine integers, without need for going into extended precision arithmetic [57] . A common implementation trick is to use a datatype containing a machine-integer (numerator , denominator ) pair or a pointer to an extended precision rational.  This approach is however very inefficient in the rare cases where the solver goes a lot into extended precision: the size of numerators and denominators grows fast. This is why it was proposed to perform linear programming in floating-point arithmetic BIB005 BIB007 BIB006  . BIB003 Because the results of floating-point computations cannot be immediately trusted, some checking is needed. One idea is not to recover floating-point numeric information, but the final partition between basic and nonbasic variables BIB007 BIB006  ; once this partition is known, the tableau is uniquely defined and can be computed by plain linear arithmetic -Gaussian elimination, or better algorithms, including multimodular [66, ch. 7] or p-adic approaches. 6 It is then easy to check the alleged conflicting line, in exact precision. In some cases, linear arithmetic reasoning may be used to prove the unsatisfiability of polynomial problems. One approach is to expand polynomials and consider all monomials as independent variables (e.g. xy 2 is replaced by a fresh unknown v xy 2 ). A refinement BIB008 is to consider lemmas stating that if two polynomials are nonnegative, then so is their product: e.g. 7 Because the set of such products has size exponential in the maximal degree, heuristics are used to pick the most promising ones. Experiments have shown this approach to be competitive, even with a rudimentary and sub-optimal connection between linear SMT-solver and nonlinear reasoning. Some earlier solvers (e.g. CVC3) solver linear real arithmetic by FourierMotzkin elimination  . This approach is generally not considered efficient, since Fourier-Motzkin elimination tends to generate many redundant constraints, which then may need to be eliminated by linear programming, which defeats the purpose of avoiding using the simplex algorithm. Assume variables x 1 , . . . , x n have been assigned values v(x 1 ), . . . , v(x n ) in the current branch of the search, and that two atoms x n+1 ≤ a and x n+1 ≥ b, where a and b are linear combinations of variables other than x n+1 , have been assigned to t, such that b > a in the assignment v; then it is impossible to pick a value for x n+1 in that assignment. In fact, it is impossible to pick a value for it in any assignment such that b > a. Assignments that conflict for the same reason are eliminated by a FourierMotzkin elimination  elementary step, valid for all x 1 , . . . , x n+1 : Example 7. Consider Ex. 5 with n = 3. The solver has clauses x i − t i ≤ 2, But then, there is no way to assign t 3 , because of the current assignment x 2 → 0 and the inequalities t 3 − x 2 ≤ 3 and t 3 ≥ 16. The solver then learns by Fourier-Motzkin: (20) which may in fact be immediately simplified by resolution with the original clause t 3 ≥ 16 to yield ¬(t 3 − x 2 ≤ 3) ∨ x 2 ≥ 13. The assignment to x 2 is retracted. But then, there is no way to assign x 2 , because of the current assignment t 2 → 0 and the inequality x 2 −t 2 ≤ 2. The solver then learns by Fourier-Motzkin: The truth assignment to t 3 − x 2 ≤ 3 is retracted. At this point, the solver has t 0 → 0, By similar reasoning in that branch, the solver derives t 3 − x 2 ≤ 3 ∨ t 2 ≥ 11. By resolution between the outcomes of both branches, one gets t 2 ≥ 11. By similar reasoning, one gets t 1 ≥ 6 and then t 0 ≥ 1, but then there is no satisfying assignment to t 0 . The problem has no solution. In contrast to the exponential behavior of DPLL(T) on Ex. 5, MCSAT has linear behavior: each branch of each individual disjunction is explored only once, and the whole disjunction is then summarized by an extra atom. The dynamic generation of new atoms by MCSAT, as opposed to DPLL(T), creates two issues. i) If infinitely many new atoms may be generated, termination is no longer ensured. One can ensure termination by restricting the generation of new atoms to a finite basis (this basis of course depends on the original formula); this is the case for instance if the numeric variables x 1 , . . . , x n are always assigned in the same order, thus the generated new atoms are results of Fourier-Motzkin elimination of x n , then of x n−1 etc. down to x 2 . 9 In practice, the interest of being able to choose variable ordering trumps the desire to prove termination. ii) Since many new atoms and clauses are generated, some garbage collection must be applied, as with learned clauses in a CDCL solver. Implementation-wise, note that, like a clause in CDCL, a linear inequality is processed only when all variables except for one are assigned. Similar to two watched literals per clause, one can apply two watched variables per inequality.