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

2019年7月28日 152次阅读

对于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(01/11/2017)：

谢谢@mat的回复,我无法添加评论,因为我没有足够的声誉.

weighted_sat_count / 3应该采用权重对的列表,每个变量一个(True的权重和False状态的权重),然后其他两个参数与sat_count / 2相同.

Count是每个可允许分配的权重之和.每个可允许分配的权重是每个变量权重的乘积.

计算结果的算法是：

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(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 +
...

最佳答案 基于修改简单坐标求解器的另一部分的非有效解决方案,首先要查看更简单的计数代码：

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

要看到这个简单的代码有效,让我们举一个例子(可以使用Minlog扩展在SWI-Prolog或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
点赞