Constraint Calculus and Multi-typed Algebra (cont.)

In previous figure, thick arrows indicate class hierarchy. For example, C_LIN is a sub-class of DC_LIN, EC_LIN, and transitively, DEC_LIN, meaning that a CST object of class C_LIN may be used as an argument wherever its superclasses are allowed. Each thin arrow from a CST class T1 to a CST class T2 is labeled with one or more logical or projection operators. It explicitly states that if the input to the operators (in the label) is of the CST class T1, then the output will be of the CST class T2. For example, && applied to inputs from C_LIN returns the result in the same class, while Pzero and Pone return the result in C_RNG.

The four main classes are C_LIN, for Conjunctive Linear constraints of the form Ù_{i = 1}ⁿ C_i, where C_i is a linear inequality; EC_LIN, for Existential Conjunctive constraints of the form ($[x\vec]) | Ù_{i = 1}ⁿ C_i, where [x\vec] is a vector of variable names; DC_LIN, for Disjunctions of C_LIN, and DEC_LIN, for Disjunctions of EC_LIN. The class C_RNG stands for conjunctions of range constraints of the form Ù_{i = 1}ⁿ C_i, where C_i is a range constraint, i.e., is of the form a op x op b, where op is either < or £ and a and b are either real numbers of -¥ or ¥. The class DC_RNG stands for disjunctions of C_RNG constraints. Finally, the most general superclass (i.e., an upper bound in the class lattice) is CST, which stands for FO_CST (Linear), with no restrictions on representation; and the most specific subclass (i.e., the lower bound in the class lattice) is C_BOOL, just for two special constraints: TRUE and FALSE.

In CCUBE, instead of existential quantification, we use the projection operator P, in which we indicate the remaining variables, rather than those to be eliminated. However, P can also add new variables, which are part of the CST object. We also use three specialized projection operators Pzero,Pall and Pone, which correspond, intuitively, to a cheaper variable elimination: of all variables, of no variables, and of all but one variable, respectively. Essentially, in addition to changing the free variables associated with the CST object, Pzero performs the satisfiability test, and Pone does nothing with the constraint.

In addition to projection, operators corresponding to logical connectives &&, ||, and not are defined in the CCUBE constraint algebra. Although the logical meaning of these operators is the same for all CST classes, operationally they work on representations on constraints, and thus are implemented differently for individual CST (sub)classes.

presentation created by Victor E. Segal