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.