一种基于图匹配的求解可满足性问题的算法

摘要

信息传播算法求解可满足性问题时具有良好的有效性,能使难解区域变窄。在信息传播算法的设计中,是将变量的联合概率分布分解为变量子集上的局部函数的乘积形式。称局部函数为因子(factor),每一个因子依赖于一个变量子集,将变量联合分布的这一因子形式表示为图模型——因子图(factor graph)。信息传播算法是通过因子图上的边传递概率消息,这种消息传递有两种方式:变量结点传递给因子结点的消息和因子结点传递给变量结点的消息。从每个结点传出的消息由传入该结点的消息决定,通过某种迭代策略对消息进行更新。当这种消息迭代过程收敛到某一固定点时,利用某种规则(如,最小熵、最大积、最大匹配)对问题进行求解。本文提出一种利用最大匹配规则求解因子图上的信息传播算法的收敛性及算法迭代步数的上界估计方法,根据对算法的收敛性分析,在对问题解的精确性影响不大的前提下,仅需要给出算法合理的迭代步数或者强迫算法终止,使得算法提前结束,有助于求解可满足性问题算法性能的更进一步优化。