SWI-Prolog -- sat

Documentation
- Reference manual
  - The SWI-Prolog library
    - library(clpb): CLP(B): Constraint Logic Programming over Boolean Variables
      - CLP(B) predicate index
        
        sat/1
        
        taut/2
        
        labeling/1
        
        sat_count/2
        
        weighted_maximum/3
        
        random_labeling/2
- Packages

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.