基于最大可滿足性問題的專業(yè)實(shí)驗(yàn)方案設(shè)計

劉燕麗　余艷　張婷

摘要：基于最大可滿足性問題的專業(yè)實(shí)驗(yàn)方案以組合拍賣為應(yīng)用背景，采用命題邏輯建模、分支限界算法，針對問題設(shè)計優(yōu)化的存儲結(jié)構(gòu)。專業(yè)實(shí)驗(yàn)方案展現(xiàn)了一個完整的工業(yè)問題的解決過程，內(nèi)容涉及程序設(shè)計語言、數(shù)據(jù)結(jié)構(gòu)、離散數(shù)學(xué)、算法設(shè)計等計算機(jī)核心課程相關(guān)內(nèi)容，有助于加強(qiáng)學(xué)生專業(yè)知識的系統(tǒng)化。

關(guān)鍵詞關(guān)鍵詞：實(shí)驗(yàn)教學(xué)；算法設(shè)計；數(shù)據(jù)結(jié)構(gòu)；NP問題

DOIDOI：10.11907/rjdk.143639

中圖分類號：TP302

文獻(xiàn)標(biāo)識碼：A文章編號文章編號：16727800（2015）002003703

作者簡介作者簡介：劉燕麗（1980-）， 女，河南西平人，碩士，武漢科技大學(xué)理學(xué)院講師，研究方向?yàn)镹P問題的高效求解、近似算法。

0引言

目前，學(xué)生在程序設(shè)計學(xué)習(xí)過程中尚不能獨(dú)立建立課程之間的橫向聯(lián)系，對所學(xué)專業(yè)缺乏系統(tǒng)、立體的認(rèn)識[13]。造成這一問題的因素較多，若在教學(xué)活動中多設(shè)計可以展現(xiàn)計算機(jī)解決某類自然界問題的完整過程的實(shí)驗(yàn)方案，將有助于培養(yǎng)學(xué)生系統(tǒng)、立體、計算機(jī)程序方式的問題解決能力?；谧畲罂蓾M足性問題的專業(yè)實(shí)驗(yàn)方案以培養(yǎng)學(xué)生問題解決能力和建立系統(tǒng)化思維模式為目標(biāo)，以組合優(yōu)化問題為背景，給出最大可滿足性問題的求解算法設(shè)計，闡明如何利用命題邏輯對實(shí)際問題進(jìn)行建模，如何選擇數(shù)據(jù)存儲方式以及對復(fù)雜問題內(nèi)部關(guān)系進(jìn)行解剖，是利用計算機(jī)解決社會活動問題的一個完整案例。

1最大可滿足性問題模型優(yōu)化

最大可滿足性問題（Maximum Satisfiability Problem，MaxSAT）是SAT問題的一個重要擴(kuò)展，是經(jīng)典的NP難題。最大可滿足性問題利用命題邏輯以及謂詞描述絕大多數(shù)組合優(yōu)化問題，具有強(qiáng)大的建模能力，如最大團(tuán)、最少圖著色數(shù)、最大割集、最小可滿足性問題等均可轉(zhuǎn)換為MaxSAT問題來求解。同時，該問題在工業(yè)生產(chǎn)和社會活動中有廣泛應(yīng)用，如生產(chǎn)調(diào)度、組合拍賣、超大規(guī)模集成電路測試、排課問題等。MaxSAT算法國際競賽網(wǎng)站每年都接收來自不同領(lǐng)域工業(yè)問題的新算例。

1.1MaxSAT問題相關(guān)概念

設(shè)F=x1∧（x-1∨x2∨x3）∧（x-4∨x-5）。這里xi是取值為真或假的命題變元。真值指派是指命題變元取“真”或“假”的狀態(tài)。符號xi及其否定形式x-i稱為文字，記為li。xi稱為正文字，x-i稱為負(fù)文字。xi=1時，正文字為真，xi=0時，負(fù)文字為真。若干文字的析取項(xiàng)稱為子句，如x-1∨x2∨x3。特別地，若只含有1個文字，稱之為單子句，如x1。不含文字的子句是空子句，記為□。若干子句的合取構(gòu)成合取范式，記為F。文字為真，稱該文字滿足。若子句中至少有一個文字滿足，則稱該子句滿足，否則子句不滿足。如x1=1，x2=0，x3=0子句x-1∨x2∨x3不滿足，在其余7種真值指派下，該子句滿足。合取范式滿足是指范式中任意一個子句均被滿足。

1.2實(shí)際問題轉(zhuǎn)化

組合拍賣問題是現(xiàn)實(shí)商業(yè)活動中常見的一個組合優(yōu)化問題。對于若干拍賣品，每個商家給出各自競拍商品組合的價格。在滿足一個商品只能賣給一個商家的條件下，求解賣家可獲取的最大銷售額。組合拍賣問題轉(zhuǎn)換為MaxSAT問題求解的例子如下：設(shè)集合Goods={gi， i∈N且1≤i≤10}，表示有10件商品。Sales={[（ g1， g2， g3），101]， [（ g2， g3， g5， g6），150]， [（ g1， g7， g8），120]， [（ g4， g9， g10），100]， [（ g1， g5， g9），180]， [（ g4， g6， g10），200]}，表示6個買家購買的商品和出價。如[（ g1， g2， g3），101]表示第一個買家出價101元競拍1、2、3號商品。求解如何出售這10個商品可以獲得最大銷售額。建立模型，設(shè)命題變元xi表示第i個買家出價競拍商品事件。

xi=1，第i個買家拍賣成功xi=0，否則，拍賣失敗

命題變元集合V={x1，x2，x3，x4，x5，x6}。因?yàn)橥患唐分荒苜u給一個買家，所以有相同商品的購買事件不能同時為真。如第一個買家和第三個買家同時購買商品g2、g3，事件x1、x3不能同時成立。因此該問題約束條件的硬子句集合為{x-1∨x-3，x-1∨x-5，x-1∨x-2，x-2∨x-5，x-2∨x-6， x-4∨x-5，x-4∨x-6}，軟子句集合為{x1，x2，x3，x4，x5， x6}。每個買家的出價是相應(yīng)軟子句的權(quán)重。組合拍賣問題轉(zhuǎn)換為V集合上，在滿足所有硬子句的條件下，求解一組V集合上變元的指派，使得滿足的單子句權(quán)重和最大。圖1是組合拍賣所應(yīng)用的模型圖。無向圖的結(jié)點(diǎn)是6個命題變元，若第i個買家和第j個買家購買的商品有沖突，則結(jié)點(diǎn)Si與結(jié)點(diǎn)Sj間有一條無向邊。

至此，商品的組合拍賣問題轉(zhuǎn)化為加權(quán)偏MaxSAT問題。命題邏輯的建模過程，應(yīng)完成3個步驟：①設(shè)置表示某一事實(shí)的判斷命題變元；②完成約束關(guān)系的描述，利用9個關(guān)系連接詞建立約束條件；③利用等價轉(zhuǎn)換將命題邏輯轉(zhuǎn)換為最小完備集與、或、非的合取范式。

2算法設(shè)計

求解一組變元真值指派使得可滿足軟子句權(quán)重最大，算法需遍歷2n的二叉樹搜索空間。

2.1算法框架

對于含有m個文字的子句，只有當(dāng)m個文字均為假時，子句不滿足，因而對于子句而言不滿足狀態(tài)的變元真值指派較容易確定。MaxSAT算法將求解最大滿足子句數(shù)等價轉(zhuǎn)換為求解最小不滿足子句數(shù)。采用分支限界法設(shè)計的MaxSAT完備算法，上界是當(dāng)前最優(yōu)的一組完整的變元真值指派確定的不滿足子句數(shù)，其初始值為合取范式子句數(shù)。下界是在當(dāng)前分支點(diǎn)，合取范式不可滿足子句數(shù)的一個下界，其初始值為0。算法[4]描述如下：

算法1MaxSAT完備算法。輸入：合取公式F和初始上界UB輸出：F的最小不滿足子句數(shù)及對應(yīng)的真值指派if（F= or只包含空子句） return 空子句數(shù)；LB=在當(dāng)前部分真值指派下的空子句數(shù)+下界的保守估計；if（LB≥UB）return UB；選擇分支變元x；if（Maxsatz（x=0）

2.2下界保守估計計算方法

利用單子句傳播測試沖突集的方法可確定不可滿足的子句數(shù)。算法2描述了單子句傳播的過程[56]。

算法2單子句傳播。輸入：單子句ci輸出：空子句或簡化后的F①令單子句ci中的文字l為真，單子句滿足；②檢查其余子句，對形如l∨li…∨lk含有文字l的子句，移除整個子句，因?yàn)樵撟泳湟褲M足；③對形如∨li…∨lk含有的子句，刪除文字，簡化子句為li…∨lk，特別地，當(dāng)子句只含有一個文字時，該子句簡化為空子句；④若有空子句產(chǎn)生或無新的單子句產(chǎn)生，單子句傳播結(jié)束，否則，對③產(chǎn)生的新單子句重復(fù)以上步驟。單子句傳播算法中的空子句指不含任何文字的特殊子句，通常記為□。單子句傳播操作是檢測不可滿足子句的主要工具。單子句傳播操作的執(zhí)行過程如下：設(shè)F1={x1，x-1∨x2，x-1∨x6，x-1∨x4，x-4∨x-5，x5，x1∨x5，x2∨x6，x4∨x7}。子句x1的單子句傳播過程是：①令x1=1，子句x1∨x5滿足，移除該子句；子句x-1∨x2，x-1∨x6和x-1∨x4，分別簡化為x2、x6和x4，無空子句產(chǎn)；②對新產(chǎn)生的單子句x2進(jìn)行單子句傳播，令x2=1，子句x2∨x6滿足，無空子句產(chǎn)生；③對新產(chǎn)生的單子句x6進(jìn)行單子句傳播，令x6=1，無空子句產(chǎn)生；④對新單子句x4進(jìn)行單子句傳播，令x4=1，子句x-4∨x-5化簡為x-5，無空子句產(chǎn)生。移除滿足的子句x4∨x7；⑤對新單子句x-5，令x5=0，刪除相反文字后，單子句x5化簡為空子句。子句x1的單子句傳播過程結(jié)束。為了方便分析x1的單子句傳播過程，可借助推理圖進(jìn)行分析。推理圖的原理是x-i∨xj等價于xi→xj。當(dāng)xi為真時，xi→xj的值為真當(dāng)且僅當(dāng)xj的值為真。圖2顯示了x1的單子句傳播過程。

圖1組合拍賣模型圖2單子句x1傳播過程

單子句傳播是廣度優(yōu)先的一種遍歷方式。從圖2的空子句出發(fā)，逆向追溯可以找到產(chǎn)生該空子句的原因子句是{x1，x-1∨x4，x-4∨x-5，x5}。此子句集是一個沖突集，在變元x1，x4，x5的任意一種真值指派下，沖突集中至少有1個子句是不滿足的，所以一個沖突集代表一個不可滿足的子句，下界的估計值加1。

2.3數(shù)據(jù)結(jié)構(gòu)選擇

數(shù)據(jù)結(jié)構(gòu)是算法設(shè)計的一個重要實(shí)施環(huán)節(jié)，不同的數(shù)據(jù)結(jié)構(gòu)對于算法效率的影響是顯著的[710]。實(shí)驗(yàn)中數(shù)據(jù)結(jié)構(gòu)的選擇部分設(shè)計了兩個問題：①根據(jù)程序局部性原理，如何安排子句的結(jié)構(gòu)；②根據(jù)單子句傳播操作過程及回溯，如何實(shí)現(xiàn)單子句傳播。

程序局部性原理是Cache的工作原理。該原理說明程序數(shù)據(jù)的使用具有時間、空間局部性?；诖嗽?，在設(shè)計子句存儲結(jié)構(gòu)時，把單子句操作中常用的子句狀態(tài)、子句長度、子句文字等存放為結(jié)構(gòu)體，子句的其它信息存放為一維數(shù)組。原因是單子句傳播操作是算法的核心操作，被調(diào)用得非常頻繁。單子句傳播每次尋找含有相反文字的子句并將該文字從子句中刪除，該操作涉及到子句中的文字、子句的長度、子句的狀態(tài)。為了加快子句搜索，需要建立子句索引，索引中存放包含有此文字的子句序號。建立索引的優(yōu)勢是加快單子句傳播過程中相反文字子句的尋找。計算機(jī)通過索引可以快速確定包含文字及相反文字的子句，而無需掃描所有子句。索引的建立可以在算例輸入時完成，時間代價小。

單子句傳播操作是檢測沖突集的主要手段，是從1個單子句出發(fā)推理出沖突子句，再通過追溯找到造成沖突的子句構(gòu)成沖突集。通常，1個單子句可以構(gòu)成多個沖突，但只能記為1個沖突集。程序通過廣度優(yōu)先方式能找到最短路徑的沖突集，節(jié)省沖突集計算時間。由以上分析可知，單子句傳播的數(shù)據(jù)結(jié)構(gòu)應(yīng)設(shè)計為棧，以便實(shí)現(xiàn)廣度優(yōu)先。更深入地考慮，可以設(shè)置雙棧，第一個棧存儲合取范式原有的單子句，第二個棧存儲由單子句傳播造成的單子句。雙棧模式可以保證盡量使用1個單子句找到1個沖突集。

關(guān)于數(shù)據(jù)結(jié)構(gòu)選擇的實(shí)驗(yàn)內(nèi)容幫助學(xué)生通過實(shí)踐學(xué)習(xí)棧、數(shù)組、鏈?zhǔn)綏５认嚓P(guān)內(nèi)容，亦幫助學(xué)生培養(yǎng)和形成針對問題選擇優(yōu)化數(shù)據(jù)結(jié)構(gòu)的思維和方法。

3實(shí)驗(yàn)評估

在正確求解的前提下，運(yùn)行時間可衡量算法的性能好壞。時間越短，性能越好。運(yùn)行時間的長短直接表現(xiàn)為搜索樹的結(jié)點(diǎn)數(shù)和回溯數(shù)的大小，搜索樹的分支數(shù)和回溯數(shù)越小，運(yùn)行時間越短。表1列出了MaxSAT算法MaxsatzEF和Maxsatz兩個算法在同樣機(jī)器上運(yùn)行算例集的時間對比。表2列出了計算相同算例，兩個算法的搜索結(jié)點(diǎn)數(shù)、回溯數(shù)的對比。

4結(jié)語

基于最大可滿足性問題的專業(yè)實(shí)驗(yàn)方案采用實(shí)際工業(yè)問題作為算例，利用命題邏輯建模、設(shè)計算法以及選擇優(yōu)化的數(shù)據(jù)結(jié)構(gòu)。該方案涉及程序設(shè)計語言、離散數(shù)學(xué)、數(shù)據(jù)結(jié)構(gòu)、計算機(jī)組成原理、算法分析與設(shè)計等多門計算機(jī)核心課程，有助于學(xué)生系統(tǒng)地掌握知識及其應(yīng)用方法，更重要的是該方案向?qū)W生展示了一個完整的利用計算機(jī)解決實(shí)際問題的過程。

參考文獻(xiàn)參考文獻(xiàn)：

＼[1＼]陶影，張斌.數(shù)據(jù)結(jié)構(gòu)實(shí)驗(yàn)教學(xué)應(yīng)重視算法設(shè)計與分析能力的培養(yǎng)[J].實(shí)驗(yàn)室研究與探索，2008，27（12）：119122.

[2]STEPHEN A COOK.The complexity of theorem proving procedures[C].Proceedings of the 3rd annual ACM symposium on theory of computing，1971：151158.

[3]JOSEP ARGELICH， CHUMIN LI， FELIP MANYA，et al.Analyzing the instances of the MaxSAT evaluation[C].Proceedings of the 14th Theory and Application of Satisfiablity Testing，2011：360361.

[4]CHUMIN LI，MANYA FELIP，NOUREDINE MOHAMEDOU.Resolution based lower bounds in MAXSAT[J].Journal of Constraints， 2010， 15（4）：456484.

[5]劉燕麗，李初民，何琨.基于優(yōu)化沖突集提高下界的MaxSAT完備算法[J].計算機(jī)學(xué)報，2013，10（36）： 20872096.

[6]OLIVIER DUBOIS，P ANDRE，Y BOYFKHAD.SAT versus UNSAT[J].DIMACS Series in Discrete Mathematics and Theoretical Computer Science，1996（2）：415436.

[7]余艷，劉燕麗.數(shù)據(jù)結(jié)構(gòu)教學(xué)方法探討[J].計算機(jī)教育，2013（9）：5658.

[8]田運(yùn)生，劉維華，王景春.綜合性設(shè)計性試驗(yàn)項(xiàng)目建設(shè)的探索與實(shí)踐[J].實(shí)驗(yàn)技術(shù)與管理，2012，29（2）：126129.

[9]郝小江，繆志農(nóng)，黃昆.基于DSP的數(shù)字信息處理實(shí)驗(yàn)設(shè)計[J].實(shí)驗(yàn)技術(shù)與管理，2012，29（2）：4447.

[10]易昆南， 于菲菲.在綜合性、設(shè)計性實(shí)驗(yàn)中培養(yǎng)學(xué)生的創(chuàng)新能力[J].實(shí)驗(yàn)技術(shù)與管理，2007，24（8）：79.

責(zé)任編輯（責(zé)任編輯：孫娟）