Prolog 中的 CLP(B) 加权 sat_count/3

Question

对于 SWI-Prolog 的 CLP(B) 库， 我想实现一个加权版本的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（2017 年 1 月 11 日）：

感谢@mat 的回复，因为我的声望不够，我无法添加 cmets。

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 代表真，0 代表假。

---

编辑 2（2017 年 3 月 11 日）：

例如：

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

基于修改简单 sat 求解器的另一部分的非高效解决方案，首先查看更简单的计数代码：

% 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 或带有 Minlog 扩展的 Jekejeke Prolog 中运行）：

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