理论计算机科学电子笔记174（2007）45-56www.elsevier.com/locate/entcs使用QBFToni Jussila1奥地利林茨约翰内斯开普勒大学形式模型与验证研究所摘要符号模型检查是PSPACE完成的。 由于QBF是标准的PSPACE完全问题，因此将符号模型检验问题编码为QBF公式，然后使用QBF决策过程来解决它们是最自然的。我们讨论了替代编码的无限和有界的安全检查成SAT和QBF。一个贡献是简单路径约束的线性编码，这通常是使k-归纳完备所必需的。我们的实验结果表明，确实可以得到一个很大的减少所产生的公式的大小。 然而，目前的QBF求解器似乎不能利用这些紧凑的配方。尽管这些大多是负面的结果，这些基准的可用性将有助于提高QBF求解器的最新技术水平，并使基于QBF的符号模型检查成为一种可行的选择。关键词：有界模型检验，编码，QBF，SAT。1介绍Bounded Model Checking（BMC）[3]有动机通过使用SAT过程来改进基于BDD的符号模型检查。在最初的论文中，已经建议使用QBF决策程序作为一种工具，使BMC在不使用BDD的情况下完成。完整性意味着LTL属性也可以被证明成立，而不仅仅是能够找到反例。在本文中，我们专注于简单的安全属性，我们要证明一个坏的状态是不可达的。更一般的属性可以通过[14]中的技术来处理[3]的完备性结果使用了这样一个事实，即系统的直径，即两个状态之间最长最短路径的长度，是潜在反例长度的上界。问题是如何计算直径。在[3]中，给出了一个用d参数化的QBF公式，它分别是令人满意的。是的，i_d是直径的上限不过这1 电子邮件：toni. jku.at2电子邮件：armin. jku.at1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.12.02246T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）45在实验中没有使用该公式，因为当时不存在有效的QBF求解器。在图论中，直径的概念也被称为偏心率。文[10]研究了时序电路状态转移图偏心度的判定问题。作者使用专用QBF求解器进行定量消除。然而，可以处理的例子很少。[17]中给出了DPLL风格的QBF求解器不能很好地处理这类问题的原因：本质上，DPLL风格的QBF求解器需要执行显式状态空间搜索来确定直径。然而，对于几乎相同的问题，可以生成一个没有量化器的纯命题SAT公式[3]。如果不能满足，它就构成了直径的上限。该公式由r参数化，并且如果不存在长度为r的无环路径，则该公式是不满意的。在图的术语中，无圈路也称为简单路，而在[3]中，简单路的最大长度称为重现直径。这些概念可以用两种方式来定义[15]：首先可以初始化直径和重现直径。在QBF和SAT的情况下，路径都可以被强制满足附加的约束，即第一个状态是初始状态。此外，不是以向前的方式从初始状态开始寻找最大简单路径，而是可以从坏状态向后工作。特别是，一个简单路径的最大长度，它的最后一个状态是一个坏的状态，也是一个上限的最大长度的反例，需要搜索。我们称这种路径为终端。在k= 1的特殊情况下，这种技术相当于检查好的状态是跃迁关系的归纳不变量。因此，该技术也被称为k-诱导[15]。它在实践中似乎比正向检查更成功，因为它可以利用属性的局部性，即使它只是通过SAT求解器隐式地进行，而正向公式化需要考虑所有状态位。然而，简单的路径可以指数大于其相应的直径，无论是在向前和向后推理。因此，问题仍然存在，使用QBF推理的方法是否不允许更早地终止对反例的搜索。此外，近年来QBF求解器技术的最新技术水平也有了相当大的提高[11]。据我们所知，还没有发表的结果，使用QBF向后推理。不幸的是，我们的反向推理实验结果强烈表明，与[10，17]的正向推理结果类似，基于QBF的定点算法还不能真正与基于BDD的或其他使用SAT的完整模型检查算法竞争，例如[1]中所讨论的。没有一个例子是解决不了的，也可以用k-归纳法解决.在积极的一面，我们提供了新的紧凑配方的有界模型检测问题，并表明在某些情况下，QBF为基础的推理可以优于SAT为基础的推理。我们的基准将公开提供。它们将有助于提高QBF求解器的艺术水平，并有望导致T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）4547向前模型检查μ（I，T，B）C=假;N=I;当N/NC做如果BN满足，则返回C=N;N=CImg（C）;完成;返回Fig. 1. 安全性质的在线前向模型检验算法。基于QBF的模型检测算法。最后，我们尝试了下一个状态逻辑的函数和关系展开。实验清楚地表明，函数展开要紧凑得多。生成的CNF是小得多时，使用语法替代下一个状态函数，而不是结合的过渡关系。SAT求解器的运行时间也大大减少2背景量化的布尔公式（QBF）形成了一个命题逻辑，其中包含布尔变量上的量化器我们使用的QBF求解器只接受前束形式的合取范式（CNF）中的QBF。为SAT生成CNF的标准算法[18]也可以在取出量化器后用于QBF。额外的变量将在最里面的作用域中存在量化。在本文的其余部分，我们不需要前束CNF。我们的系统模型是符号模型检查中使用的标准关系模型。它是一个具有初始状态con的布尔编码Kripke结构K约束I（s）、转移关系T（s，SJ）、坏状态约束B（s）和好状态约束G（s），其中G（s）≠ <$B（s）。状态变量向量s，SJ，. 作为国家。一个状态变量向量，在下面的简短状态变量中，由n个单独的状态位组成，这些状态位只是布尔变量。个人状态位和状态变量上的等式充当原子命题。K中长度为k的有效路径是状态变量s 0，. 满足路径约束T（s0，s1）<$T（s1，s2）<$··<$T（s k−1，s k）的s k。初始化路径约束还要求I（s0）成立，而终端路径约束要求B（sk）成立。一个坏的状态是可达的，如果对于某个k存在一个可满足的路径约束，它同时是初始的和终结的。在本文中，我们只考虑检查的问题，一个坏的状态是否是可达的。48T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）453不动点图1的算法是用于使用BDD检查简单安全属性的标准BFS算法。集合C和N以及关系I、T和B用符号表示。该算法实现了从初始状态开始的定点计算，在一个步骤中添加下一个可达到的状态N其中Img（C）（sJ）<$s[T（s，sJ）<$C（s）]，从目前达到的状态C直到发现坏状态B或循环终止。BMC的重点是前者，而在本文中，我们专注于检查循环条件。循环条件初始无效，甚至没有进入循环，iI =“假的，假的。这可以通过SAT求解器来检查。在第一次迭代之后，循环条件的有效性也可以通过SAT求解器来检查，因为它等价于I（s）I（sJ）]的可满足性如果这个公式是不可满足的，那么I实际上是一个归纳不变量的过渡关系。然而，在第二次迭代之后，循环条件等价于满足s0，s1，s2[I（s0）<$t0，t1[I（t0）<$T（t0，t1）→（s2/=t0<$s2/=t1）]]这是一个有一个交替的适当QBF公式3一般来说，循环条件在k次迭代后满足，如果满足以下公式：s0，s1，. ，s k[I（s0）<$T（s0，s1）<$··<$T（s k−1，s k）<$t0，t1， .. . ，tk−1[I（t0）<$T（t0，t1）<$· ·<$T（tk−2，tk−1）→（sk/=t0··sk/=tk−1）]]该公式的变体也用于[10，17]。 其实际用途是相当有限的。在我们的实验中，没有一个实例，初始化直径检查，可以这样做，如果它涉及任何量化器的交替。显然，需要更强大的QBF求解器。使用重现直径的初始实验也不成功。这些实例对于小k是可解的，但是对于这些实例来说，重现直径太大，并且SAT实例也很快变得难以处理。这与k-归纳中简单路径约束的经验相反。因此，我们建议将符号后向定点计算的终止检查也表示为QBF决策问题：s0，s1，. ，s k[T（s0，s1）<$··<$T（s k−1，s k）<$B（s k）<$t0， t1 ， .. . ，tk−1[T（t0 ，t1 ） <$· · ·<$T（tk−2 ，tk−1 ） <$B（tk−1）→（s0/=t0···s0/=tk−1）]][3]这里我们需要一个共同的假设，即转移关系T是全的，这一点我们将在本文的其余部分进行假设。T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）4549在我们的实验中，结果表明，在这种情况下，k= 2的两个实例可以解决，对于这两个实例，k-归纳也很容易确定终止然而，这个否定的结果仍然表明，即使在使用QBF时，向后计算也可能优于向前计算，因为它是检查重现直径与k-归纳的情况。对于向后定点计算，我们实际上使用了一个稍微不同的公式，也用于基于SAT的k-归纳[15]，其中T被TG替换为TG（s，sJ）<$G（s）<$T（s，sJ）。 如果公式是不满足的，那么k是上界，必须搜索的最大路径长度，以便找到一条通往坏路径的路径。状态，它只遍历好的状态，除了最后一个状态。这种优化可以大大减少必须检查的界限。4非线性迭代平方根据QBF [13，16]的PSPACE硬度的经典证明，我们可以使用非复制迭代平方来象征性地计算过渡关系的传递闭包，如下所示：T2·i（s，SJ）=m[nc [nl，r [（c→（l = s r=m））（c→（l=m<$r=sJ））<$Ti（l，r）]通用的这只是一个紧凑的QBF重新公式化的复制迭代平方T2·i（s，sJ）<$$>m[Ti（s，m）<$Ti（m，sJ）]这使得每次应用时公式的大小加倍，而非复制公式每次只添加一些状态变量等式。在[12]中讨论了类似的公式，并且在[2]中也用于对非常简单的计数器电路进行有界模型检查。在后一篇论文中，已经观察到，目前最先进的QBF求解器几乎不能跟上基于SAT的有界模型检查这些例子。然而，QBF公式在模型中是线性的，在步骤的数量上是对数的，这在状态位的数量上给出了至多二次公式。最坏的情况只发生在序列深度，例如初始化直径，实际上是2n。5简单路径约束在[3，15]中，引入了简单路径约束（1）si/=sj0≤i j≤k对于多个状态位的比较，其大小不一定是在[9]中，通过对si进行符号排序，可以实现O（k·log（k））50T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）45i=0时可以获得大小界限。在实践中，由于大的常数，更简单的排序网络的大小为O（k·（log（k））2）是首选，如双调排序或奇偶归并排序。在我们的实验中，我们使用了后者，因为它需要的时间稍微少一点。与[9]中使用的双调排序网络相比如果这些约束与路径约束相结合，它们允许获得完整的模型检查过程。如果路径约束被初始化并且结果变得不可满足，则k是重现直径的界限[3]。如果不存在达到此长度的计数器示例，则无法访问坏状态。类似地，如果简单路径约束与终端路径约束相结合，如在k-归纳[15]中，则结果的不满足性再次表明k是需要考虑的反例的最大长度的上界。在k-归纳法中检查的公式如下：（二）k−1T（si，si+1）k−1G（si）B（sk）si/=sji=0时i=0时0≤i j k注意，作为“好状态”的最后一个状态sk从Eqn。我们可以在k-归纳中去掉与最后一个状态的比较。类似的参数可以用于计算重现直径。5.1 QBF中的紧凑简单路径约束本文的贡献之一是重新表述了方程的简单路径约束。QBF中的1，如下所示：（三）10.，l k[s [|克i=0时L i| = 1→Ki=0时（li参与者（s=si））]所得到的公式需要一个交替的量化器，并且与原始公式的二次复杂度相反，在k中是线性的。请注意，相应路径约束的状态变量是这个公式的自由变量，并且在我们的应用程序的最外层范围中存在量化。为了获得线性复杂度，基数约束|克 L i|中的一个或多个条目，该条目简单地说，只有一个Li是真的，必须用线性大小的电路.这是很容易实现的，因为例如对于任何变量阶的基数约束的ROBDD具有k的线性大小。附加的“比特”10，. ..li将si保存为s，并强制s与所有其他sj不同w ithi/=j. 一个简单的索引编码的恢复是可操作的，只需要[log2k|额外的通用变量这个例子已经显示了QBF的一些建模能力，我们相信，QBF在实践中还很少使用。但我们可以更进一步，如[6]中那样，共享跨时间框架的转换关系我们的QBF重新制定如下T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）4551（l）i=0ii[6]的路径约束如下：10.，l k[s，sJ][T（s，sJ）]（四）克i=0时 L i| =1 →k−1i=0时 我 →（s=s isJ=si+1）））]]把两者放在一起，我们得到了一个紧凑的简单路径约束在QBF与过渡关系共享的重新表述10.，l k[s，sJ][T（s，sJ）]（五）克i=0时 L i| =1 →k−1（l→（s=ssJ=s））i=0时 我我K（l） 参加人（s=s））]]一期+1可以根据需要分别添加初始和终端约束。在k-归纳的上下文中，实践经验表明，将良好的状态约束添加到转换关系的当前状态，如在等式11中。2，提高了性能，特别是大大降低了界限k。我们可以在QBF公式中实现相同的效果，只需将G（s）添加到最内部的存在范围，因此，实际上也在时间框架上共享G在实验中，我们使用了后一个版本。6过渡函数和关系SMV [5]允许两种方式来指定系统可以进行的转换。我们将这些部分称为功能和关系部分。在函数部分（SMV文件的ASSIGN部分），下一个状态的变量值被定义为当前状态变量值的布尔函数。关系部分只是一个布尔公式，其中原子公式是当前和下一个状态变量，并且这个公式（在SMV文件的TRANS部分中给出）必须在任何两个状态之间保持。SMV文件可以包含关系和功能部分来描述系统当转换关系（或简单路径约束）被展开时，函数转换关系允许在到SAT/QBF的转换中的优化。也就是说，对于功能状态变量，可以在初始状态之后的任何状态中替换其下一个状态函数。此后，可以通过将信息从初始状态传播到后续状态来简化表示。例如，考虑变量x0和x1，让SMV文件包含init（x 0）：=0和next（x1）：=！x0。 然后，显然可以推断出，在转换关系展开一次之后，x1的值为1等。我们将这种优化称为函数替换。 请注意，如果QBF用于共享转换关系和简单状态约束，则这种替换是不可能的。在我们的实验中，我们将这种优化的翻译与功能替换被禁用的翻译进行比较（考虑模型是纯关系的）。我们（|（|52T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）45实验结果表明，在某些情况下，功能允许的优化起着重要的作用。7实验我们已经在一个名为SMV2qBF的工具中实现了我们的方法。它以简单的安全属性作为输入读取SMV规范，并将其转换为QBF。该工具有几个开关对应于不同的模型检测问题。可以执行标准BMC，计算直径和重现直径，计算定点，并进行k-归纳证明[8]。对于这些问题中的大多数，有两种或更多种编码，标准命题编码和使用更紧凑的QBF的编码。我们给出了两组结果，第一组是可以使用k-归纳法证明安全性的问题其次，我们有一些例子，其中使用标准BMC找到了一个反例。在实验中，我们使用了一组Pentium IV 3.0 GHz的PC，它们的主内存为2GB，运行Debian Sarge Linux。时间限制设置为1000秒，内存限制为1GB的主内存。我们使用的例子是从TIP到E′en和So′renss on[8]。我们使用QUANTOR（version2.13）[2]作为QBF求解器。qUANTOR使用SAT求解器作为后端，为此，我们使用PICOSAT（版本1.251）。我们还将qUANTOR与另一种最先进的QBF求解器qUBE（版本1.3）进行了比较[7]。在我们尝试的每一个例子中，quantor都表现得更好。在表1和表2中示出了证明了该性质的实施例的结果。表中各栏如下。在这两个表中，最左边的两列给出了示例的名称和证明该属性所需的范围其后是形式为s（x）（表1）和t（x）（表2）的6列，其中x是编码类型，s（x）代表大小，t（x）代表时间。我们对k-归纳步骤使用以下编码：(i) i是标准的完全命题编码（Eqn. （2），(ii) ir是没有功能取代的i（参见Sect.6），(iii) IS用排序网络实现简单的状态约束，(iv) ISR是没有功能取代的，(v) l是一种编码，其中转换关系被展开，但简单路径约束被编码，如等式n中给出的。三、(vi) LR是没有官能取代的L(vii) L是使用Eqn. 5使用独热索引编码，以及(viii) B是一个修正的方程。5二进制索引编码。形式为s（x）的列给出了用于编码x的（SAT/QBF）公式的以字节为单位的大小以及列k中给出的界限。列t（x）中给出的运行时间是解决编码x的单个实例所需的时间，对应于T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）4553列k中给出的深度。如果条目的格式为N/A，则超出了内存限制（我们没有遇到超时）。名称Ks（i）s（ir）s（是）s（ISR）s（l）s（lr）s（L）s（B）厘米单位周期数9641372414162799628096 9832984421002112eijk.S208.S25814672817082849772728083232 2686436563696eijk.S208c.S258 148840186168513328271632123379238843924eijk.S208o.S25812978816474044240774803048 3751629202956eijk.S298.S58138681975210740165841136681216681672eijk.S510.S106562504126830683722404632636eijk.S820.S118443468130039045843500664664eijk.S832.S119003592140040726283704700700eijk.S953.S7448261274829123602748776776ken.oop1.C29320442043536450411162184608608nusmv.guid*1.C10136025642192332011122224752752nusmv.guid*7.C278208119969520133162712617217281732nusmv.tcas2.B611763936182045841016436412841288nusmv.tcas3.B5892296414203704836364011721172德克萨斯州.par*2.E2364804448844548356356与生产有关的费用 *12.E29106126548811352662726008 6832833203320与生产有关的费用 *13.E815561611218841648814721879224442444与生产有关的费用 *14.E16411233700477634440 31643731227762776相对于生产量c*15.E237260498088496510244664 534963068 3068与生产有关的费用 *16.E58009752100499808241174023202320与生产有关的费用 *17.E27944460076103926109255285987232363236与生产有关的费用 *18.E133036262843708270442500 2861626522652与生产有关的费用 *19.E226772474848012487124468512043028 3028与生产有关的费用 *24.E3715832877601688888900 7924 8909236523656表1k-感应尺寸表3和表4遵循与表1和表2相同的约定，但是，这次k是找到反例所需的最小深度。编码如下：(i) b.标准命题BMC编码，(ii) Br是没有官能取代的B(iii) C，具有转变关系的单个副本的紧凑BMC编码（参见等式10）。（4），以及(iv) S，BMC编码与非复制迭代平方（见节。4）.表1应用QBF表示在许多情况下产生更小的公式，并且差异似乎随着更大的界限而增长当模型是完全相关的时，尤其如此。这个结论是相当明显的，虽然，因为54T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）45QBF线性增长，在命题的情况下，一个新的副本的过渡关系时，需要增加的界限。一个可能更有趣的观察是，命题编码的优化版本（列t（i）和t（b））的运行时间总是低于使用更紧凑公式的编码。我们确定了两个原因。首先，命题编码允许执行优化（prepro，T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）4555名称Kt（i）t（ir）t（is）t（ISR）t（l）t（lr）t（L）t（B）厘米单位周期数96144.7144.6178.4173.3162.5162.3345.1153.5eijk.S208.S258N/AN/AN/AN/AN/AN/AN/AN/Aeijk.S208c.S258N/AN/AN/AN/AN/AN/AN/AN/Aeijk.S208o.S258N/AN/AN/AN/AN/AN/AN/AN/Aeijk.S298.S5866.061.5N/AN/AN/A207.7195.1132.2eijk.S510.S101.92.4163.7174.8N/A5.45.75.9eijk.S820.S112.23.493.882.1N/A5.33.63.4eijk.S832.S112.33.595.584.9N/A6.03.93.6eijk.S953.S70.81.78.68.338.42.83.12.8ken.oop1.C2923.018.3N/AN/A30.430.950.337.8nusmv.guid*1.C101.42.01.52.16.36.27.66.2nusmv.guid*7.C2761.760.2173.785.887.592.6116.5116.7nusmv.tcas2.B61.22.51.32.63.94.911.16.4nusmv.tcas3.B50.51.41.02.03.23.46.54.9德克萨斯州.par*2.E20.00.20.00.20.10.20.40.2与生产有关的费用 *12.E2930.3197.925.0173.1N/A245.874.357.0与生产有关的费用 *13.E81.413.31.612.65.016.88.68.1与生产有关的费用 *14.E165.646.64.644.423.764.620.217.6相对于生产量c*15.E2315.3113.517.3100.585.0146.243.834.4与生产有关的费用 *16.E50.86.20.96.22.18.67.46.9与生产有关的费用 *17.E2732.1163.725.2145.6N/A200.264.652.1与生产有关的费用 *18.E133.628.73.729.613.937.914.512.7与生产有关的费用 *19.E2212.697.612.394.470.6130.136.732.0与生产有关的费用 *24.E3759.8N/A49.4N/AN/AN/A125.0103.9表2k-感应运行时间名称Ks（b）s（br）s（C）s（S）nusmv.tcas1.B10960558045121524nusmv.tcas4.B141604925664961516nusmv.tcas5.B2326881310497961668nusmv.tcas6.B16281614900101881668texas.parsesys1.E914023922140568texas.parsesys3.E810020881812516texas.twoproc2.E15481383296761636texas.twoproc4.E1922419004124081676vis.eisenberg1963219644121721580表3 BMC尺寸cessing步骤），像功能替代（见第6节），但也有界锥的迭代[4]以有效的方式。4实56T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）45际上，应该注意的是，对于某些测试用例（如vis.prodcell. * 示例），当SMV模型是完全相对的并且因此不可能进行函数替换时，共享转换关系（列t（L）和t（B））的QBF编码比SAT编码（列t（IR））执行得更好。第二，研究界已经投入了更多的精力来实现有效的SAT求解器，而不是QBF。我们期待更高效的QBF4.注意，我们总是在每个编码中通过锥的不确定性约简来约简模型，特别是对于转移关系和比较状态变量。此外，我们只比较在当前状态和下一个状态中出现的状态变量[8]。T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）4557名称Kt（b）t（br）t（C）t（S）nusmv.tcas1.B100.942.3364.656.7nusmv.tcas4.B141.646.8558.056.7nusmv.tcas5.B233.351.4N/A81.9nusmv.tcas6.B163.246.9N/A76.1texas.parsesys1.E90.110.286.410.8texas.parsesys3.E80.19.169.08.8texas.twoproc2.E150.0133.4N/A141.8texas.twoproc4.E190.3147.4N/A213.3vis.eisenberg191.180.9N/A117.5表4BMC运行时间未来的解决方案8结论本文一方面再次提供了负面的结果，使用QBF的无界模型检查和有界模型检查较少的负面。另一方面，我们能够表明，在实践中QBF公式可以比SAT实例更紧凑，有时解决关系编码更快。我们的研究结果清楚地表明，需要更多的研究QBF能够使用QBF作为替代SAT基于模型检查，即使在有界的情况下。工具SMV2qBF和DIMACS格式的基准测试可在http://fmv.jku.at/smv2qbf上获得。我们目前也在制作结构基准，以与逆变器图（AIG）的形式。引用[1] N. Amla，X. Du，A.屈尔曼河P. Kurshan和K. L.麦克米兰工业环境中基于SAT的模型检测技术分析。在Proc.CHARME斯普林格。[2] A. 比尔解决和扩展。 在proc SAT'04，LNCS第3542卷。斯普林格。[3] A. Biere，A.Cimatti，E.Clarke和Y.竹没有BDD的符号模型检查在Proc. TACAS斯普林格。[4] A. Biere，E.克拉克河Raimi和Y.竹PowerPC微处理器的安全特性，使用符号模型检查没有BDD。 在proc CAV'99，LNCS第1633卷。[5] A. Cimatti，E.M. Clarke，E.Giunchiglia，F.Giunchiglia，M.Pistore，M.罗韦里河阿斯塔纳，和A.塔切拉NuSMV 2：一个用于符号模型检查的开源工具。 在Proc.CAV[6] N. Dershowitz，Z.汉娜和J·卡茨使用QBF进行有界模型检查。在Proc.SAT斯普林格。[7] A. 塔切拉E.Giunchiglia，M.纳里扎诺系统描述：QuBE一个用于确定量化布尔公式满足性的系统在Proc IJCAR[8] N. E'enandN. Sürens s on. 通过自动化系统实现的时间戳导入。 在中国。 BMC' 03，ENTCS的第8 9卷。爱思唯尔[9] D. Kr？oningandO. Strichman. E. E.C. E. C.C.D. D. E. C. E. C. D. E. C. E. C. D. E. C. E. C. E. D. E. C. E. C. E.E. C. E. C. E. E. C. E. C. E. E. C. E. C. E. D. E. E. C. E. C. E. E. C. E. C. E. E. C. E. C. E. E. C. E. C.在中国。VMCA I'03，LNCS的第2575卷。斯普林格。[10] M. Mneimneh和K.萨卡拉计算指数大图中的顶点偏心率：QBF公式和解决方案。 在proc SAT'03，LNCS第2919卷。斯普林格。58T. Jussila，A.Biere/Electronic Notes in Theoretical Computer Science 174（2007）45[11]M. 纳 里 扎 诺 湖 Pulina 和 A. 塔 切 拉 第 三 次 QBF 求 解 器 评 估 报 告 。 Journal on Satifiability ， BooleanModeling and Computation，2006。[12] 林塔宁量化布尔公式的Davis-Putnam过程中的部分隐式展开。在2001年的International Conference onLogic for Programming，Arti Ficial Intelligence and Reasoning（LPAR[13] W. J·萨维奇不确定性和确定性磁带复杂性之间的关系。计算机与系统科学杂志，1970年4月。[14] 维克多·舒潘和阿明·比尔。有限状态模型检验到可达性分析的有效简化。Software Tools for TechnologyTransfer（STTT），5（1-2）：185[15] M. Sheeran，S. 是的， 是的。 我的天啊。使用导入和SAT解决方案，可以轻松地进行配置。在Proc.FMCAD'00，LNCS的1954卷中。斯普林格。[16] L. J. Stockmeyer和A. R.迈耶需要指数时间的应用题。1973年，第五届ACM计算。[17] Daijue Tang，Yinlei Yu，Darsh Ranjan，and Sharad Malik.电路状态空间直径问题中量化布尔公式的可满足性的搜索算法分析。在Proc.SAT斯普林格。[18] G. S.蔡廷论命题演算中导子的复杂性。在建构数学和数理逻辑研究中，第二部分，数学研讨会第8卷。V.A.斯捷克洛夫数学研究所，1968年。
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
