Courcelle定理：树宽图上的MSO问题线性时间解决方法

联系我们⊆∃理论计算机科学电子笔记251（2009）65-81www.elsevier.com/locate/entcsCourcelle定理1的一种实用方法Joachim Kneis2 亚历山大·兰格3部德国亚琛工业大学计算机摘要1990年，Courcelle证明了在一元二阶逻辑（Monadic Second-Order Logic，MSO）中可以定义的每个问题都可以在有界树宽的图上在线性时间内解决。这个强大而重要的定理是其他几个固定参数易处理性结果的基础。Courcelle定理的标准证明是构造一个有限的自下而上的树自动机来识别图的树分解。 然而，自动机的大小，通常在朗道符号中隐藏为常数， 可以变得非常大，并且不能被任何基本函数限制，除非P = NP（Frick和Grohe，2004）。这使得这个问题在实践中很难解决，因为不可能构造树自动机。针对一个实际的实现，我们给出了Courcelle定理限制于形式为opt U的扩展MSO公式的证明V（U），其中是具有词汇（adj，U）的一阶公式，选择最小值、最大值注意，许多优化问题，如最小顶点C OVER，最小顶点D OMINATING S ET，和最大I_NDE_PENDENT_S_（et）可以用这样的公式表示。证明使用一种新的技术，基于使用Hintikka游戏属性的动态规划。为了证明这种方法的可用性，我们提出了一个实现，解决了这样的公式图与小路径宽度事实证明，大常数可以在不太复杂的图上绕过关键词：精确算法，参数化算法，树宽，模型检查，一元二阶逻辑，Courcelle1介绍图论中有大量的NP-难问题，它们的精确解可以在树上高效地计算。例如，众所周知[4，12，30，31]，一元二阶逻辑（MSO）中定义的所有问题都可以在树类上在线性时间内解决。MSO是一阶逻辑（FO）的扩展，它不仅允许对对象进行量化，还允许对对象集进行量化，如 例如，D（D），其中（D）是具有自由集变量D的MSO公式。 在树上进行MSO模型检查的经典方法是构造一个确定性的自底向上树自动机，该自动机在线性时间内识别由下式定义的语言：1由DFG根据RO 927/8号赠款提供支助2电子邮件：kneis@cs.rwth-aachen.de3电子邮件：langer@cs.rwth-aachen.de1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.08.02866J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）65−| || |配方对于有限结构（如图），有几个优化的实现可用，例如在奥胡斯大学开发的MONA工具[22]。许多困难的问题甚至可以在图上有效地解决，这些图可能不是树，但在某种意义上仍然是类似树的。 一个被广泛接受的形式参数来衡量这种相似性是图的树宽。例如，树和森林的树宽为1，但n个节点上的完全图的树宽为n1. 与树宽的定义交织在一起的是一个图G的树分解这样的树分解基本上是用G的图分隔符注释的树T，使得某些性质保持。树宽和树分解是由Robertson和Seymour在一系列关于图子式的论文中引入的[27，28，29]，但在其他领域也非常有用，例如解决图上的困难问题。其原因是，人们往往可以用树结构的树分解来解决G。由于前面提到的图分隔符的大小由树宽加1限定，因此这种方法可以导致具有多项式限定的运行时的算法。如果G有有界树宽。 这也是树宽在参数化复杂性理论中有许多应用参数化复杂性理论是一种探索在“行为良好”的实例上是否可以用接近多项式时间的运行时间来精确地解决困难问题的方法例如，如果一个问题在树型图上是有效可解的，那么可以认为树宽低的图对于这个问题来说是形式上，一个参数化问题L是一组对（I，k），其中I是一个实例，k是参数。一个参数化问题L称为固定参数可处理的，并且属于复杂性类FPT，如果存在一个算法决定L在时间f（k）poly（I）上的成员资格，其中f是一个任意函数。 如果参数是小的，这样的算法可以是相当有效的，尽管NP-困难的问题，特别是如果f是一个中度指数函数。有关参数化复杂性的更多信息，我们建议读者参考介绍性文本，如[9，15，26]。在1990年，Courcelle [6]证明了在计数MSO中定义的每个问题，MSO的扩展，具有额外的谓词评估集合的大小，可以在具有有界树宽的图上在线性时间内解决。 换句话说，当在图的树宽中参数化时，每个这样的问题都在FPT中。 Arnborg、Lagergren和Seese [1]将这一结果推广到了扩展MSO（EMSO），它进一步引入了集合大小上的关系评估。其中，可以例如在满足公式的所有集合中取最小或最大大小，并进一步评估该整数这个一般的和强有力的结果，通常被称为“Courcelle定理”，允许在参数化复杂性理论领域的广泛应用，有时甚至当原始参数化不是树宽时。例如，它被用于最近关于C交叉数问题的参数化复杂性的工作[19，21]，对于该问题没有直接算法。Courcelle定理的标准证明J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）6567一| |||/日本语ϕ⇒ϕ∗？T∈L（A）TTFig. 1.经典的自动机理论方法Courcelle定理：给定一个公式和一个图G的树分解T，首先计算一个标记二叉树T和一个公式，使得T|=G|=0。然后，利用树上MSO模型检验的方法，构造了一个满足L（A）=L（λ）的树自动机A，它在线性时间内检验隶属度Tλ∈L（A）. 因为这只取决于在图的宽度和树 的宽度上，A 的构造与输入图G无关。接近当然，细节比构造MSO公式的经典树自动机要复杂一些，但一般的方法（见图1）是很好理解的：给定一个公式和一个树分解，问题首先归结为标记二叉树上的MSO模型检查问题。用于对树进行MSO模型检查的公知方法涉及识别该标记二叉树的确定性树自动机，然后产生FPT运行时间界限，因为自动机仅取决于树的宽度和树的宽度，并且树分解的实际识别可以在线性时间内完成。特别地，的构造与输入图G有几个其他的证明库尔塞勒[6、5、1、8、9、7、17、24]）。然而，自动机理论方法是最常见的，并且已经在很大程度上进行了研究，特别是关于朗道符号中隐藏的常数的上限和下限[17，14，32]。即使算法渐近地只需要节点数的线性时间，这些隐常数的大小在实际应用中也不能忽略。不幸的是，它们可能变得非常巨大[18]（参见[25，23]）：除非P=NP，否则不存在初等函数f，使得这些常数可以由f（Φ，w）限定，其中Φ取决于定义问题的公式Φ，w是图的树宽。因此，唯一已知的上限非常大也就不足为奇为了得到一些实数，我们可以使用Weyer [32，pp.[213]发现：事实证明，即使对于只有四个量化器的相当简单的MSO-FO公式（MSO增加了一个额外的指数），他得到的上限也大到2（w +4）|Φ|2个2.很容易看出，即使对于恒定的树宽w=1（即，树木和森林）的自动机的大小不能在实践中构建。与此同时，下限[18，32]22o（|Φ|）22对于FO和w=1，表明这个上限已经相当好了，至少如果FTP=W[1]成立，这是普遍认为的。因此，即使是限制性的MSO公式，D68J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）65自动机理论方法通常以类似的方式从瓶颈中支持，即使自动机没有显式构造。粗略地说，在第二阶段（识别或动态编程）中允许线性运行时间所需的所有信息都在第一阶段中以恒定时间计算，假设它是自动机的构造，或者是决策规则的计算或者用于动态编程的查找表。 第一步通常只取决于公式和树宽。 例如，构造的自动机 (cf.、图1）对于所有以该树宽为界的图都是相同的。 换句话说，被计算的自动机必须包含它需要跟踪在最坏情况下出现的所有不同“可能性”的所有状态类似的瓶颈出现在相关的方法中。例如，Courcelle和Mosbah [8]在树分解上使用直接动态规划。动态规划步骤使用布尔连接词作为决策规则，这些规则是从Feferman-Vaught-Theorem [13]的变体（参见[6]）中获得的。Feferman-Vaught定理也被Makowsky [24]用来计算动态规划的大型查找表。最后，Frick然而，由于这个定理的构造性证明类似于树自动机的构造，因此人们经历类似的爆炸并不奇怪。已经开发了几种技术来在可能的情况下解决这个问题，结果好坏参半（参见，例如，[2，22]）。由于在实践中出现的公式通常是非常简单的，不会导致这种爆炸，相应的自动机通常保持小得多。另一方面，我们发现，当目前无法给出更好的直接算法时，可以使用Courcelle定理。手头的问题。这一观点得到了Grohe [19]的评论的加强，他的上述工作C罗辛编号问题：“This涉及到一个非平凡的量化器的交替，这就是为什么翻译成一个算法的困难。在这一点上，我认为通过逻辑和Courcelle定理的路线对我们的证明至关重要。不难看出，数量的变化是自动机规模爆炸的原因因此，每当我们实际上需要Courcelle这是不令人满意的，因为它应该是完全可能解决的问题，只作为一个公式，在简单的图形，例如，长的路径，即使自动机可能太大，即使有技巧。我们认为，上述问题是事实上没有实际实现Courcelle定理的原因，因此没有，例如， 交叉数问题。 一个快速的算法将不仅产生一个快速实现这个问题本身的重要性，但也为任何其他结果的基础上Courcelle因此，我们的目标是开发一种不受此瓶颈影响的Courcelle定理的替代证明J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）6569⊆相反，它应该包含关于整个输入的知识，即，考虑作为输入的一部分的图，使得最坏情况下的下限保持那些，直到公式和图都是最坏情况的实例。 为此，我们采取了更直接的方法，即，它不应该使用从自动机理论背景中获得的方法，而应该直接在树分解和图上工作。在本文中，我们还不能完全证明库尔塞勒这产生了以下形式的选择UV（U），其中，n是一个一阶公式，具有词汇（adj，U）和opt∈ { min， max}。请注意，仍然有许多常见的优化问题，如M最小顶点COVER、MMINIMUM DOMINATING SET和MMAXIMUM INDEPENDENT SET可以用这样的公式表示，并且非初等下界也成立，因为我们可以表示所有的一阶性质。我们的方法的基本思想是在树分解上使用动态规划，但在每一步中，我们使用Hintikka游戏（模型检查游戏）来决定公式是否仍然在图G中成立。模型检测游戏只是游戏理论的形式主义，简化了证明，但可以很好地和直接地转化为直接算法。由于具有数量秩q的MSO公式不能区分Gi的子图，复制者在具有q轮的Escherfeu c ht-Fras'e博弈中具有获胜策略，因此我们仅使用子图的等价类进行模型检查博弈。如果图是相当“简单”的，在这种情况下并不一定意味着“小”，只有几种方法可以在q轮中执行Escherfeu c h t-Fr a ıs 'e游戏，因此只有几个等价类，表仍然很小。通过这种方式，我们考虑了作为输入一部分的实际图形。当然，我们的方法也受到上面提到的非初等最坏情况下限的影响，因为这些下限已经适用于FO。然而，如果我们被一个产生一个非常巨大的自动机的坏公式卡住了，我们可能仍然能够解决实际中出现的各种各样的图形问题为了证明概念，并为了显示可行性，我们开发了一个C++程序的基础上，我们的方法。 在写这篇文章的时候，它已经能够解决由一个公式定义的问题，在路径宽度很小的图上只有很少的量化器，而且实际上所需的空间比我们从目前已知的边界所能预期的要小得多。2预赛我们从本文中使用的符号和我们的方法的基本概念的介绍开始。一个集合U的幂集记为2U。对于图G=（V，E）和UV，U的导出子图记为G [U]，G的节点集记为V（G）。图G=（V，E）的树分解（T，X）是有根树T=（I，F），70J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）65⊕⊂⊂--联系我们|∈ }联系我们以及函数X：I→2V，使得：(i) 对于每个节点v∈V，有一个i∈I，其中v∈X（i）。(ii) 对于每一条边{u，v}∈E，有一个i∈I，{u，v}<$X（i）。(iii) 对于每个节点v V，由i I v X（i）诱导的T的子树 是有关联的集合X（i）称为袋。树分解的宽度是它的最大袋的大小减1，G的树宽度是G的所有树分解中的最小宽度。不失一般性，我们假设本文中使用的所有树分解都是好的，即，(i) 每个i∈I最多有两个孩子，(ii) 如果i∈I恰好有一个孩子j∈I，则X（i）和X（j）恰好相差一个节点v∈V，并且(iii) 如果i∈I有两个子元素l，r∈I，则X（i）=X（l）=X（r）.T中有两个孩子的节点被称为join节点，而只有一个孩子j的节点i被称为forget（resp）。引入）节点，如果X（i）X（j）（X（j））（第十㈠段）。一个终端图是一个带有终端X的标号图（V，E，X）。具有相同终端集X且T1 [X] = T2[X]的两个终端子图T1和T2可以等价地粘在X上，记为T1T2，通过识别X中的节点.这产生一个新的终端子图。大多数使用树宽的算法（包括我们自己的算法）所利用的树分解的一个显着性质是每个包X（i）是G的图分隔符。因此，对于每个袋子X（i），我们可以将两个（forget，introduce）或三个（join）定义良好的终端子图与终端集X（i）相关联。关于树宽和树分解的更多信息，我们建议读者参考Bodlaender结构域上的逻辑的模型检验问题是确定给定的结构是否是该逻辑中公式的模型。本文研究（扩展）一元二阶（（E）MSO）逻辑中词汇adj上的图和公式的定义域。MSO通过集合上的泛量化和存在量化扩展了一阶逻辑，EMSO还允许评估这些集合的大小（见[1]）。我们将使用小写字母表示一阶变量，使用大写字母表示一元二阶（集合）变量。在整个工作中，我们只使用EMSO扩展来表达优化问题，并将自己限制在形式为optU（U）的EMSO公式中，其中opt min， max和恰好包含自由集变量U，但没有进一步的集合量化（仍然允许一阶量化器换句话说，“A”是一个带有词汇（adj，U）的FO-公式在稍微滥用模型理论形式主义的情况下，语义是该公式应“返回”最优集合U的大小，在该最优此外，我们假设，在否定范式，即，否定只发生在原子表达式上。公式Φ中量化器的嵌套深度称为量化器秩qr（qr）。我们只简要介绍本文中使用的博弈论基础，更多信息见，例如。[10 ]第10段。首先，众所周知，J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）6571一B一|一一∈⊆∃∃AB∈≤ABA组B组{}A B ABA组B组|惠B|AB.∩∅关系MSO和FO的检验问题可以表示为有限Hintikka（模型检验）游戏中的获胜策略问题：对于具有论域A的任何结构、具有否定范式的相同词汇表的任何公式Φ（x）以及对Φ的自由变量x的任何赋值a，我们关联模型检验游戏MCG（，Φ（a））。有两个玩家，验证者和伪造者。前者试图证明=Φ（a），而后者想要证明相反的情况。 这个博弈是位置博弈，位置为（n，b），其中n是Φ的子公式，b是对n的自由变量的赋值。如果当前位置是（u，b）或（U，b），验证者必须选择uA或UA，博弈继续进行（n，bJ），其中bJ是通过根据b的选择分配u或U而从b在位置（101，102，b），验证者必须选择2001年，2002年 博弈在（1，b）中继续。同样地，证伪者以普遍的量化或合取来移动。如果n是一个原子或一个被否定的原子，博弈就在位置（n，b）处停止。验证者赢得了I A|=（b）。然后|=（a）i验证者有MCG（A，Φ（a））的获胜策略，从（Φ，a）开始。我们称两个位置（B1，B1）和（B2，B2）是等价的，如果A| = 1（b1）优惠A| = n（b2）.如果A是有限的，很容易看出，一个简单的递归算法可以用来决定A|通过详尽地模拟MCG（A，Φ（a）），其次，Escherfeu c ht-Fras的电子游戏表明，量化等级限制了MSO公式区分结构的能力：在相同的关系词汇表τ上，Let和be结构。对于每个MSO-，对于具有qr（Φ）q的mulaΦverτ，我们写q i = Φ = Φ。 Ekufeu cht-Fras'电子游戏最多可进行qN轮。在每一轮中，扰流器必须从或中选择新的元素或集合。接下来，复制器必须用先前没有从相反结构中选择的元素或集合来回答，使得所选择的元素和集合a in 和b in形成（，a）和（，b）之间的部分同构。 如果一个玩家不能移动，他就输了。如果复制者总能找到部分同构，那么它就赢得了整个游戏。 则q当且仅当复制者在第q轮的Efeu c ht-Fraıs 'e博弈 中有获胜策略[16，11]。 注意，如果我们理解了被选作标号的集合，那么每个这样的部分同构对应于和的导出的标号子图。我们进一步指出了模型检验与Escherfeu c ht-Fra？s？e-博弈之间的关系：后一个博弈可以用于对前一个博弈中Φ的自由变量的赋值最后，非初等函数tow（u，v）：N×N→N定义为：tow（u，v）：=2v·toow（u−1，v）u>01u = 03Courcelle定理的一个限制形式的证明从现在开始，我们固定一个图G=（V，E），其中（wlog）VN=，G的一个宽度为w的漂亮的树分解（T，X），以及一个EMSO公式optUΦ（U，x1）：=optUx1（U，x1），72J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）65∈|⊆∈∈⊆⊆|⊆∈联系我们⊆⊆∈||∈其中，opt min， max和Φ是词汇表adj，U上的FO公式，具有量化器秩t：=qr（Φ）= qr（Φ）+1。借助树分解解决问题的一个典型框架可以概括如下：对于每个袋子X（i），首先将所有局部解存储在表Si中 然后，通过动态规划开始在树叶的树分解，局部解扩展到最优的全局解在可能的情况下。我们使用这个框架来找到一个最优的全局解UV，即，最大或最小集合U V，其中G=Φ（U）。 我们称UX（i）为树分解i的一个节点i的局部（i）验证者具有从博弈MCG（G，Φ（U））中的位置（X，（x1））开始的获胜策略。 现在很容易看出G=Φ（U）当且仅当U是树分解的每个节点的局部解。 从叶子到根部，我们计算到目前为止看到的所有节点的局部解的最优集合（的大小）。从根本上说，只有全球性的解决办法。然而，我们必须避免枚举所有可能的集合U每个节点的V这是树分解的结果，因为否则我们也可以在同一时间内解决初始问题。为此，我们使用观察结果，即Φ不能区分两个集合U1，U2<$V与（V，E，U1）<$t（V，E，U2）。例如，考虑一个公式最小Ux1x2（U，x1，x2）其中qr（i）= 0，并假设模型检查博弈对于某个U V和x1X（i）处于位置（i，（U，x1））现在，证伪者有五种可能选择x2V，但只有五种选择x2V的方法，使得新的位置是成对不等价的：要么选择x2=x1，要么选择x2是否与x1相邻以及x 2是否与x2U相邻的任何组合--这是原子公式中仅有的五种情况。这与埃弗弗赫特-弗腊伊斯电子博弈在（V，E，U）（加1）上的“有效”方式数一致：同样，有限回合中的部分同构已经由x1和x2是否相邻以及x2是否在U中确定。 这个论点很容易推广到具有更大数量级的公式（即使每个数量级都将进一步的指数引入上限）。现在的想法是，对于每一个集合U V，我们只使用在Escherfeu c ht-Fraïssss′e-博弈下的等式类（V，E，U）的表示，这样可以更快地枚举。然后，给定所有等价类的集合，我们可以判定每个等价类中的成员是否是X（i）在FPT运行时间范围内的局部解，并且在动态规划中，我们只保存每个等价类中最优解的 大小 。我们在这里使用的表示是一个有根树，它描述了如何在G的终端子图T上“局部地”执行Escherfeu c ht-Fra？es？e-博弈：由于集合应该是局部解（根据模型检查博弈定义），我们也将Escherfeucht-Fra？es？e-博弈的第一轮限制在终端上，但同时保留在第一轮中明确选择的xX（i）。 我们称之为“Ejufeu c ht”- 然后树表示的每一个节点对应于局部Escherich-Fraıs′e-game中的一轮J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）6573∈--关于我们1公司简介K≥ ||−DA B CE一B一1B一1B一B12一1一1B2B2图二、本文给出了左端点图T的Effeu cht-Fraıs ′e-对策表示E FG3（T，U），其中X=甲乙丙U=C（显示为方形节点）：我们限制博弈，使得在第一轮，玩家必须选择任意的x X（树的根）。在下一轮中，参与人在选择第一个非终结图（标记为1）时，只能有两个选择：要么选择非终结图C，这会产生左子博弈，要么选择D、E中的任何一个作为右子博弈：节点D和E在下一轮中总是产生相同的诱导标记子图（直到同构），其中第二个非终结图被选择（标记为2），因此，在下一轮中，不会引入新的子博弈。节点对应于某个非终端的选择。每个节点都用该轮中获得的部分同构标记，或者更准确地说，用当前诱导的标记子图标记（参见图2的示例）。定义3.1设X是一个袋，T是G的一个终端子图，U∈V（T），且对于每个k ≥ 0，令（v1，...，vk）∈（V（T）\X）k，使得对 于 每 个 i ， vi vjJ. 部分同构表示<$（T，v1，...，vk，U），（v1，.，vk），并且U是从标记（终端）子图（T [X∈ {v1，...，vk}]，U（X{v1，.，通过将每个非终结符vj标识为整数j（回想一下，V_N=v_k））。对于任意的终端图T，任意的集合U∈V（T），每个0≤k≤t− 1，每个（v1， . ，vk）∈（V（T）\X）k递归地定义标号树E FGv···v如下.E FGv1···vk的根标记为SUB（T，v1， . ，vk， U）。Furgent，ifkt−1，for eachE FG∈{E FGv1···vkv|v∈V（T）\X<$vv1，.， vk}有一个子树E FG。T和U的Ehrenfeucht-Frais的电子博弈表示定义为EFGt（T，U）：= EFG，其中是空序列。如果对于某个集合UV与UV（T），我们可以将EFG t（T，UV（T））作为EFGt（T，U）。事实证明（见下一个引理），不同的局部Escherich-Fraüs'e-对策的数量是根据w从b到e有界的。X1（树宽）和量化器秩，特别是不依赖于G的大小（输入大小）。这对于我们想要实现的FPT运行时间来说是好的，但是如果我们想要避免我们在介绍中提到的全面爆炸，然而，请注意，即使每个量化器将指数引入上限-由于已知的下限，这是预期的-获得的局部博弈的实数取决于输入（终端）图，如图2中的示例所示。74J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）65||−≤⊂⊕⊕∈∈\\∈··-∈−⊕ ⊆⊆引理3.2设X是一个袋子（即，X1w），T是一个终端图. 非等价Eh renfeucht-Fraïs ′e-对策表示E FGt（T，U）的个数，即，的大小{EFG t（T，U）|U V（T）}，是由O（2 w 2 tow（t−1，w+t+2））限制的，每个表示的大小由O（tow（t− 1，w+ t + 2））限制。证据 我们通过归纳法证明了l ocalEscherfeu c ht-Fra？s？e-对策中回合数的上界。回想一下，我们只考虑了第一轮选择在X中的博弈，但我们留下了开放的，其中x是明确选择的。因此，我们使用一种表示来考虑所有这些博弈对于任何0≤kt，我们用nk表示参与者可以对任意UV（T）（结构（T，U））玩的游戏数(i) 从具有先前选择（x，v1，...，vk），(ii) 对于所有x∈X（同时），(iii) 但有明显的V1，...，vk∈ V（T）\X，vivj.如果k= t1，游戏结束，因此只能玩空游戏。 如果K k必须增加它们的索引。最后，通过删除x和复制子树，从老树确定新树的根的标签，即，那些代表等价子博弈的，必须被剔除Q我们现在可以勾画出我们的主要算法（在算法1中描述），并获得 我们的主要成果。定理3.6算法1在时间上返回Φ（U）的最优解U V，O（2w24·to ow（t−1，w+t+2）·|不|）的。证据Wlog，让opt = max。对于任何节点i，设Ti，p是i的过去的终端图，即，终端图包含i以下的包中的所有节点，并且令Ti，f是i的未来，即，唯一的Ti，f，使得G = Ti，p<$Ti，f.通过对第一次自底向上遍历的直接归纳，人们可以借助引理3.3，3.4和3.5首先证明（此处省略），对于每个i，Pi包含一个元素EFG t（Ti，p，U），它对应于所有U∈V（Ti，p）。同样，自上而下遍历在Fi中产生条目EFGt（Ti，f，U），对于所有U∈V（Ti，f）和所有i。通过对i的第二次自底向上遍历的归纳，我们现在将表明该算法计算正确的值。也就是说，如果Si包含一个条目，J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251（2009）6577∀∈⊆⊕∪∈∈|∩|{}∈{ ∞ −∞}∈⊕∪∈ ∈∈∪ ∪ ⊕⊕算法1输入：一个图G=（V，E），一个宽度为w的G的漂亮的树分解（T，I），一个EMSO公式opt U Φ（U）= opt U x1（U，x1），Φ和qr（Φ）= t中没有量化器。输出：最优集合U的大小，其中G| = Φ（U）。(i) 对于每个i V（T），创建空表Pi和Fi（称为过去和未来），它们可以保存一组l ocalEh renfeucht-Fraıs 'e-game representations，并为i的每个子j创建指向Pj和Fj中条目的指针列表。(ii) 自底向上遍历T并相应地更新过去的Pi：对于叶子i，枚举所有U X（i）并将EFGt （ G[X （ i ） ] ， U ） 插入 Pi 。 对于join 、 introduce 和 forget-nodes，分别使用引理3.3、3.4和3.5的算法(iii) 在根r中，枚举所有U ∈ X（r）并将EFGt（G[X（r）]，U）插入Fi。(iv) 自上而下遍历T，并相应地更新未来的Fi：引入和忘记对其子节点使用相应的相反算法;对于具有两个子节点l和r的连接节点i，Fl从F i和P r“连接”; F r类似。(v) 对于每个i V（T），创建一个表Si，该表对于成对的游戏表 示 保存N中的值失败，失败的地方+，（ 取 决 于 opt ） 是 默 认值。(vi) 自底向上遍历T并更新每个Si如下：如果i是叶节点、引入节点或连接节点，则对于每个Ep：=EFGt（Tp，Up）Pi和Ef：=EFGt（Tf，Uf）Fi，使用建模博弈来测试UpUf是否是TpTf=G的局部解。 如果不是，则令Si[Ep，Ef]：=失败并继续。 如果是，则必须使用先前计算的表中的条目更新Si[Ep，Ef]（这里，我们使用指针）：• 如果i是一个零节点，只需设置Si[Ep，Ef]：=UpX（i），它可以从Ep导出。• 如果i是一个具有子节点j的整数，则EpJ是来自Ep是由edbottom-up得到的，设EfJe是由Eftop得到的项ed下，使得x∈U在EfJSj[EpJ，EfJ]+|{x} UJ|.i∈U在EpJ中。然后令Si[Ep，Ef]：• 如果i是一个有子节点j的节点，l∈Si[Ep，Ef]e是其中的最优值，所有条目Sj[EpJ，EfJ]，使得从EpJ向上获得Ep，且EfJ是从Ef自顶向下获得的唯一条目否则，如果i是具有子节点l和r的连接节点，则我们遍历所有El，p：=EFGt（Tl，Ul）Pl，a1lEr，p：=EFGt（Tr，Ur） Pr和a1lEf：=EFGt（Tf，Uf）Fi（其中Ul，Ur和Uf仅是隐式的）。LetEp：=E FGt（T1Tr，U1Ur）（引理3.3）。我们现在再次使用模型检查游戏来测试U是否为UlUr是TfTlTr=G的局部解. 如果不是，则令Si[Ep，Ef]：=失败并继续。否则，我们可能更新Si，即， 我们让Si [Ep，Ef]：=opt{Si [Ep，Ef]，sl+sr-|UpX（i）|}的情况下，其中resl= Sl[El，p，E FGt（TfTr，UfUr）]，sr= Sr[Er，p，E FGt（TfTl，UfUl）]，并且|UpX（i）|可以从E p中扣除。78J. Kneis，A.Langer/Electronic Notes in Theoretical Computer Science 251