殷明浩,劉 華,谷文祥

(東北師范大學(xué)計(jì)算機(jī)科學(xué)與信息技術(shù)學(xué)院,吉林長(zhǎng)春 130117)

一種基于知識(shí)編譯的模型計(jì)數(shù)方法

殷明浩,劉 華,谷文祥

(東北師范大學(xué)計(jì)算機(jī)科學(xué)與信息技術(shù)學(xué)院,吉林長(zhǎng)春 130117)

提出一種新的基于知識(shí)編譯的模型計(jì)數(shù)方法——M TREE.該方法以一個(gè)否定范式(NF)作為輸入,利用命題表推演過程,結(jié)合香農(nóng)擴(kuò)展和簡(jiǎn)化規(guī)則,將輸入的否定范式編譯成與之等價(jià)的R-模型樹,在R-模型樹上應(yīng)用多項(xiàng)式時(shí)間算法求出其模型個(gè)數(shù),即為原輸入NF的模型個(gè)數(shù).嚴(yán)格證明了該算法是完備有效的.

模型計(jì)數(shù);知識(shí)編譯;否定范式;模型樹;R-模型樹;香農(nóng)擴(kuò)展

0 引言

模型計(jì)數(shù)(#SA T)是求解給定命題公式模型個(gè)數(shù)的問題,是命題可滿足問題(SA T)的泛化,其計(jì)算復(fù)雜性高于SA T,是標(biāo)準(zhǔn)的#P完備問題.隨著SA T研究的日益成熟,許多NP問題都可以轉(zhuǎn)化成SA T求解,如智能規(guī)劃問題.有些求解難度高于NP的問題無法轉(zhuǎn)化成SA T求解,卻可以轉(zhuǎn)換成#SA T求解,如一致性規(guī)劃問題和概率推理問題[1-2].模型計(jì)數(shù)正日趨完善,目前模型計(jì)數(shù)可分為精確模型計(jì)數(shù)和近似模型計(jì)數(shù),精確模型計(jì)數(shù)已經(jīng)可以求解數(shù)百變量規(guī)模的問題,而近似模型計(jì)數(shù)已經(jīng)可以求解上千變量規(guī)模的問題.其中精確模型計(jì)數(shù)是源于SA T求解方法的,它可以分為兩類:一類是基于DPLL的,擴(kuò)展系統(tǒng)DPLL式SA T求解器求解模型計(jì)數(shù)問題最早是由E.Birnbaum和E.L.Lozinskii在其模型計(jì)數(shù)器CDP中提出的[3];另一類是基于知識(shí)編譯的,簡(jiǎn)單來說這種方法是將要求解的命題公式先編譯成與之邏輯等價(jià)的一種易處理的目標(biāo)語言,再用一個(gè)多項(xiàng)式時(shí)間算法計(jì)算該目標(biāo)語言的模型個(gè)數(shù).現(xiàn)有的基于知識(shí)編譯的模型計(jì)數(shù)有文獻(xiàn)[4]中提到的Darw iche的編譯器c2d和文獻(xiàn)[5]中提到的基于擴(kuò)展規(guī)則的模型計(jì)數(shù)器JLU-ERWMC,其中文獻(xiàn)[4]將CNF編譯成d-DNNF來求解模型個(gè)數(shù);文獻(xiàn)[5]則是以CNF作為輸入,利用擴(kuò)展規(guī)則求解模型個(gè)數(shù).文獻(xiàn)[4-5]中算法均依賴于CNF,不是所有的命題公式都能在多項(xiàng)式時(shí)間轉(zhuǎn)換成CNF,所以已有的這兩種算法不能對(duì)所有命題公式的模型個(gè)數(shù)求解.本文在基于知識(shí)編譯的基礎(chǔ)上提出一種新的模型計(jì)數(shù)方法——基于表推演的模型計(jì)數(shù)算法M TREE,該方法能求解所有命題公式的模型個(gè)數(shù).M TREE以否定范式(NF)作為輸入,先將原公式編譯成一棵與之等價(jià)的R-模型樹,之后在多項(xiàng)式時(shí)間內(nèi)遍歷R-模型樹求出原公式模型個(gè)數(shù).M TREE方法是完備有效的,并且編譯后模型計(jì)數(shù)是多項(xiàng)式時(shí)間的.

1 相關(guān)概念

為便于展開討論,對(duì)本文中使用的符號(hào)進(jìn)行如下約定:Σ,α,β…表示命題公式;Ai,F,G表示子命題公式;p,pi表示變量,其中i={1,2,…},pi,pi,…表示變量對(duì)應(yīng)的文字;VAR(Σ)表示一個(gè)命題公式Σ中所有變量的集合;T表示一個(gè)表推演(tableau).

表推演方法是一種經(jīng)典邏輯和各種非經(jīng)典邏輯統(tǒng)一的推理框架.以下表推演相關(guān)定義見文獻(xiàn)[6].

定義1.1(表推演tableau)令{A1,A2,…,An}為公式的有限集合.

(1)下列分枝樹為公式{A1,A2,…,An}的一個(gè)表推演:

(2)如果T為{A1,A2,…,An}的一個(gè)表推演,且T′為T應(yīng)用表推演擴(kuò)展規(guī)則后的結(jié)果,那么T′也是{A1,A2,…,An}的一個(gè)表推演.

利用表推演進(jìn)行定理證明可以將命題公式分為兩類:α型公式和β型公式.見圖1-2.

圖1 α型公式

圖2 β型公式

根據(jù)α型公式和β型公式可得到命題表推演的擴(kuò)展規(guī)則:

定義1.2(命題表推演擴(kuò)展規(guī)則)

α擴(kuò)展規(guī)則處理α型公式,若使命題公式α成立必須使命題公式集{α1…αn}同時(shí)成立;β擴(kuò)展規(guī)則處理β型公式,若使命題公式β成立,命題公式集{β1…βn}中一個(gè)成立即可.

本文采用樹形結(jié)構(gòu)表示α和β擴(kuò)展規(guī)則,同一分支上節(jié)點(diǎn)為合取關(guān)系(α擴(kuò)展規(guī)則),分支之間為析取關(guān)系(β擴(kuò)展規(guī)則).形式如圖3.

圖3 樹形結(jié)構(gòu)

本文提出的基于知識(shí)編譯模型計(jì)數(shù)方法——M TREE,是將表推演過程結(jié)合香農(nóng)擴(kuò)展規(guī)則和簡(jiǎn)化規(guī)則實(shí)現(xiàn)的.其定義見文獻(xiàn)[7].

定義1.3(香農(nóng)擴(kuò)展)給定任意的一個(gè)命題公式Σ和一個(gè)變量p,Σ關(guān)于p的香農(nóng)擴(kuò)展:

文獻(xiàn)[8]中已經(jīng)證明經(jīng)過香農(nóng)擴(kuò)展的命題公式與原公式是邏輯等價(jià)的.

給定任意的命題公式Σ,假設(shè)F,G是Σ的任意子公式,令Σ[G/F]表示用G替換Σ中所有子公式F的結(jié)果.p是Σ中的一個(gè)變量.本文將用到如下簡(jiǎn)化規(guī)則:

定義1.4[9](否定范式NF)由變量、邏輯常量0,1及二元連接符∧,∨,?構(gòu)成命題公式.

定理1.1[7]所有的命題公式都可以在線性時(shí)間內(nèi)轉(zhuǎn)換成NF.

2 模型樹

本文提出的M TREE方法是將輸入的否定范式轉(zhuǎn)換成與之等價(jià)的R-模型樹來處理的,模型樹、R-模型樹定義如下:

定義2.1(模型樹)令VAR(Σ)={p1,…,pn}為任意命題公式Σ的變量,Σ的模型樹是以1為根, p1和p1分別為其左右子樹的根,pi+1和pi+1分別為pi和pi的左右子女,pn和pn為葉子節(jié)點(diǎn),同一分支上所有文字取正后Σ為真的分支組成的與或二叉樹.

注模型樹為n+1層,規(guī)定根為第0層,第i層節(jié)點(diǎn)由變量pi的文字標(biāo)記,每個(gè)分支上不會(huì)出現(xiàn)相同變量,并且樹的同一分支路徑上的節(jié)點(diǎn)是與(∧)關(guān)系,分支間節(jié)點(diǎn)是或(∨)關(guān)系,一個(gè)分支路徑上所有文字為真即是Σ的一個(gè)模型.不可滿足的命題公式的模型樹為空樹.

例2.1令Σ=p1∧(p2?p3),它的模型樹如圖4.

圖4 Σ的模型樹

圖5 R-模型樹

定理2.1命題公式的模型樹與其本身是邏輯等價(jià)的.

證明根據(jù)定義2.1,我們知道模型樹遍歷命題公式中所有變量取值情況,是類DPLL的,討論所有賦值情況之后保留所有使命題公式為真的分支,這樣得到的模型樹與原命題公式解相同,即為邏輯等價(jià)的.

定理2.2求解一棵模型樹的模型個(gè)數(shù)可以在多項(xiàng)式時(shí)間完成.

證明求解一棵模型樹的模型個(gè)數(shù)只需遍歷該模型樹,記錄數(shù)的分支個(gè)數(shù)d,model_c=d.顯然算法是樹寬的線性時(shí)間.

根據(jù)定義2.1,要用模型樹表示一個(gè)有效的命題公式,則需要一個(gè)n+1層的完全二叉樹,這種表示非常浪費(fèi)空間,因而我們給出簡(jiǎn)化模型樹(R-模型樹).

R-模型樹是在模型樹的基礎(chǔ)上應(yīng)用簡(jiǎn)化規(guī)則SR5-SR8得到的,簡(jiǎn)化后R-模型樹與模型樹是邏輯等價(jià)的.規(guī)則中合取關(guān)系是在同一路徑上,析取關(guān)系在兩個(gè)分支之間.這樣得到的R-模型樹葉子節(jié)點(diǎn)不存在葉子兄弟,樹的層數(shù)至多為n+1層,有效命題公式的R-模型樹將只有根節(jié)點(diǎn)1.

例2.2將例2.1中模型樹轉(zhuǎn)換成R-模型樹.

顯然,當(dāng)模型樹中存在多對(duì)兄弟葉節(jié)點(diǎn)時(shí),簡(jiǎn)化可以有效地節(jié)約空間.這里的M TREE算法采用R-模型樹,如圖5.

定理2.3求解一棵R-模型樹的模型個(gè)數(shù)可以在多項(xiàng)式時(shí)間完成.

證明一個(gè)命題公式對(duì)應(yīng)的R-模型樹有三種形式:

(1)R-模型樹為空,表示該命題公式無解.

(2)R-模型樹只含根節(jié)點(diǎn)1,表示命題公式是有效的,即有2n個(gè)解.

(3)R-模型樹含有文字節(jié)點(diǎn),其分支有兩種:一種是含n個(gè)變量文字,這樣的分支是命題公式的一個(gè)解;另一種變量文字個(gè)數(shù)為c(c＜n),沒在分支中出現(xiàn)的變量取值0或1均可,這樣的分支包含命題公式2n-c個(gè)解.我們用d表示R-模型樹中的分支數(shù),ci記錄第i個(gè)分支的文字個(gè)數(shù),命題公式的模型個(gè)數(shù)

綜上所述,計(jì)算一棵R-模型樹的模型個(gè)數(shù)是樹寬的線性時(shí)間.

3 模型計(jì)數(shù)方法——M TREE

將輸入的NF公式Σ編譯成與之等價(jià)的R-模型樹,再利用多項(xiàng)式時(shí)間算法求出模型個(gè)數(shù).編譯過程是用表推演結(jié)合香農(nóng)擴(kuò)展和簡(jiǎn)化規(guī)則完成的.具體算法如下:

定理3.1M TREE算法是完備有效的.

證明(完備性)M TREE方法以NF作為輸入,根據(jù)定理1.1,它可以處理所有命題公式的模型計(jì)數(shù)問題.

(有效性)M TREE方法中的表推演過程、香農(nóng)擴(kuò)展、簡(jiǎn)化規(guī)則都保證公式的等價(jià)性,所以算法是有效的.

例3.1 求p1∧(p2?p3)的模型個(gè)數(shù).

算法說明:首先設(shè)置R-模型樹的根節(jié)點(diǎn)為1,從下標(biāo)為1的變量開始,每個(gè)分支都會(huì)對(duì)應(yīng)一個(gè)Σ(每個(gè)分支上的Σ不同),對(duì)Σ先簡(jiǎn)化再香農(nóng)擴(kuò)展,簡(jiǎn)化可以減少香農(nóng)擴(kuò)展的難度或直接剪枝(Σ=0刪除該分支,Σ=1停止擴(kuò)展該分支),香農(nóng)擴(kuò)展是為表推演過程按順序擴(kuò)展出變量,之后利用β規(guī)則和α規(guī)則推演,如此循環(huán)直到i=n.該算法與文獻(xiàn)[4-5]中的方法比較其優(yōu)點(diǎn)在于:它具有完備性,不依賴任何一種命題語言,能求解所有命題公式的模型計(jì)數(shù)問題.

4 總結(jié)

提出一種新的知識(shí)編譯模型計(jì)數(shù)方法——M TREE.對(duì)本算法我們提出了R-模型樹,它能完備有效地表示一個(gè)NF公式,并可以在多項(xiàng)式時(shí)間內(nèi)求出其模型個(gè)數(shù).M TREE算法通過表推演結(jié)合香農(nóng)擴(kuò)展和簡(jiǎn)化規(guī)則,將輸入的NF命題公式編譯成文中給出的R-模型樹,再利用一個(gè)多項(xiàng)式時(shí)間算法求出輸入公式的命題個(gè)數(shù).理論證明M TREE方法不依賴任何一種命題語言,是完備有效的.

[1] HéCTOR PALACIOS,BLA IBONET,ADNAN DARW ICHE,et al.Pruning conformant plans by countingmodelson compiled d-DNNF rep resentations[C]∥Monterey,California:Proceedings of ICAPS,AAA IPress,2005:141-150.

[2] STEPHEN M MAJERCIK,M ICHAEL L.Littman:contingent planning under uncertainty via stochastic satisfiability[J]. A rtificial Intelligence,2003,147(1/2):119-162.

[3] BIRNBAUM E,LOZINSKII E L.The good old Davis-Putnam p rocedure helps counting models[J].Journal of A rtificial Intelligence Research,1999,10:457-477.

[4] DARW ICHE A.New advances in compiling CNF into decomposable negation normal form[C]∥In Proceedings of ECA I-04: 16th European Conference on A rtificial Intelligence,Spain:Valencia,2004:328-332.

[5] 殷明浩,林海,孫吉貴.JLU-ERWMC:基于擴(kuò)展規(guī)則的#SA T求解系統(tǒng)[J].軟件學(xué)報(bào),2009,20(7):1714-1725.

[6] 劉全,孫吉貴,于萬鈞.基于tableau的自動(dòng)推理技術(shù)綜述[J].計(jì)算機(jī)科學(xué),2005,32(11):1-5.

[7] REINER H?HNLE,NEIL V MURRA Y,ERIK ROSENTHAL.Normal forms for know ledge compilation[C]∥New York: ISM IS,2005:304-313.

[8] SHANNON C E.A symbolic analysis of relay and sw itching circuits[J].Transactions of the A IEE,1938,57:713-723.

[9] DARW ICHE A,MARQUISP.A know ledge compilationmap[J].Journalof A rtificial Intelligence Research,2002,17:229-264.

A model coun ting method using knowledge com pilation

YIN M ing-hao,L IU Hua,GU Wen-xiang

(College of Computer Science and Information Technology,Northeast Normal University,Changchun 130117,China)

A model counting methods using know ledge compilation w as p roposed,it w as called M TREE.This method used a negated form as input,and used p ropositional tableau,together w ith Shannon expansion and simp le rules made the input compiled into a R-model tree w hich w as logical equal to the input NF,then used a polynomial algorithm to compute themodel number of the R-model tree,also the input NF's.Thismethod w as p roved comp lete and valid.

model counting;know ledge compilation;normal form s;model tree;R-model tree;Shannon expansion

TP301

520·10

A

1000-1832(2010)04-0046-05

2009-06-04

國(guó)家自然科學(xué)基金資助項(xiàng)目(60473042,60573067,608003102).

殷明浩(1979—),男,博士,講師,主要從事自動(dòng)推理與智能規(guī)劃研究;谷文祥(1947—),男,教授,博士研究生導(dǎo)師,主要從事計(jì)算機(jī)網(wǎng)絡(luò)管理與智能規(guī)劃、規(guī)劃識(shí)別研究.

(責(zé)任編輯:陶 理)