An algorithm for linear constraint solving: its incorporation in a prolog meta-interpreter for CLP

AbstractThe paper presents an incremental and efficient algorithm for testing the satisfiability of systems of linear equalities, inequalities (strict or unrestricted), and disequalities. In addition, it describes the incorporation of that algorithm into a metalevel interpreter capable of processing both tree constraints and the mentioned linear constraints in the domain of rationals. Important characteristics of the described algorithm are (1) detection of fixed variables within the context of Gaussian elimination, including the simplex method. (2) efficient dereferencing by considering subclasses of solved forms, and (3) efficient testing of inconsistencies between equality and disequality subclasses. The metalevel interpreter is written in Prolog. Examples of its usage are provided. Finally, the paper outlines how the approach may be generalized to consider the efficient and incremental testing of constraint satisfiability in various domains