SWI-Prolog -- weighted

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

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