Incremental Linear Constraint Solving and Detection of Implicit Equalities

The incremental linear constraint satisfaction problem consists of repeatedly solving the satisfiability problem for a growing set of linear constraints. This problem is important to constraint logic programming systems where constraints are discovered one at a time and added to a current constraint set, and the satisfiability of this constraint set must be known at all times. Implicit equalities of a system of constraints are inequality constraints that are satisfied as an equality in all solutions of the system of constraints. Detecting implicit equalities is important in determining the minimal (canonical) representation of a system of linear constraints. In incremental constraint solving systems detecting implicit equalities provides information that can simplify further constraint solving. We present an algorithm which efficiently solves the incremental linear constraint satisfaction problem and detects all the implicit equalities present in the constraints. The algorithm forms a basis for the inequality constraint solver in the CLP(ℜ) system.

INFORMS Journal on Computing, ISSN 1091-9856, was published as ORSA Journal on Computing from 1989 to 1995 under ISSN 0899-1499.