A.8.10 CLP(B) predicate index

In the following, each CLP(B) predicate is described in more detail.

We recommend the following link to refer to this manual:

http://eu.swi-prolog.org/man/clpb.html

[semidet]sat(+Expr)

True iff Expr is a satisfiable Boolean expression.

[semidet]taut(+Expr, -T)

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.

[multi]labeling(+Vs)

Enumerate concrete solutions. Assigns truth values to the Boolean variables Vs such that all stated constraints are satisfied.

[det]sat_count(+Expr, -Count)

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 sat_count(+[1|Vs], Count): This counts the number of admissible assignments to Vs without imposing any further constraints.

Examples:

?- sat(A =< B), Vs = [A,B], sat_count(+[1|Vs], Count).
Vs = [A, B],
Count = 3,
sat(A=:=A*B).

?- length(Vs, 120),
   sat_count(+Vs, CountOr),
   sat_count(*(Vs), CountAnd).
Vs = [...],
CountOr = 1329227995784915872903807060280344575,
CountAnd = 1.

[multi]weighted_maximum(+Weights, +Vs, -Maximum)

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 satisfied, and Maximum is the maximum of sum(Weight_i*V_i) over 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.

Example:

?- sat(A#B), weighted_maximum([1,2,1], [A,B,C], Maximum).
A = 0, B = 1, C = 1, Maximum = 3.

[det]random_labeling(+Seed, +Vs)

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.