多值知識編譯

谷文祥，郭鴻鶴，殷明浩，王金艷，劉日仙

（1.東北師范大學(xué)計算機科學(xué)與信息技術(shù)學(xué)院，吉林長春 130117；2.金華職業(yè)技術(shù)學(xué)院信息工程學(xué)院，浙江金華 321017）

多值知識編譯

谷文祥1，郭鴻鶴1，殷明浩1，王金艷1，劉日仙2

（1.東北師范大學(xué)計算機科學(xué)與信息技術(shù)學(xué)院，吉林長春 130117；2.金華職業(yè)技術(shù)學(xué)院信息工程學(xué)院，浙江金華 321017）

定義了一類新的易處理理論：s－EPCCL理論.在此基礎(chǔ)上，提出了一種以s－EPCCL理論為目標(biāo)語言的多值知識編譯方法.該方法與現(xiàn)有知識編譯方法不同的是，它可以對多值知識庫進行編譯.經(jīng)過多值編譯后，任意查詢都可以在多項式時間內(nèi)得到應(yīng)答.

多值邏輯；知識編譯；標(biāo)記邏輯；EPCCL

0 引言

近年來，知識編譯已經(jīng)成為自動推理研究中的一個重要方向［1－10］.其主要思想是將推理分為兩個階段：離線編譯階段和在線推理階段.在離線編譯階段，將給定知識庫編譯成與之等價的易處理的目標(biāo)語言理論；在后一階段，利用目標(biāo)語言回答查詢.知識編譯方法的關(guān)鍵在于它將大部分計算時間花費在離線編譯階段，編譯只需一次，而且編譯所花的時間可以通過對同一個知識庫的多次詢問得到補償.

自知識編譯方法提出后，涌現(xiàn)出許多知識編譯的目標(biāo)語言，如BDD［11］，OBDD［2］，IP／PI［1，3］，Horn clauses［3］，DNNF［6－7］，F(xiàn)NNF［8］等.另一方面，文獻［12］提出了一類新的目標(biāo)語言理論－EPCCL，并提出了以EPCCL作為目標(biāo)語言的知識編譯方法.該方法與現(xiàn)有其他知識編譯方法的一個重要的不同是，不論在編譯階段還是查詢階段都是基于擴展規(guī)則的，而其他方法都是基于歸結(jié)原理的.對于互補因子較高的知識庫，基于擴展規(guī)則的知識編譯方法比基于歸結(jié)的知識編譯方法更為高效.因此，它被看做是與歸結(jié)方法互補的一種方法.

然而，現(xiàn)有知識編譯方法處理的知識庫都是以經(jīng)典的布爾變量為基礎(chǔ)的.經(jīng)典邏輯對知識的表示能力是有限的，而多值邏輯比經(jīng)典邏輯具有更強的表示能力，更能適應(yīng)實際需要.本文提出了一種基于擴展規(guī)則的多值邏輯推理方法.這里，我們關(guān)注標(biāo)記邏輯.因為對于任意一個多值邏輯知識庫，我們都可以找到一個與之等價的標(biāo)記邏輯知識庫.反之亦然.

本文工作如下：首先，基于經(jīng)典的擴展規(guī)則，提出了標(biāo)記擴展規(guī)則的概念.第二，在經(jīng)典的易處理可滿足性和易處理蘊含［12］之上我們提出了標(biāo)記易處理蘊含類的概念.只有滿足易處理蘊含類性質(zhì)的語言才可以作為知識編譯的目標(biāo)語言.第三，在標(biāo)記擴展規(guī)則基礎(chǔ)上提出了一種新的知識編譯語言s－EPCCL，并且證明了s－EPCCL是在易處理蘊含類中的.第四，提出了一種基于標(biāo)記擴展規(guī)則知識編譯算法SKCER.并證明了該算法的完備性和可靠性.即給定一個任意標(biāo)記知識庫，都可以轉(zhuǎn)化為一個等價的s－EPCCL理論.

1 背景知識

假定語言Λ，其中的邏輯公式由原子集合、連接符集合和邏輯常量集合組成.語言Λ的真值集合是Δ，Λ的解釋是從原子集合到真值集合Δ的一個映射.

定義1.1［13］（標(biāo)記） 一個標(biāo)記是真值集合Δ的一個子集，一個標(biāo)記公式是形式為S：F的表達式，其中S是一個標(biāo)記，F(xiàn)是Λ中的一個公式.如果F是Λ中的一個原子，則稱S：F是一個標(biāo)記原子.

我們可以在多值邏輯上應(yīng)用標(biāo)記邏輯進行元推理.標(biāo)記原子只有兩個真值：真或假.標(biāo)記邏輯是經(jīng)典邏輯的一種，它為多值邏輯推理提出了一個經(jīng)典邏輯框架.

為了能夠應(yīng)答任意查詢，將Λ中的公式映射為經(jīng)典命題邏輯Λs中的公式，即標(biāo)記公式語言.

定義1.2［13］（標(biāo)記公式語言） 在Λs中，如果原子是標(biāo)記公式，連接符是經(jīng)典的合取和析取，那么Λs稱為標(biāo)記公式語言.

與Λ的真值集不同的是，Λs的真值集為｛1，0｝，即真和假.

在介紹正規(guī)標(biāo)記公式之前，假定真值集Δ是有排序≤的一個完備格.用Sup和Inf表示真值集Δ子集的最小上界和最小下界.

令（P；≤）是一個任意的偏序集，且Q?P.則定義↑Q＝｛y∈P｜（?x∈Q）x≤y｝.如果Q是一個單元素集｛x｝，則簡寫為↑x.

定義1.3［14］（正規(guī)集）Q是P的子集，如果對于某一x∈P，Q＝↑x或Q＝（↑x）′（↑x的補集），則稱Q是正規(guī)的.前一種情況，我們稱Q是正的；后一種情況，我們稱Q是負(fù)的.

定義1.4［14］（正規(guī)標(biāo)記公式） 如果一個標(biāo)記公式中出現(xiàn)的所有標(biāo)記都是正規(guī)的，則稱該標(biāo)記公式是正規(guī)的.

這里，給出正規(guī)標(biāo)記歸結(jié)的簡單定義.首先介紹互補標(biāo)記文字的定義.

定義1.5［14］（互補標(biāo)記文字） 兩個標(biāo)記文字↑a：A和（↑b）′：A，如果滿足a≥b，則稱這兩個標(biāo)記文字互補.

定義1.6［14］（正規(guī)標(biāo)記歸結(jié)） 給定兩個帶有標(biāo)記的子句S1∨D1和S2∨D2，其中S1和S2是互補標(biāo)記文字，則兩個子句在標(biāo)記文字S1和S2上的標(biāo)記歸結(jié)式是D1∨D2.

2 標(biāo)記擴展規(guī)則

定義2.1［8］給定一個子句C和一個集合M：C′＝｛C∨a，C∨﹁a｜a是一個原子，a∈M且a不在C中出現(xiàn)｝.我們稱從C到C′的操作為C上的擴展規(guī)則，稱C′是擴展規(guī)則的結(jié)果.

在定義標(biāo)記擴展規(guī)則之前，我們給出如下假設(shè)：語言中有兩類變量——布爾變量和標(biāo)記變量.標(biāo)記變量都是正規(guī)標(biāo)記變量，多值邏輯變量的域是以在某一排序≤下的完備格.

根據(jù)經(jīng)典的擴展規(guī)則，我們可以定義正規(guī)標(biāo)記公式上的擴展規(guī)則，簡稱為標(biāo)記擴展規(guī)則.標(biāo)記擴展規(guī)則可以看作是正規(guī)標(biāo)記歸結(jié)的逆操作.

給定一個子句C，一個標(biāo)記變量集合S，↑a：A是S中的一個標(biāo)記原子，則子句C在該標(biāo)記原子上應(yīng)用擴展規(guī)則得到結(jié)果是｛C∨↑a：A，C∨（↑b）′：A｝，其中↑a：A和（↑b）′：A是互補文字.

為了減少由于使用擴展規(guī)則而出現(xiàn)的文字個數(shù)，我們用（↑a）′：A代替（↑b）′：A.下面定義了標(biāo)記原子上的擴展規(guī)則.

定義2.2（標(biāo)記擴展規(guī)則） 給定一個子句C，一個標(biāo)記原子集合S：C′＝｛C∨↑a：A，C∨（↑a）′：A｜↑a：A是一個標(biāo)記原子，↑a：A∈S并且↑a：A不出現(xiàn)在C中｝.

我們稱從C到C′的操作是C上的標(biāo)記擴展規(guī)則.

定理2.1一個子句C邏輯上等價于標(biāo)記擴展規(guī)則的結(jié)果C′.

定理2.1保證了標(biāo)記擴展規(guī)則是一個合法的規(guī)則.

定義2.3一個標(biāo)記子句是集合M上的最大項（包括布爾和標(biāo)記原子）當(dāng)且僅當(dāng)它或以正文字形式或以負(fù)文字形式包含M中的所有原子.

定理2.2給定一個標(biāo)記子句的集合Σ，其中的原子集合為M（｜M｜＝m），如果Σ中的子句都是M上的最大項，則Σ是不可滿足的當(dāng)且僅當(dāng)它包含2m個子句.

上述定理描述了一個最大項公式集合可滿足時的條件.

所有子句都擴展為最大項所需要的空間是不可估計的.針對這一問題，我們使用容斥原理計算在Σ上應(yīng)用經(jīng)典和標(biāo)記擴展規(guī)則后得到的最大項數(shù)目.

給定一個子句集合Σ＝｛C1，C2，…，Cn｝，M是Σ中出現(xiàn)的所有原子的集合，并且在子句集合中存在標(biāo)記子句.令Pi為在Ci上應(yīng)用經(jīng)典和標(biāo)記擴展規(guī)則得到的所有最大項的集合.令S為在Σ上應(yīng)用經(jīng)典和標(biāo)記擴展規(guī)則后得到的不同最大項的個數(shù).可以得到：

基于上述公式，我們可以通過計算最大項的數(shù)目來確定子句集的可滿足性.由公式可知，如果知識庫中子句間兩兩包含互補對，計算最大項數(shù)目的過程簡化為只計算公式的前N項.所以，我們可以利用經(jīng)典的和標(biāo)記的擴展規(guī)則方法更有效率地得到一個標(biāo)記知識庫的可滿足性.

另外，在帶有標(biāo)記變量的知識編譯中，如果需要在一個標(biāo)記變量上擴展某一子句，則使用標(biāo)記擴展規(guī)則方法；否則，使用經(jīng)典的擴展規(guī)則方法.

3 標(biāo)記EPCCL理論

定義3.1（標(biāo)記EPCCL理論） 一個標(biāo)記EPCCL理論（s－EPCCL）是一個帶有標(biāo)記文字的子句集合，其中每一對子句之間都存在互補文字，或者是互補的布爾文字，或者是互補的標(biāo)記文字.

標(biāo)記EPCCL理論的可滿足性可以由經(jīng)典擴展規(guī)則和標(biāo)記擴展規(guī)則在線性時間內(nèi)得到.

Del Val證明了“易處理蘊含”與“易處理可滿足性”之間的關(guān)系.文獻［12］證明了一個泛化的定理，說明EPCCL理論在“易處理蘊含”類中.

定理3.1［12］令L為滿足下述條件的任意一類理論：（1）Σ∈L是不可滿足的當(dāng)且僅當(dāng)Σ├p□；（2）如果Σ∈L，則對于每個單元子句l，Σ∪｛l｝∈L，或在一個多項式過程之后滿足Σ∪｛l｝∈L.則對于任意的Σ∈L，關(guān)于Σ的任意查詢可以在多項式時間內(nèi)被回答.

上述定理是基于經(jīng)典邏輯的，而一個s－EPCCL理論并不屬于經(jīng)典邏輯.下面我們將上述定理進行泛化，得到標(biāo)記易處理蘊含，并證明s－EPCCL理論屬于“標(biāo)記易處理蘊含”類.

定理3.2（標(biāo)記易處理蘊含） 令L是滿足下述條件的任意一類標(biāo)記邏輯理論：（1）Σ∈L是不可滿足的當(dāng)且僅當(dāng)Σ├p□；（2）如果Σ∈L，對于任意一個經(jīng)典的或標(biāo)記的單元子句l，有Σ∪｛l｝∈L成立，或在一個多項式過程之間滿足Σ∪｛l｝∈L.則對于每個Σ∈L，Σ上的任意查詢都可以在多項式時間內(nèi)得到應(yīng)答.即Σ屬于“標(biāo)記易處理蘊含”類.

上述定理說明s－EPCCL可以作為多值邏輯（可轉(zhuǎn)化為標(biāo)記邏輯）知識編譯的目標(biāo)語言.也就是說，標(biāo)記子句集可以由經(jīng)典擴展規(guī)則和標(biāo)記擴展規(guī)則編譯得到一個等價的s－EPCCL理論.編譯得到的子句集可以在多項式時間內(nèi)應(yīng)答任意查詢.這一過程稱作基于經(jīng)典和標(biāo)記擴展規(guī)則的多值知識編譯.

定理3.3標(biāo)記EPCCL理論上的任意查詢都可以在多項式時間內(nèi)得到應(yīng)答.

證明對于任意標(biāo)記EPCCL理論，它的可滿足性可以由標(biāo)記擴展規(guī)則在多項式時間內(nèi)決定.定理3.2的第一個條件滿足.下面證明第二個條件也是滿足的.新添加的子句l或者是以布爾文字組成的經(jīng)典的單元子句，或者是一個標(biāo)記單元子句.如果添加的單元子句是前者，那么根據(jù)定理3.2的證明過程可知，加入新單元子句后的子句集一定滿足第二個條件.如果添加的單元子句是標(biāo)記單元子句，則需要對原始子句集中的每一個子句進行處理，使之與新添加單元子句之間存在互補文字.有三種情況：如果兩個子句之間已經(jīng)存在互補文字，不需要做任何處理；如果新添加的標(biāo)記單元子句蘊含某一原始子句，即當(dāng)標(biāo)記單元子句為真時原始子句也為真，則刪除被蘊含的原始子句；除了上述兩種情況，其他的子句都必須在標(biāo)記單元子句的標(biāo)記文字上用標(biāo)記擴展規(guī)則進行擴展，然后用擴展得到的結(jié)果代替原子句.在這三種情況里，子句集的大小不會增加.以上證明了如果向原始理論中加入一個標(biāo)記單元子句，可以在多項式時間內(nèi)得到一個等價的標(biāo)記EPCCL理論.根據(jù)定理3.2，標(biāo)記EPCCL理論屬于“標(biāo)記易處理蘊含”類.

由上述定理及證明過程可知，標(biāo)記EPCCL理論可以看做是多值邏輯知識編譯的目標(biāo)語言.

4 標(biāo)記EPCCL知識編譯

在文獻［12］中提到的變量都是布爾變量，公式都是經(jīng)典的CNF.然而，在許多領(lǐng)域里，我們不僅需要布爾變量，還需要一些多值變量去表示實體的一些屬性.但是，直接向經(jīng)典公式中加入多值變量可能會增加原始問題的難度.另外，目前也沒有一種有效的方法可以處理帶有多值變量的公式集.因此，我們提出了一種可以處理多值變量的新的知識編譯方法.

在標(biāo)記公式中標(biāo)記文字和布爾文字有著相同的定義域，所以標(biāo)記知識編譯算法與經(jīng)典的應(yīng)用擴展規(guī)則的知識編譯算法類似.

下面我們給出一個帶有標(biāo)記的知識編譯算法，即標(biāo)記EPCCL知識編譯算法.其基本思想是基于“桶刪除（bucket elimination）”的思想.

定理4.1算法SKCER中，Σ3邏輯上等價于Σ1，Σ3是一個s－EPCCL理論.

證明由于刪除規(guī)則和擴展規(guī)則（經(jīng)典和標(biāo)記擴展規(guī)則）都具有等價保持性質(zhì)，所以Σ3邏輯上等價于Σ1.下面我們證明Σ3是一個s－EPCCL理論.算法SKCER中，如果一個子句移入Σ2，該子句擴展后的結(jié)果一定與Σ1中所有其他的子句之間有互補文字（布爾或／和標(biāo)記互補文字）.很顯然，在一個子句被移入Σ2之前，Σ3中的所有子句都一定已經(jīng)與之有互補文字.將子句移入Σ2中后，擴展該子句并不會使得原本已經(jīng)存在的子句間的互補文字消失.所以，當(dāng)算法結(jié)束時，Σ3中的所有子句都與知識庫中的所有其他子句含有互補文字.因此，算法的輸出一定是一個s－EPCCL理論.

由于編譯后子句集的大小直接關(guān)系到在線推理的時間，為了能使編譯后子句集的規(guī)模盡量小，我們給出了下面一條策略.

策略1在使用帶標(biāo)記的擴展規(guī)則進行知識編譯過程中，如果需要擴展一個子句來確保它與其他子句包含互補文字，則優(yōu)先選擇布爾變量作為子句擴展時的擴展原子；如果所有的布爾變量都無用，選擇一個適當(dāng)?shù)臉?biāo)記變量.

文獻［12］給出了兩條策略來優(yōu)化編譯后的知識庫規(guī)模.

策略2［12］如果同時有兩個子句需要擴展，擴展較長的那個.

策略3［12］在編譯過程中優(yōu)先考慮單元子句.

在帶有標(biāo)記的知識編譯過程中綜合考慮上述三條策略，我們可以將編譯后知識庫的大小進行優(yōu)化，保證編譯的簡潔性，并且降低子句的復(fù)雜性.

5 總結(jié)

現(xiàn)有的知識編譯方法都是以經(jīng)典命題理論為基礎(chǔ)的.然而，在我們的現(xiàn)實世界中，很多問題更傾向于用現(xiàn)有知識編譯方法不能處理的多值公式來表示.因此，我們提出了一類新的目標(biāo)語言理論，即標(biāo)記EPCCL理論.在此基礎(chǔ)上，進一步提出了一種基于標(biāo)記擴展規(guī)則的多值知識編譯方法，該方法用標(biāo)記擴展規(guī)則對帶有標(biāo)記的公式進行處理，得到一個與原理論邏輯等價的標(biāo)記EPCCL理論.

［1］REITER R，DE KLEER J.Foundations of assumption－based truth maintenance systems：preliminary report［J］.AAAI，1987，87：183－189.

［2］BRYANT R E.Symbolic Boolean manipulation with ordered binary decision diagrams［J］.ACM Computing Surveys，1992，24（3）：293－318.

［3］SELMAN B，KAUTZ H.Knowledge compilation and theory approximation［J］.J of the ACM，1996，43（2）：193－224.

［4］CADOLI M，DONINI F M.A survey on knowledge compilation［J］.AI Communications，1997，10：137－150.

［5］DARWICHE A，MARQUIS P.A knowledge compilation map［J］.JAIR，2002，2：229－264.

［6］DARWICHE A.Decomposable negation normal form［J］.Journal of the ACM，2001，48（4）：608－647.

［7］DARWICHE A.A compiler for deterministic，decomposable negation normal form［J］.AAAI，2002，2：627－634.

［8］HAHNLE R，MURRAY NV，ROSENTHAL E.Normal forms for knowledge compilation［J］.Proceedings of the International Symposium on Methodologies for Intelligent Systems，Lecture Notes in Computer Science，2005，3488：304－313.

［9］劉日仙，袁利永，谷文祥.智能規(guī)劃學(xué)習(xí)和學(xué)習(xí)型智能規(guī)劃系統(tǒng)架構(gòu)研究［J］.東北師大學(xué)報：自然科學(xué)版，2010，42（2）：44－49.

［10］蔡增玉，甘勇，谷文祥，等.基于應(yīng)對規(guī)劃的入侵防護系統(tǒng)設(shè)計與研究［J］.東北師大學(xué)報：自然科學(xué)版，2010，42（3）：43－47.

［11］BRYANT R E.Graph－based algorithms for Boolean function manipulation［J］.Transactions on Computers，1986，8：677－691.

［12］LIN HAI，SUN JIGUI.Knowledge compilation using the extension rule［J］.Journal of Automated Reasoning，2004，32：93－102.

［13］JAMES J LU，NV MURRAY.A framework for automated reasoning in multiple－valued logics［J］.Journal of Automated Reasoning，1998，21：39－67.

［14］JAMES J LU，MURRAY NV，ERIK ROSENTHAL.Duction and search strategies for regular multiple－valued logics［J］.Journal of Multiple－valued logic and soft computing，2005，11：375－406.

Compiling multi－valued knowledge base

GU Wen－xiang1，GUO Hong－h(huán)er1，YIN Ming－h(huán)ao1，WANG Jin－yan1，LIU Ri－xian2

（1.College of Computer Science and Information Technology，Northeast Normal University，Changchun 130117，China；2.Institute of Information Engineering，Jinhua College of Profession and Technology，Jinhua 321017，China）

In this paper，a new class of tractable theories are defines：s－EPCCL theories.Using s－EPCCL theories as a target language，a method for multiple－valued knowledge compilation is Proposed.Different from the existing knowledge compilation，the proposed method is used to compile on multiple－valued knowledge base.With the compilation method，any query on the multiple－valued knowledge theories can be answered in polynomial time in the size of the compiled knowledge base.

multiple－valued logic；knowledge compilation；signed logic；EPCCL

TP 301

520·20

A

1000－1832（2011）04－0044－05

2010－12－18

國家自然科學(xué)基金資助項目（60803102；61070084；60573067）；浙江省教育廳科研計劃項目（Y200908315）.

谷文祥（1941—），男，教授，博士研究生導(dǎo)師，主要從事智能規(guī)劃與規(guī)劃識別研究.

陶 理）