布爾方程形式的np問題可滿足性閾值估計

0求解可滿足性閾值估計的應用現(xiàn)狀“非營利”問題是指在圖靈機意義上的多個時間證明的問題。它不僅在計算機科學中具有重要的理論價值，而且在許多領域都得到了廣泛應用。近年來,隨著對NP問題算法實驗和理論分析研究的逐漸深入,人們發(fā)現(xiàn)對于一大類NP完全問題都可以通過定義某個序參數(shù)將問題劃分為可滿足和不可滿足兩個區(qū)域:可滿足區(qū)域中幾乎所有隨機實例都是可滿足的,而不可滿足區(qū)域中幾乎所有的隨機實例都是不可滿足的。在這兩個區(qū)域之間可滿足概率發(fā)生突變的現(xiàn)象稱為可滿足性的相變現(xiàn)象,發(fā)生突變的參數(shù)區(qū)間稱為可滿足性閾值。對相變現(xiàn)象的研究不僅有助于更加深入地探索NP問題的難解實質(zhì),而且對于設計求解相關(guān)實際難解問題的高效算法也有重要的指導意義。目前,對NP問題閾值的數(shù)值估計和相變機制的嚴格描述已經(jīng)成為當前理論計算機科學和人工智能領域研究的熱點問題之一。特別是在以SAT問題、XORSAT問題等為代表的一類約束滿足問題相變現(xiàn)象的研究方面取得了一系列的重要成果,并被廣泛地應用于集成電路驗證、圖像識別、自然語言理解、規(guī)劃診斷、LDPC編碼等相關(guān)領域。在數(shù)學、物理和計算機科學的交叉領域,對隨機約束滿足問題可滿足性閾值的研究經(jīng)歷了一個逐步由相變現(xiàn)象向相變機制的過程:Cheeseman等人于1991年發(fā)現(xiàn)了難解約束滿足問題與相變現(xiàn)象的聯(lián)系;Kirkpatrick等人于1994年通過算法得到了隨機布爾表達式的臨界相變行為;Monasson等人于1999年指出了約束滿足問題相變特征與計算復雜性的關(guān)系;Mezard等人于2002年通過統(tǒng)計物理的方法得到了隨機SAT問題的可滿足性閾值估計,并提出了具有劃時代意義的SurveyPropagation算法;Krzakala等人于2007年又進一步指出了解空間的結(jié)構(gòu)特征與可滿足性相變機制之間的內(nèi)在聯(lián)系。迄今為止,如何通過算法實驗或者理論分析給出一個NP問題的可滿足性閾值估計仍然是一個受到廣泛重視的開放問題。一般認為,在NP問題可滿足性相變區(qū)域內(nèi)的隨機實例求解復雜度最高,即難解實例大都分布在可滿足概率的突變區(qū)域內(nèi)(可滿足性閾值),因此,研究可滿足性相變區(qū)域的參數(shù)范圍即可滿足性閾值是該領域的核心研究基礎問題。針對這一問題有三種主要的研究方法:a)傳統(tǒng)的算法分析方法,即通過對作用在給定參數(shù)條件下大量隨機實例上的完全算法進行數(shù)值實驗,確定問題的可滿足概率隨參數(shù)變化的演化曲線,進而得到可滿足性閾值的估計;b)統(tǒng)計物理分析方法,即通過研究問題所對應的統(tǒng)計物理模型,從能量分布的角度對解空間結(jié)構(gòu)隨參數(shù)變化的演化進行定性和定量的分析,進而得到完整的可滿足性相圖和閾值估計;c)數(shù)學的嚴格上下界估計方法,通過對模型具有的可滿足性閾值類型進行判斷,使用一階矩和二階矩等概率方法對問題的可滿足性閾值上界和下界進行估計,進而得到可滿足性閾值對應的參數(shù)區(qū)間。上述三種方法的側(cè)重點各不相同:方法a)基于可滿足性閾值的原始定義得到的結(jié)果最為精確,但是該方法數(shù)值實驗的高效算法往往很難設計,而且計算過程十分復雜,要消耗大量的時間和空間資源;方法b)將統(tǒng)計物理中的工具有效的應用于可滿足性閾值估計,并取得了良好的效果,但是該方法中存在的經(jīng)驗性假設和近似分析方法使得估計結(jié)果的真實可信度難以保證;方法c)的突出優(yōu)點是推導論證過程嚴格且論證方法可以形式化描述,但是該方法所能有效應用的問題范圍有限,而且其對可滿足性閾值上下界的精確估計往往難以實現(xiàn)。一般地,針對問題可滿足性閾值的數(shù)值估計進行不同方法間的對比,可以得到更加精確的參數(shù)區(qū)間估計。本文通過將隨機布爾方程組的高斯消去算法與基于隨機圖的摘葉算法相結(jié)合,針對MAS這一具有布爾方程組形式的NP問題提出了一種新的完全算法——LGC算法。以等概率混合線性和非線性布爾方程的MAS模型為研究對象,本文基于LGC算法對不同參數(shù)條件下大量隨機實例進行求解驗證,將計算結(jié)果用于研究在等概率混合參數(shù)條件下MAS模型所對應具體問題的可滿足性閾值,得到了可滿足性的相變曲線,并給出了閾值的數(shù)值估計,與其他理論分析方法得到閾值的上下界估計進行了對比。1模型生成的條件作為對在低密度驗證編碼、約束協(xié)同等方面有著廣泛應用的XORSAT問題的推廣,海量代數(shù)系統(tǒng)模型(簡稱MAS模型)由一類線性布爾方程組和一類非線性布爾方程組混合構(gòu)成,成為能夠代表一大類布爾方程組問題的參數(shù)化模型。MAS模型已經(jīng)被證明是一個新的NPC類約束滿足問題,同時被認為是構(gòu)建NP類問題與P類問題形式化聯(lián)系的有效途徑之一。一個MAS模型實例的定義為:考慮由N個布爾變量組成的集合{x1,x2,…,xN},獨立隨機地從所有可能給定形式方程中選取M=aN個方程組成一個方程組就得到一個隨機MAS模型實例。其中給定方程的形式為:類型Ⅰ,線性布爾方程形式xi+xj+xk=Ji,j,k,J∈{0,1};或者類型Ⅱ,非線性布爾方程形式xi+xj×xk=0,在類型Ⅱ中xi稱為線性部分,xj和xk稱為方程的非線性部分。在實例的生成中,選擇兩種類型方程的概率都是1/2。這里需要特別指出,參數(shù)a是模型中約束方程與變量個數(shù)之間的比值,一般被稱為約束方程密度,其決定了MAS模型的約束強度。通過MAS模型的構(gòu)造方式可以看出,一個隨機生成的MAS模型實例可以被拆分為兩個子問題。其中由類型Ⅰ的布爾方程組成的方程組可以看做是約束方程密度為a/2的隨機3-XORSAT問題,由類型Ⅱ的布爾方程組成的方程組可以看做是約束方程密度為a/2的隨機MAS-nonlinear問題。在一般布爾運算的意義下,第一個子問題的所有解組成的集合對布爾加法構(gòu)成群,第二個子問題的所有解組成的集合對布爾乘法構(gòu)成半群。最新的研究成果表明,該模型子問題的特殊代數(shù)結(jié)構(gòu)與解空間結(jié)構(gòu)和可滿足性相變之間存在著很強的關(guān)聯(lián)性,這對啟發(fā)式完全算法和局部搜索算法設計有重要的指導意義。2解空間由于MAS模型的任意實例都可以拆分為線性和非線性兩個子問題,筆者認為對該模型實例求解的過程可以轉(zhuǎn)換為先對兩個子問題分別求解,再將得到的解集相交得到原問題解空間的過程。在這一思想的基礎上,通過結(jié)合隨機布爾方程組的高斯消去算法和基于隨機圖的摘葉算法提出相應的啟發(fā)策略,實現(xiàn)求解MAS模型實例高效啟發(fā)式完全算法的設計。2.1缺失約束因素的摘葉由于本文研究的完全算法求解的是在一般模型定義和特定的參數(shù)條件下按照等概率生成的隨機實例,實例中有可能出現(xiàn)滿足某些特定消去條件的變量,這些變量的取值對方程組是否存在解沒有影響。所以,在針對該模型的完全算法設計中加入摘葉算法的消去策略,將會有效地縮減求解對象所含變量的規(guī)模,進而提高算法的整體求解效率。通過將變量和約束表示為隨機圖中的節(jié)點和邊,摘葉算法被廣泛地應用于尋找大規(guī)模約束滿足問題的滲流核。對于一般的線性布爾方程組求解問題,摘葉算法的思想是將問題對應隨機圖中的葉子節(jié)點(度為1的節(jié)點)和與其連接的邊全部刪除,得到新圖之后重復進行上面的操作,直至得到的圖中不含有葉子節(jié)點。由于對每個含有葉子節(jié)點的約束方程總可以通過調(diào)整葉子節(jié)點的取值使得該方程有解,去掉這個葉子節(jié)點對應變量所在的方程后,方程組是否有解的性質(zhì)不會發(fā)生改變,即原問題的可滿足性質(zhì)不會發(fā)生改變。所以,可以通過摘葉算法的思想將原始問題的可滿足性判定問題化簡為一個等價但包含更少變量和約束問題的可滿足性判定問題。由于MAS模型的約束方程中含有三個變量,其對應的隨機圖中的邊是由三個節(jié)點連接關(guān)系表示的超邊。通過分析保持該問題可滿足性不變的摘葉方式,本文總結(jié)出了以下的摘葉算法執(zhí)行條件:a)如果一個變量只在惟一一個類型Ⅰ方程中出現(xiàn),那么刪去該方程原問題可滿足性不變;b)如果一個變量只在惟一一個類型Ⅱ方程中的線性部分出現(xiàn),那么刪去該方程原問題可滿足性不變;c)如果某個類型Ⅱ方程中非線性部分的兩個變量只在該方程中出現(xiàn)而不在其他方程中出現(xiàn),那么刪去該方程原問題可滿足性不變。對于一個給定的MAS模型實例T,進行兩步操作:a)對實例中的變量在方程中出現(xiàn)的位置和頻率進行統(tǒng)計;b)對符合上述條件的變量和方程全部刪除,這樣就得到了在可滿足性意義下等價實例T(1)。接下來再對實例T(1)進行同樣的兩步操作,得到在可滿足意義下等價實例T(2)。如此下去直到某個實例T(n)中無法找出符合上述條件的方程則算法停止,接下來再通過2.2節(jié)中的高斯消去算法對符合停止條件的實例T(n)進行下一階段的預處理。上述算法的流程描述詳見2.2節(jié)中的LFprocedure。2.2基于高斯消去的啟發(fā)式排序一般意義上針對隨機約束滿足問題的完全算法框架中,因為要保證算法對所有可能賦值組的遍歷,所以設計出的算法往往是一個帶有啟發(fā)式條件的分支定界過程,也就是帶有啟發(fā)式條件的回溯過程。現(xiàn)有的回溯過程都是以無序的變量集合為基本對象,通過賦值后的矛盾情況進行變量賦值的修正。由于變量在實例中的分布存在不確定性,導致每個變量對其他變量的影響程度和約束共享程度也不盡相同,再加上一般回溯過程中需要修改賦值的變量是隨機選取的,在完全算法的運行過程中有大量的時間消耗在影響范圍相對較小的變量上。因此,如何恰當?shù)貙厮葸^程中要修改賦值的變量進行排序,使影響范圍較大的變量盡可能地排在影響范圍較小的變量之前被修正是提高算法效率的有效途徑,同時也是理解問題計算復雜性成因的關(guān)鍵。本文中提出的完全算法不僅將隨機圖上的摘葉算法引入作為有效縮減問題規(guī)模的預處理模塊,而且還首次通過高斯消去過程將變量按照約束傳播影響進行重新排序,實現(xiàn)了對回溯算法搜索解的策略優(yōu)化。根據(jù)高斯消去的思想,這里對MAS模型實例的線性子問題對應的增廣矩陣作行列變換來實現(xiàn)增廣矩陣的對角化。具體的算法可以分為三步:a)在現(xiàn)有的變量序下,檢查與當前方程對應的增廣矩陣對角元位置是否不為零;b)如果對角元位置不為零則將該行與矩陣中的每一行按照布爾加法相加,實現(xiàn)對角元所在列的非對角元消去;c)如果對角元位置為零,則將該列的位置依次后移至倒數(shù)第二列。將上述三步循環(huán)進行直至無法繼續(xù)消去,然后將非對角元按照其所在列非零元的數(shù)量由大到小進行排列,就得到了基于高斯消去預處理算法變量啟發(fā)式排序。從矩陣分析的角度不難發(fā)現(xiàn),這樣的啟發(fā)式排序?qū)⑿问缴蠀⑴c較多約束的變量排在了較為靠前的位置。需要指出的是,這樣的序并不是一個全局變量間實質(zhì)約束關(guān)系的最精確排序,其中仍然存在某些變量的形式約束影響范圍與實質(zhì)影響范圍不一致的情形,但是通過第3章中LGC算法對隨機實例的求解效果可以看出,這樣的啟發(fā)式排序已經(jīng)可以實現(xiàn)比較有效的將變量按照影響范圍的大小進行排序的目標。上述算法的流程描述詳見第3章中的GEprocedure。3實體法上可構(gòu)建的算法在實現(xiàn)對MAS模型實例求解過程中摘葉預處理算法模塊和高斯消去預處理算法模塊的設計基礎上,本文提出的完全求解算法中基本回溯策略采用了基于布爾可滿足性問題求解算法中非常著名的Davis-Putnam-Logemann-Loveland(DPLL)算法框架作為回溯搜索模塊。將上述實現(xiàn)不同功能的模塊進行組合連接,就得到了一個針對MAS模型的新完全求解算法LGC算法。該算法描述如下:a)按照模型要求生成MAS模型隨機實例T(0),并構(gòu)建相應的增廣矩陣S(0)。將T(0)分解為線性子問題TL(0)和非線性子問題TNL(0),并記相應的增廣子矩陣為MTL(0)和MNTL(0)。b)循環(huán)運行摘葉算法預處理模塊即在第i輪循環(huán)中檢查T(i)是否存在符合2.1節(jié)中摘葉算法執(zhí)行條件的方程:如果存在這樣的方程,則執(zhí)行摘葉算法預處理程序LFprocedure,得到新的等價實例T(i+1)和相應的增廣矩陣S(i+1);否則跳出循環(huán)體。c)如果此時等價實例T(i)為空,則返回SAT,實例有解;如果此時等價實例T(i)不為空,則以實例線性子問題TL(i)對應的矩陣MTL(i)為對象運行高斯消去算法預處理程序GEprocedure,即依次確定對角元變量,并用對角元變量所在行對其他行進行布爾加法運算,直至確定所有的對角元。d)對非對角元變量的列進行非零元素統(tǒng)計,按照統(tǒng)計值由小到大的順序重新排列非對角元變量,并重新以與現(xiàn)有矩陣排列相反的順序?qū)λ凶兞窟M行排序標號。e)按照現(xiàn)有的變量標號順序運行回溯算法程序CBprocedure,如果出現(xiàn)退回無法再回溯的矛盾,則返回UNSAT,實例無解;如果所有變量均被賦值且無矛盾,則返回SAT,實例有解。以下是三個具體的算法模塊描述:將上述的三個子程序模塊按照LGC算法的框架描述進行組合鏈接再加上相應的輔助進程,就可以得到實際的求解MAS模型問題的實際算法程序。其中CBprocedure中的矛盾分析程序和回溯程序描述見文獻。4模型閾值估計及與理論分析的對比本文將LGC算法應用于等概率MAS模型實例的求解,通過計算在給定約束方程密度a的條件下大量隨機實例中可滿足實例(存在解的實例)所占的比例,本文研究了等概率MAS模型平均可滿足概率隨著約束方程密度a增加的變化曲線,并進一步給出了等概率MAS模型的閾值估計和相應的偏差范圍。在對1000個不同規(guī)模的隨機MAS模型實例運行LGC算法確定其是否有解的基礎上,得到的平均可滿足概率隨著約束方程密度變化的相圖,針對三類不同變量規(guī)模實例求解的數(shù)值結(jié)果如圖1所示。同時,本文通過定位不同規(guī)模變量對應相圖中曲線交點,得到了可滿足性閾值的估計結(jié)果及其與理論分析結(jié)果的對比,如表1所示。為了將LGC算法的效率與一般帶回溯的完全算法效率進行比較,文中給出了對10000個實例運行摘葉算法預處理