二階修正KROM 邏輯的表達(dá)能力與復(fù)雜性

馮世光 王克詡 趙希順

1 引言

有窮模型論以有窮結(jié)構(gòu)為主要研究對象，其發(fā)展受到了計(jì)算復(fù)雜性理論、數(shù)據(jù)庫理論和形式語言的影響。1950 年B.Trakhtenbrot 證明了在有窮模型上一個(gè)公式的可滿足性問題是不可判定的（[17]），標(biāo)志著有窮模型論的誕生。描述復(fù)雜性理論是有窮模型論的一個(gè)分支，它從邏輯的角度對計(jì)算復(fù)雜性進(jìn)行研究。計(jì)算復(fù)雜性理論關(guān)心的是解決一個(gè)問題所需要的時(shí)間和空間資源，而描述復(fù)雜性則主要研究定義一個(gè)問題所需要的最小邏輯的表達(dá)能力。判斷一個(gè)結(jié)構(gòu)A是否滿足公式φ的復(fù)雜性有三種：(1)數(shù)據(jù)復(fù)雜性，即公式φ給定，結(jié)構(gòu)A作為問題的輸入；(2)表達(dá)式復(fù)雜性，即結(jié)構(gòu)A給定，公式φ作為問題的輸入；(3)混合復(fù)雜性，即結(jié)構(gòu)A和公式φ同時(shí)作為問題的輸入。

本文主要考慮數(shù)據(jù)復(fù)雜性，一般隨著表達(dá)能力的增強(qiáng)一個(gè)邏輯的數(shù)據(jù)復(fù)雜性也會變大。例如一階邏輯的數(shù)據(jù)復(fù)雜性在L 中，但它不能表達(dá)圖的三著色問題。存在型二階邏輯（?SO）可以表達(dá)圖的三著色問題，但它的數(shù)據(jù)復(fù)雜性是NP 完全的。在描述復(fù)雜性中用“刻畫”來定義這種表達(dá)能力與數(shù)據(jù)復(fù)雜性之間的關(guān)系。稱邏輯L刻畫復(fù)雜性類C，則他們滿足：(1)邏輯L的數(shù)據(jù)復(fù)雜性在C中；(2)復(fù)雜性類C中的問題在邏輯L中可表達(dá)。

有了刻畫的概念之后，可以通過比較不同邏輯的表達(dá)能力來研究他們所刻畫的復(fù)雜性類之間的關(guān)系，即如果邏輯L1刻畫復(fù)雜性類C1，邏輯L2刻畫復(fù)雜性類C2，則C1=C2當(dāng)且僅當(dāng)L1≡L2。（[5]）1974 年，R.Fagin 證明了?SO 能夠刻畫NP（[6]），這一定理的證明開啟了描述復(fù)雜性研究的先河。1982 年，N.Immerman 和M.Vardi 分別證明了最小固定點(diǎn)邏輯FO(LFP)可以在有序結(jié)構(gòu)上刻畫P。（[13,19]）1987 年，N.Immerman 證明了確定傳遞閉包邏輯FO(DTC)和傳遞閉包邏輯FO(TC)可以在有序結(jié)構(gòu)上分別刻畫L 和NL。（[14]）1989 年，S.Abiteboul 和V.Vianu 證明了部分固定點(diǎn)邏輯FO(PFP) 可以在有序結(jié)構(gòu)上刻畫PSPACE。（[1]）還有一些研究者繼續(xù)從二階邏輯的角度對描述復(fù)雜性進(jìn)行了研究。J.Büchi（[2,3]）和B.Trakhtenbrot（[18]）分別獨(dú)立證明了一個(gè)語言是正則的當(dāng)且僅當(dāng)它可以被單二階邏輯（MSO）定義。E.Gr?del 證明了二階HORN 邏輯（SO-HORN）和二階KROM邏輯（SO-KROM）在有序結(jié)構(gòu)上分別可以刻畫P 和NL。（[10,11]）S.Cook 和A.Kolokolova 提出了基于約束算術(shù)的V-Krom 邏輯，并研究了其對NL 的刻畫關(guān)系。（[4]）本文作者提出了二階修正HORN 邏輯，證明了其與FO(LFP)邏輯的等價(jià)性，并研究了對復(fù)雜性類P 的刻畫關(guān)系。（[7,8]）

本文對二階KROM 邏輯進(jìn)行擴(kuò)充，然后提出了二階修正KROM 邏輯（SOKROMr），二階擴(kuò)展KROM 邏輯（SO-EKROM）和二階擴(kuò)展修正KROM 邏輯（SO-EKROMr），并對他們的表達(dá)能力和復(fù)雜性進(jìn)行了研究。本文結(jié)構(gòu)如下：第二節(jié)是預(yù)備知識，給出了一些基本概念和定義。第三節(jié)研究了SO-KROMr的描述復(fù)雜性，證明了在有序結(jié)構(gòu)上SO-KROMr的存在型部分等價(jià)，可以刻畫NL；而它的全稱存在型部分可以刻畫co-NP。第四節(jié)研究了二階擴(kuò)展KROM 邏輯（SO-EKROM）與二階擴(kuò)展修正KROM 邏輯（SOEKROMr）的描述復(fù)雜性，證明了SO-EKROM 與其全稱存在型部分等價(jià)，他們可以在有序結(jié)構(gòu)上刻畫co-NP；在所有結(jié)構(gòu)上，SO-EKROMr的全稱存在型部分等價(jià)，也可以刻畫co-NP。本文的部分結(jié)果見圖1。

圖1:SO-KROMr、SO-EKROM 與SO-EKROMr 的表達(dá)能力與刻畫關(guān)系

2 預(yù)備知識

本文假設(shè)讀者對數(shù)理邏輯和計(jì)算復(fù)雜性理論有基本的了解，相關(guān)內(nèi)容可以查閱文獻(xiàn)[5,12,16]。下面我們簡單介紹本文所涉及的概念和定義。

令τ={c1,c2,...,cm,P1,P2,...,Pn}是一個(gè)詞匯表，其中c1,c2,...,cm是常項(xiàng)符號，P1,P2,...,Pn是關(guān)系符號。一個(gè)τ-結(jié)構(gòu)A具有如下形式：

其中A是一個(gè)非空集合，是結(jié)構(gòu)A的論域，分別是τ中的常項(xiàng)符和關(guān)系符在A上的解釋(我們默認(rèn)每個(gè)詞匯表都包含等詞“=”，并且被解釋為論域中元素之間的相等關(guān)系)。在不引起歧義的情況下我們通常會省略常項(xiàng)和關(guān)系的上標(biāo)A。我們稱A是有窮結(jié)構(gòu)當(dāng)且僅當(dāng)它的論域A是一個(gè)有限集。如無特別說明，本文中所涉及到的結(jié)構(gòu)均為有窮結(jié)構(gòu)。我們用符號|·|來代表一個(gè)集合的基數(shù)或者一個(gè)元組的維數(shù)，例如|A|代表論域A的基數(shù)。如果在有窮結(jié)構(gòu)A上添加一個(gè)二元關(guān)系“≤”并且解釋為線序關(guān)系，添加二元關(guān)系“SUCC”并解釋為相對于“≤”的后繼關(guān)系，添加常項(xiàng)“min”和“max”分別作為對最小元和最大元的解釋，則稱A為有序結(jié)構(gòu)。

定義2.1.以τ為詞匯表的二階KROM 邏輯，記為SO-KROM(τ)，是具有下列形式的二階公式的集合

其中Qi ∈{?,?}，R1,...,Rm是二階變元，C1,...,Cn是相對于R1,...,Rm的KROM 子句，即每個(gè)Cj都是一個(gè)具有如下形式的析取式

則我們稱這一邏輯為二階修正KROM 邏輯，記為SO-KROMr(τ)。

在不引起混淆時(shí)我們通常省略記號SO-KROMr(τ)中的τ，簡記為SO-KROMr。我們用來分別代表SO-KROMr中型公式和型公式的集合，即公式前綴中的二階量詞分別以全稱量詞“?”和存在量詞“?”開始，并且不同類型的量詞一共交替k-1 次。

例1.一個(gè)有向圖是強(qiáng)連通的當(dāng)且僅當(dāng)任意兩點(diǎn)之間都有一條路徑相連。圖的強(qiáng)連通問題定義為

輸入：一個(gè)有向圖G=(V,E)，其中V是頂點(diǎn)的集合，E是邊的集合。

輸出：是，如果G是強(qiáng)連通的；否則為否。

圖的強(qiáng)連通問題是NL 完全的，因?yàn)镹L=co-NL，因此它的補(bǔ)也是NL 完全的。下面的公式定義了圖的強(qiáng)連通問題的補(bǔ)：

其中二階變元R定義了圖上的連通關(guān)系，T定義了R的補(bǔ)。若某個(gè)圖滿足上述公式，則必然存在兩個(gè)節(jié)點(diǎn)a,b使得Tab為真，即a不可通達(dá)b，此圖為非強(qiáng)連通圖。

一個(gè)非強(qiáng)連通圖的子圖可能是強(qiáng)連通的，SO-KROM 在子結(jié)構(gòu)下保持（[11]），因此圖的強(qiáng)連通的問題的補(bǔ)在SO-KROM 中無法表達(dá)。例1 說明了SO-KROMr的表達(dá)能力要嚴(yán)格強(qiáng)于SO-KROM。

例2.集合{φ|φ是一個(gè)不可滿足的命題CNF 公式}的判定問題是co-NP 完全的。（[16]）令詞匯表τ={C,V,P,N}，其中C和V是兩個(gè)一元關(guān)系符，P和N是兩個(gè)二元關(guān)系符。對每個(gè)CNF 公式φ，可以用一個(gè)τ-結(jié)構(gòu)Aφ=〈A,C,V,P,N〉對其進(jìn)行編碼（[15]），其中A是論域，對任意i,j ∈A有：Ci為真當(dāng)且僅當(dāng)i是一個(gè)子句；V j為真當(dāng)且僅當(dāng)j是一個(gè)變元；Pij為真當(dāng)且僅當(dāng)變元j在子句i中有正出現(xiàn)；Nij為真當(dāng)且僅當(dāng)變元j在子句i中有負(fù)出現(xiàn)。例如公式(p1∨p3)∧(p2∨?p3)∧(p1∨p2)∧(?p1)可以編碼成〈{1,2,3,4},C,V,P,N〉，其中

一個(gè)CNF 公式不可滿足當(dāng)且僅當(dāng)對任意的賦值都存在一個(gè)子句使得這個(gè)子句中的所有文字在這個(gè)賦值下都為假。這一事實(shí)可以用下面的SO-KROMr公式表達(dá)：

公式Φ 表達(dá)了對任意的賦值X（Xj為真當(dāng)且僅當(dāng)變元j在這個(gè)賦值下為真），都存在一個(gè)子句的集合Y使得其中的子句在這一賦值下都為假。容易看出對所有的CNF 公式φ，Aφ |=Φ 當(dāng)且僅當(dāng)φ不可滿足。上面的公式Φ 是一個(gè)公式，由此可知SO-KROMr可以表達(dá)co-NP 完全的問題。

3 修正KROM 邏輯的描述復(fù)雜性

本節(jié)研究SO-KROMr的描述復(fù)雜性。由例2 可以知道SO-KROMr的數(shù)據(jù)復(fù)雜性至少是co-NP 難的。本節(jié)證明它的存在型部分的數(shù)據(jù)復(fù)雜性在NL 中，并且可以在有序結(jié)構(gòu)上刻畫NL；而它的全稱存在型部分可以在所有結(jié)構(gòu)上刻畫co-NP。

命題3.1.公式都等價(jià)于一個(gè)全稱型的一階公式?ˉxφ，其中φ是一個(gè)不含量詞的CNF 公式。

從命題3.1 可知如果一個(gè)SO-KROMr公式的前綴中最后的二階量詞是全稱型的，則可以把通過變換把它刪除，由此可以得出以下推論。

推論1.令k ≥1，如果k為奇數(shù)，則；如果k為偶數(shù)，則

引理3.1.令?x1...?xnφ是一個(gè)量化命題布爾公式，則它等價(jià)于如下公式

證明.?x1...?xnφ為真當(dāng)且僅當(dāng)要么所有變元x1,...,xn都為假時(shí)φ為真，要么某個(gè)xi(1≤i ≤n)為真時(shí)?x1...?xi-1?xi+1...?xnφ為真。

由例2 可以知道每個(gè)命題CNF 公式都可以編碼成一個(gè)τ-結(jié)構(gòu)，并且存在一個(gè)公式Φ 定義所有不可滿足的CNF 公式編碼成的結(jié)構(gòu)。下面我們根據(jù)Ψ 構(gòu)造一個(gè)τ在σ中的不含量詞的解釋（即用σ-結(jié)構(gòu)來編碼τ-結(jié)構(gòu)，相關(guān)定義可參考文獻(xiàn)[5]，第十一章第二節(jié)）

其中Π 中的公式均為不含量詞的σ-公式，πuni定義了τ-結(jié)構(gòu)的論域，πC,πV,πP,πN分別定義了τ-結(jié)構(gòu)中的關(guān)系C,V,P,N。Π 的寬度即元組的維數(shù)且我們根據(jù)例2 中的Φ 構(gòu)造出一個(gè)公式Φ-Π使得對任意至少包含兩個(gè)元素的σ-結(jié)構(gòu)A都有A|=Θ 當(dāng)且僅當(dāng)A|=Φ-Π。

公式ψ中包含的子句的數(shù)目最多為(n+1)|As|，由于把每個(gè)看成是一個(gè)命題變元，那么它包含的變元的數(shù)目最多為因此可以找到一個(gè)固定的數(shù)k使得可以用Ak中的元素對所有的子句和變元進(jìn)行編碼。令g=max{arity(R1),...,arity(Rm)}，k=3+max{(n+1+s),(g+m)}。定義解釋Π 的寬度為定義對于Ak中的元組=(a1,a2,...,ak)，我們用前兩個(gè)元素a1,a2來表示這一元組編碼的是子句還是變元，即如果a1/=a2則這一元組編碼子句，否則編碼變元。

對于任意有窮結(jié)構(gòu)A，都有一個(gè)不含量詞的一階公式φiso(x1,...,x|A|)刻畫它的同構(gòu)型（[5]），其中A是A的論域。所有單元素（論域中只包含一個(gè)元素）σ-結(jié)構(gòu)是有限的，因此對單元素結(jié)構(gòu)組成的集合都可以用一個(gè)一階公式對其進(jìn)行刻畫。由此可知任何二階公式在單元素σ-結(jié)構(gòu)上都等價(jià)于一個(gè)全稱型的一階公式。假設(shè)Θ 等價(jià)于（在單元素結(jié)構(gòu)上），其中φ是一個(gè)不含量詞的公式。那么對任意的σ-結(jié)構(gòu)A都有A|=Θ當(dāng)且僅當(dāng)由于全部是不含量詞的公式，因此通過基本的變換操作可以將Φ-Π∨?wˉφ轉(zhuǎn)化為一個(gè)公式。

根據(jù)命題3.4 和命題3.5 我們可以得出以下結(jié)論。

定理3.3.在所有的結(jié)構(gòu)上，具有相同的表達(dá)能力，可以刻畫co-NP。

4 擴(kuò)展修正KROM 邏輯的描述復(fù)雜性

在SO-KROM 的定義中如果我們要求每個(gè)子句都只相對于存在二階變元是KROM 的，那么可以得到二階擴(kuò)展KROM 邏輯（SO-EKROM）。與此類似，如果在SO-KROMr的定義中要求每個(gè)子句都只相對于存在二階變元是KROM 的，那么可以到二階擴(kuò)展修正KROM 邏輯（SO-EKROMr）。本節(jié)證明SO-EKROM 可以在有序結(jié)構(gòu)上刻畫co-NP，而可以在所有結(jié)構(gòu)上刻畫co-NP。

定義4.1.以τ為詞匯表的二階擴(kuò)展KROM 邏輯，記為SO-EKROM(τ)，是下面一些二階公式的集合

其中T1,...,Tm,R1,...,Rm是關(guān)系符號，C1,...,Cn是相對于R1,...,Rm的擴(kuò)展KROM 子句，即每個(gè)Cj是一個(gè)具有如下形式的析取式

則我們稱這一邏輯為二階擴(kuò)展修正KROM 邏輯，記為SO-EKROMr。

下面我們首先考慮SO-EKROM 和SO-EKROMr的數(shù)據(jù)復(fù)雜性。

命題4.1.SO-EKROM 的數(shù)據(jù)復(fù)雜性在co-NP 中。

與命題3.4 的證明類似，我們還可以得到以下結(jié)論。

命題4.2.的數(shù)據(jù)復(fù)雜性在co-NP 中。

定理4.1.在所有的結(jié)構(gòu)上，可以刻畫co-NP。

下面我們研究SO-EKROM 在有序結(jié)構(gòu)上的描述復(fù)雜性。

根據(jù)定理4.2 和命題4.1 容易得出：

定理4.3.在有序結(jié)構(gòu)上，SO-EKROM 等價(jià)于它的全稱存在型部分，并且可以刻畫co-NP。

5 結(jié)論