CLP (B) weighted sat_count / 3 in Prolog

Question

For the CLP (B) SWI-Prolog library, 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 the detailed library documentation for modifying the code. How to implement a weighted version of sat_count / 2?

---

EDIT 1 (11/11/2017) :

Thanks @mat for your answer, I can not add comments because I do not have enough reputation.

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

A graph is the sum of the weights of each valid destination. The weight of each valid assignment is the product of the weight of each variable.

The algorithm for calculating the result:

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))

node, . weight[,] - , 1 True 0 False.

---

EDIT 2 (03/11/2017):

:

• A + B + C, SAT

• : [(0,7, 0,3), (0,9, 0,1), (0,5, 0,5)],

?- 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

, , :

% 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).

, , ( SWI-Prolog, Jekejeke Prolog Minlog):

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,

:

% 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).

:

?- 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