A Survey of Satisfiability Modulo Theory <s> Linear Integer Arithmetic <s> If K is a compact polyhedron in Euclidean έ/-space, defined by linear inequalities, βt > 0, and if / is a polynomial in d variables that is strictly positive on AT, then / can be expressed as a positive linear combination of products of members of {/?,}. In proving this and subsidiary results, we construct an ordered ring that is a complete AGL(d, R)-invariant for K, and discuss some of its properties. For example, the ordered ring associated to K admits the Riesz interpolation property if and only if it is AGL(d, R)-equivalent to a product of simplices. This is exploited to show that certain polynomials are not in the positive cone generated by the set {/?,}. Let L be a subfield of the real numbers, and let j8, = y ai4+\ (Ϊ = 1,2, 3,..., J) be linear polynomials ("linear forms") in the d variables {Xj}9 with coefficients from L. Suppose the convex polyhedron in R^ defined by K = f){βi)~~ι{[0,oo)) is compact and has interior. Let / be a polynomial in the d variables with entries from L, such that the restriction, f\K, is strictly positive. Then our first result (1.3) asserts that / may be represented as a combination with coefficients from L n R+ (that is, positive numbers in L) of terms that are products of the original set of /Γs that determine K. If / vanishes at only a vertex of K (and is strictly positive elsewhere), this decomposition does not hold in general (§ΠI). Our second principal result concerns the Riesz decomposition property in an ordered ring naturally associated to K, and leads to some interesting geometric characterizations of those polytopes that are affinely homeomorphic to products of simplices. With K defined as above, define a monomial (in the βfs) to be a polynomial in the JΓs that can be expressed as a product of the form βw = βw(\)βw(2) m m , βw(s) <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer Arithmetic <s> The Omega test is an integer programming algorithm that can determine whether a dependence exists between two array references, and if so, under what conditions. Conventional wisdom holds that integer programming techniques are far too expensive to be used for dependence analysis, except as a method of last resort for situations that cannot be decided by simpler methods. We present evidence that suggests this wisdom is wrong, and that the Omega test is competitive with approximate algorithms used in practice and suitable for use in production compilers. The Omega test is based on an extension of FourierMotzkin variable elimination to integer programming, and has worst-case exponential time complexity. However, we show that for many situations in which other (polynomial) methods are accurate, the Omega test has low order polynomial time complexity. The Omega test can be used to simplify integer programming problems, rather than just deciding them. This has many applications, including accurately and efficiently computing dependence direction and distance vectors. <s> BIB002 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer 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> BIB003 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer 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> BIB004 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer Arithmetic <s> Algorithms for solving linear systems of equations over the integers are designed and implemented. The implementations are based on the highly optimized and portable ATLAS/BLAS library for numerical linear algebra and the GNU Multiple Precision library (GMP) for large integer arithmetic. <s> BIB005 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer 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> BIB006 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer Arithmetic <s> 'Satisfiability (SAT) related topics have attracted researchers from various disciplines: logic, applied areas such as planning, scheduling, operations research and combinatorial optimization, but also theoretical issues on the theme of complexity and much more, they all are connected through SAT. My personal interest in SAT stems from actual solving: The increase in power of modern SAT solvers over the past 15 years has been phenomenal. It has become the key enabling technology in automated verification of both computer hardware and software' - Edmund M. Clarke (FORE Systems University Professor of Computer Science and Professor of Electrical and Computer Engineering at Carnegie Mellon University). 'Bounded Model Checking (BMC) of computer hardware is now probably the most widely used model checking technique. The counterexamples that it finds are just satisfying instances of a Boolean formula obtained by unwinding to some fixed depth a sequential circuit and its specification in linear temporal logic. Extending model checking to software verification is a much more difficult problem on the frontier of current research. One promising approach for languages like C with finite word-length integers is to use the same idea as in BMC but with a decision procedure for the theory of bit-vectors instead of SAT. All decision procedures for bit-vectors that I am familiar with ultimately make use of a fast SAT solver to handle complex formulas' - Edmund M. Clarke (FORE Systems University Professor of Computer Science and Professor of Electrical and Computer Engineering at Carnegie Mellon University). 'Decision procedures for more complicated theories, like linear real and integer arithmetic, are also used in program verification. Most of them use powerful SAT solvers in an essential way. Clearly, efficient SAT solving is a key technology for 21st century computer science. I expect this collection of papers on all theoretical and practical aspects of SAT solving will be extremely useful to both students and researchers and will lead to many further advances in the field' - Edmund M. Clarke (FORE Systems University Professor of Computer Science and Professor of Electrical and Computer Engineering at Carnegie Mellon University). <s> BIB007 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer Arithmetic <s> We propose a novel, sound, and complete Simplex-based algorithm for solving linear inequalities over integers. Our algorithm, which can be viewed as a semantic generalization of the branch-and-bound technique, systematically discovers and excludes entire subspaces of the solution space containing no integer points. Our main insight is that by focusing on the defining constraints of a vertex, we can compute a proof of unsatisfiability for the intersection of the defining constraints and use this proof to systematically exclude subspaces of the feasible region with no integer points. We show experimentally that our technique significantly outperforms the top four competitors in the QF-LIA category of the SMT-COMP '08 when solving linear inequalities over integers. <s> BIB008 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer Arithmetic <s> This paper develops abstract quantifier elimination procedures for linear arithmetic over the reals and integers. They are formulated as theory solvers in the context of an abstract DPLL-based search. The resulting procedures allow the solvers to maintain integral control of the search process. We also evaluate this procedure and compare it with several alternatives. So far, the evaluation indicates that the proposed approach has some compelling advantages. <s> BIB009 </s> A Survey of Satisfiability Modulo Theory <s> Linear Integer 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> BIB010
In the case of linear integer arithmetic, the scheme generally used is the same as the one generally used for integer linear programming: the solver first attempts solving the rational relaxation of the problem (nonstrict inequalities are kept, strict inequalities x < e are rewritten as x ≤ e − 1). If there is no solution over the rationals, there is no integer solution. If a rational solution is found, and has only integral coefficients (say, (x, y, z) = (0, 1, 2)), then the problem is decided. If the proposed solution has non-integral coefficients (say, (x, y, z) = ( 1 3 , 0, 1)), then it is excluded by a constraint removing not only that spurious solution but a whole chunk of them. Traditional approaches include i) branch-and-bound [63, Sec. 24.1]: add a lemma excluding one segment of non-integral values of the fractional unknowns (here, x ≤ 0 ∨ x ≥ 1); branching is however not guaranteed to 4 e.g. ZArith https://forge.ocamlcore.org/projects/zarith BIB004 The performance with linear programming solvers meant for large industrial instances was however disappointing BIB006 , due to overhead. Closer integration is needed. BIB007 As implemented in e.g. Linbox (http://www.linalg.org/ ), IML (https://cs.uwaterloo.ca/~astorjoh/iml.html) BIB005 and SageMath (http://www.sagemath.org/). BIB009 One can in fact prove a form of completeness of that approach when the problem contains linear constraints defining a bounded polyhedron, and one nonlinear constraint: if such a problem is unsatisfiable, then this can be proved by going to a sufficiently high degree of products. This follows from Krivine-Handelman's theorem BIB001 43] . terminate in general BIB010 . ii) Gomory cuts BIB003 Ch. 23] iii) branch-and-cut  , a combination of both of the above iv) cuts from proofs or extended branches BIB008 , which can generate e.g. x ≤ z ∨ x ≥ z + 1. The full integer linear decision procedure can be encapsulated and only export theory lemmas and theory propagation, just as the rational linear procedure, or export the branching lemma to the SMT solver, as a learned clause, so as to allow propositional reasoning over it. An alternative to linear programming plus branching and/or cuts is Pugh's Omega test BIB002 , which may also be used to simplify constraints. This test is based on Fourier-Motzkin elimination  , with the twist that, due to divisibility constraints, it may need to enumerate cases up to the least common multiple of the divisors.