Basics of Linear Arithmetic

For more info about our services contact : help@bestpfe.com

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