基于MiniSAT的命題極小模型計(jì)算方法

張 麗 王以松,2 謝仲濤 馮仁艷

1(貴州大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 貴陽(yáng) 550025) 2(公共大數(shù)據(jù)國(guó)家重點(diǎn)實(shí)驗(yàn)室(貴州大學(xué)) 貴陽(yáng) 550025) (gs.lizhang18@gzu.edu.cn)

命題可滿足性問(wèn)題(satisfiability problem, SAT)是計(jì)算機(jī)科學(xué)和人工智能研究的中心問(wèn)題之一，在自動(dòng)推理和人工智能等領(lǐng)域都具有非常重要的理論意義和實(shí)踐價(jià)值，世界各國(guó)的相關(guān)研究人員在這方面做了大量的工作，提出了許多求解算法和大量的改進(jìn)技術(shù).

SAT問(wèn)題的模型即為命題公式可滿足時(shí)，使得命題公式可滿足的一組真值指派中賦值為真的原子集合.當(dāng)命題公式可滿足時(shí)，極小模型的計(jì)算和驗(yàn)證問(wèn)題就成了人們關(guān)注的重點(diǎn)問(wèn)題.當(dāng)命題公式不可滿足時(shí)，人們通常對(duì)分析不可滿足性感興趣.極大可滿足問(wèn)題(maximum satisfiability problem, MaxSAT)[1-2]和極小不可滿足子集(minimal unsatis-fiable subset, MUS)問(wèn)題都屬于這種分析.MaxSAT是SAT問(wèn)題的優(yōu)化版，其目標(biāo)是找到一組真值指派使得CNF公式中滿足(不滿足)子句的數(shù)量極大化(極小化).隨著MaxSAT技術(shù)的不斷發(fā)展，MaxSAT問(wèn)題在Android惡意軟件檢測(cè)[3]、排課[4]和診斷[5]等問(wèn)題中都得到了很好的應(yīng)用.MUS是SAT問(wèn)題的擴(kuò)展，是計(jì)算一個(gè)公式集的極小不可滿足公式子集，其所有真子集均是可滿足的.在現(xiàn)實(shí)中許多重要問(wèn)題可以編碼為MUS問(wèn)題進(jìn)行求解[6-8].

基于極小模型的推理一直是人工智能研究的重要主題[9-11].極小模型也是回答集程序設(shè)計(jì)(answer set programming, ASP)和其他非單調(diào)知識(shí)表示和推理范式的核心[12]，例如，限制邏輯[13-16]、缺省邏輯[17]、極小診斷[18-22].和穩(wěn)定模型語(yǔ)義下的邏輯程序[23-24]等.極小模型主要涉及2個(gè)任務(wù)，對(duì)于一個(gè)給定的子句理論T，計(jì)算(任務(wù)1)：尋找極小模型即計(jì)算出T的一個(gè)極小模型；判定(任務(wù)2)：驗(yàn)證極小模型即檢驗(yàn)給定的一個(gè)原子集是否是T的極小模型.

關(guān)于極小模型推理的研究結(jié)果表明，在一般情況下，這些問(wèn)題是難以處理的.事實(shí)上，即使是正子句理論，計(jì)算其極小模型也是PNP[O(log n)]-hard[25].對(duì)于一個(gè)給定的理論，驗(yàn)證一個(gè)模型是否是其極小模型是co-NP-complete[26].關(guān)于極小模型求解這一問(wèn)題的研究也吸引了一部分專家學(xué)者的注意，他們認(rèn)為挑選出能夠有效解決這些問(wèn)題的各個(gè)理論是有意義的[27-29].目前計(jì)算子句理論的極小模型，可將子句理論轉(zhuǎn)換成邏輯程序后用ASP求解器計(jì)算其回答集，ASP求解器的典型代表有clasp[30]，clingo[31]，DLV[32]等.

2016年Ben-Eliyahu-Zohary等人[33-34]提出了基于極小模型分解的計(jì)算極小模型的算法ModuMin和驗(yàn)證極小模型的算法CheckMin，使極小模型計(jì)算和驗(yàn)證的艱巨任務(wù)在原始理論的子集之間進(jìn)行分解，把一個(gè)任務(wù)分解成多個(gè)子任務(wù)進(jìn)行計(jì)算.但是該驗(yàn)證算法CheckMin并不可靠.

2020年王以松等人對(duì)這一問(wèn)題展開(kāi)了進(jìn)一步的研究，提出了極小歸約(minimal reduct, MR).極小歸約是對(duì)Ben-Eliyahu-Zohary等人[33-34]的分解極小模型定理的補(bǔ)充，從而得到一個(gè)可靠的驗(yàn)證極小模型的算法CheckMinMR.

每年可滿足性理論和應(yīng)用方面的國(guó)際會(huì)議都會(huì)組織SAT競(jìng)賽，以求能夠找到一組最快的SAT求解器.MiniSAT[35]是一個(gè)極簡(jiǎn)并開(kāi)源的SAT求解器，贏得了2005年SAT競(jìng)賽的所有工業(yè)類別測(cè)試.MiniSAT的出現(xiàn)對(duì)于SAT問(wèn)題的未來(lái)研究以及使用SAT的應(yīng)用都是一個(gè)很好的起點(diǎn).MiniSAT始于2003年，其目的是通過(guò)小型而高效的，并且提供有良好文檔的SAT求解器來(lái)幫助人們進(jìn)入SAT領(lǐng)域.其第1個(gè)版本只有600多行C語(yǔ)言代碼，同時(shí)MiniSAT仍包含了2003年最新SAT求解的核心算法.在之后的版本中，代碼量雖有所增長(zhǎng)，但相較于其他的SAT求解器而言MiniSAT的代碼量仍然非常小，為我們的代碼實(shí)現(xiàn)提供了非常有利的基礎(chǔ).

本文的主要工作有3個(gè)部分：

1) 在MiniSAT求解器的最新版本MiniSAT2.2的基礎(chǔ)上，對(duì)源代碼進(jìn)行修改實(shí)現(xiàn)了計(jì)算子句理論極小模型的算法MMSAT.

2) 將MMSAT算法與CheckMinMR算法結(jié)合成MRSAT實(shí)現(xiàn)快速極小模型的求解，將2個(gè)算法進(jìn)行結(jié)合的目的是在驗(yàn)證一個(gè)模型是否是極小模型時(shí)，采用分解模型的思想將1個(gè)任務(wù)分解成多個(gè)子任務(wù)的方法來(lái)驗(yàn)證.即分解一個(gè)理論及其模型，當(dāng)兩者都變?yōu)榭諘r(shí)，則意味著該模型確實(shí)是給定理論的極小模型.

3) 使用本文的2個(gè)算法對(duì)大量隨機(jī)生成的子句理論以及SAT國(guó)際競(jìng)賽上的部分基準(zhǔn)測(cè)試用例進(jìn)行極小模型的計(jì)算；本文選擇clingo作為評(píng)估標(biāo)準(zhǔn)，將所有測(cè)試用例分別轉(zhuǎn)換成邏輯程序，使用clingo計(jì)算其回答集，clingo是目前計(jì)算邏輯程序回答集最有效的實(shí)現(xiàn)，它是gringo和clasp的組合；同時(shí)記錄本文的2個(gè)算法計(jì)算極小模型使用的時(shí)間及clingo使用的時(shí)間.實(shí)驗(yàn)結(jié)果表明，本文提出的2個(gè)方法對(duì)隨機(jī)子句理論和SAT競(jìng)賽工業(yè)測(cè)試用例十分有效，計(jì)算極小模型的速度都明顯快于clingo.而且從在計(jì)算結(jié)果正確率上的表現(xiàn)來(lái)看，本文的2個(gè)方法也更加穩(wěn)定.

1 預(yù)備知識(shí)

子句δ是由1個(gè)或多個(gè)文字通過(guò)邏輯或(∨)連接組成.子句理論Σ是由1組有限子句構(gòu)成.SAT問(wèn)題中的CNF公式由1個(gè)或多個(gè)子句通過(guò)邏輯與連接起來(lái)組成.若子句δ在模型M下為真，則稱M滿足δ，記為Mδ.

定義1.極小模型.給定一個(gè)命題公式Φ及其一個(gè)模型M，稱M是Φ的極小模型，當(dāng)且僅當(dāng)不存在M′?M，使得Φ可滿足.

一個(gè)析取邏輯程序P是由具有如下形式的規(guī)則構(gòu)成的有限集合：

a1∨a2∨…∨am←am+1,am+2,…,an,
notan+1,notan+2,…,notal，

(1)

其中ai(1≤i≤l)是原子，a1∨a2∨…∨am表示該規(guī)則的頭(head)，am+1,am+2,…,an,notan+1,notan+2,…,notal表示該規(guī)則的體(body).令r是形如式(1)的規(guī)則，記H(r)={a1,a2,…,am}，B+(r)={am+1,am+2,…,an}，B-(r)={an+1,an+2,…,al}，B(r)=B+(r)∪notB-(r)，通常將規(guī)則r表示成H(r)←B(r).令A(yù)(r)表示規(guī)則r中的原子的集合，A(P)表示邏輯程序P中原子的集合.當(dāng)l=n時(shí)，規(guī)則r被稱作是正規(guī)則，如果程序中所有規(guī)則都是正規(guī)則，則該程序?yàn)檎绦?令M?A(P)，P關(guān)于M進(jìn)行GL-歸約的結(jié)果記為PM，PM={H(r)←B+(r)|r∈P,B-(r)∩M=?}.若M是PM的極小模型，則稱M就是P的穩(wěn)定模型(也稱為回答集).

一個(gè)子句δ可轉(zhuǎn)換析取邏輯程序的規(guī)則r，且B-(r)=?，即由CNF公式轉(zhuǎn)換的邏輯程序?yàn)檎绦?因?yàn)閷?duì)正程序P，PM=P，故正程序的回答集就是其極小模型.

1.1 依賴圖

令P是邏輯程序，P的依賴圖(dependency graph)是一個(gè)有向圖，記為GP=(V,E).GP的定義為：

1)P中的所有原子A(P)和子句δ都是GP中的節(jié)點(diǎn)；

2) 如果a∈B+(δ)，則對(duì)應(yīng)的邊e表示為(a,δ)；如果a∈H(δ)，則e表示為(δ,a)；

邏輯程序P的強(qiáng)依賴圖SGP是由依賴圖GP構(gòu)造的有向無(wú)環(huán)圖，對(duì)于GP中的每一個(gè)強(qiáng)連通組件，在SGP中都將其折疊成為一個(gè)節(jié)點(diǎn).若GP中存在一條邊e，在GP中是由強(qiáng)連通組件sc1中的一個(gè)節(jié)點(diǎn)指向強(qiáng)連通組件sc2中的節(jié)點(diǎn)；在SGP中這條邊表示為由sc1指向sc2即可.一個(gè)有向圖中入度為0的節(jié)點(diǎn)被稱為源(source).若SGP中源中不包含原子，則稱該源為空.

1.2 極小模型分解

CheckMin算法是Ben-Eliyahu-Zohary等人[33-34]提出對(duì)給定子句理論的一個(gè)模型進(jìn)行驗(yàn)證，檢驗(yàn)該模型是否為該子句理論的極小模型.

對(duì)于任意一個(gè)子句理論T，令X和Y為原子集合，且X∩Y=?，則Reduce(T,X,Y)是將X在T中的原子全部賦值為真，Y在T中的原子全部賦值為假，從而得到約簡(jiǎn)的子句理論.

對(duì)于給定T的一個(gè)源S，TS表示在T中只包含S的子句集.

定理1.極小模型分解定理[33-34].給定一個(gè)子句理論T和T的一個(gè)模型M，令圖G表示T的強(qiáng)依賴圖SG，如果G中存在一個(gè)源S使得X=S∩M是TS的極小模型，令T′←Reduce(T,X,S-X)，則M-X是T′的極小模型.

根據(jù)定理1，Ben-Eliyahu-Zohary等人[33-34]提出CheckMin算法(算法1).然而B(niǎo)en-Eliyahu-Zohary等人[33-34]提出的CheckMin算法并不是完備的，因此他們又提出了完備性的充分條件——模塊化性質(zhì).

定義2.模塊化性質(zhì).

1) 如果子句理論T的強(qiáng)依賴圖SGT中只有一個(gè)強(qiáng)連通組件，則T的一個(gè)極小模型M相對(duì)于T具有模塊化性質(zhì)；

2) 給定一個(gè)子句理論T和T的一個(gè)模型M，如果T中存在源S使得X=S∩M是TS的一個(gè)極小模型，并且M-X是T′←Reduce(T,X,S-X)的極小模型，則M-X相對(duì)于T′具有模塊化性質(zhì).

算法1.CheckMin(T,M).

輸入：一個(gè)子句理論T、T的一個(gè)模型M;

輸出：true或false.

①G←SGT;

② 迭代地刪除G中所有為空的源;

③ whileG中存在源S，且S是TS的極小模型

do

④X←M∩S;

⑤M←M-X;

⑥T←Reduce(T,X,S-X);

⑦G←SGT;

⑧ 迭代地刪除G中所有為空的源;

⑨ end while

⑩ ifM=? then return true;

如果T的極小模型M關(guān)于T具有模塊化性質(zhì)，則CheckMin(T,M)返回true.

1.3 極小歸約

對(duì)于極小模型分解定理的不完備，王以松等人對(duì)此提出了極小歸約，對(duì)極小模型分解定理進(jìn)行補(bǔ)充.同時(shí)對(duì)算法CheckMin也進(jìn)行了修改得到新的完備算法CheckMinMR(算法2).

算法2.CheckMinMR(T,M).

輸入：一個(gè)子句理論T、T的一個(gè)模型M;

輸出：true或false.

returnCheckMin(MR(T,M),M).

定義3.Minimal Reduct.給定一個(gè)邏輯程序P和原子集S，S?A(P)則P關(guān)于S的極小歸約表示為MR(P,S)，MR(P,S)是正邏輯程序：

{H(r)∩S←B+(r)|r∈P,
B+(r)?S&B-(r)∩S=?}.

(2)

從極小歸約的定義可以得到一個(gè)非常明顯的結(jié)論A(MR(P,S))?S.極小歸約是根據(jù)閉區(qū)間假設(shè)來(lái)約簡(jiǎn)一個(gè)邏輯程序，即S中的原子被假定為真，而其它原子被假定為假.

引理1[35].令δ表示一條子句，M表示一個(gè)模型，有：

1)Mδ當(dāng)且僅當(dāng)MMR({δ},M)；

定理2.極小模型性質(zhì)[35].令T是可滿足的子句理論，且S?A(T)，則3種情況是等價(jià)的：

1)S是T的一個(gè)極小模型；

2)S是MR(T,S)的最小模型；

3)S={p|MR(T,S)p}.

2 計(jì)算極小模型的新方法MMSAT和MRSAT

本節(jié)將詳細(xì)介紹本文提出的2個(gè)計(jì)算子句理論的極小模型算法，分別是基于SAT求解器的算法MMSAT和基于極小歸約的算法MRSAT.

2.1 基于SAT的極小模型算法MMSAT

MMSAT算法的主要思想是：當(dāng)子句理論T是可滿足時(shí)，SAT求解器可計(jì)算出T的一個(gè)模型M；將該模型取反得到一子句∨M，并且將不屬于M的其余原子也分別取反得到子句集將這些子句添加到T中得到一個(gè)新的子句集T′，再用SAT求解器迭代該過(guò)程計(jì)算.若M是T的極小模型，則新的子句集T′是不可滿足的；反之，則說(shuō)明M不是T的極小模型.根據(jù)這個(gè)思想我們?cè)O(shè)計(jì)出MMSAT算法(算法3).

算法3.MMSAT(T).

輸入：一個(gè)子句理論T;

輸出：T的一個(gè)極小模型M或無(wú)模型.

① ifT是不可滿足的

② return無(wú)模型;

③ end if

④ whileT是可滿足的do

⑤M←MiniSAT(T);

⑥T←T∪{∨M}∪

⑦ end while

⑧ returnM.

引理2.給定一個(gè)子句理論T及其一個(gè)模型M，M是T的極小模型當(dāng)且僅當(dāng)T∪{∨M}∪不可滿足.

引理2顯然成立.MMSAT算法(算法3)的行⑤計(jì)算T的一個(gè)模型，其while循環(huán)(行④～⑦)每次迭代生成的模型是其前一次生成的模型的真子集，因M是有窮的，故循環(huán)一定會(huì)在有限步內(nèi)終止，引理2保證終止時(shí)計(jì)算出來(lái)的M是輸入子句理論T的極小模型.

2.2 基于極小歸約的極小模型算法MRSAT

MRSAT算法(算法4)是MMSAT與基于極小歸約的極小模型驗(yàn)證算法CheckMinMR的結(jié)合.首先由MiniSAT計(jì)算子句理論的模型，然后由Check-MinMR檢驗(yàn)計(jì)算出的模型是否是其極小模型.

下面的引理3可保證算法MRSAT的可靠性.

引理3.給定一個(gè)子句理論T，及其一個(gè)模型M，若M′?M，M′T，則MR(T′,M′)≡MR(T,M′)，其中T′=MR(T,M).

證明.

基始：當(dāng)T=T′時(shí)，MR(T,M′)≡MR(T′,M′)成立.

步驟：令δ∈T，{δ′}=MR({δ},M)，由極小歸約的定義可得MR({δ},M′)={H(δ)∩M′←B+(δ)|B+(δ)?M′}.MR({δ′},M′)=MR(MR({δ},M),M′)={H(δ)∩M∩M′←B+(δ)|B+(δ)?M′?M}.已知M′?M，綜上可得MR({δ},M′)≡MR({δ′},M′).又因δ∈T，所以MR(T,M′)≡MR(T′,M′)，T′=MR(T,M).

證畢.

算法4.MRSAT(T).

輸入：一個(gè)子句理論T;

輸出：T的一個(gè)極小模型M或無(wú)模型.

① ifT是不可滿足的

② return無(wú)模型;

③ end if

④ whileT是可滿足的do

⑤M←MiniSAT(T);

⑥ ifCheckMinMR(MR(T,M),M)

⑦ returnM;

⑧ end if

⑨T←T∪{∨M}∪

3 實(shí)驗(yàn)結(jié)果與分析

我們?cè)贛iniSAT的基礎(chǔ)上實(shí)現(xiàn)了算法3和算法4，在隨機(jī)3CNF公式和SAT國(guó)際競(jìng)賽上的部分基準(zhǔn)測(cè)試用例上進(jìn)行了測(cè)試.在實(shí)驗(yàn)中我們使用的clingo是目前的最新版本clingo5.4(1)https://potassco.org，它是基化器gringo[36]和ASP求解器clasp的結(jié)合.本實(shí)驗(yàn)的工作環(huán)境是Linux5.1.11、8核3.50 GHz的CPU和32 GB內(nèi)存.實(shí)驗(yàn)代碼及數(shù)據(jù)地址：https://github.com/zhangli-hub123/minimal-model.

3.1 隨機(jī)3CNF公式

實(shí)驗(yàn)中的3CNF公式是通過(guò)設(shè)置原子數(shù)量和子句數(shù)量隨機(jī)生成的子句長(zhǎng)度為3的CNF公式，其中原子數(shù)量n的范圍設(shè)置為50～1 000，增幅為50；子句數(shù)量m的范圍是3.0×n～5.0×n，增幅為0.1×n；對(duì)于其中的每種情況都分別有10個(gè)不同的3CNF文件，一個(gè)文件即一個(gè)CNF公式.我們使用MMSAT，MRSAT，clingo分別計(jì)算這些3CNF公式的極小模型，并統(tǒng)一設(shè)置計(jì)算時(shí)間上限為1 800 s.文件的計(jì)算結(jié)果的輸出類型有可滿足(SAT)、不可滿足(UNSAT)和計(jì)算超時(shí)被終止(TO).我們按照輸出類型分別統(tǒng)計(jì)了所有計(jì)算的平均結(jié)果.

圖1～3分別展示了clingo，MMSAT，MRSAT計(jì)算隨機(jī)3CNF公式的極小模型的平均CPU時(shí)間.如圖1所示，clingo的峰值在原子數(shù)量為900，子句數(shù)量為3.8×900時(shí)，CPU時(shí)間為1 711 s;MMSAT和MRSAT在相同情況下的CPU時(shí)間分別為499 s和505 s.此時(shí)MMSAT用時(shí)最少，而clingo所用時(shí)間幾乎是MMSAT和MRSAT的3倍.如圖2和圖3所示，MMSAT和MRSAT耗時(shí)最多的情況均是原子數(shù)量為800，子句數(shù)量為3.9×800，此時(shí)它們的CPU時(shí)間分別是760 s和758 s，而clingo在此情況下的CPU時(shí)間為842 s.此時(shí)也是clingo用時(shí)最長(zhǎng)，而MRSAT用時(shí)最少.

Fig.1 The average CPU time of minimal model by clingo on random 3CNF formulas圖1 clingo計(jì)算隨機(jī)3CNF公式極小模型的平均CPU時(shí)間

Fig.2 The average CPU time of minimal model by MMSAT on andom 3CNF formulas圖2 MMSAT計(jì)算隨機(jī)3CNF公式極小模型的平均CPU時(shí)間

Fig.3 The average CPU time of minimal model by MRSAT on random 3CNF formulas圖3 MRSAT計(jì)算隨機(jī)3CNF公式極小模型的平均CPU時(shí)間

實(shí)驗(yàn)結(jié)果表明：計(jì)算隨機(jī)3CNF公式的極小模型時(shí)，MMSAT和MRSAT在計(jì)算速度上的優(yōu)勢(shì)十分顯著，從整體來(lái)看，幾乎所有的情況下MMSAT和MRSAT的用時(shí)均比clingo少很多.而MMSAT和MRSAT之間則無(wú)十分明顯的差別.

3.2 SAT競(jìng)賽基準(zhǔn)測(cè)試實(shí)例

本實(shí)驗(yàn)所用的基準(zhǔn)測(cè)試實(shí)例均獲取自SAT國(guó)際競(jìng)賽，分別是2009年工業(yè)上的SAT實(shí)際測(cè)試用例(2)http://satcompetition.org/和2020年的測(cè)試實(shí)例(3)https://satcompetition.github.io/2020/downloads.html.我們從2009年的工業(yè)實(shí)例中隨機(jī)挑選了7類實(shí)例，共計(jì)109個(gè)測(cè)試文件；從2020年的實(shí)例中隨機(jī)選出43個(gè)實(shí)例，記為SAT2020，本文實(shí)驗(yàn)所用實(shí)例共計(jì)152個(gè)，即152個(gè)CNF公式.首先分別使用MMSAT，MRSAT計(jì)算所有測(cè)試實(shí)例的極小模型；并且以clingo5.4作為對(duì)比的基準(zhǔn)程序，使用clingo5.4計(jì)算這些測(cè)試實(shí)例所對(duì)應(yīng)的邏輯程序的回答集.由于clingo5.4在工業(yè)實(shí)例中出現(xiàn)了計(jì)算出錯(cuò)情況，因此我們?cè)谠u(píng)估比較中加入gringo3.0.5+claspD1.1(其中g(shù)ringo是claspD的前端).由于實(shí)例比較復(fù)雜，計(jì)算實(shí)例模型所需時(shí)間較長(zhǎng)，并且本文算法是在計(jì)算模型的基礎(chǔ)上更進(jìn)一步計(jì)算極小模型，此時(shí)可能需要迭代多次，因此本實(shí)驗(yàn)將所有實(shí)例的計(jì)算時(shí)間上限設(shè)置為7 200 s.

如表1所示，我們對(duì)4種方法分別按照輸出類型可滿足(SAT)、不可滿足(UNSAT)和超時(shí)(TO)統(tǒng)計(jì)了實(shí)例的計(jì)算結(jié)果(4)SAT，UNSAT，TO之外的其他實(shí)例均為內(nèi)存不足.MRSAT在所有的實(shí)例類中均未出現(xiàn)內(nèi)存不足..在規(guī)定時(shí)間內(nèi)clingo和claspD計(jì)算完成(即輸出類型為可滿足或不可滿足)的實(shí)例的數(shù)量均明顯少于MMSAT和MRSAT，其中，clingo在bioinfo，c32sat，sat08實(shí)例類中共有11個(gè)實(shí)例發(fā)生了內(nèi)存不足(而被killed)；在SAT2020中有8個(gè)實(shí)例發(fā)生了內(nèi)存不足.gringo+claspD在c32sat中也有一個(gè)實(shí)例發(fā)生了內(nèi)存不足(而出現(xiàn)std∷bad_alloc)；且在SAT2020中有8個(gè)實(shí)例發(fā)生了內(nèi)存不足.MMSAT在SAT2020中有1個(gè)實(shí)例發(fā)生了內(nèi)存不足(而出現(xiàn)INDETERMINATE).

值得注意的是，如表1所示，bioinfo實(shí)例類中clingo在規(guī)定時(shí)間內(nèi)完成計(jì)算的實(shí)例數(shù)量為12，全部為不可滿足.而MMSAT和MRSAT完成計(jì)算的實(shí)例數(shù)量均為20個(gè)，其中可滿足的實(shí)例數(shù)量為9個(gè)，不可滿足的為11個(gè).通過(guò)對(duì)實(shí)驗(yàn)記錄數(shù)據(jù)對(duì)比，我們發(fā)現(xiàn)在clingo計(jì)算的結(jié)果為不可滿足的12個(gè)實(shí)例中，有7個(gè)實(shí)例在claspD，MMSAT，MRSAT中的結(jié)果都為可滿足.表1中括號(hào)內(nèi)的數(shù)字表示clingo計(jì)算出錯(cuò)(5)可滿足的實(shí)例由clingo計(jì)算出的結(jié)果為不可滿足.的實(shí)例個(gè)數(shù).因此，我們將MMSAT和MRSAT計(jì)算的極小模型分別與文件中的子句進(jìn)行了驗(yàn)證，驗(yàn)證結(jié)果均表明這7個(gè)實(shí)例確實(shí)是可滿足的.同時(shí)，我們對(duì)所有測(cè)試實(shí)例的結(jié)果都進(jìn)行了對(duì)比，在用例類sat08中和SAT2020也分別發(fā)現(xiàn)了一個(gè)實(shí)例為clingo計(jì)算出錯(cuò)的情況.

我們還統(tǒng)計(jì)了計(jì)算完成的實(shí)例的平均CPU執(zhí)行時(shí)間，如圖4所示.圖4中MMSAT在crypto/md5gen實(shí)例類下計(jì)算極小模型的用時(shí)最多，除此之外，均是claspD完成計(jì)算的所需平均時(shí)間最長(zhǎng)，其次便是clingo用時(shí)較長(zhǎng).整體來(lái)看MMSAT計(jì)算極小模型的平均時(shí)間最短，效果最好，MRSAT次之.對(duì)計(jì)算結(jié)果為可滿足的實(shí)例的平均CPU執(zhí)行時(shí)間我們也做了統(tǒng)計(jì)，如圖5所示，在c32sat用例類下是MRSAT用時(shí)最多，在此實(shí)例類下clingo和claspD均沒(méi)有算出實(shí)例的極小模型；其余均是claspD耗時(shí)較長(zhǎng)，而MMSAT用時(shí)最短.

Table 1 The Results on Industrial SAT Benchmarks表1 計(jì)算SAT工業(yè)實(shí)例的結(jié)果對(duì)比

Fig.4 The average CPU time on industrial SAT benchmarks correctly completed圖4 正確完成計(jì)算SAT工業(yè)實(shí)例平均CPU執(zhí)行時(shí)間

Fig.5 The average CPU time of computing a minimal model on industrial SAT benchmarks圖5 計(jì)算SAT工業(yè)實(shí)例極小模型的平均CPU執(zhí)行時(shí)間

綜上，在MiniSAT2.2基礎(chǔ)上實(shí)現(xiàn)的計(jì)算極小模型的算法MMSAT和MRSAT是非常有效的，其計(jì)算極小模型的速度都明顯快于最新版的clingo和claspD，并且clingo發(fā)生了計(jì)算錯(cuò)誤，clingo和claspD均出現(xiàn)了內(nèi)存不足，而我們提出的算法則更加穩(wěn)定.

4 總 結(jié)

本文提出了基于SAT和基于極小歸約的計(jì)算命題極小模型的算法MMSAT和MRSAT，首先證明了算法的可靠性，其次對(duì)算法進(jìn)行了實(shí)現(xiàn).最后，分別使用MMSAT，MRSAT，clingo5.4在隨機(jī)3CNF公式和SAT國(guó)際競(jìng)賽上的工業(yè)實(shí)例上做了實(shí)驗(yàn)，在SAT國(guó)際競(jìng)賽上的工業(yè)實(shí)例上還使用gringo3.0.5+claspD1.1進(jìn)行了測(cè)試.實(shí)驗(yàn)表明，使用MMSAT算法和MRSAT算法計(jì)算命題的極小模型，在時(shí)間上明顯快于claspD和clingo，在正確率上也明顯優(yōu)于clingo.

在未來(lái)的工作中，根據(jù)分解極小模型的主要思想，在基于極小歸約的算法MRSAT中可以做進(jìn)一步的改進(jìn).通過(guò)采用并行計(jì)算的方式，使得對(duì)極小模型的驗(yàn)證更高效，從而提高極小模型計(jì)算的速度.此外，根據(jù)極小歸約的性質(zhì)，我們考慮將其直接應(yīng)用在MMSAT算法中，將求解子句理論T的極小模型轉(zhuǎn)化為求解極小歸約之后子句理論的極小模型.我們將對(duì)這些問(wèn)題做更進(jìn)一步的研究.