SWI-Prolog -- sat

Availability::- use_module(library(clpb)).

[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.