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/3
should 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 +
...