Page 138 - 《软件学报》2021年第5期

1362 Journal of Software 软件学报 Vol.32, No.5, May 2021

squares)标准进行状态估计,文献[52]基于协方差分析了信息传播算法收敛的动态行为.特别是在文献[53]中,利
用赋范空间中函数的压缩映射原理,给出了信念传播算法收敛的一个统一框架.然而,对于具体的 SAT 问题,该
条件验证复杂,可判定的范围有限,在大多数 SAT 实例上判定条件失效.不难看出:上述关于信息传播算法的收
敛性分析都是基于某个具体模型,或者使用范围窄,或者判定条件验证复杂等.因此,对信息传播算法的收敛性
分析仍然不完善.
综上,本文针对 BP 算法在求解 SAT 问题中的信息传播策略,对该算法的性能表现进行了系统的理论分析,
将信息迭代方程的取值由(0,1)扩大到整个实数空间,得出了验证 BP 算法收敛的一个有效条件,检查该条件相对
简单.最终,通过实验分析了该条件的有效性.至此,我们系统分析了 3 种求解 SAT 问题的信息传播算法的收敛
性,这对于基于信息传播算法的求解器设计以及信息传播算法的广泛应用具有重要意义.

1 信念传播算法

1.1 因子图
一个 CNF 公式 F={C 1 ,C 2 ,…,C m },公式由变元 x 1 ,x 2 ,…,x n 构成,为了方便表示,将 x i 简记 i.则 CNF 公式能够表
示为一个二部网络 G=(C∪X,E),该二部网络称为因子图.图中包含两类结点,分别为由所有变元构成的变元结点
集,记为 X={1,2,…,n},以及由变元的析取构成的子句结点集,记为 C={C 1 ,C 2 ,…,C m }.图中的虚边和实边包含原
CNF 公式中两种不同的信息:
• 实边:(C i ,j)∈E⇔子句 C i 含正文字 x j ;
• 虚边:(C i ,j)∈E⇔子句 C i 含负文字¬x j .
为了方便在后文进行表示,本文用 a,b,…表示子句 C 1 ,C 2 ,….
例 1:公式 F={(x 1 ∨¬x 2 ∨¬x 3 ),(¬x 1 ∨x 2 ∨¬x 4 ),(¬x 2 ∨x 3 ∨x 5 ),(¬x 2 ∨x 4 ∨x 5 )}={a,b,c,d}的因子图 G=(C∪X,E)如图 1
所示.
1 2 3 4 5

a b c d

Fig.1 Factor graph
图 1 因子图

• V(a):子句 a 所包含的所有变元的集合,V(a)=V + (a)∪V − (a).其中,
¾ V + (a):在子句 a 中正出现的变元集合;
¾ V − (a):在子句 a 中负出现的变元集合;
¾ V(a)\i 表示集合 V(a)中剔除结点 i.
在图 1 中,V(a)={x 1 ,x 2 ,x 3 },V + (a)={x 1 },V − (a)={x 2 ,x 3 }.
• V(j):包含变元 x j 的子句的集合,V(j)=V + (j)∪V − (j).其中,
¾ V + (j):表示变元 x j 正出现的子句集合;
¾ V − (j):表示变元 x j 负出现的子句集合;
¾ V(j)\a=V(j)−{a}.
在图 1 中,V(2)={a,b,c,d},V + (2)={b},V − (2)={a,c,d}.
定义两个一致性集合V a u ()j 和V a s ()j :
• 如果 x j ∈V + (a),那么V a u ()j = V − ( ),j V a s ( )j = V + ( ) \j a ;
• 如果 x j ∈V − (a),那么V a u ()j = V + ( ),j V a s ( )j = V − ( ) \j a .
集合V a u ()j 和V a s ()j 如图 2 所示.