The Constraint Programming Solver (Experimental)

The REIFY predicate specifies a reify constraint, which associates a binary variable with a constraint. The value of the binary variable is 1 or 0, depending on whether the constraint is satisfied or not, respectively. The constraint is said to be reified, and the binary variable is referred to as the control variable. Currently, only linear constraints can be reified.

The REIFY predicate provides a convenient mechanism for expressing logical constraints, such as disjunctive and implicative constraints. For example, the disjunctive constraint

can be expressed by the following statements:

var X integer, Y integer,
    P binary,  Q binary;
con reify(P, 3 * X + 4 * Y < 20);
con reify(Q, 5 * X - 2 * Y > 50);
con AtLeastOneHolds: P + Q >= 1;

The binary variable P reifies the linear constraint

The binary variable Q reifies the linear constraint

The following linear constraint enforces the desired disjunction:

The following implicative constraint

can be enforced by the linear constraint

You can also use the REIFY constraint to express a constraint that involves the absolute value of a variable. For example, the constraint

can be expressed by the following statements:

var X integer, P binary, Q binary;
con Xis5:      reify(P, X = 5);
con XisMinus5: reify(Q, X = -5);
con OneMustHold: P + Q = 1;