Project Topics
Get Complete Project Material File(s) Now! »
Linear Arithmetic in Automated Reasoning
Automated reasoning is a research area that is dedicated to teaching com-puters how to reason autonomously. This is accomplished by encoding rea-soning problems as logical formulas and by (dis-)proving the resulting for-mulas via automated reasoning programs, e.g., SMT solvers and theorem provers. Since most problems can be encoded as logical formulas (although not necessarily as rst-order formulas), the potential applications for auto-mated reasoning are in nite. The applications are, however, limited by the undecidability of some logics and the e ciency of the existing automated re-asoning programs. Practically relevant example applications for automated reasoning appear in analysis, testing, veri cation, and synthesis of hard- and software, as well as in interactive theorem proving [13, 23, 24, 43, 50, 51, 124].
Linear arithmetic is relevant to automated reasoning because many tar-get applications for automated reasoning use arithmetic on their own. For instance, most programs use arithmetic variables (e.g., integers) and perform arithmetic operations on those variables. Therefore, software veri cation has to deal with arithmetic; often in combination with other theories, e.g., for arrays and other data structures [108]. This is also the reason why there exist many approaches that combine automated reasoning programs for dif-ferent theories in a modular way. Examples of such modular approaches are CDCL(T) [11, 57, 68, 113, 114] (con ict-driven clause-learning modulo theories) for SMT solving and SUP(T) (superposition modulo theories) [5, 14, 64] for theorem proving. CDCL(T), for instance, abstracts the input formula into a propostional formula and repeatedly selects propositionally satis able models with a SAT solver, until a (combined) theory solver veri es that one of the abstracted propositional models is also a theory satis able model.
Modular approaches can also be used to extend less expressive theory solvers. For instance, a theory solver for CDCL(LA) only has to handle problems and the CDCL(LA) framework extends it to a solver for all CNF problems. Moreover, a combined theory solver, i.e., a theory solver handling multiple theories, can be created with the Nelson-Oppen method [111].
Theory solvers also have to ful ll certain requirements or the modular approach is not e cient enough in practice [61]. To be more precise, the-ory solvers for SMT solving and theorem proving have to be incrementally e cient, i.e., gain an advantage from subsequently solving incrementally connected problems, and have to produce con ict explanations(certi cates of unsatis ability) for unsatis able problems in order to instantly recognize other problems that are unsatis able for the same reason. Also important are certi cates of satis ability (e.g., solution assignments) and theory pro-pagation and theory learning capabilities.
We are interest in decision procedures for linear arithmetic in the context of automated reasoning because of a possible combination with superposi-tion via the SUP(T) approach [5, 14, 64]. In the superposition context, the modular theory solver often has to handle so-called unbounded problems, which are particularly hard to solve linear arithmetic problems. Unboun-ded problems occur so often in SUP(T) because (i) SUP(T) isolates linear arithmetic inequalities to their respective clauses, i.e., inequalities belonging to di erent clauses interact only under very speci c conditions; and (ii) the inequalities that bound an existential variable are often split over multiple clauses (especially in the ground case of SUP(T)) [5].
Unbounded problems also appear in other areas of automated reasoning, although less frequently. Either because of bad encodings, necessary but complicating transformations, e.g., slacking (see Chapter 6.5), or the sheer complexity of the veri cation goal. Hence, e cient techniques for handling unbounded problems are necessary for a generally reliable combined proce-dure and their development became the focus of this thesis.
Basics of Linear Arithmetic
The input problems for linear arithmetic are systems of constraints C, i.e., nite sets of constraints corresponding to and sometimes used as conjuncti-ons over their elements. The standard constraints for linear arithmetic are non-strict inequalities ai1x1 + : : : + ainxn bi and strict inequalities ai1x1 + : : : + ainxn < bi. In some cases, we also have to handle a third type of constraint, a so-called divisibility constraint di j ai1x1 + : : : + ainxn bi.2 Note, however, that divisibility constraints are introduced only during the execution of some of our algorithms (CutSat, CutSat++, and CutSatg). Our actual input problems never contains divisibility constraints. Therefore, we only have to handle them explicitly in algorithms where they are intro-duced, which happens only in the algorithms presented in Chapter 3.
In all of the above constraints, the aij are constant rational values called coe cients, the bi are constant rational values called constraint bounds, the di are constant positive integer values called constraint divisors, and the xj are distinct variables, i.e., the variables xj and xi are di erent unless i = j. Each of those variables is also assigned a type: either rational or integer. If our problem contains only integer variables, then it belongs to the theory of linear integer arithmetic (LIA). If our problem contains only rational variables, then it belongs to the theory of linear rational arithmetic (LRA). If our problem contains both types of variables, then it belongs to the theory of linear mixed arithmetic (LIRA).
For easier access to the components of our constraints and problems, we also de ne the following functions: coe (I; xj) := aij denotes the coe cient of variable xj in the constraint I, where I := ai1x1 + : : : + ainxn bi or I := ai1x1 + : : : + ainxn < bi or I := di j ai1x1 + : : : + ainxn bi; vars(C) := fx1; : : : ; xng denotes the set of all variables that appear in the problem C, i.e., that appear with a non-zero coe cient in any of its constraints; similarly, Qvars(C) and Zvars(C) denote the sets of rational and integer variables that appear in the problem C, respectively. Due to convenience, we assume that the rst n1 := j Qvars(C)j variables x1; : : : ; xn1 are rational variables and the remaining n2 := j Qvars(C)j variables xn1+1; : : : ; xn are integer variables, where n = n1 + n2 := j vars(C)j.
Constraint Representations
We previously de ned constraints as either non-strict inequalities of the form ai1x1 + : : : + ainxn bi; strict inequalities of the form ai1x1 + : : : + ainxn < bi; and divisibility constraints of the form di j ai1x1 + : : : + ainxn bi.
We say that a constraint is in standard representation if it is in one of those three forms. However, not all linear constraints t into this standard repre-sentation, e.g., 3 2(x3+2(x1 x2) 5). Still, all of them can be transformed into it by using basic mathematical properties, e.g., associativity, commu-
tativity and distributivity. For instance, 3 2(x3 + 2(x1 x2) 5) can be transformed into 4×1 4×2 + 2×3 13. Whenever we construct a new constraint, we assume that it is transformed into an equivalent constraint in the standard representation.
Equivalent and Equisatis able
Now that we have de ned the solutions to our constraints systems, we can also de ne when two constraint systems are equivalent. Two constraints systems are equivalent if they have the same solutions. Since we have three di erent types of solutions, this means that we also need three di erent types of equivalence.
De nition 2.2.4 (Equivalences). Let C1 and C2 be constraint systems. C1 is (rationally) equivalent to C2 if Q(C1) = Q(C2). C1 is mixed equivalent to C2 if M(C1) = M(C2). C1 is integer equivalent to C2 if Z(C1) = Z(C2).
Due to the subset relationship of our solution sets, we get the following relationship between our equivalences: C1 is rationally equivalent to C2 implies that C1 is mixed equivalent to C2; and C1 is mixed equivalent to C2 implies that C1 is integer equivalent to C2. The reverse is not necessarily true.
We typically talk about equivalent constraint systems when we have to transform our original system into an equivalent system. We need such transformations whenever our original system is too hard, either because it is too hard to solve or because it does not comply to some requirements of our algorithms/theorems. Obviously, we cannot always nd easier equivalent systems. A good alternative is to look for systems that are easier but only equisatis able:
De nition 2.2.5 (Equisatis ability). Let C1 and C2 be constraint systems. C1 is rationally equisatis able to C2 if the following two statements are equivalent: C1 is rationally satis able and C2 is rationally satis able. C1 is mixed equisatis able to C2 if the following two statements are equivalent: C1 is mixed satis able and C2 is mixed satis able. C1 is integer equisatis able to C2 if the following two statements are equivalent: C1 is integer satis able and C2 is integer satis able.
Equisatis able systems are especially useful if there is an e cient way to convert solutions between the two equisatis able systems.
Reduction to Non-Strict Inequalities
The common de nition of linear arithmetic in the literature supports only one type of constraint: non-strict inequality constraints [28, 83, 89, 93, 103, 128]. There are multiple reasons for this choice.
First of all, the rational solutions of system of inequalities have some very useful properties. For instance, they de ne a polyhedron in the n-dimensional vector space Qn, where each rational solution is equivalent to a point in the polyhedron [128]. In the case that our system C contains only non-strict inequalities, the polyhedron is even closed convex [128]. This entails two very useful properties: rstly, the closed convex polyhedron has a surface if it is neither empty nor encompasses the whole Qn; secondly, any supremum hmax = supfhT x : x 2 Qn satis es Cg over a linear objective h 2 Qn is either hmax = because there exists no point satisfying our constraints, hmax = 1 because the supremum is unbounded, or there exists an actual maximum, i.e., there exists an x 2 Qn that satis es the constraints and its cost hT x is equal to our supremum hmax.
Adding strict inequalities to our constraint system has the e ect that our rational solutions are no longer guaranteed to be a closed set. And if we add divisibility constraints, then our rational solutions describe no longer a polyhedron nor are they a convex set. However, these properties are necessary for most classical algorithms and theorems in linear arithmetic. For instance, the classical dual simplex algorithm [128] returns only rational solutions on the surface of the polyhedron. It is, therefore, not trivial to adapt all classical algorithms and theorems to also handle strict inequalities or divisibility constraints directly. Instead, we show how to represent both divisibility constraints as well as strict inequalities via non-strict inequalities.
Table of contents :
1 Introduction
1.1 The Theory of Linear Arithmetic
1.2 Linear Arithmetic in Automated Reasoning
1.3 Unbounded Problems
1.4 Measuring Eciency
1.5 Contributions
2 Preliminaries
2.1 Basics of Linear Algebra
2.1.1 Norms
2.1.2 Distance
2.2 Basics of Linear Arithmetic
2.2.1 Constraint Representations
2.2.2 Assignments and Solutions
2.2.3 Equivalent and Equisatisable
2.2.4 Substitutions
2.3 Reduction to Non-Strict Inequalities
2.3.1 Reducing Divisibility Constraints
2.3.2 Reducing Strict Inequalities
2.4 Standard Input Formats
2.4.1 Systems of Inequalities
2.4.2 Tableau Representation
2.5 Implied Constraints and Linear Combinations
2.5.1 Minimal Sets of Unsatisable Inequalities
2.6 CDCL(T): A Framework for SMT Solvers
2.6.1 Propositional Abstraction
2.7 Standard Arithmetic Decision Procedures for SMT
2.7.1 A Simplex Version for SMT
2.7.2 Bound Renements/Propagations
2.7.3 Branch-And-Bound
2.7.4 Extensions to Branch-And-Bound
2.8 (Un)Bounded and (Un)Guarded
2.8.1 A Priori Bounds
2.8.2 Bounded Basis
2.8.3 Types of Unbounded Systems
2.9 Other Geometric Objects
2.9.1 d-Norm Balls
2.9.2 (Axis-Parallel) Hypercubes
2.9.3 Flat Cubes
2.10 Basics of Transition Systems
3 CutSat++: A Complete and Terminating Approach to Linear Integer Solving
3.1 Related Work and Preliminaries
3.2 The Guarded Case
3.2.1 States and Models
3.2.2 Decisions and Propagations
3.2.3 (Guarded) Conict Resolution
3.2.4 Learning
3.2.5 Reaching the End States
3.2.6 Slack-Intro
3.3 Divergence of CutSat
3.4 Weak Cooper Elimination
3.5 Unguarded Conict Resolution
3.6 Termination and Completeness
3.6.1 Termination
3.6.2 Stuck States
3.6.3 Completeness
3.7 Summary
4 Fast Cube Tests (for Linear Arithmetic Constraint Solving)
4.1 Related Work and Preliminaries
4.2 Fitting Cubes into Polyhedra
4.3 Fast Cube Tests
4.3.1 Largest Cube Test
4.3.2 Unit Cube Test
4.3.3 Cube Tests for Linear Mixed Arithmetic
4.4 Absolutely Unbounded Polyhedra
4.5 Experiments
4.6 Summary
5 Computing a Complete Basis for Equalities (Implied by a System of LRA Constraints)
5.1 Related Work and Preliminaries
5.2 From Cubes to Equalities
5.2.1 Finding Equalities
5.2.2 Computing an Equality Basis
5.3 Implementation
5.3.1 Integration in the Simplex Algorithm
5.3.2 Incrementality and Explanations
5.4 Application: The Nelson-Oppen Method
5.4.1 Finding Valid Equations Between Variables
5.4.2 Nelson-Oppen Justications
5.5 Application: Exploration of (Un)Bounded Directions
5.6 Application: Quantier Elimination
5.7 Summary
6 A Reduction (from Unbounded Linear Mixed Arithmetic Problems) into Bounded Problems
6.1 Related Work and Preliminaries
6.2 Mixed-Echelon-Hermite Transformation
6.3 Double-Bounded Reduction
6.4 Incremental Implementation
6.4.1 Finding Bounded Inequalities Incrementally
6.4.2 An Incremental Version of the Mixed-Echelon-Hermite Transformation
6.4.3 The Complete Incremental Procedure
6.4.4 Avoiding the Solution Conversion
6.5 Experiments
6.5.1 Comparison with SMT Solvers
6.5.2 Comparison with MILP Solvers
6.5.3 Further Remarks on SPASS-IQ
6.6 Summary
7 Implementation of SPASS-IQ
7.1 Simplex Implementation
7.1.1 Pivoting
7.1.2 Violated Variable Heap
7.1.3 Backtracking through Recalculation
7.1.4 Data Structures
7.2 Branch-and-Bound Implementation
7.2.1 Branching Tree Implementation
7.2.2 Branch-And-Bound Selection Strategies
7.2.3 Extensions to Branch-And-Bound
7.2.4 An Ecient Combination of Techniques
7.2.5 Branch-And-Bound Experiments
8 Implementation of SPASS-SATT
8.1 CDCL(LA) Implementation
8.1.1 Interaction Between SAT and Theory Solver
8.1.2 CDCL(LA) Experiments
8.2 Preprocessing
8.2.1 SMT-LIB Language
8.2.2 Term Sharing
8.2.3 If-Then-Else Preprocessing
8.2.4 Other Simplications
8.2.5 Preprocessing Experiments
9 Conclusion
