CLP(B) взвешенный sat_count/3 в Прологе

Question

Для библиотеки CLP(B) SWI-Prolog я хочу реализовать взвешенную версию 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).

Я не нашел подробную документацию библиотеки для модификации кода. Как реализовать взвешенную версию sat_count/2?

---

РЕДАКТИРОВАТЬ 1 (01/11/2017):

Спасибо @mat за ваш ответ, я не могу добавлять комментарии, потому что мне не хватает репутации.

weighted_sat_count/3 следует взять список пар весов, по одному для каждой переменной (вес для True и вес для False), а затем два других параметра совпадают sat_count/2,

Количество является суммой весов каждого допустимого назначения. Вес каждого допустимого присваивания является произведением веса каждой переменной.

Алгоритм расчета результата:

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

Алгоритм может быть более эффективным с картой посещенного узла, связанной с вычисленным весом.weight[,] список пар весов, 1 для True и 0 для False.

---

РЕДАКТИРОВАТЬ 2 (11/11/2017):

Например:

1. A + B + C, простая формула SAT

2. Список пар для весов: [(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