# 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