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.