多值知識編譯

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

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

多值知識編譯

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

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

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

多值邏輯；知識編譯；標記邏輯；EPCCL

0 引言

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

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

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

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

1 背景知識

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

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

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

為了能夠應答任意查詢，將Λ中的公式映射為經典命題邏輯Λs中的公式，即標記公式語言.

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

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

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

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

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

定義1.4［14］（正規標記公式） 如果一個標記公式中出現的所有標記都是正規的，則稱該標記公式是正規的.

這里，給出正規標記歸結的簡單定義.首先介紹互補標記文字的定義.

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

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

2 標記擴展規則

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

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

根據經典的擴展規則，我們可以定義正規標記公式上的擴展規則，簡稱為標記擴展規則.標記擴展規則可以看作是正規標記歸結的逆操作.

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

為了減少由于使用擴展規則而出現的文字個數，我們用（↑a）′：A代替（↑b）′：A.下面定義了標記原子上的擴展規則.

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

我們稱從C到C′的操作是C上的標記擴展規則.

定理2.1一個子句C邏輯上等價于標記擴展規則的結果C′.

定理2.1保證了標記擴展規則是一個合法的規則.

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

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

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

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

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

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

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

3 標記EPCCL理論

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

標記EPCCL理論的可滿足性可以由經典擴展規則和標記擴展規則在線性時間內得到.

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

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

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

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

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

定理3.3標記EPCCL理論上的任意查詢都可以在多項式時間內得到應答.

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

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

4 標記EPCCL知識編譯

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

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

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

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

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

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

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

文獻［12］給出了兩條策略來優化編譯后的知識庫規模.

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

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

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

5 總結

現有的知識編譯方法都是以經典命題理論為基礎的.然而，在我們的現實世界中，很多問題更傾向于用現有知識編譯方法不能處理的多值公式來表示.因此，我們提出了一類新的目標語言理論，即標記EPCCL理論.在此基礎上，進一步提出了一種基于標記擴展規則的多值知識編譯方法，該方法用標記擴展規則對帶有標記的公式進行處理，得到一個與原理論邏輯等價的標記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］劉日仙，袁利永，谷文祥.智能規劃學習和學習型智能規劃系統架構研究［J］.東北師大學報：自然科學版，2010，42（2）：44－49.

［10］蔡增玉，甘勇，谷文祥，等.基于應對規劃的入侵防護系統設計與研究［J］.東北師大學報：自然科學版，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－her1，YIN Ming－hao1，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

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

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

陶 理）