具計數量詞雙變量邏輯可滿足性之新演算法

Abstract

雙變量邏輯（FO2）為使用至多兩個變數之一階邏輯子類，其可滿足性（satisfiability）問題已知為可判定（decidable），更確切地說，該問題複雜度為非確定性指數時間完備（NEXPTIME-complete）。其上界通常透過指數大小模型（ESM）性質導出，該性質陳述如下，若一雙變量邏輯句子為可滿足，則該句子具有一包含至多其長度指數數量元素之模型。指數大小模型性質亦意味著雙變量邏輯之可滿足性及有限可滿足性（finite satisfiability）問題相等。 具計數量詞雙變量邏輯（C2）為雙變量邏輯在計數量詞下之擴展。計數量詞之語法為 ∃=k x φ(x)，其語意為於模型中恰有 k 個元素滿足 φ(x)。具計數量詞雙變量邏輯於知識表示與推理（KRR）領域中有著重要應用。儘管其可滿足性及有限可滿足性問題之複雜度依舊為非確定性指數時間完備，指數大小模型性質在具計數量詞雙變量邏輯上不再成立。一般來說，其複雜度上界乃通過非確定性指數時間規約（non-deterministic exponential-time reduction）至整數線性規劃（ILP）問題導出，因此，其相應之演算法相當繁雜，並且，因規約中包含指數數量之非確定性猜測，此演算法通常難以實現。於此之外，自具計數量詞雙變量邏輯中提取具有效率實現之子類亦相當困難。具計數量詞雙變量邏輯之有效率演算法仍為一未解研究問題。 於此論文中，我們重新審視具計數量詞雙變量邏輯。我們引入並證明組態指數上界（CEB）性質，此性質可視為指數大小模型性質之於雙變量邏輯之擴展。我們演示如何通過組態指數上界性質導出具計數量詞雙變量邏輯之可滿足性及有限可滿足性問題之非確定指數時間演算法。該性質亦可用於提取具計數量詞雙變量邏輯之強可滿足（strongly satisfiable）語義子類，我們證明具計數量詞雙變量邏輯之強可滿足性及有限強可滿足性問題之複雜度亦為非確定指數時間完備，其複雜度上界乃通過確定性指數時間規約（deterministic exponential-time reduction）至布林可滿足性（Boolean satisfiability）問題導出，此種規約得以導出更佳且有效率之演算法實現。 我們所提出針對具計數量詞雙變量邏輯之強可滿足性及有限強可滿足性問題之演算法亦可應用於具計數量詞雙變量邏輯之守衛子類（guarded fragment）之可滿足性及有限可滿足性問題。我們提出之演算法用於該問題之複雜度為確定性指數時間，此結果與該問題複雜度已知為確定性指數時間完備（EXPTIME-complete）相匹配。由此可知，具計數量詞雙變量邏輯之強可滿足子類乃介於具計數量詞雙變量邏輯之守衛子類與具計數量詞雙變量邏輯之間。 我們亦提出自具計數量詞雙變量邏輯之強可滿足性問題至雙變量邏輯之可滿足性問題之確定性多項式時間規約（deterministic polynomial-time reduction），以及自具計數量詞雙變量邏輯之守衛子類之可滿足性問題至雙變量邏輯之守衛子類之可滿足性問題之確定性多項式時間規約。

Two-variable logic (FO2) is the subclass of first-order logic using at most two variables. It is a well-known fragment of first-order logic whose satisfiability problem is decidable. More precisely, the exact complexity is NEXPTIME-complete. The upper bound is usually established by the so-called exponential size model (ESM) property, i.e., if an FO2 sentence is satisfiable, then it is satisfiable by a model whose size is exponential in its length. Moreover, the ESM property implies that the satisfiability and finite satisfiability problems of FO2 coincide. Two-variable logic with counting quantifiers (C2) is the extension of FO2 with counting quantifiers of the form ∃=k x φ(x). The semantics of the counting quantifier is that exactly k elements exist in the model satisfying φ(x). The class C2 is important for many knowledge representation and reasoning (KRR) applications. Though the exact complexity of the satisfiability and finite satisfiability problems of C2 is also NEXPTIME-complete, the ESM property no longer holds. In general, these two problems do not coincide. Usually, the upper bound is established by the non-deterministic exponential-time reduction to the integer linear programming (ILP) problem. Hence, the algorithms are very involved, and due to the exponential amount of non-determinism in the reduction, they are complicated to implement. It is also difficult to extract the subclasses of C2 for which there are efficient implementations. Obtaining explicit algorithms for C2 is still an open research problem. In this thesis, we revisit C2. We introduce and prove the configuration exponential bound (CEB) property for C2. This property can be viewed as the extension of the ESM property for FO2. We show that the CEB property can be used to obtain alternative NEXPTIME algorithms for the satisfiability and finite satisfiability problems of C2. It can also be used to extract a semantic subclass that we call the strongly satisfiable fragment. We show that the complexity of the strong satisfiability and finite strong satisfiability problems of C2 is NEXPTIME-complete. The upper bound is established by the deterministic exponential-time reduction to the Boolean satisfiability problem. Such reduction may yield a better and more efficient implementation. Our algorithms for the strong satisfiability and finite strong satisfiability problems of C2 can also be used for the satisfiability and finite satisfiability problems of the guarded fragment of C2 (GC2). The running time of our algorithms for GC2 is deterministic exponential in the length of the sentence, which matches that the known complexity of GC2 is EXPTIME-complete. Thus, the class strong satisfiability of C2 lies in between the satisfiability of GC2 and C2. Finally, we present a deterministic polynomial-time reduction from the strong satisfiability problem of C2 to the satisfiability problem of FO2. We also present a deterministic polynomial-time reduction from the satisfiability problem of GC2 to the satisfiability problem of GF2.