Solving Linear Arithmetic Constraints

---

Authors

Harald Rueß and Natarajan Shankar

Abstract

Linear arithmetic constraints in the form of equalities and inequalities constitute the vast majority of proof obligations that arise in embedded applications of theorem proving such as extended typechecking, software and hardware verification, and compiler optimization. Such constraints involve the conjunction of equalities, inequalities, and disequalities over arithmetic, uninterpreted functions, and other datatypes. Nelson presented a practical scheme for solving linear inequalities based on the simplex algorithm for linear programming. We extend Nelson's version of the simplex algorithm in a number of ways. Among these extensions are an improved treatment of the combination of restricted (non-negative slack) and unrestricted variables, a method for adding equalities and disequalities to a simplex tableau, an optimized method for propagating equality information, and efficient techniques for generating proofs and models. Our algorithms are supported by simple and rigorous correctness arguments.

gzipped postscript or postscript or PDF

BibTeX Entry

submitted for publication, Mar 4 2005

---

Harald Ruess: ruess@csl.sri.com