Deciding Linear Inequalities by Computing Loop Residues ROBERT SHOSTAK SRI International, Menlo Park, Cahforma ABSTRACT V R Pratt has shown that the real and integer feastbdlty of sets of linear mequallUes of the form x _< y + c can be decided quickly by examining the loops m certain graphs Pratt's method is generahzed, first to real feaslbdlty of mequahues m two variables and arbitrary coefficients, and ultimately to real feaslbdlty of arbitrary sets of hnear mequahtles The method is well suited to apphcatlons m program verification KEY WORDS AND PHRASES theorem proving, decision procedures, program venficauon, linear programmmg CRCATEGORIES 3 15,369,521,532,541 1. lntroductton Procedures for deciding whether a given set of linear inequalities has solutions often play an important role in deductive systems for program verification. Array bounds checks and tests on index variables are but two of the many common programming constructs that give rise to formulas involving inequalities. A number of approaches have been used to decide the feasibdity of sets of inequalities [3, 8, 9, 16, 22], ranging from goal-driven rewriting mechanisms [27] to the powerful simplex techniques [8] of linear programming. Some simple methods are well suited to the small, trivial problems that most often arise, but are insufficiently general. Full-scale simplex techniques, on the other hand, are general and fast for medium to large problems, but do not take advantage of the trivial structure of the small problems (revolving only a few variables and equations) encountered most frequently in program verifi- cation and related applications. The algorithm presented here retains the generality needed in the exceptional case, without sacrifice of speed and simplicity in the more typical small problem case. It builds on V. R. Pratt's observation [18, 20] that most of the inequalities that arise from verification conditions are of the form x _< y + c, where x and y are variables and c is a constant. Pratt showed that a conjunction of such inequalities can be decided quickly by examining the loops of a graph constructed from the inequalities of the conjunction. We generalize this approach, first to inequalities with no more Permission to copy without fee all or part of this material ts granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyrtght notice and the title of the publication and its date appear, and notice is gwen that copying is by permission of the Association for Computing Machinery To copy otherwise, or to republish, reqmres a fee and/or spectfic permission This work was supported m part by the National Science Foundation under Grant MCS 76-81425, the Air Force Office of Scientific Research under Contract F44620-73-C-0068, and the Rome Air Development Center under Contract F30602-78-C-0031 A condensed version appeared in the Proceedings of the Fourth Workshop on Automatic Deduction, Austin, Texas, February 1979 Author's address SR1 International, 333 Ravenswood Avenue, Menlo Park, CA 94025 © 1981 ACM 0004-5411/81/1000-0769 $00 75 Journal of the Association for Computing Machinery, Vol 28. No 4. October 1981. pp 769-779770 ROBERT SHOSTAK than two variables and with arbitrary coefficients, and then to arbitrary linear inequalities. Our generalization reduces to Pratt's test for inputs having the simple structure he describes. The algorithm has recently been used by Aspvall and Shiloach [1] as the basis for a polynomial-time algorithm for the two-variable case. It should be remarked that the usefulness of the algorithm for verification-type applications is not affected by the recent work of L. G. Khachiyan showing that linear programming requires polynomial time m the worst case [16]. While Khachi- yan's algorithm has not yet been thoroughly evaluated (at least in the West), a number of researchers have expressed doubt as to its usefulness in practice. In any case, Khachiyan's algorithm is clearly not suited to very small problems of the kind that arise in program verification. For the examples gwen in this paper, the imtiali- zation step alone of Khachiyan's algorithm requires more computation than does their complete solution using the method of loop residues. The discussion is presented in six sections. Sections 2 and 3 are concerned with preliminary definitions and a statement of the method for inequahtles with two variables and arbitrary coefficients. Section 4 discusses issues of complexity and usefulness for integer problems and relates the method to Pratt's. Sections 5 and 6 deal with the extension of the method to sets having strict inequalities and sets with arbitrary linear inequalities. The last section presents a proof of the theorem that underlies the method. 2. Defimtions Let S be a set of hnear inequalities each of whose members can be written in the form ax + by _< c, where x, y are real variables and a, b, c are reals. Without loss of generality we require that all variables appearing in S other than a special variable v0, called the zero variable, have nonzero coefficients. We also assume that v0 appears only with coefficient zero. Construct an undirected multigraph G from S as follows. Gwe G a vertex for each variable occurring in S and an edge for each inequality. Let the edge associated with an inequality ax + by _< c connect the vertex for x with the vertex for y. Label each vertex with its associated variable I and each edge with Its associated inequality. G is said to be the graph for S. Now let P be a path through G, given by a sequence va, vz ..... vn+a of vertices and a sequence ea, ez ..... en of edges, n _> 1. The triple sequence for P is given by (al, bx, ca), (az, bz, c2) ..... (an, bn, cn), where for each i, 1 <_ i <_ n, a,v, + b,v,+a <- c, is the inequahty labehng e,. 2 P is admtssible if, for 1 _< t _< n - 1, b~ and a,+~ have opposite signs, that is, one is strictly positwe and the other is negative. Intuitively, admissible paths correspond to sequences of inequalities that form transmvity chains. For example, the sequence x _< y, y _ z, z _< 3 gives rise to an admissible path, as does 2x_>3y-4, 2y>_4-z, -z>_x. In what follows It Is notat~onally convenient to write v for both the varmble v and the vertex