A Partially Solved Form for Heterogeneous Constraints in Disjunctive Normal Form

Abstract

Summary form only given. In order to support constraint solving for challenging engineering applications, as e.g. accomplished by the Relational Constraint Solver, we need to implement join and project operators for heterogeneous constraints. The heterogeneity is due to finite domain and real-valued variables, linear and non-linear arithmetic constraints, (dis-)equations and inequalities. In such a framework, it turns out advantageous to spend reasonable effort on the computation of ""convenient representations"" of intermediate constraints, especially in view of subsequent projection steps. A constraint is ""conveniently represented"" if it is in a so-called partially solved form. The equivalence z = x . y implies/implied by (x = z / y ^ y not= 0) V (z = 0 ^ y = 0) relates an atomic constraint in solved form for z to a disjunction in solved form for x. Although more complex, the right-hand side representation is more useful when we are about to eliminate variable x, since it provides a substitute for x. In our implementation of a Relational Constraint Solver, we have realised a partially solved form to speed up the computation of projections, which is based on and extends known normal forms. Establishing our partially solved form may involve the reformulation of non-linear constraints, as examplified above. Therefore, our approach goes beyond the postponement of non-linear constraints until they have simplified to linear ones, as e.g. deployed in CLP(R)