劉燕麗　余艷　張婷

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

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

DOIDOI：10.11907/rjdk.143639

中圖分類(lèi)號(hào)：TP302

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

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

0引言

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

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

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

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

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

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

組合拍賣(mài)問(wèn)題是現(xiàn)實(shí)商業(yè)活動(dòng)中常見(jiàn)的一個(gè)組合優(yōu)化問(wèn)題。對(duì)于若干拍賣(mài)品，每個(gè)商家給出各自競(jìng)拍商品組合的價(jià)格。在滿足一個(gè)商品只能賣(mài)給一個(gè)商家的條件下，求解賣(mài)家可獲取的最大銷(xiāo)售額。組合拍賣(mài)問(wèn)題轉(zhuǎn)換為MaxSAT問(wèn)題求解的例子如下：設(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個(gè)買(mǎi)家購(gòu)買(mǎi)的商品和出價(jià)。如[（ g1， g2， g3），101]表示第一個(gè)買(mǎi)家出價(jià)101元競(jìng)拍1、2、3號(hào)商品。求解如何出售這10個(gè)商品可以獲得最大銷(xiāo)售額。建立模型，設(shè)命題變?cè)獂i表示第i個(gè)買(mǎi)家出價(jià)競(jìng)拍商品事件。

xi=1，第i個(gè)買(mǎi)家拍賣(mài)成功xi=0，否則，拍賣(mài)失敗

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

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

2算法設(shè)計(jì)

求解一組變?cè)嬷抵概墒沟每蓾M足軟子句權(quán)重最大，算法需遍歷2n的二叉樹(shù)搜索空間。

2.1算法框架

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

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

2.2下界保守估計(jì)計(jì)算方法

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

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

圖1組合拍賣(mài)模型圖2單子句x1傳播過(guò)程

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

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

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

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

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

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

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

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

4結(jié)語(yǔ)

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

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

＼[1＼]陶影，張斌.數(shù)據(jù)結(jié)構(gòu)實(shí)驗(yàn)教學(xué)應(yīng)重視算法設(shè)計(jì)與分析能力的培養(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ì)算機(jī)學(xué)報(bào)，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ì)算機(jī)教育，2013（9）：5658.

[8]田運(yùn)生，劉維華，王景春.綜合性設(shè)計(jì)性試驗(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ì)[J].實(shí)驗(yàn)技術(shù)與管理，2012，29（2）：4447.

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

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