计算复杂性理论（六）

因此，将 P≠NP 问题的现状总结如下似乎是合理的：(i) 基于收敛归纳和启发式证据，人们普遍认为 P≠NP 是正确的；(ii) 我们目前没有理由怀疑该陈述在形式上独立于我们在实践中接受的数学理论；但 (iii) 证明 P≠NP 仍然被认为超出了现有技术的范围。

4.2 可满足性、有效性和模型检验

我们已经看到，逻辑提供了许多在复杂性理论中研究的问题的例子。其中，最常考虑的是可满足性、有效性和模型检验。为了统一地表述这些问题，可以方便地将逻辑 L 取为三元组 ⟨FormL,A,⊨L⟩，它由一组公式 FormL、一类结构 A（其中 FormL 的成员被解释）和一个满足关系 ⊨L（结构和公式之间成立）组成。我们可以假设 FormL 以命题逻辑所代表的方式指定——即一组句法原语和归纳公式规则。另一方面，A 和⊨L 的定义会根据所讨论的逻辑类型而有所不同——例如在经典命题逻辑的情况下，A 将是原子估值类 v:N→{0,1}，并且 v⊨Lϕ 在 ϕ 关于 v 为真（由通常的真值表规则定义）的情况下成立，而在模态逻辑的情况下，A 通常是满足给定框架条件的一类 Kripke 模型，⊨L 是标准强制关系 A,w⊩ϕ，它存在于模型、世界和公式之间。

给定以这种方式指定的逻辑 L，我们现在可以制定以下问题：

可满足性 L 给定公式 ϕ∈FormL，是否存在结构 A∈A 使得 A⊨Lϕ？

有效性L  给定一个公式 ϕ∈FormL，是否对于所有 A∈A，A⊨Lϕ？

模型检查L  给定一个公式 ϕ∈FormL 和一个结构 A∈A，是否 A⊨Lϕ？

为了正式指定这些问题，必须提供 FormL 和 A 成员作为有限二进制字符串的适当编码。虽然这在 FormL 的情况下通常没有问题，但 A 有时可能包含无限结构。在这种情况下，模型检查问题仅考虑有限结构（我们还必须假设它们被编码为有限字符串 - 例如以 Marx 2007 描述的方式）。并且，在逻辑的标准特征是理论证明而非语义证明的情况下——即从 ΓL 的某些公理集推导出的公式集，而不是在所有结构中都为真的公式类——有效性问题被理解为与决定 ϕ 是否可以从 ΓL 推导出的问题相一致。在这种情况下，可满足性和模型检查问题通常不予考虑。

哲学、计算机科学和人工智能中使用的许多逻辑都研究了可满足性、有效性和模型检查问题。表 1 总结了一些结果，重点关注本百科全书其他文章中调查的系统。读者可以参考这些和其他参考资料，了解所讨论的片段或系统的定义以及 A、⊨L 或 ⊢ΓL 的相关定义。[42]

经典逻辑可满足性有效性模型检查完全命题NP-完全coNP-完全∈P   (Cook 1971; Buss 1987)

 Horn 子句P-完全P-完全∈P   (Papadimitriou 1994)

 完全一阶coRE-完全RE-完全PSPACE-完全   (Church 1936a; Vardi 1982)

 一元一阶NEXP-完全coNEXP-完全   (Löwenheim 1967; Lewis 1980)

 ∃∗∀∗NEXP-完全coNEXP-完全   (Bernays and Schöfinkel 1928; Lewis 1980)

 ∃∗∀∃∗EXP-完全EXP-完全   (Ackermann 1928; Lewis 1980)

∃∗∀∀∃∗NEXP-completecoNEXP-complete   (Gödel 1932; Lewis 1980)

直觉逻辑可满足性有效性模型检查完全命题PSPACE-completePSPACE-completeP-complete   (Statman 1979; Mundhenk and Weiß 2010)

完全一阶coRE-completeRE-complete   (Church 1936a; Gödel 1986a)

模态逻辑可满足性有效性模型检查K,T,S4PSPACE-completePSPACE-completeP-complete   (Ladner 1977; Fischer and Ladner 1979; Mundhenk and Weiß 2010)

 S5NP-completecoNP-complete∈P   (Ladner 1977; Mundhenk and Weiß 2010)

认识逻辑SATISFIABILITYVALIDITY模型检查S5n, n≥2PSPACE-completePSPACE-complete   (Halpern and Moses 1992; Fagin et al. 1995)

 KCn,TCn, n≥2  EXP-completeEXP-complete   (Halpern and Moses 1992; Fagin et al. 1995)

可证明性逻辑SATISFIABILITYVALIDITYMODEL CHECKINGGLPSPACE-completePSPACE-complete   (Chagrov 1985)

证明逻辑SATISFIABILITYVALIDITYMODEL CHECKINGLPΣP2-completeΠP2-complete   (Kuznets 2000; Milnikel 2007)

动态逻辑SATISFIABILITYVALIDITYMODEL CHECKINGPDLEXP-completeNEXP-completeP-complete   (Fischer and Ladner 1979; Kozen and Parikh 1981; Lange 2006)

时间逻辑SATISFIABILITYVALIDITYMODEL CHECKINGPLTLPSPACE-completePSPACE-completePSPACE-complete   (Sistla and Clarke 1985)

 CTLEXP-completeEXP-complete∈P   (Emerson and Jutla 1988; Vardi and Stockmeyer 1985; Wolper 1986)

 CTL∗2-EXP-complete2-EXP-completePSPACE-complete   (Emerson and Jutla 1988; Vardi and Stockmeyer 1985; Clarke et al. 1986)

相关性逻辑SATISFIABILITYVALIDITYMODEL CHECKINGT,E,RRE-complete   (Urquhart 1984)

线性逻辑SATISFIABILITYVALIDITYMODEL CHECKINGMLLNP-complete   (Kanovich 1994)

 MALLPSPACE-complete   （Lincoln 等人 1992）

 LLRE-complete   （Lincoln 1995）

表 1. 一些常见逻辑的可满足性、有效性和模型检查问题的复杂性。

4.3 证明复杂性

我们已经看到，命题逻辑的可满足性和有效性问题分别对于 NP 和 coNP 是完整的。虽然这些问题是用命题逻辑的语义来表征的，但有关其证明理论的某些问题也可以使用复杂性理论的技术来解决。通过命题逻辑的证明系统 P，我们理解符号 ⊢P 的定义，它表征公式 ϕ 可以从给定的一组公理和规则中推导出来的含义。我们写为 ⊢Pϕ，以表示系统 P 中存在以 ϕ 为结论的推导 D（例如，有限树或公式序列）。此类形式主义的例子包括希尔伯特系统 P1、[43] 自然演绎系统 P2 和命题逻辑的顺序系统 P3 的标准定义（参见，例如，Troelstra 和 Schwichtenberg 2000；Negri 和 Von Plato 2001）。这些系统中的每一个都可以证明对于命题有效性是健全和完备的——即对于所有命题公式 ϕ，ϕ∈VALID 当且仅当 ⊢Piϕ 对于 i∈{1,2,3}。

在复杂性理论的背景下，将证明系统的定义重新表述为一个映射 P:{0,1}∗→VALID 很方便，其定义域由所有二进制字符串组成，其值域是所有有效公式的类。例如，回想一下，希尔伯特导子是公式 ψ1,…,ψn 的有限序列，其每个成员要么是逻辑公理，要么通过肯定前件推理从早期成员得出。公式的有限序列可以编码为二进制字符串，这样，如果 x∈{0,1}∗ 是合式证明的代码，则可以在多项式时间内识别它。现在可以定义 P 为，如果 x 编码了这样的导子，则 P(x)=ψn（即导子的结果），否则 P(x) 就是某个固定的重言式。

如果存在一个多项式 p(n)，使得对于所有 ϕ∈VALID，存在一个导数 D，使得 P(⌜D⌝)=ϕ 且 |⌜D⌝|≤p(|ϕ|)，即所有大小为 n 的重言式都拥有最多大小为 p(n) 的 P 个证明，则称该系统为多项式有界的。

关于此类系统的基本观察如下：

定理 4.1（Cook 和 Reckhow 1979）当且仅当 NP=coNP 时，才存在多项式有界的证明系统。[44]

由于强烈怀疑 NP≠coNP（参见第 3.4.1 节），目前的共识是多项式证明系统不存在。然而，目前大多数常见的证明系统（包括 P1、P2 和 P3）都无法证明多项式有界性的失效。

因此，关于证明系统 P 的一个自然问题是，是否有可能识别出“硬”的重言式 H 类，即任何证明 ϕ∈H 有效的 P 证明相对于 ϕ 的大小都必须长得不可行。Haken (1985) 对许多自动定理证明器所基于的称为解析度的系统给出了肯定的答案。 Haken 的证明利用了 Cook 和 Reckhow (1979) 的观察，即我们可以在命题逻辑中制定鸽子洞原理 (PHP)，即任何将 n+1 只鸽子分配到 n 个洞中都必须将两只鸽子分配到某个洞中的陈述，使用原子字母 Pij 来表示鸽子 i 被放置在洞 j 中。公式

PHPn=⋀0≤i≤n ⋁0≤j＜nPij→⋁0≤i＜m≤n⋁0≤j＜n(Pij∧Pmj)

形式化了 PHP 的 n 鸽版本，因此对于每个 n 都是一个同义反复。因此，PHPn 可以在任何完整的命题逻辑证明系统中得到证明。

Haken 表明，PHPn 的任何解析证明都必须至少具有 n 的指数大小。由此可知，解析度不受多项式限制。然而，Buss (1987) 后来证明，系统 P1（以及可以证明有效模拟 P1 的系统 P2、P3）确实承认 PHPn 的证明，其大小为 n 的多项式。证明复杂性的一个后续研究方向是确定其他证明系统，对于这些系统，PHP 或相关组合原理也很难。参见 Buss (2012)、Segerlind (2007)。

4.4 描述复杂性

描述复杂性理论这一主题提供了逻辑和计算复杂性之间的另一种联系。正如我们所见，问题 X 在计算复杂性理论的意义上被视为“复杂”，其复杂程度与其算法决策的难度成正比。另一方面，描述复杂性认为问题的“复杂性”与描述其实例所需的逻辑资源成正比。换句话说，X 的描述复杂性是根据定义其实例所需的公式类型来衡量的，相对于适当的背景类有限结构。

描述复杂性始于这样的观察：由于计算问题由有限的组合对象（例如字符串、图形、公式等）组成，因此可以将它们的实例描述为传统意义上的一阶模型论中的有限结构。具体而言，给定一个问题 X，我们将其每个实例 x∈X 都与一个关系签名 τ 上的有限结构 Ax 相关联，该签名的非逻辑词汇将取决于组成 X 的对象类型。[45]

给定这样的签名 τ，我们将 Mod(τ) 定义为具有有限域的所有 τ 结构的类。在描述复杂性理论的背景下，逻辑 L 被视为一阶逻辑语言的扩展，具有一类或多类附加表达式，例如高阶量词或定点运算符。这些在语义上被视为逻辑符号。如果 L 是这样一种逻辑，而 τ 是签名，则我们写为 SentL(τ) 来表示使用来自 L 的逻辑符号和来自 τ 的关系符号构造的格式良好的句子类。句子 ϕ∈SentL(τ) 被称为定义问题 X，只要 X 与满足 ϕ 的 τ 结构集同延——即

{Ax∣x∈X}={A∈Mod(τ)∣A⊨ϕ}

如果 C 是一个复杂性类，那么逻辑 L 被称为捕获 C，只要对于每个问题 X∈C，都有一个签名 τ 和一个定义 X 的公式 ϕ∈FormL(τ)。

对于第 3 节中考虑的许多主要复杂性类，已经获得了描述性特征，其中一些总结在表 2 中。第一个这样的特征是针对二阶存在逻辑 (SO∃) 建立的。该系统的语言包括形式为 ∃Z1…∃Znϕ(→x,Z1,…,Zn) 的公式，其中变量 Zi 是二阶的，并且 ϕ 本身不包含其他二阶量词。Fagin (1974) 建立了以下内容：

定理 4.2 NP 由逻辑 SO∃ 捕获。

该结果提供了第一个与机器无关的重要复杂性类的特征之一 - 即其公式化不参考特定计算模型（例如 T 或 A）的类。此类特征的可用性通常被认为为 NP 等类的数学稳健性提供额外证据。

定理 4.2 加以推广，提供了构成多项式层次结构的类的特征。例如，逻辑 Σ1i 和 Π1i 统一捕获复杂度类 ΣPi 和 ΠPi（其中 SO∃=Σ11）。此外，SO（即完整的二阶逻辑）捕获 PH 本身。另一方面，也可以证明一阶逻辑 (FO) 仅捕获一个非常弱的复杂度类，称为 AC0，该类由可由常数深度的多项式大小电路判定的语言组成。

为了表征其他类，必须考虑扩展一阶逻辑表达能力的其他方法，例如添加最小不动点或传递闭包算子。例如，考虑一个公式 ψ(R,→x)，其中 n 元关系 R 仅以正数出现（即在偶数个否定的范围内），并且 →x 的长度为 m。如果 A 是结构 A 的定义域，则这样的公式将诱导一个类型为 Φψ(R,→x) 的单调映射，从 An 的幂集到 Am 的幂集，其定义为 Φψ(R,→x)(B)={→a∈Am∣ARB⊨ψ(R,→a)}，其中 ARB 表示符号 R 被解释为 B⊆An 的模型，否则与 A 一样。在这种情况下，映射 Φψ(R,→x) 存在一个最小不动点，即集合 F⊆An 使得 Φψ(R,→x)(F)=F 并且包含在所有具有此属性的其他集合中（参见 Moschovakis 1974 等）。我们用 FixA(ψ(R,→x)) 表示这个集合。[46]

逻辑 FO(LFP) 现在可以定义为一阶逻辑的扩展，对于每个公式 ψ(R,→x)，都有新的关系符号 LFPψ(R,→x)，其中关系变量仅以正数出现，并且有新的原子公式形式 LFPψ(R,→x)(→t)。此类公式解释如下：当且仅当 →tA∈FixA(ψ(R,→x))时，A⊨LFPψ(R,→x)(→t)。逻辑 FO(TC) 类似地通过添加传递闭包算子 TCψ(→x)(→x) 来定义，该算子只要 →tA 位于 A 中 ψ(→x) 所表示的关系的传递闭包中，则对项 →t 成立。逻辑 SO(LFP) 和 SO(TC) 类似地通过将这些算子添加到 SO 并允许它们应用于包含二阶变量的公式来定义。

现在我们可以陈述描述复杂性理论的另一个主要结果：

定理 4.3（Immerman 1982；Vardi 1982）相对于有序模型（即，将 ≤ 解释为 A 上的线性序的结构的模型 A），P 由 FO(LFP) 捕获。

Immerman（1999，第 61 页）将定理 4.3 描述为“增强了我们的直觉，即多项式时间是一个其基本性质超越了通常定义它的机器模型的类”。结合定理 4.2，它还提供了 P≠NP？问题本身的逻辑表述——即，当且仅当存在一类有序结构可以在存在性二阶逻辑中定义，而不能通过 FO(LFP) 公式定义时，P≠NP。

另一方面，定理 4.3 的表述中对有序结构的限制是必要的，因为 P 中存在简单可描述的语言 - 例如

PARITY={w∈{0,1}∗:w 包含奇数个 1}

- 如果不采用 ≤，则无法在 FO(LFP) 上定义。更一般地说，是否存在一种逻辑可以捕获无序结构上的 P，这是目前描述复杂性中的主要悬而未决的问题之一。例如，参见（Ebbinghaus and Flum 1999）和（Chen and Flum 2010）。

复杂度类别逻辑参考AC0FO(Immerman 1999)NLFO(TC)(Immerman 1987)PFO(LFP)(Immerman 1982)，(Vardi 1982)NPSO∃(Fagin 1974)ΣPiSOΣ1i(Stockmeyer 1977)ΠPiSOΠ1i(Stockmeyer 1977)PHSO(Stockmeyer 1977)PSPACESO(TC)(Immerman 1987)EXPSO(LFP)(Immerman 1999)

表 2. 复杂度类别的描述性特征。

4.5 有界算术

逻辑与计算复杂性之间的另一种联系是由一阶算术理论提供的，其形式类似于熟悉的系统，例如原始递归算术和皮亚诺算术。自 20 世纪 40 年代以来，人们就已经知道形式算术和可计算性理论之间的联系，例如，在算术标准模型中，分别用 Δ01 公式和 Σ01 公式定义的自然数集对应于递归和递归可枚举集，IΣ01 的可证明全函数对应于原始递归函数，而 PA 的可证明全函数对应于 ϵ0 递归函数（参见，例如，Schwichtenberg 2011）。从 20 世纪 70 年代以来，人们获得了许多类似的结果，将多项式层次的级别与一类统称为有界算术的一阶理论联系起来。

在研究算术和复杂性理论之间的关系时，除了集合之外，考虑函数通常也很有用。例如，我们可以考虑可由确定性图灵机在多项式时间内计算的函数类 FP=df◻P1。类似地，我们将◻Pn+1 定义为可由确定性图灵机在多项式时间内使用 PH 的 ΣPn 级集合的预言机计算的函数类。与 PH 的情况一样，尚不清楚层次结构◻P1⊆◻P2⊆… 是否会崩溃。