参数化证明复杂度：湿斯两斯的研究成果

参数化证明复杂度Stefan Dantchev、Barnaby Martin和Stefan Szeider英国杜伦大学[s.s.dantchev，b.d.martin，stefan.szeider]@durham.ac.uk摘要我们提出了一个证明理论的方法，以获得证据，某些参数化的问题是不固定参数听话。我们考虑证明给定的命题CNF公式不能满足一个真值赋值，它将至多k个变量设置为真，将k视为参数（我们称这样的公式为参数化矛盾）。 我们可以把它分开-rameterized复杂性类FPT和W[2]通过显示没有FPT有界参数化证明系统，即，没有一个证明系统可以证明f（k）nO（1）的大小，其中f是一个可计算的函数，n表示命题公式的大小。作为第一步，我们引入了参数化树型归结系统，并证明了这个系统不是fpt-有界的。事实上，我们给出了一个一般性的结果，最短的树状分辨率证明参数化的矛盾，统一编码的大小为n的宇宙的一阶原则的大小。我们建立了一个二分法的- orem分裂指数的情况下，里斯我们还讨论了如何设置参数化的矛盾-可以通过添加新的公理将条件嵌入到（普通）矛盾的集合当嵌入到一般（DAG类）的决议，我们证明了π-geonhole原则有一个证明的大小为2kn2。这与树状分辨率的情况形成对比，在树状分辨率中，嵌入的pi-geonhole原则属于我们二分法中的1介绍近年来，参数化复杂性和固定参数算法已成为算法设计和分析的一个重要分支，已有数百篇研究论文发表。英国工程和物理科学研究委员会支持的研究，项目EP/C526120/1和EP/E001394/1。已经在该领域发表（参见，例如，参考文献[2，6，8，11]）。在参数化复杂性中，人们考虑二维集合中的计算问题：第一维是通常的输入大小n，第二维是正整数k，即参数。一个问题是固定参数易处理的，如果它可以在时间f（k）nO（1）内求解，其中f表示一个可计算的，可能是指数函数。一些NP困难问题具有自然的参数化，允许固定参数的易处理性。例如，给定一个有n个顶点的图，可以在时间O（1）内检查。273k+nk）（和多项式空间）是否图的顶点覆盖的大小最多为k[3]。 上另一方面，几个参数化问题，如CLIQUE（有一个给定的图的团的大小至少为k？）被认为不是固定参数可处理的。有界CNF SAT-ISFIABILITY 是另一个被认为不是固定参数可处理的问题（并且将在续集中发挥特殊作用）：给定合取范式的命题公式，是否存在令人满意的真值赋值，使至多k个变量为真？参数化的复杂性也提供了一个完备性理论。许多似乎不是固定参数可处理的参数化问题已经被分类为在所谓的纬层次W[1] W[2] W[3]·· ·的复杂性类的fpt-约简下 是 完 全 的 。 例 如 ， CLIQUE 和 BOUNDED CNFSATISFIABILITY分别对于纬纱层级的前两个级别是完整的。我们将在第2.1节中概述参数化复杂性的基本概念;为了深入讨论参数化复杂性类和fpt约简，我们建议读者参考Flum和Grohe人们普遍认为，对于纬纱层次来说困难的问题不是固定参数可处理的。到目前为止，主要有三种类型的证据：1. 累积证据：已知许多问题对于纬纱层次的类别是困难的或完整的，并且尽管有相当大的效果，但没有发现固定参数的算法[2]。2. 非确定性图灵机的k步停机问题对于W[1]（单带）和W[2]（多带）类是完备的。图灵机是这样一个不透明和通用的对象，它看起来不合理，我们应该能够决定一个给定的图灵机在一个给定的输入是否有一些接收路径，而不看路径。3. 如果对于一类纬向分层来说很难的问题被证明是固定参数可处理的，则指数时间假设（ETH）失败，即，对于n个变量的3-SAT问题[9]，存在一个2o（n）ETH与位于FPT和FPT之间的参数化复杂性类M[1]密切相关。[1]（见[8]）。我们提出了一种新的方法，以获得进一步的证据，某些参数化的问题是不固定参数听话。我们将证明复杂性的概念推广到参数化复杂性的二维设置。这使我们能够制定Cook和Reckhow [4]程序的参数化版本。他们的计划试图通过以下方式获得NP/= co-NP的证据，进而获得P/= NP的证据：证明命题证明系统不是多项式的Ally bounded.我们引入了参数化证明系统的概念，在我们的程序中，在这些新系统中证明长度的下限证明某些参数化问题是不固定参数的易处理的。分格化的矛盾构成co-W[2]-完备语言。因此，FPT =co-W[2]= W[2]意味着存在一个证明系统，该证明系统允许最多f（k）nO（1）的证明。对于参数化矛盾（F，k），其中n表示F. 我们称这样一个（假设的）证明系统fpt有界的本文研究了相对弱的树型分解系统。参数化矛盾（F，k）的参数化树形归结反驳内置访问所有大于k个否定的子句变量作为额外的公理。我们证明了一个元定理，它对参数化矛盾的参数化树形归结反驳的复杂性进行了精确的我们的定理允许一个精炼的观点指数的情况下Riis对于一个积极的-我们得到一个参数化的矛盾<$（C<$，n，k）<$n∈N.我们证明了以下两种情况之一成立（并提供了一个判断标准）。2a. （C_n，n，k）有一个参数化的树形分解，其大小为βknα，其中α和β是只依赖于k的常数.2b.存在一个常数γ，0γ≤1，使得对于每一个n>k，每一个参数化的树型分解<在命题证明的复杂性中，人们通常构造一系列重言式（或矛盾），并显示反驳（Ca，n，k）的大小至少为nkγ。该序列需要在所考虑的证明系统中的超多项式大小的证明（或反驳）。在矛盾和反驳的情况下，这样的命题公式序列经常编码一个一阶（FO）句子（如鸽子洞原理）其中序列的第n个公式表明FO语句没有大小为n的模型。S. Riis [13]建立了一个元定理，精确地指出了在什么情况下一个给定的FO语句产生一系列命题公式，这些命题公式在树状归结系统中具有多项式大小的反驳。也就是说，如果序列没有多项式大小的树状归结反驳，则最短树状归结反驳有对于仅取决于FO语句的正常数ε，大小至少为2εn因此，两个位置之间存在差距可证明的复杂性。指数大小的情况下prevail正是当FO句子没有有限的，但一些无限的模型。在本文中，我们证明了一个元定理的复杂性参数化树型决议。为此，我们考虑参数化矛盾，pairs（F，k）其中F是CNF中的命题公式，k是整数，使得F不能被设置至多k个变量为真的真值赋值所满足。啪-我们建立了上界βknα通过某些布尔决策树。对于下界nkγ，我们使用博弈论的论证.我们为以上每一个类别提供了FO句子的例子。特别地，针对nkγ情况的示例（示例15和16）示出了参数化树状解析不是fpt有界的。如所讨论的，针对参数化矛盾（F，k）的参数化树状归结返回可以访问具有多于k个被否定变量作为加法的所有子句。理性公理然而，这些公理不被认为是输入参数化矛盾的一部分;相反，它们被认为属于归结系统本身（因此“参数化”在“参数化树状归结”中）。在论文的最后一节，我们考虑了如何将这些公理引入到参数化的矛盾中，从而为普通的证明系统创建一个成熟的普通矛盾。通过这种方式，我们可以将参数化矛盾集嵌入到（普通）矛盾集中。给定一个证明系统，并考虑到要保留的参数，这种嵌入本身会产生一个参数化的证明系统。我们考虑的嵌入行为良好，因为它保留了参数化树状解析的复杂度差距在特别地，当嵌入树状解析时，鸽子洞原理仍然是“硬的然而，当考虑一般（DAG类）决议，嵌入鸽子洞原则反驳的大小为2kn2。由于篇幅所限，省略完整的证明和进一步的例子可以在技术报告中找到[5]。2预赛2.1固定参数可追溯性在下文中，让表示任意但固定的有限字母表。参数化语言是一个集合L × N，其中N表示正整数的集合。 如果（I，k）在参数化语言L中，那么我们称I为主要部分，k为参数。 我们确定一个参数化的语言与决策问题“（I，k）∈ L？”因此将同义地使用术语参数化问题和参数化语言。一个参数化问题L称为固定参数易处理的，如果（I，k）在L中的隶属度可以在时间上确定f（k）|我|（1）（1）其中f表示可计算函数。FPT表示所有固定参数易处理决策问题的类;达到时间复杂度（1）的所有算法称为固定参数算法。这个定义的关键点是，指数增长仅限于参数，与形式|O（f（k））。|O (f (k)).（二）有理论证据表明，像CLIQUE这样的参数化问题不是固定参数可处理的。这个证据是通过一个类似于NP完备性理论的完备性理论提供的。这个完备性理论是基于以下的归约概念：设L1∈N×N和L2∈N×N是参数化的要看到FPT在fpt-约简下是封闭的，因此FPT是一个参数化的复杂性类。参数化的问题似乎有几个程度的棘手性，如manifest的纬纱层次。这个类的W[t]形成一个链FPTW[1] W[2]··· XP其中假设所有内含物都是适当的。在这里，XP定义了在时间O内解决问题的类，|我|f （k））;已知FPT i=XP [6]。每个类W[t]被定义为某个规范加权满足的等价类决策电路的能力问题。对于W[2]，规范问题等价于以下可满足性问题：加权CNF满意度例子：一个合取范式（CNF）的命题公式F和一个正整数k。参数：k。问题：F能被一个恰好使k个变量为真的真值赋值τ所满足吗？（k是τ的权重。）注意，如果CNF公式的子句被要求最多包含三个文字，我们得到W[1]-完全问题加权3-CNF满意度。让有界CNF满意度表示从加权CNF满意度中得到的问题，允许权重最多为k的真值分配。很容易看出，这种松弛并没有改变问题的参数化复杂性，因为有界CNF SATISFIABILITY包含W[2]-完全问题击中集[6]作为特殊情况。引理1. 在fpt-约化下，类W[2]的有界CNF满足是完备的。1 2问题 从L1到L2的FPT约简是一个映射R：×N→×N，使得12相关问题的界定 3-CNF满意度是1. （I，k）∈L1当且仅当R（I，k）∈L2.2. R可通过固定参数算法计算，即，存在一个可计算函数f，使得R（I，k）可以在时间f（k）内计算|我|O（1）。3. 存在一个可计算函数g，使得无论何时R（I，k）=（I′，k′），则k′≤g（k）.参数化复杂性类C是参数化问题在fpt-约简下的等价很容易实际上是固定参数的;这解释了为什么我们的研究关注W[2]而不是W[1]。在经典复杂性理论中，我们可以为参数化复杂性类 C 定 义 互 补 复 杂 性 类 C={L ： L∈ C }， 其 中 L=（L∈N）\L对于一个参数化问题L×N.显然FPT=co-FPT。 很容易看出，如果C在FPT下是封闭减少，那么co-C也是如此。因此，特别地，纬纱层级的每个类W[t]产生参数化复杂度类ω-W [t]。112.2参数化证明系统定义2. 设L_n×N为参数化语言. L的一个参数化证明系统是一个到映射Γ：（N× N）→ L的映射，其中Γ可以通过一个固定参数算法计算。我们称Γ是fpt-有界的，如果存在可计算函数f和g，使得对每个（I，k）∈L，有is（I′，k′）∈N，其中hΓ（I′，k′）≤（I ，k），|我|=f（k）|我|O（1），且k′≤ g（k）.注意，纬层次的类W[t]的问题具有fpt有界证明系统，因为这些问题的是实例具有小的见证。例如，考虑W[2]-完全问题L=BOUNDEDCNF满意度。设SF，τ，k表示某个环一个字母表1，它编码一个CNF公式F以及F的满足的权重≤k的真值分配τ。L的证明系统Γ现在可以通过设置Γ（w，k）=（F，k）如果w=S，否则，Γ（w，k）=（F，k）为了更清楚地说明，注意，我们可以在单个FO语句中模拟常数，并在新变量上添加最外面我们假设FO句是由FO句组成的连词，每一个FO句都是前束范式;因此，我们只需要解释单个前束范式的FO句的翻译。纯普遍句的情况很简单1，. . . ，xkF（x1，. . . （xk）其中F是无量词的，被转化为CNF<$C <$，n<$n∈N中的命题公式序列，其中第n个成员C<$，n构造如下。让[n]={1，2，. . . ，n}。 对于实例化x1，. . . ，xk∈[n]，我们可以考虑F（x1，. . . ，xk）是两类命题变量R（xi1，. . . ，xip），其中R是p元谓词符号，并且（xi=xj）。我们将F变换成CNF，然后取所有这样的CNF公式的并集（x1，. . . ，xk）测距超过[n]k。 形式为（xi=xj）的变量计算对于一些固定的F，τ，k0 0 为真或假，因此我们只剩下（F0，k0）∈L.显然，Γ是fpt-有界的。然而，对于类co-W[t]，情况是不同的;具体地，在这种情况下，对于co-W[2]。通过列出所有的O（k·nk）赋值，我们可以知道一个n元CNF公式没有令人满意的权≤k的的权重≤k，然后检查没有一个是满意的。然而，这个列表需要太多的空间，显然我们不能用它来构造一个fpt有界证明系统。引理3. 设C是一个参数化复杂性类，L是一个余C-完全参数化问题.如果L不存在fpt有界的参数化证明系统，则形式R（xi1，. . . ，xip）。一般情况下，一个句子的形式2000年1月1日2000年2月2日。. . x k. . ，xk，y1，. . . ，yk），可以通过Skolemization简化为前一种情况 引入Skolem关系Si（x1，. . . ，xi，yi），对于1 ≤ i ≤K. Si（x1，. . . ，xi，yi）对于任何给定的xi，. . . ，xi，所以我们需要加上斯科伦条款说明这样的证人总是存在的，即，_nSi（x1，. . . ，xi，yi）对于所有（x1，. . . ，xi）∈ [n]i.C= FPT。这个结果遵循一个标准的论点，其中图灵机的计算被认为是一个证明。针对这一引理，我们提出了一个程序，yi=1原来的句子可以转换成下面的纯普遍句_k<$S（x，. . . x，y）Cook-Reckhow用于获得证据，证明纬层次的复杂性类与FPT不同。这1，. . . xk，y1，. . .yki=1i1i iF（x1，. . . xk，y1，. . .yk）。程序包括显示特定的参数化证明系统不是FPT有界的。对于这种方法，我们将从弱系统开始，例如树状分辨率的参数化版本。对更强系统的考虑留待今后研究。2.3从一阶逻辑到命题逻辑接下来，我们描述了一个翻译的FO句子的一个序列的命题CNF公式。我们使用的FO逻辑的语言与平等，但既没有功能，也没有常数符号。我们只省略函数和常量通过构造可以清楚地看出，对于FO语句n，CNF公式Cn，n是可满足的，当且仅当n有一个大小为n的模型。序列的可满足性问题<$C<$，n<$n∈N涉及非空有限模型的存在性问题。备注4. 请注意，相对于某种合理编码，C，n的大小是n中的多项式。实施例5. 我们考虑鸽子洞原理（的否定）。假设PHP是以下内容的合取。xy <$x<$R（x，y）<$x <$w <$y <$R（x，y）<$$> R（w，y）<$x = w.我们把它翻译成下列通用分句的连词<$x<$y<$S2（x，y）<$R（x，y）<$y<$x<$S1（y）<$<$R（x，y）<$x<$y <$w<$R（x，y）<$$>R（w，y）<$x=w连同斯科伦条款n=2（x，y）1（y）.对于x，y∈[n]，我们认为R（x，y），S2（x，y）和S1（y）是命题变量.CPHP，n因此是子句系统<$S2（x，y）<$R（x，y），<$S1（y）<$<$R（x，y）和<$R（x，y）<$<$R（w，y），对于x，y，w∈[n]，w x，连同斯科伦条款不难看出，一个给定子句集的树形归结反驳等价于一个布尔决策树解决了该子句集的搜索问题。不可满足子句集的搜索问题被 定 义 为 以 下 几 个 问 题 ：例如，在一个实施例中，Krajcek布尔决策树通过查询命题变量的值然后在答案上分支来解决搜索问题。在不失一般性的情况下，我们可以假设，没有命题变量在同一个分支上被质疑两次，一旦发现一个伪造的子句，树的一个分支就被关闭，根据迄今为止沿着该分支获得的部分赋值当一个分支这样闭合时，我们说一个基本矛盾已经得到。请注意，我们认为决策树的一个节点由迄今为止获得的事实与所质疑的比例变量的连接来标记这类似于树型归结反驳中的节点被标记为_ni=1S2（x，i），其中x∈[n]，且_ni=1S1（i）。它的子句和刚刚解析的变量一起。由于类树归结反驳和布尔决策树之间的等价性，我们将集中讨论后者。2.4参数化树状解析一个字面量要么是一个命题变量，要么是一个命题变量的否定一个子句是一个L- als的析取（并且一个命题变量在一个子句中只能出现一次）。一组子句是一个连词，即，它是可满足的，如果存在同时满足所有子句的真值赋值。归结是一种证明系统，旨在反驳一组给定的子句，即，来证明它是不可满足的。这是通过一个单一的推导规则C vD、CD我们使用它从两个已经存在的子句中获得一个新子句我们的目标是推导出空分句当且仅当初始子句集是不可满足的时，我们可以从初始子句导出空子句在本文中，我们将工作的限制版本的决议，即树型决议。在树状解析中，我们不允许重用已经导出的任何子句，即，我们需要推导出一个子句的次数和我们使用它的次数一样多换句话说，一个树型归结反驳可以被看作是一个二叉树，其节点被标记为子句。每个叶子都标记有一个原始子句，内部节点处的每个子句都是通过两个子节点处的子句的归结步骤获得的，并且树的根标记有空子句。我们通过节点的数量来度量树状归结反驳的大小当我们需要证明某个不可满足子句集存在某种树状归结反驳时，我们将为相应的搜索问题构造一棵布尔决策树。另一方面，每当我们要求一个树型的分辨率下限，我们将证明它的一个对手的论点对任何布尔决策树，解决了搜索问题。我们给出了参数化矛盾和参数化树状归结的工作定义，我们将使用它们来陈述和证明参数化树状归结的复杂性缺口定义6.参数化矛盾是一个对（F，k），其中F是一个命题CNF公式，k是一个正整数，使得F在至多k处没有令人满意的权分配。实施例7. 让我们考虑一个无向图G=（V，E），它没有大小≤k的顶点覆盖。对每个顶点v∈V，我们引入一个命题变量pv.则该对.V{u，v}∈E（pu<$pv），k是一个参数化的矛盾。让参数化矛盾 被 兰-参数化矛盾的标尺。请注意，PA-量化指令是有界CNF满意度的补充，因此是co-W[2]。在FPT缩减下完成。现在我们可以定义一个参数化的树形解析。正如我们已经解释过的，我们将给出布尔决策树的定义。定义8. 给定参数化矛盾P=（F，k），参数化布尔决策树是查询命题变量值的决策树，答案上的分支;一旦（1）或（2）发生，树的分支就会关闭：(1) 就产生了一个基本矛盾，即，沿分支得到的部分赋值证伪了F;(2) 沿着分支获得的部分赋值具有多于K个被设置为真的命题变量，即，重量> k。我们可以通过准则（2）关闭分支的事实等价于我们拥有，内置为公理，所有子句的否定变量超过k。这表示参数化布尔决策树和（普通）布尔决策树之间的区别;因此也是参数化树状解析和（普通）树状解析之间的区别。3参数化树型分解我们首先回顾Riis [13]证明的树形解的复杂性缺口定理定理9. 给定一个在所有有限模型中都失败的FO语句，考虑将其转换为一个命题CNF矛盾序列<$C <$，n <$n∈N。然后1或2保持不变：1. 在n个树形分解中，C_n，n具有多项式大小。2. 存在一个正的常数ε，使得对于每个n，C，n的每个树状归结反驳的大小至少为2εn。此外，2成立当且仅当n有一个无限模型。在参数化设置中，我们可以希望上面的第二种情况，也就是最难的情况，分成两个子情况。这确实是正确的，因为我们将证明下面的参数化树状解析的复杂度缺口定理：定理10. 给定一个FO语句<$N，它在所有有限模型中失败，但在某些无限模型中成立，考虑参数化矛盾序列<$D<$N，n，k<$n∈N=<$（C<$，n，k）<$n∈N，其中<$C<$，n<$n∈N是矩阵的平移，已定义。然后2a或2b成立：2a.对于只依赖于λ的常数α和β，Dλ，n，k有一个大小为βknα的2b.存在一个常数γ，0 <γ≤ 1，使得对于每一个n>k，每一个参数化的树型分解此外，2b成立的充要条件是有一个无穷模型，其导出超图没有有限控制集。通过证明情况2b可以达到（见例15和16），并记住注释4，我们得出以下推论。推论11.参数 化的树型分解不是fpt有界的。如果我们可以证明参数化推理的参数化证明系统都不是FPT有界的，那么我们就可以导出W[2]/= FPT。在我们证明定理10之前，我们需要给出一些定义。initions.对于模型M，令|M|表示M的宇宙。给定一个FO句子的模型M，M是有限的或无限的，由模型M导出的超图具有以下元素：|M|作为顶点和超边{y1，. . . y1}，使得（y1，. . . ，y1）在某种关系中表现为元组。（回想一下，有两种关系一个顶点集是独立的，如果它不包含超边作为子集。 设X为一个集合 ， x∈/X ， A 为 一 个 集 合 A ， 使 得 X<${y}<$A<$|M|，我们说y是A-in- dependent from X当且仅当（i）在y处不存在自环{y}，（ii）不存在包含y且与X相交的超边E<$A. 我们说y独立于X如果y是|M|- 独立于X;否则我们说X优于y。最后，支配集是支配超图的所有其他顶点的顶点的集合X3.1定理10我们提供了一个证明方法的概述。我们首先描述定理9的情形1的证明所涉及的方法，然后建议如何对定理10的情形2a进行修改。虽然我们不允许在签名中使用常量，但我们确实将决策树中被质疑的元素称为常量。对于定理9的情形1，我们构造了一个判定树来反驳FO语句的错误.决策树的问题分为两类：I）关于已经被证明的常数的（扩展）关系R的真值的布尔问题，以及II）要求证明Skolem关系S中已经被证明的常数的问题。在后一种情况下，潜在的见证可能是已经被见证的常数之一，或者它可能是一个新的常数。重要的一点是，这个决策树是有限的这是相对简单的把这个FO决定-D，n，k的反驳其大小至少为nkγ。一个布尔决策树，对于每个命题，C，n，其大小至多为（max{m，n}）h，即，n中多项式如所要求的。对于定理10的情形2a，我们构造了一个确定的不同决策树来反驳参数化设置中的FO语句该决策树在第二个新常数独立于第一个新常数和已经证明的常数集的附加假设下成对地添加新常数。我们能够证明，这棵树是有限的同样，我们可以把它变成一个参数化的布尔决策树，对于每个命题Dn，n，k，其大小至多为（mabh）knh，其中a是任意关系的最大值，b是关系的个数（包括两种情况下的Skolem关系）.结果如下。我们以定理10的情形2a的一个例子来结束本节。这个样本提供了一个有点微不足道的例子，因为它确实具有参数化的树状解析反驳，不仅是n中的多项式，而且实际上与n无关。案例2a的例子是非-平凡的，因为最小参数化树状反驳的大小取决于n（参见[5]）。实施例12 我们考虑全序最小数原理的否定。设LNP1为下列的合取。<$x<$R（x，x）（反自反性）R（y，x）（反对称）<$x<$y<$z<$R（x，y）<$$>R（y，z）<$R（x，z）（传递性）<$x<$yR（x，y）<$R（y，x）（总体）y所有的模型都有一个大小为1的支配集;而且，模型的每个元素都构成这样一个支配集。很容易验证，<$D<$LNP1，n，k<$n∈N有参数化的树状归结反驳，大小为2k，与n无关。3.2定理10现在我们把注意力转向证明Theo-rem 10的情形2b。我们的论点将通过一个游戏来促进，这个游戏是基于Pudla'k[12] 和 Riis[13] 在 其 中 我 的 证 明 者 （ 女 性 ） 与Adelion（男性）的比赛中所创造的。在这个博弈中，Prover的策略会在一组子句上生成一个参数化的布尔决策 树 。 Prover 会 询 问 标 记 树 节 点 的 命 题 变 量 ，Advertisement会尝试回答这些问题，以便既不破坏任何特定的子句，也不承认多于k个变量为真（），因为在这两种情况下，Prover都被认为是赢家。当然，假设这组子句是不可满足的，那么Addison注定会输：问题是在失败的过程中他能把树造得多大。请注意，树的每个分支对应于这个博弈的一次博弈，因此每个参数化的决策树对应于一个证明者策略。我们将关注的是Adjuster策略，它在所有Prover策略上表现良好，因此在所有参数化的决策树上推导出一个下界，从而推导出所有参数化的树状解析反驳。当考虑某种Prover策略（参数化决策树）时通过这种方式，在这个子树中有两种类型的非叶节点，那些度为1的非叶节点，其中Adjuster他承认失败的替代估值）和那些他很高兴继续在任何一个结果中。在后一种情况下，我们可以认为他给了证明者一个自由选择相关变量的值的自由选择节点在确保该子树的大尺寸方面起着至关重要的作用设C_n，n是某个FO语句的命题翻译，它没有有限模型，但在某个有限模型中成立.我们将对策G（C_n，n，k）正式定义为：在每一轮中，证明者选择一个她以前没有质疑过的命题变量C n，n，而Advertisement要么回答这个变量为真（n），要么回答它为假（n），或者允许证明者在这两个变量中自由选择。如果在任何时候，证明者持有与C_n，n的子句相矛盾的信息，或者她持有多于k个被评估为真的变量，则证明者获胜。在这种形式主义中，给出了一个关于她移动的证明者策略，并考虑到两个可能的-在自由选择节点上的所有可能性，我们生成一个博弈树，即前面段落中提到的参数化决策树的子树。然而，我们考虑的情况下，在某些模型中，没有有限的控制集。我们将在博弈G（C，n，k）中给出一个Advertisement的策略，该策略保证所有反对的Prover策略都有一个大的博弈树在游戏的任何一点-游戏树中的节点-Advertisement将承认某些信息的他总是在脑海中有两个不相交的集合已经提到的常数P和Q，他已经承认某些信息：最初这些集都是空的。集合Q是一个（P<$Q）-独立的集合，其成员也是（P<$Q）-独立于P的。 在一些意义P是唯一的一组常数，实际上承认一个解释;所有他承认的Q是，它是一个浮动集与某些独立的性质。如果X是一组常数，设MX是模型类与Adelaide在X上承认的信息一致的信息。在每一点上，Prover都会问Adjuster一个形式为Ri（c）或Sj（c）的问题。Adjudan- swers如下：I. 如果c的所有常数都在P中，那么Adjectives应该选择MP中的某个模型并根据该模型回答。II. 如果c的所有常数都在P<$Q中，并且至少有一个来自Q，则Adjuster应该回答false（n）。III. 如果c中的某个常数不在P≠Q中，则– 如果MP中没有模型满足这个问题，那么Adjuster应该回答false（否），否则– 他应该让普罗弗在这个问题上自由选择。在所有情况下，集合P和Q保持相同，除了在情况III第2部分。如果证明者选择真（true），那么Adver- sary将c的所有常数放在P中，可能在这个过程中从Q中删除一些。如果Prover选择false（false），Advertisement会将c中任何不在PQ中的常数放入Q中。事实证明，在情形II和情形III中，从来没有出现过这样的情形，即Adjectile被迫回答为真。特别是，在情形III中，绝不会是MP中的所有模型都满足这个问题的情形。 这对Addison战略的成功至关重要我们现在必须证明这个策略会导致一个大的参数化决策树;我们需要以下内容：owing引理引理13. 考虑博弈树G（C_n，n，k）中从根到叶的任意路径。如果有k个或更少的命题变量被叶求值为真，则不在P中，这将在M上生成P的有限控制集。让我们进一步讨论这一点设c′是c的子元组，由后者的那些不在P<$Q中的常数组成。c′的某些常数可能在以前的问题中提到过，但只在以下问题中提到：Adelaide设P<$Q不是M的控制集，则存在独立于P<$Q的元素x∈M.但是这个元素是这样的，它可以填充元组c′，并在M中证伪Ri（c）或Sj（c）（并证伪先前涉及它的任何问题，这些问题已经被回答为假）。这违背这个问题在一开始就被强迫为真回想一下，我们只能通过违反Skolem子句来达到一个基本的矛盾，现在我们可以完成证明了。设c′是一个永远不会出现在博弈树中的自由选择节点上的常数。为了违反Skolem子句，Adjunct必须否认某些S（c，x），对于替换为x的n个常数中的每一个。 但他的对S（c，c′）的否定是被迫的，这意味着矛盾。由于c′在MP中的任何模型中都是不可解释的，因此S（c，c′′）对于MP中的任何模型中的所有c′′都是假的。这就告诉我们，MP是空的，因此，MP没有无限模型我们现在可以在本节中讨论关键引理了。引理14. 设a是命题翻译中任一关系的最大元数，并假设命题翻译中的不同关系不超过b个（包括两种情况下的Skolem关系）。按照我们对博弈G（C，n，k）详细描述的策略，p和q分别是集合P和Q的基数，当p k;（iii.）n≥7a+1;（iv.）k1/ab≥（16a2）2，则涉及kK（分别为k+ 1）S（0，0）≥nkγ，其中γ：=1/16a3b.当k（≥（16a2）2ab）和n（≥7a+1）足够大时，由这一陈述可直接得出结果通过注意否定变量。这两种方法都失败了--这是因为Nk和N′都是假设情形2b的所有参数化布尔决策树的大小≥2，我们可以将给定的γ修改为适用于所有n，k≥1的γ。请注意，假设（最大元数）a≥2是无害的因此，我们既不是在情况2a中，也不是在情况2b中。≥nk+1。因此，这个证明系统中的所有证明都将失效。进入另一种可能性涉及使用新的辅助变量qvi，j，i∈[n]，j∈[k]。 我们现在加上鸽子洞条款实施例15 我们认为最小数（的否定）第五章焕光l=1 qvi，l和<$qvi，jqv′，j对于i，i′∈[n]（i/=i′）PR IN C IPL EF O RPA LOR D E S. 令NLP∞为例12中给出的FO子句的连接，不带第四个子句（tot a lity）。在有限决策集上，有NP∞H例如，如果Z是整数的集合，则在严格偏序下N×Z（n，z）<$（n′，z′）当且仅当n=n′且zz′<提供了这样一个模型。且j∈[k]。 用N′′表示这组子句。 这些子句本质上指定了从n到k的弱鸽子洞原理，并且相当直接地看出，只有当不超过k个变量Vi为真时，才能满足子句。这种辅助变量的方法导致一个参数化的证明系统，其行为相对于树状分辨率是类似的参数化树状分辨率。由于子句N′可以从这些导出，示例16. 我们回到判决简体中文定义在Ex-公理在一个大小为2k的子树中！，服务，高达2k的可能因子！. 也是实施例5.这有没有有限支配集的模型：例如，正整数N，R（x，y）惠y=x+1，提供了这样一个模型。4嵌入到普通证明系统中给定一个参数化矛盾（F，k），我们可以通过直接公理化F的不超过k个变量可能是设置为true。然后我们可以用一个普通的证明系统来反驳F′。 考虑到参数保持不变，我们得到（2）通过相同的证明。我们还没有定义一个参数化的解析系统，但这样的定义将是一个简单的一般化。目前还不清楚鸽子洞原理在这个系统中的复杂性，但我们可以通过辅助变量的方法解决鸽子洞原理嵌入到归结中的复杂性重新调用鸽子洞原理属于参数化树状解析的“硬”情况（2b）（并且当通过辅助变量的方法嵌入树状解析时也是如此），可能令人惊讶的是鸽子洞原理∨⊥Kqq。. .∨QKKKj=1ijKKKqj=1j=1不不国际新闻报2当嵌入到分辨率中时，原理落入17号提案利用辅助变量的方法，给出了大小为2kn 2的π- Geonhole原理的一个解析反驳。证据请注意，k ≥ n的情况很简单;假设k

下载后可阅读完整内容，剩余1页未读，立即下载