殷明浩,劉 華,谷文祥

(東北師范大學計算機科學與信息技術學院,吉林長春 130117)

一種基于知識編譯的模型計數方法

殷明浩,劉 華,谷文祥

(東北師范大學計算機科學與信息技術學院,吉林長春 130117)

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

模型計數;知識編譯;否定范式;模型樹;R-模型樹;香農擴展

0 引言

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

1 相關概念

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

表推演方法是一種經典邏輯和各種非經典邏輯統一的推理框架.以下表推演相關定義見文獻[6].

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

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

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

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

圖1 α型公式

圖2 β型公式

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

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

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

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

圖3 樹形結構

本文提出的基于知識編譯模型計數方法——M TREE,是將表推演過程結合香農擴展規(guī)則和簡化規(guī)則實現的.其定義見文獻[7].

定義1.3(香農擴展)給定任意的一個命題公式Σ和一個變量p,Σ關于p的香農擴展:

文獻[8]中已經證明經過香農擴展的命題公式與原公式是邏輯等價的.

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

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

定理1.1[7]所有的命題公式都可以在線性時間內轉換成NF.

2 模型樹

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

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

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

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

圖4 Σ的模型樹

圖5 R-模型樹

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

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

定理2.2求解一棵模型樹的模型個數可以在多項式時間完成.

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

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

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

例2.2將例2.1中模型樹轉換成R-模型樹.

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

定理2.3求解一棵R-模型樹的模型個數可以在多項式時間完成.

證明一個命題公式對應的R-模型樹有三種形式:

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

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

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

綜上所述,計算一棵R-模型樹的模型個數是樹寬的線性時間.

3 模型計數方法——M TREE

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

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

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

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

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

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

4 總結

提出一種新的知識編譯模型計數方法——M TREE.對本算法我們提出了R-模型樹,它能完備有效地表示一個NF公式,并可以在多項式時間內求出其模型個數.M TREE算法通過表推演結合香農擴展和簡化規(guī)則,將輸入的NF命題公式編譯成文中給出的R-模型樹,再利用一個多項式時間算法求出輸入公式的命題個數.理論證明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:基于擴展規(guī)則的#SA T求解系統[J].軟件學報,2009,20(7):1714-1725.

[6] 劉全,孫吉貴,于萬鈞.基于tableau的自動推理技術綜述[J].計算機科學,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

國家自然科學基金資助項目(60473042,60573067,608003102).

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

(責任編輯:陶 理)