In the following, each CLP(B) predicate is described in more detail.
We recommend the following link to refer to this manual:
- True iff Expr is a satisfiable Boolean expression.
- Tautology check. Succeeds with T = 0 if the Boolean
expression Expr cannot be satisfied, and with T =
1 if Expr is always true with respect to the current
constraints. Fails otherwise.
- Enumerate concrete solutions. Assigns truth values to the Boolean
variables Vs such that all stated constraints are satisfied.
- Count the number of admissible assignments. Count
is the number of different assignments of truth values to the variables
in the Boolean expression Expr, such that Expr is
true and all posted constraints are satisfiable.
A common form of invocation is
This counts the number of admissible assignments to Vs
without imposing any further constraints.
?- sat(A =< B), Vs = [A,B], sat_count(+[1|Vs], Count).
Vs = [A, B],
Count = 3,
?- length(Vs, 120),
Vs = [...],
CountOr = 1329227995784915872903807060280344575,
CountAnd = 1.
- Enumerate weighted optima over admissible assignments. Maximize a linear
objective function over Boolean variables Vs with integer
coefficients Weights. This predicate assigns 0 and 1 to the
variables in Vs such that all stated constraints are
Maximum is the maximum of
all admissible assignments. On backtracking, all admissible assignments
that attain the optimum are generated.
This predicate can also be used to minimize a linear Boolean
program, since negative integers can appear in Weights.
?- sat(A#B), weighted_maximum([1,2,1], [A,B,C], Maximum).
A = 0, B = 1, C = 1, Maximum = 3.
- Select a single random solution. An admissible assignment of truth
values to the Boolean variables in Vs is chosen in such a way
that each admissible assignment is equally likely. Seed is an
integer, used as the initial seed for the random number generator.