最大可滿足性問題的博弈算法研究.pdf

1、最大可滿足性問題(MaxSAT)是人工智能領(lǐng)域研究的核心問題之一，很多復(fù)雜的實際問題都可以通過MaxSAT建模并求解，對于MaxSAT問題的研究具有理論和實際的雙重意義。近些年，隨著科學(xué)研究的進步和工業(yè)技術(shù)的發(fā)展，MaxSAT問題的規(guī)模成倍增長。為滿足新的MaxSAT問題求解的需求，本文基于布爾博弈模型提出兩個適用于不同規(guī)模MaxSAT實例求解的博弈算法，包括用于求解一般規(guī)模MaxSAT實例的基本博弈算法bgmaxsat和用于求解大規(guī)模

2、MaxSAT實例的分組博弈算法bgmaxsat_m。
　　本文的主要工作總結(jié)為以下四點。(1)我們提出一種將MaxSAT實例映射為布爾博弈模型的建模方法，通過博弈參與者的策略選擇過程來模擬MaxSAT實例中的變量賦值過程。博弈參與者的策略基于重新定義的目標(biāo)函數(shù)和收益計算函數(shù)進行選擇，并依據(jù)其他參與者的策略不斷更新。(2)針對MaxSAT問題的特征，我們對經(jīng)典布爾博弈模型進行改進，提出基于動態(tài)收益矩陣的動態(tài)博弈模型。在動態(tài)博弈模型中

3、，參與者的收益矩陣在博弈過程中實時變化，使得所有參與者都能夠按照自身的目標(biāo)函數(shù)快速收斂?；趧討B(tài)博弈模型，我們提出求解一般規(guī)模MaxSAT實例的基本博弈算法bgmaxsat。(3)針對大規(guī)模MaxSAT實例產(chǎn)生大量博弈參與者的問題，我們提出一種新的博弈參與者聯(lián)盟構(gòu)建方法。我們基于無向圖重建博弈參與者間的關(guān)系，將相互間無關(guān)系的參與者劃分為一組來構(gòu)建聯(lián)盟，從而有效降低博弈規(guī)模。(4)基于博弈參與者聯(lián)盟，我們提出求解大規(guī)模MaxSAT實例的分

4、組博弈算法bgmaxsat_m在bgmaxsat_m算法中，我們將博弈的基本單位設(shè)定為參與者聯(lián)盟，并將信息共享通道僅設(shè)定在聯(lián)盟之間。
　　在實驗部分，我們基于4個測試數(shù)據(jù)集進行了多組對比實驗。首先，我們在846個一般規(guī)模MaxSAT實例上評估bgmaxsat算法，并與CCLS2016、Swcca-ms、ahmaxsat155三個最新算法進行對比。實驗結(jié)果表明，在求解一般規(guī)模的MaxSAT實例時，bgmaxsat算法的性能與CCLS

5、2016算法相近，其分別在不同分類的實例上各占優(yōu)勢，同時優(yōu)于Swcca-ms算法和ahmaxsat155算法。其次，我們在100個變量規(guī)模超過105的大規(guī)模MaxSAT實例上評估bgmaxsat_m算法，并與CCLS2016、wbo、Open-wbo、pwbo、CnC-LS五個最新算法進行對比。實驗結(jié)果表明，在求解大規(guī)模MaxSAT實例時，bmgaxsat_m算法的性能在所有分類的實例上均明顯優(yōu)于CCLS2016算法、wbo算法和pwb