### A.7.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.