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

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

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