增量式满足性检验算法在有界模型检验中的应用

有界模型检验的增量式满足性检验算法及有效性验证 有界模型检验（Bounded Model Checking，BMC）是一种形式验证方法，用于检查模型是否满足一定的性质。该方法通过将模型转换为布尔可满足性（Satisfiability，SAT）问题来实现。然而，在BMC中，对长度递增的反例的搜索被转化为一系列满足性（SAT）检查。为提高搜索效率，需要开发出高效的搜索算法。 为解决该问题，本文提出了一种增量式满足性检验算法。该算法通过学习从一个实例转发在冲突分析期间学习的子句，尝试利用这些SAT实例的相似性来提高搜索效率。该算法分为两类：不注意生成SAT实例序列的机制的方法和那些依赖于它的方法。 在BMC运行的情况下，Strichman观察到，在一次SAT检查期间学习的那些仅依赖于模型结构的子句在检查更长的子句时仍然有效。E'en和Sorensson指出，如果翻译成SAT遵守通常遵循的规则，则可以转发所有已学习的子句许多条款，然而，以这种方式转发的数据几乎没有用处，并且可能降低性能。 本文提出了一个扩展斯特里奇曼的方法的形式，一个更一般的标准，以过滤冲突条款，可以有利地转发到连续的实例。这一标准，特别是，仍然是句法和相当有效的，但帐户的存在，主要和辅助目标的SAT实例。 此外，本文还介绍了一种技术，即使他们没有通过语法检查提取子句转发。蒸馏是一种语义方法，通常可以应用于增量SAT，并且经常产生独立于主要目标，因此对于实例序列的其余部分保持有效。此外，蒸馏通常可以提高子句的质量，即防止检查搜索空间的大区域的能力。 使用CirCU获得的实验结果SAT求解器确认了所提出的技术的有效性，特别是对于大的、困难的问题。 有界模型检验的增量式满足性检验算法的有效性验证是通过实验结果来确认的。实验结果表明，该算法可以提高搜索效率和解决问题的能力。此外，该算法还可以应用于其他形式验证方法，例如模型检查和形式验证等领域。 有界模型检验的增量式满足性检验算法是一种高效的搜索算法，可以应用于形式验证和模型检查等领域，以提高搜索效率和解决问题的能力。