CLP(B) weighted sat_count/3 in Prolog

Question

For the CLP(B) library of SWI-Prolog, I want to implement a weighted version of sat_count/2

sat_count(Sat0, N) :-
        catch((parse_sat(Sat0, Sat),
               sat_bdd(Sat, BDD),
               sat_roots(Sat, Roots),
               roots_and(Roots, _-BDD, _-BDD1),
               % we mark variables that occur in Sat0 as visited ...
               term_variables(Sat0, Vs),
               maplist(put_visited, Vs),
               % ... so that they do not appear in Vs1 ...
               bdd_variables(BDD1, Vs1),
               partition(universal_var, Vs1, Univs, Exis),
               % ... and then remove remaining variables:
               foldl(universal, Univs, BDD1, BDD2),
               foldl(existential, Exis, BDD2, BDD3),
               variables_in_index_order(Vs, IVs),
               foldl(renumber_variable, IVs, 1, VNum),
               bdd_count(BDD3, VNum, Count0),
               var_u(BDD3, VNum, P),
               % Do not unify N directly, because we are not prepared
               % for propagation here in case N is a CLP(B) variable.
               N0 is 2^(P - 1)*Count0,
               % reset all attributes and Aux variables
               throw(count(N0))),
              count(N0),
              N = N0).

I did not find a detailed documentation of the library for modifying the code. How to implement a weighted version of sat_count/2?

---

EDIT 1 (01/11/2017):

Thank you @mat for your reply, I can't add comments because I've not enough reputation.

weighted_sat_count/3 should take a list of couples of weights, one for each variable (a weight for True and a weight for False state) and then the other two parameters are the same of sat_count/2.

The Count is the sum of weights of each admissible assignment. The weight of each admissible assignment is the product of the weight of each variable.

The algorithm to calculate the result is:

bdd_weight(BDD_node)
 if BDD_node is 1-terminal return 1
 if BDD_node is 0-terminal return 0
 t_child <- 1-child of BDD_node
 f_child <- 0-child of BDD_node
 return (weight[BDD_node, 1] * bdd_weight(t_child) + weight[BDD_node, 0] * bdd_weight(f_child))

The algorithm can be more efficient with a map of visited node associated with calculated weight. weight[,] is the list of couples of weights, 1 for True and 0 for False.

---

EDIT 2 (03/11/2017):

For example:

1. A+B+C, a simple SAT formula

2. List of couple for weights: [(0.7, 0.3), (0.9, 0.1), (0.5, 0.5)], one for each varible

?- weighted_sat_count([(0.7, 0.3), (0.9, 0.1), (0.5, 0.5)], +([A, B, C]), Count).

Count = 
0.7*0.9*0.5 +
0.3*0.9*0.5 +
0.7*0.1*0.5 +
...

---

Answer 1

A non-efficient solution, based on modifying another part of a simple sat solver, starts with looking at a more simpler count code:

% my_sat_count(+List, -Integer)
my_sat_count([X|L], C) :-
   findall(D, (X=0, my_sat_count(L,D); 
               X=1, my_sat_count(L,D)), H),
   sum_list(H, C).
my_sat_count([], 1).

% sum_list(+List, -Number)
sum_list([D|L], C) :-
   sum_list(L, H),
   C is D+H.
sum_list([], 0).

To see that this simple code works, lets make an example (can be run in both SWI-Prolog or Jekejeke Prolog with the Minlog Extension):

Jekejeke Prolog 2, Runtime Library 1.2.5
(c) 1985-2017, XLOG Technologies GmbH, Switzerland
?- use_module(library(finite/clpb)).
% 8 consults and 0 unloads in 93 ms.
Yes
?- sat(X#Y#Z), labeling([X,Y,Z]).
X = 0, Y = 0, Z = 1 ;
X = 0, Y = 1, Z = 0 ; 
X = 1, Y = 0, Z = 0 ; 
X = 1, Y = 1, Z = 1
?- sat(X#Y#Z), my_sat_count([X,Y,Z],N).
N = 4,

Now adding weighting is a simple extension as follows:

% my_weighted_sat_count(+List, +Pairs, -Float)
my_weighted_sat_count([X|L], [(P,Q)|R], C) :-
   findall(D, (X=0, my_weighted_sat_count(L,R,J), D is P*J; 
               X=1, my_weighted_sat_count(L,R,J), D is Q*J), H),
   sum_list(H, C).
my_weighted_sat_count([], _, 1.0).

Here are some example runs:

?- sat(X#Y#Z), my_weighted_sat_count([X,Y,Z],
                    [(0.5,0.5),(0.4,0.6),(0.3,0.7)],W).
W = 0.5
?- sat(X#Y#Z), my_weighted_sat_count([X,Y,Z],
                    [(0.3,0.7),(0.3,0.7),(0.3,0.7)],W).
W = 0.532