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. In this setting, the constraint solving procedure must be incremental while yielding equality information. The usual methods of solving linear arithmetic constraints are based on Fourier elimination which can be quite expensive in practice. Nelson presented a simple and 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, the integration of integer variables, and the generation of models from satisfiable tableaux. Our algorithms are implemented in the ICS software package distributed by SRI International.

gzipped postscript or postscript or pdf

BibTeX Entry

@techreport{RuessShankar:Simplex04,
        TITLE = {Solving Linear Arithmetic Constraints},
        AUTHOR = {Rue{\ss} and Natarajan Shankar},
        MONTH = {January},
        INSTITUTION = {SRI International, Computer Science Laboratory},
        YEAR = {2004},
        ADDRESS = {333 Ravenswood Ave, Menlo Park, CA, 94025},
        NOTE = {revised, August 2004},
        NUMBER = {CSL-SRI-04-01}
}

---

Harald Ruess: ruess@csl.sri.com