10.9.2 Solver Interface
The following predicates are defined:
sat(
+Expression)

Expression is a Boolean expression. This checks the consistency
of the expression wrt. the accumulated constraints, and, if the check
succeeds, tells the constraint that the expression be true.
If a variable X, occurring in the expression, is
subsequently unified with some term T, this is treated
as a shorthand for the constraint
 ? sat(X=:=T).
taut(
+Expression,
?Truth)

Expression is a Boolean expression. This asks whether the
expression is now entailed by the accumulated constraints
(Truth=1), or whether its negation is entailed by the accumulated
constraints (Truth=0). Otherwise, it fails.
labeling(
+Variables)

Variables is a list of variables. The variables
are instantiated to a list of 0s and 1s, in a way that
satisfies any accumulated constraints. Enumerates all solutions by
backtracking, but creates choicepoints only if necessary.
Send feedback on this subject.