一種基于圖匹配的求解可滿足性問題的算法

于千城

摘要：信息傳播算法求解可滿足性問題時具有良好的有效性，能使難解區(qū)域變窄。在信息傳播算法的設(shè)計中，是將變量的聯(lián)合概率分布分解為變量子集上的局部函數(shù)的乘積形式。稱局部函數(shù)為因子（factor），每一個因子依賴于一個變量子集，將變量聯(lián)合分布的這一因子形式表示為圖模型——因子圖（factor graph）。信息傳播算法是通過因子圖上的邊傳遞概率消息，這種消息傳遞有兩種方式：變量結(jié)點傳遞給因子結(jié)點的消息和因子結(jié)點傳遞給變量結(jié)點的消息。從每個結(jié)點傳出的消息由傳入該結(jié)點的消息決定，通過某種迭代策略對消息進行更新。當(dāng)這種消息迭代過程收斂到某一固定點時，利用某種規(guī)則（如，最小熵、最大積、最大匹配）對問題進行求解。本文提出一種利用最大匹配規(guī)則求解因子圖上的信息傳播算法的收斂性及算法迭代步數(shù)的上界估計方法，根據(jù)對算法的收斂性分析，在對問題解的精確性影響不大的前提下，僅需要給出算法合理的迭代步數(shù)或者強迫算法終止，使得算法提前結(jié)束，有助于求解可滿足性問題算法性能的更進一步優(yōu)化。

關(guān)鍵詞：信息傳播算法；可滿足性問題；收斂性；因子圖；最大匹配

中圖分類號：TP316 文獻標(biāo)識碼：A 文章編號：1009-3044（2015）05-0209-04

An Algorithm for Solving The Satisfiability Problem Based on Graph Matching

YU Qian-cheng

（Department of Computer Science，Beifang Ethnic University，YinChuan 750021，China）

Abstract： Message passing algorithms are very effective in finding satisfying assignments for SAT instances， and hard region become narrower. In the design of the Message passing algorithms， the joint probability distribution of the variables is decomposed into the product form of the local function of the variable quantum set. The local function is a factor， and each factor is dependent on a variable subset， which is represented as a graph model factor.Message passing algorithms is a kind of message passing through a factor graph， which has two ways： the variable node is passed to the message and the factor node of the node. The message from each node is determined by the decision of the incoming message， and the message is updated by an iterative strategy. When the convergence of this kind of message is fixed to a fixed point， the problem is solved by using some rules （e.g.， minimum entropy， maximum product and maximum matching）. In this paper， we propose a method to estimate the convergence and the upper bound of the algorithm. Based on the convergence analysis of the algorithm， we only need to give a reasonable number of iteration steps or forced the algorithm to terminate.

Key words： Message Passing Algorithms；Satisfiability Problem；Convergence；Factor Graph； Maximum Matching.

SAT 問題是計算機科學(xué)中的核心問題，其理論及其應(yīng)用研究，是計算機與數(shù)理邏輯界學(xué)者共同關(guān)注的一個重大問題[1]。在工程技術(shù)、人工智能、并發(fā)控制等領(lǐng)域中，諸多帶有協(xié)調(diào)性（或一致性）檢驗、組合優(yōu)化等問題均可以編碼到SAT 問題[2]。在SAT 問題理論及應(yīng)用方面的研究，包括硬件模型檢測，軟件模型搜索，可信計算，等價性檢測，安全性驗證，證明系統(tǒng)，證明復(fù)雜性，搜索算法，啟發(fā)式算法，算法分析，難解實例，隨機公式，問題編碼，求解器設(shè)計，簡化器設(shè)計，實例研究與工業(yè)應(yīng)用等。大型數(shù)據(jù)庫的維護，大規(guī)模集成電路的自動布線，機器人動作規(guī)劃等，都涉及SAT 問題[3]。

隨著SAT 問題的深入研究，各類具有特殊結(jié)構(gòu)的SAT 問題受到越來越多的學(xué)者重視規(guī)則結(jié)構(gòu)的實例對應(yīng)的因子圖是一個規(guī)則結(jié)構(gòu)的二部圖（如，k-CSP 實例、k-SAT實例等，它們的因子圖是一個規(guī)則結(jié)構(gòu)的二部圖），借助于規(guī)則二部圖的結(jié)構(gòu)性質(zhì)，便于理解和分析信息傳播算法的數(shù)學(xué)原理及性能。圖論中規(guī)則二部圖的許多良好的性質(zhì)對于研究實例的結(jié)構(gòu)性質(zhì)具有潛在的作用；基于這種規(guī)則結(jié)構(gòu)的實例，信息傳播算法的收斂性研究則更為具體和直觀；在規(guī)則結(jié)構(gòu)的因子圖上，有助于研究與分析消息傳播方式與迭代過程中消息的穩(wěn)定性，這對利用信息傳播算法求解可滿足性問題非常有效，幾乎能夠在多項式時間內(nèi)給出解。

1 基本知識

設(shè)[F={a1，......，am}]為一個k-CNF公式，含有n個變量[x1，......，xn]。公式F可以用一個二分圖[G=（X?A，E）]表示，稱為因子圖 （factor graph）或變量-子句圖，其中，變量結(jié)點集[X={1，......，n}]，子句結(jié)點[A={a1，......，am}]。G中的邊分為兩類：實邊和虛邊。有時用a，b，c，d，…表示子句結(jié)點，用i，j，k，…表示變量結(jié)點。

實邊：[（ai，j）∈E?]子句[ai]含正文字[xj]；

虛邊：[（ai，j）∈E?]子句[ai]含負文字[?xj]。

例1.1：

[F={（x1∨?x2∨?x3），（?x1∨x2∨x4），（?x2∨x3∨x5），（?x2∨x4∨x5）}={a1，a2，a3，a4}]

的因子圖[G=（V，E）]為：

圖1 變量-子句圖

公式F的子公式指由F的部分子句所構(gòu)成的公式。若子句中含有一對互補文字，稱該子句為重言子句。在公式中刪去重言子句后，不影響公式的可滿足性。var（F）和cl（F）表示出現(xiàn)在公式F中變元的集合、F中子句的集合。#var（F）和#cl（F）分別表示公式F中的變元個數(shù)和子句的個數(shù)。

可滿足性問題是指，給定命題變元集M={x1，x2，…，xn}上的一個合取范式（簡稱CNF）公式F，判斷是否存在真值指派v，使F是可滿足的，即v（F）=1。對于公式F，如果每個子句最多只含3個變元，則稱判斷F的可滿足性問題為3-SAT問題[4]。

稱頂點集合V`（V`[?]V）為G的一個獨立集，如果V`中任兩頂點都不相鄰接。稱頂點集合K（K[?]V）為G的一個覆蓋，如果G中每邊至少有一端點在K中。頂點數(shù)最小的覆蓋稱為最小覆蓋。G的最小覆蓋的元素個數(shù)稱為G的覆蓋數(shù)。稱頂點集S為G的團，如果G[S]為一完全圖[3]。

如果在圖G的一個邊子集M中，每條邊的兩端點不同，且任意兩邊不相鄰，則稱M為G的一個匹配（matching）。若邊uv為M的一條邊時，則稱u與v在M下相匹配；稱M-飽和（saturate）u（與v）。也稱u（與v）為M飽和的[6]。類似地，可給出一頂點x為M-不飽和的定義。顯然M的任一子集仍然是G的匹配。例如，圖2所示的圖中，邊子集{ab，gh，ef}，{cg，de}，{ab}以及空集都是該圖的匹配。

圖2

如果G的每個頂點都是M-飽和的，則稱M為圖G的完美匹配[6]。顯然，這時G的頂點數(shù)一定是偶數(shù)；且邊導(dǎo)出子圖G[M]是G的1-正則生成子圖，稱為G的1-因子（1-factor）。當(dāng)然，頂點數(shù)為偶數(shù)的圖也可能沒有完美匹配，例如圖2所示的圖屬于這種情況。稱M為圖G的最大匹配，如果對圖的G的任一匹配M`都有|M`|≤|M|。例如圖2中，邊子集{ab，gh，ef}及{ab，cg，de}都是該圖的最大匹配。顯然，當(dāng)G的最大匹配M不是完美匹配時，G中M不飽和頂點集是非空獨立集。

稱G中的路P為M-交錯路（M-alternating path），如果P的邊交替地屬于M及E＼M。如果M-交錯路P的起點與終點都是M-不飽和的，稱P為M-可擴路（M-augmenting path） [7]。

2 重要的結(jié)論

定理1：G為一個變量-子句圖，M為G中的最大匹配，當(dāng)且僅當(dāng)G中不存在M-可擴路。

證明： [?]：假設(shè)G中有M-可擴路P，將P中M邊與非M邊進行交換，而其它M邊不變，得新的匹配M`，且|M`|=|M|+1，這與M為最大匹配相矛盾。（其實上述運算就是：M`=M[Δ]E（P），其中[Δ]為集合對稱差運算，即對任意兩集合A與B有A[Δ]B=（A∪B）-（A∩B）。）

[?]：反正，假設(shè)M不是最大匹配，取G中任一最大匹配M*。令

H=G[M[Δ] M*]

則H中每個頂點至多與一條M的邊及一條M*的邊相關(guān)聯(lián)，因此

dH（v）=1 or 2 [?]v∈V（H）

從而，H的每個分支都是一圈或路，由M及M*的邊交錯組成。但| M*|>|M|，H中一定有一分支是一條路P，且其起點和終點都是M*-飽和的。從而P是G中的M-可擴路，矛盾。

顯然，對于一個變量-子句圖，如果存在一個匹配，包含圖中的所有子句頂點，那么，此圖對應(yīng)的公式一定可滿足。

定理2：S為變量-子句圖G的覆蓋，當(dāng)且僅當(dāng)V＼S為G的獨立集。

證明：S為G的覆蓋[?] 不存在兩端點全在V＼S中的邊[?]V＼S為G的獨立集。

推論3：變量-子句圖G，[β]為G的最小覆蓋的元素個數(shù)，[α]為G的最大獨立集的元素個數(shù)，[γ]為G的頂點個數(shù)，則[α]+[β]=[γ]。

證明：設(shè)S為G的最大獨立集，則V＼S為其覆蓋，因此

[β]≤|V＼S|=[γ]-[α]

又，設(shè)K為G的最小覆蓋，則V＼K為其獨立集，因此

[α]≥|V＼K|=[γ]-[β]

所以

[α]+[β]=[γ]

結(jié)論：S為G的最大獨立集[?]V＼S為G的最小覆蓋。

關(guān)于圖G中任一覆蓋K及任一匹配M，由覆蓋定義，M中每邊至少有一端屬于K，且匹配M中任兩邊無公共頂點，因此

|M|≤|K|

特別地，對G的最大匹配M*及最小覆蓋K*有

| M*|≤| K*|

引理4：設(shè)M與K分別為G中的匹配與覆蓋，如果

|M|=|K|

則M為最大匹配，K為最小覆蓋。

證明：由|M|≤| M*|≤| K*|≤|K|得到。

定義1：對于一個二分圖G=（X，Y，E），應(yīng)滿足什么條件才能有一個飽和X中每個頂點的匹配。稱這種匹配為完全匹配。

稱N（S）為S的鄰集，指G中所有與S中頂點相鄰接的頂點。一般而言，N（S）中也可能包含S中的頂點。

定理5：在變量-子句圖[G=（X?A，E）]中，G包含使A中每個頂點都飽和的匹配

[?]|N（S）| ≥|S| [?]S[?]A

證明：[?]：假設(shè)G包含一個飽和A中所有頂點的匹配M，S為A的一個子集。因為在S中的頂點在M下匹配N（S）中的頂點，顯然，有|N（S）| ≥|S|。

[?]：假設(shè)存在變量-子句圖G，它滿足條件|N（S）| ≥|S| 對于 [?]S[?]A，但不包含使A中每個頂點都飽和的匹配。令M*為G的最大匹配，u為A中M*-不飽和頂點。設(shè)

Z={v|[?]M*-交錯（u，v）路}

由于M*為最大匹配，由定理1，Z-u中每個頂點都是M*-飽和的。令

S=Z∩A，T=Z∩X

則S＼{u}與T的頂點在M*下相匹配。因此

|T|=|S|-1； N（S）[?]T

但我們有N（S）[?]T。故N（S）=T，由此得

|N（S）|=|T|=|S|-1<|S|

矛盾。

結(jié)論：如果公式F對應(yīng)的變量-子句圖[G=（X?A，E）]有完全匹配M，那么公式F一定可滿足。

例2.1：對于例1.1中的公式F，對應(yīng)的變量-子句圖[G=（X?A，E）]，有完全匹配M，假設(shè)M={（a，1），（b，2），（c，3），（d，4）}，容易驗證，公式F是可滿足的。

推論6：對于一個k-CNF公式F對應(yīng)的變量-子句圖[G=（X?A，E）]，如果G是一個k-正則圖，則公式F一定可滿足。

證明：由于k|A|=|E|=k|X|，所以|X|=|A|。

又，對任意S[?]A，令E1和E2分別為S和N（S）相關(guān)聯(lián)的邊集。E1[?] E2，所以

k|S|=|E1|≤|E2|=k|N（S）|，有|S|≤|N（S）| 對于[?]S[?]A

根據(jù)定理5，圖G包含完全匹配，因此公式F可滿足。

例2.2：一個3-CNF公式F={（x1[∨]x2[∨]x3），（[?]x1[∨]x2[∨][?]x3），（x1[∨][?]x2[∨][?]x3）}

顯然，對應(yīng)的變量-子句圖是一個3-正則圖，公式F對應(yīng)的圖G有完全匹配，根據(jù)推論6，公式F可滿足。

3 求解可滿足性問題的算法

定義：在一個變量-子句圖[G=（X?A，E）]中，稱M為G最優(yōu)匹配，如果M為G完美匹配，并且邊的權(quán)值和[w（M）]=[e∈Mw（e）]為最大（或最?。8]。

稱X∪Y上定義的實函數(shù)[l]為可行頂點標(biāo)號（feasible vertex labeling，簡記為f.v.l.），如果它滿足

[l（x）+l（y）≥w（xy）] [?x∈X，y∈Y]

對任一權(quán)變量-子句圖可行頂點標(biāo)號總是存在的，例如下面就是一個可行頂點標(biāo)號：

[l（x）=maxy∈Y{w（xy）}x∈Xl（y）=0y∈Y]

我們記[El={xy∈E|l（x）+l（y）=w（xy）}]

并稱以[El]為邊集的G的生成子圖為相等子圖（equality subgraph），記為[Gl]。

定理7：設(shè)變量-子句圖[G=（X?A，E）]的可行頂點標(biāo)號[l]，使[Gl]含一完美匹配M*，則M*是G的最優(yōu)匹配。

證明：顯然，M*也是G的完美匹配，且

[w（M*）=e∈M*w（e）=v∈X?Al（v）]

但對G的任一完美匹配M有

[w（M）=e∈Mw（e）≤v∈X?Al（v）]

因此[w（M）≤w（M*）]，即M*是G的最優(yōu)匹配。

算法1：

（1）以任一匹配M作為開始；（可取M=[φ]）

（2）若M飽和A中的每個頂點，停止（M為完美匹配，公式F可滿足）。否則，取A中M-不飽和頂點u，令S←{u}，T←[φ]；

（3）若N（S）=T（無完美匹配）。轉(zhuǎn)入求最大匹配；

（4）（此時有N（S）[?]T）取y∈N（S）＼T。若y為M-飽和的，設(shè)yz∈M，則 S←S∪{z}，T←T∪{y}，并返回（2）；否則（y為M-不飽和的），存在M可擴路P，令M←M[Δ]E（P），并返回（1）；

（5）得到最大匹配后，用最大匹配中的變量去化簡公式，設(shè)X*={x|x是M-飽和的變量頂點}，A*={a|a是M-飽和的子句頂點}，X**={x|x是M-不飽和的變量頂點}，A**={a|a是M-不飽和的子句頂點}，如果滿足

x∈X*，[?]a∈A**，（x，a）∈E （注意：變量x代表的文字必須是一致的）

那么

A*←A*∪{a}，A**←A**＼{a}

（6）若滿足|A*|=|A|，則輸出公式滿足；否則，輸出不滿足；

下面是求解最優(yōu)匹配算法的基本思想：任取一f.v.l.[l]作為開始。定[Gl]，并在[Gl]上任取一匹配M作為開始的匹配。算法在非賦權(quán)圖[Gl]上找完美匹配。若找到，它就是G的最優(yōu)匹配；否則算法停止于某非完美匹配Mn及一Mn-交錯樹H，在[Gl]中它不能再生長（即[NGl（S）=T]）。將[l]適當(dāng)修改成新的f.v.l.[l`]，使[Gl`]仍包含Mn及H，且H在[Gl`]中又可繼續(xù)生長（即[NGl`（S）?T]）。為此只要取[al=minx∈Sy?T{l（x）+l（y）-w（xy）}]，并把S中每個頂點的標(biāo)號都減少[al]；把T每個頂點標(biāo)號都增加[al]即可。重復(fù)上述過程，直到在某個[Gl]中找到完美匹配為止，它就是所求的最優(yōu)匹配。

算法2：

以任f.v.l.[l]作為開始。定[Gl]，并在[Gl]任取一匹配M（可為[φ]）作為開始的匹配。

（1）若M飽和A的每個頂點，則M為最優(yōu)匹配，停止；否則，任取一M-不飽和頂點u，令S←{u}，T←[φ]；

（2）若[NGl（S）=T]，計算

[al=minx∈Sy?T{l（x）+l（y）-w（xy）}]

及新的f.v.l.[l`]

[l`（v）=l（v）-alv∈Sl（v）+alv∈Tl（v）其他]

并令[l←l`]，[Gl←Gl`]；

（3）（此時有[NGl（S）?T]）選取[y∈NGl（S）＼T]，若y為M-飽和的，設(shè)yx∈M，作

S←S∪{x}，T←T∪{y}

并返回到（2）；否則，令P為[Gl]中的M-可擴-（u，y）路，令

M←M[Δ]E（P）

并返回到（1）；

上述算法中的權(quán)值，代表變量-子句圖中變量頂點的度數(shù)。

4 結(jié)束語

利用最大匹配規(guī)則求解因子圖上的信息傳播算法的收斂性作為信息傳播算法收斂性的一個新的研究方法，主要是基于實例結(jié)構(gòu)限制下的信息傳播算法的收斂性分析。這對于實際應(yīng)用中的信息傳播算法的設(shè)計具有指導(dǎo)意義，希望能夠得出一些具體結(jié)果，豐富信息傳播算法的理論及算法研究。

參考文獻：

[1] Heskes T. On the uniqueness of loopy belief propagation fixed points. Neural Computation， 2004，16：2379-2413.

[2] Ihler A T. Loopy belief propagation： Convergence and effects of message errors. Machine Learning Research， 2005，6：905-936.

[3] Mooij J M， Kappen H J. Sufficient conditions for convergence of the sum-product algorithm. IEEE Transactions on Information Theory， 2007，53：4422-4437.

[4] Shi X Q， Schonfeld D， Tuninetti D. Message error analysis of loopy belief propagation for the sum-product algorithm. Computer and Information Science， 2010， 1009：1-30.

[5] Feige U， Mossel E， Vilenchik D. Complete convergence of message passing algorithms for some satisfiability problems.Theory of computing， 2013，9（19）：617-651.

[6] Brunsch T， Cornelissen K， Manthey B， Roglin H. Smoothed analysis of BP for minimum cost flow and matching. Journal of Graph Algorithms and Applications， 2013，17（6）：647- 670.

[7] Norshams N， Wainwright M.J. Stochastic belief propagation： A low complexity alternative to the sum product algorithm. IEEE Transactions on Information Theory， 2013，59（4）：1981-2000.

[8] Bollobas B. Random graphs， 2nd edn. Cambridge University Press， Cambridge，2001.