Constraint Reification

As a further convenience we also provide reification. Reification comes with a set of Boolean operators (#\)/1, (#\/)/2, etc.. and the possibility to embed membership (in)/2 and equalities respectively inequalities (#=)/2, (#>)/2, etc.. in Boolean expressions. The constraint solver main use case is as follows. The reified variable should on one hand allow firing the con-straint, but it should also reflect the entailed of the constraint.

Examples:
?- X #< 100-Y #<==> B, B = 0.
B = 0,
X #> -Y+99

?- X #< 100-Y #<==> B, Y = 74, X = 25.
X = 25,
Y = 74,
B = 1

Under the hood the reification is implemented via a couple of new guarded constraints. We find the guarded domain range, the guarded equality and the guarded membership. The latter two guarded constraints are based on the scalar product. Each reified constraint is modelled by a pair of guarded constraints. At the moment only the main use case is implemented, so we don’t find yet interactions of the guarded constraints.

The following Boolean value predicates are provided:

A #==> B:
If A and B are Boolean expressions then the implication is posted.
A #<== B:
If A and B are Boolean expressions then the converse implication is posted.
A #<==> B:
If A and B are Boolean expressions then the bi-implication is posted.
A #\/ B:
If A and B are Boolean expressions then the disjunction is posted.
A #/\ B:
If A and B are Boolean expressions then the conjunction is posted.
#\ A:
If A is a Boolean expression then the negation is posted.

Kommentare