The most frequently used CLP(B) predicates are:
- sat(+Expr)
- True iff the Boolean expression Expr is satisfiable.
- taut(+Expr, -T)
- If Expr is a tautology with respect to the posted
constraints, succeeds with T = 1. If Expr
cannot be satisfied, succeeds with T = 0. Otherwise,
it fails.
- labeling(+Vs)
- Assigns truth values to the variables Vs such that all
constraints are satisfied.
The unification of a CLP(B) variable X with a term T is
equivalent to posting the constraint sat(X=:=T).