有界模型检验的增量式满足性检验算法及有效性验证

理论计算机科学电子笔记119（2005）51-65www.elsevier.com/locate/entcs有界模型检验的一种增量式满足性检验算法Fabio Somenzi3科罗拉多大学博尔德摘要在Bounded Model Checking（BMC）中，对长度递增的反例的搜索被转化为一系列满足性（SAT）检查。 通过从一个实例转发在冲突分析期间学习的子句，尝试利用这些SAT实例的相似性是很自然的下一个提出的用于识别仍然有效的子句的方法分为两类：那些不注意生成SAT实例序列的机制的方法和那些依赖于它的方法。在BMC运行的情况下，Strichman [ 20 ]观察到，在一次SAT检查期间学习的那些仅依赖于模型结构的子句在检查更长的子句时仍然有效。E'en和Sorensson[9]指出，如果翻译成SAT遵守通常遵循的规则，则可以转发所有已学习的子句 许多条款，然而，以这种方式转发的数据几乎没有用处，并且可能降低性能。本文提出了一个扩展斯特里奇曼的方法的形式，一个更一般的标准，以过滤冲突条款，可以有利地转发到连续的实例。这一标准，特别是，仍然是句法和相当有效的，但帐户的存在，主要和辅助目标的SAT实例。 本文还介绍了一种技术，即使他们没有通过语法检查提取子句转发。蒸馏是一种语义方法，通常可以应用于增量SAT，并且经常产生独立于主要目标，因此对于实例序列的其余部分保持有效。此外，蒸馏通常可以提高子句的质量，即防止检查搜索空间的大区域的能力。 使用CirCU获得的实验结果 SAT求解器确认了所提出的技术的有效性，特别是对于大的，困难的问题。关键词：有界模型检查，命题可满足性，冲突学习子句，增量算法。1这项工作得到SRC合同2003-TJ-920的部分支持2 电子邮件：Jinh@Colorado.EDU3 电子邮件：Fabio@Colorado.EDU1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.06.06252H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）51K−KK1介绍Bounded Model Checking（BMC）[3]确定模型是否存在长度小于或等于k的属性k的反例。如果找到这样的反例，或者如果k足够大[19，18，6，1]，那么BMC有效地回答了问题K|否则，它增加了用户对K的正确性的信心。BMC将搜索某个最大长度的反例转换为一系列命题满足性（SAT）检查。在其最简单的形式中，长度从0开始，每个实例递增1。在此迭代的第i步，由以下公式构建命题公式：和 当且仅当存在一个长度为k=i1的反例。虽然这个方案的变化是很容易想象的，并可以容纳在本文中讨论的技术，我们将限制我们的讨论这种情况。每一个满足性检查的公式由三个部分组成，分别对应于初始状态约束、展开的转换关系和要满足的属性。在最后一部分，人们通常区分一个主要目标（例如，反例的最后状态违反不变量）从辅助目标（例如， 除了最后一个状态，没有状态违反该不变式）。辅助目标表达了从失败的寻找较短反例的尝试中收集到的关于问题的信息。他们可以帮助指导搜索过程。在过去的十年中，有效的SAT求解器的出现[21，25，26，11]极大地促进了BMC的成功。新一代SAT求解器在几个方面改进了经典的DPLL程序[8，7]。我们感兴趣的是冲突分析和小句记录：当发现一个冲突赋值时，分析它以识别仍然冲突的子集。子集中文字的否定的析取是一个冲突学习子句（或更简洁地说，冲突子句），可以将其添加到给定的SAT实例中，以防止检查搜索空间中保证不包含解的区域。并非所有的冲突子句都值得保留;许多SAT求解者会定期丢弃那些被证明无效的子句增量式SAT求解器[24，20，9]试图利用SAT实例序列的元素之间的相似性;大多数通过重新利用冲突子句来做到这一点，但是当必须解决许多密切相关的实例时，缓存解决方案[15]和增量翻译[2]也可以有效。如果一个SAT实例是通过添加一些子句从另一个SAT实例获得的（如[12]中所示），则第一个合同的所有冲突条款都可以转交给第二个合同。这是正确的，因为第二个例子意味着第一个，这反过来又意味着所有其（冲突）条款。因此，当子句仅通过实例序列添加时，不需要筛选冲突子句来确定H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）5153哪些可以转发。另一方面，当添加和减去任意子句以创建新实例时，这是必要的。对于这种一般情况，一种常见的方法是让增量SAT求解器跟踪冲突子句是否依赖于某些删除的子句。[24]的方法是为每个冲突子句记录组成相应蕴涵图的子句该方法不需要增量地求解后续SAT实例的任何先验知识，并且不限制从一个实例到下一个实例的可能改变;然而，跟踪依赖性可能是昂贵的。Strichman [20]是第一个观察到在BMC中，已知某些子句在序列中的所有实例中都存在。BMC传递给SAT求解器的公式包含描述模型多次展开的转换关系的子句。当反例的长度增加时，这些子句不会被丢弃。因此，可以转发仅依赖于它们的冲突条款。这种方法的优点是不再需要完整的依赖信息;每个子句一位标记就足够了。这样的标记是从产生该子句的蕴涵图因此，在这种情况下，我们说一个句法[9]的作者指出，如果只删除单元子句，则不需要跟踪依赖关系。这样的子句可以被SAT求解器视为假设。因此，冲突条款包含其假设或其某些隐含文字，并且在假设被废除时不会无效。在[9]中进一步观察到，将目标编码到SAT中的标准编码保证了当反例长度增加时必须删除的子句是单位子句。因此，所有的冲突条款都可以提交。[9]的方法举例说明了那些知道生成SAT实例序列的机制的增量满足性算法。另一方面，当其中一个单位条款的假设被颠倒时，冲突条款就被满足了，因此是无效的。在求解器中有许多惰性子句可能是一个很好的执行。因此，我们只想转发那些在连续实例中很有可能保持活动的子句。为此，我们提出了一个句法准则，它从两个方面改进了[20]中的准则首先，它考虑了辅助目标，因此可以转发更多的子句。其次，它不需要在标记一个合同条款。我们还提出了一个语义转发准则，将不能根据语法检查转发的子句提取为新实例所隐含的子句这些经过提炼的子句有时独立于54H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）51|¬¬新实例的目标，并且通常比它们所源自的原始子句更有效地防止搜索空间的无效区域的探索。本文的其余部分组织如下。第2节审查背景材料。第3节描述了增量SAT算法，而第4节讨论了进行实验，以评估其有效性。第5节结论。2预赛令V ={v1，...，v n}且W ={w1，...，w m}是布尔变量的集合。我们将集合{v1J， . ，vnJ}，由V的元素的素数版本组成，并且通过V i，集合{vi，.，v i}。同样地，W i={W i，. w i}。 1n1m一个开放系统是一个4元组=其中V是（当前）状态变量的集合，W是组合变量的集合，I（V）是初始状态谓词，T（V，W，VJ）是转换关系。VJ中的变量是下一个状态变量。 所有的集合都是有限的，所有的变量都在有限域上变化有界模型检验（BMC）[3]将对反例的搜索减少到线性时间属性，以满足命题。给定一个开放系统，一个LTL公式和一个界限k，BMC试图通过证明长度为k的证明LTL公式的否定来反驳=BMC生成一个命题公式[[k，< $k]]k，当且仅当在k中存在一个长度为k的对k的反例时，该命题公式是满足的; [[k，<$k]]k定义如下：[[，<$]]k=I（V0）0≤i kT（Vi，Wi，Vi+1）]]k，（1）其中，[<$]] k表示<$在这条路径上的满足（有关翻译的详细信息，请参见[ 3 ]）。习惯上把[<$k]] k写成ω k<$F k，其中ω k是一个称为主要目标的文字。如果已知[[，]]j对于j k是不满足的，那么可以将（1）与0≤i k] i.（二）每个项<$[[<$$>]]i被写作<$ωi<$Fi，其中<$ωi是辅助目标。H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）5155{≤}1数字锁相环2而（C HOOSE N EXT A SIGNMENT（））3而（DEDUCE（）== CONFLICT）4blevel =ANALYZE CONFLICT（）;5if（0） returnUnsatisfiable;6elseBACKTRACK（blevel）; 78返回满意; 9}Fig. 1. 一种带冲突分析的SAT求解器将赋值返回给满足它的命题公式的变量，如果这样的赋值存在的话。一个文字是一个变量或它的补语，一个子句是一个从不同变量的文字的析取，一个合取范式（CNF）公式是一个子句的合取。与反相图（英语：And Inverter Graph，AIG）[16]是一个布尔电路，每个节点的输 出是 其 两 个输 入 的合 取 。 电 路的 弧 可以 是 互 补的 。 二进 制 决 策图（Binary Decision Diagram，BDD）[5]是一种布尔电路，每个节点都是一个由输入变量控制的多路复用器。大多数SAT求解器在CNF中的命题公式上操作。另一方面，我们的SAT求解器Cir-CU [14，13]接受CNF子句、AIG和简化有序BDD的组合。冲突分析的每个结果都表示为一个子句[10]。 因此，本文中描述的算法可以应用于任何SAT求解器的子句记录的基础上图1显示了在大多数现代SAT解算器（包括CirCU）中实现的DPLL过程的伪代码。该算法维护一个赋值列表，该列表使用来自SAT实例的unit子句进行初始化。如果所有的变量都被赋予了一个值，那么就找到了一个令人满意的赋值集。否则，就从列表中提取一个赋值，或者由一个新的决策创建一个赋值;它被添加到赋值堆栈中，并推导出它的结果。每次做出新决策时，决策级别（最初为0）递增。如果检测到冲突，则对其进行分析。分析的结果是一个冲突子句和一个回溯决策层。后者告诉在继续搜索之前应该擦除多少赋值堆栈（降低决策级别）。冲突分析依赖于蕴涵图，蕴涵图是一个有向无环图（DAG），其节点是当前赋值集合中的变量加上一个特殊的冲突节点（如果赋值是冲突的）。DAG的弧是这样的，如果节点ν的前导是ν1，.，ν m，则存在子句、AIG节点或BDD，使得它在给定ν 1，.的值的情况下暗示ν的值，vm.冲突节点的前置节点标识子句、AIG节点或BDD，其赋值不一致。图的根对应于决策分配。请注意，不同的蕴涵图可以从同一组赋值中获得，这取决于{56H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）51¬ ∨∧其含义传播的顺序。通过分离文字的否定来获得冲突子句，该文字在蕴涵图中形成切割第一唯一蕴涵点（UIP）方法[26]从冲突节点开始，寻找第一个切割，使其包含最近决策所暗示的一个文字。蕴涵图的每个非根节点都标识一个先行子句：节点的隐含值提供一个文字，而对先行值的求反提供其他文字。这些子句中的一些子句对应于输入描述中的子句或从先前的冲突中导出其他人来自AIG节点或BDD。例如，AIG节点a=b c，并且赋值a= 1意味着c= 1隐式地给出子句（a c）。通过从与冲突节点相关联的冲突子句开始的连续解析来获得冲突子句。在每一步中，使用其先行子句解析当前决策级别中隐含的一个文字。决议中涉及的所有条款都隐含在正在检查其可满足性的函数中。3转发条款我们考虑一个增量SAT算法，利用SAT实例之间的相似性我们假设序列的第二个和连续的实例是通过从紧接在它们之前的实例中删除一些子句，然后添加一些其他子句而获得的。在BMC中，SAT问题的不满足性通常来自于路径的初始和最终状态的同时约束，因为表示展开的转移关系的公式和初始状态通常是令人满意的。然而，这并不意味着求解器在证明不满意性时所经历的冲突涉及大多数时间框架的变量。首先，由于对某些电路元件的输入和输出的不一致分配，可能存在冲突。其次，不满足性的证明可能依赖于建立关于可能反例的中间状态的非平凡事实的冲突，给定初始状态的约束。图2提供了局部冲突如何产生的一些直观信息。 它显示了通过展开两次转换关系产生的AIG。被检查的属性是不变量。图中的三个部分是在搜索过程中拍摄的三个快照。 每个圆圈都是AIG的一个节点。如果节点被赋值，则圆被填充这三张照片显示H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）5157图二. 正义云蕴涵图最初由几个连通的部分组成。如果在扩展其中一个不包括目标的组件（最右边的菱形）时发生冲突，则由此产生的冲突条款完全独立于当前目标，是转发的良好候选。如第1节所述，在[9]中指出，当目标由文字标识时，所有冲突子句都可以转发。然而，一个包含旧的主要目标的条款，当该目标58H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）51x9@0€x7@0€x8@0x1@1x1@1€x5@3x6@3联系我们€x2@1x3@3x4@2x4@2(a)（b）第（1）款图三. 跟踪目标示例通过否定它的字面意义变成助动词。一般来说，依赖于主要目的的冲突条款的有用性是值得怀疑的，即使它们不包含客观的字面意思。因此，在下文中，我们提出两种技术来识别客观独立子句。3.1目标追踪我们有兴趣扩展[20]的标准来解释辅助目标，因为它们有助于许多冲突，特别是在寻找循环反例时。定义3.1设[<$k]k=ωk<$Fk。一个冲突子句γ是目标依赖的，如果ωk是蕴涵图中冲突节点的祖先，或者至少有一个目标依赖子句用于其归结。否则，γ是客观独立的。我们在图3中展示了一个AIG及其含义图。图3（a）中的每条横线代表一个AIG节点;点代表完整的心理状态目标是x9，在对x1、x4和x3做出三个决定后，就会发生冲突。随着影响，我们还通过蕴涵图传播的目标的标记。例如，我们标记x7和x8，因为它们是目标所暗示的。图3（b）中的虚线包围了标记的节点。在我们的增量算法中，冲突分析具有额外的目标，以检查冲突是否与目标相关。 图中的冲突-第3步是目标相关的，因为冲突节点的祖先之一是x9。一种简单的方法可以通过检查€x7@0x9@0€x2@1€x8@0连续记录x3@3€x5@3H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）5159目标是否在冲突节点的传递扇中。然而，大多数现代SAT求解器，包括CircCU，使用第一个UIP来找到冲突的简明解释。因此，标准的冲突分析不需要遍历冲突节点的所有传递扇。因此，朴素的方法可能招致开销。由于我们在蕴涵过程中传播了目标标记，我们可以通过检查冲突节点的标记来检查冲突是否与目标相关如果冲突节点没有被标记，那么我们需要遍历蕴涵图来检查对象依赖冲突子句是否是当前冲突的原因然而，我们只遍历直到找到第一个UIP为止，即使蕴涵图的其余部分具有对象依赖的冲突子句，它们也可以被忽略。第一个UIP将冲突原因与这些条款隔离开来。在[20]中，作者提出了一种仅基于电路结构来识别要在BMC中转发的冲突子句的方法。首先，标记从电路结构创建的所有子句。一旦发生冲突，检查是否所有导致冲突的条款都被标记。因此，该冲突源自电流分配与电路结构之间的不一致。因此，该合同被标记为转发。这种方法没有考虑辅助目标，如第4节所示，辅助目标通常会加速BMC。其次，当BMC应用于优化电路时，其中大多数冗余已经被去除，仅从电路结构导出的子句往往很少。这发生在我们的实验设置中，因为我们应用BDD扫描[16]来去除冗余。3.2蒸馏虽然3.1节的标准比[20]的标准向前提出了更多的条款，但它仍然相当保守，可能会遗漏许多有用的冲突条款。因此，在本节中，我们开发了一个语义标准，应用于基于对目标的依赖而未通过句法检查的小子句。为了在新目标下提取一个子句，我们检查该子句是否在新SAT实例的单元子句所隐含的赋值下得到满足。如果满足该子句，则丢弃该子句。否则，我们断言其字面量的否定并执行由此产生的含义。如果这不会导致冲突，则丢弃该子句。（因此，当并非所有子句都可以转发时，也可以应用蒸馏。）否则，通过冲突分析获得的子句是给定子句的提炼版本并被转发。即使我们限制了候选子句中的文字数量，60H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）51∨ ∨ ¬∨∨ ∨ ¬ ∨∨（abc）（a bc）（<$af）（ag）（ah）见图4。以Trie子句为例。每个节点有两组子节点，对应于每个变量的两个字面值。可能还有很多人 因此，我们建立一个trie（参见）。[25]与集的候选人。图4显示了一个示例。使用trie，我们可以提取最多7个决策的子句，而不是逐个处理子句所需的12个决策。当子句可以合并时，我们不显式优化trie。在图4中，（abc）和（a）BC.可能是合并为（a b）。如果新条款确实引起了冲突，在尝试（a b）时会发现（c）。trie的大小取决于变量的顺序。 我们根据变量在候选分句中出现的次数对变量进行排序。图5显示了蒸馏算法。对于trie中的每个元素，如果存在以下情况，则在Distillation A ux（）中对子元素“0”和“1”进行决策：是一个非空的后缀。当BCP（）导致冲突时，调用冲突分析。如果产生的冲突子句的文字数少于从根开始的路径上的trie节点数，则将其转发。否则，将根据已作出的决定提交冲突条款。前一种情况更为常见。由于我们想一个接一个地遍历所有的trie节点，所以我们使用基于trie结构的时间回溯。蒸馏过程有几个优点。首先，它是一种语义方法，可以导出先前SAT检查未产生的子句。其次，这些子句中的一些是可重用的，因为它们不依赖于当前目标。 由于基于追踪目标的标准是保守的，我们经常从前一次运行的目标依赖子句中发现许多目标独立子句。第三，合同条款的质量通常通过提炼来提高。这部分是由于赋值的顺序不同，这是由于trie的遍历。此外，第一个UIP往往比它所替换的要提取的子句中10F10G10H根一 01B01C01H. Jin，F.Somenzi/Electronic Notes in Theoretical Computer Science 119（2005）5161}{{1D蒸馏（Trie）{2对于Trie中的每个t{3if（V）value（t.node）！=X）{4DISTILLATION（t.child[VVALUE（（t.node）]）;5继续;（六）7D蒸馏AUX（t，0）;8D蒸馏 AUX（t，1）; 9101112INTMAXIMUM（t，value）{13if（t.child[value]）14level=基于TRIE（t.node，value）的决策;15如果（BCP（level）==冲突）16conflict=CONFLICTANALYSIS（level）;17if（NUMLITERALS（conflictClause）

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