Basic formal verification algorithms 形式验证基本算法 第2章

本章将将介绍形式验证工具中使用的算法类型的一般概念，以及一些术语的介绍。形式验证提供了完整的行为覆盖，而无需进行详尽的仿真。

一、验证过程中的形式验证（FV）

验证的三个中心任务是激励设计，检查设计是否根据其规格产生结果，以及衡量设计的可执行空间有多少已被仿真和检查（覆盖率）。在制造器件之前，验证通常通过运行寄存器传输级（RTL）模型的仿真来完成。

即使对于比较简单的设计，可能的不同输入激励序列的数量似乎是无限的，实际上是可能输入的大小、启动状态和运行时间的指数函数，但出于实际目的，这似乎是无限的。有了仿真等硬件支持，仿真可以大大加快，但对所有可能情况进行商业设计所需的时间仍将远超过产品的使用寿命。因此通过仿真不可能实现所有可能的执行序列的完全覆盖，并且覆盖目标被仔细设置为包括特征条件的良好表示以及关键和繁重的场景，以发现大多数但不是所有的错误。达到覆盖目标本身并不是最终目的，但收集的信息是在未执行的设计目标方面帮助验证人员。

FV技术不是检查每个独特的序列，而是建立一个数据结构，捕捉所有可能激励序列的结果（指的是信号可以取的所有值都可以进行全验证，而不是像仿真那样构造某种特定的激励去验证逻辑是否满足规格书）；根据此结构检查属性，然后根据所有可能的激励验证所需的属性。这种检查可以发现深度复杂的错误，使用传统的激励生成技术很难找到这些错误。

本章将讨论如何使用形式化模型检查实现是否满足其需求，包括对两种不同技术的基础数学的讨论：二进制决策图（BDD）和SAT。

1、一个简单的自动售货机示例

下面是一个小例子展示了如何使用一个巧妙的数据结构，将一个看似指数级的复杂问题转化为更容易处理的问题。

布尔逻辑通常通过真值表来表示，真值表根据每个输入来描述系统的预期输出值。可以使用真值表来定义具有多个激励参数和多个结果的函数或系统。下面的真值表描述了简单ADD操作（表2.1）

随着激励的增加，真值表的大小迅速增加：每增加一列输入，就将新的可能激励值的行数增加一倍。例如，定义MUX操作所需的行数是2位ADD的两倍（表2.2）：

这意味着n个输入的真值表将有行；这种指数式的增长的设计很难用简单的工具和技术进行分析。

许多FV算法利用了一个关键的洞察力来缓解这个问题：在实际中，这样的真值表在信息内容上往往非常稀疏，因为许多行产生0值，而许多行产生相同的值。

例如，为一个简单的自动售货机真值表制定一个规范，该表可以确定35美分是否已存入。要求机器只接受由五分硬币（5美分）、一角硬币（10美分）或25美分组成的精确零钱。自动售货机应接受的合法输入如下：

• 25美分、10美分

• 25美分、两个10美分

• 三个10美分、一个5美分

• 两个10美分、三个5美分

• 一个10美分、五个5美分

• 七个5美分

对于这六种情况，真值表结果应为1，否则应为0。为了随时跟踪可能的输入，我们需要六位：

• 1位表示跟踪已输入多少个25美分（0或1）；

• 2位表示跟踪已输入多少个10美分（0-3）；

• 3位表示跟踪已输入多少个5美分（0-7）

要写出一个完整的真值表，需要64行（），但只有6行会产生1个结果，如果在自动售货机规范中允许使用硬币，需要再增加六位才能数到35便士，那么表格将增加到4096行（212），但只有18个有效的输入组合—— 一个非常稀疏的表格。

可以选择只显示结果为1的输入行的表，而不是枚举所有行。在表2.3中，为自动售货机示例提供了这样的简化表

有许多其他最小化技术和其他heuristics 方法可以有效地处理布尔公式（ formulas）。关键点是：通过巧妙选择算法和数据结构，布尔函数通常可以以紧凑高效的方式表示和分析，而布尔函数似乎需要处理指数级的不同情况。

二、比较规格

验证设计时需要比较两种规格；一个捕获设计需求（“specification”），一个捕获实现细节（“implementation”）。specification通常比implementation更抽象，描述的是预期结果，而不是实现逻辑是如何连接在一起的。specification通常是一组属性的形式，如SystemVerilog Assertions SVA）断言、RTL模型或SystemC之类的高级语言中的模型。implementation通常是更详细的RTL模型或简图网表；抽象差距比较小时，通常使用形式化技术来比较两种不同的implementation的等价性，例如在项目的小错误修复之后。

首先深入了解FV工具如何完成其任务的，在图2.1中，方框A和B表示接收相同输入并由检查器（checker）比较其输出的specification。

如果检查器记录了导致fail的输入序列，则检查器可以提供反例（counterexample ）跟踪，以证明A和B不等价。

这是一个黑盒检查器，因为检查器不观察A和B内部的状态或信号值，尽管黑盒检查器的可见性较低，但其定义不受内部变化的影响，因此维护成本低于白盒检查器。

如果A和B足够简单，能够测试所有可能的序列，或者使用FV来显示两个框产生等效的结果，然后可以使用这个等价证明来简化其他问题。例如，考虑图中A和B是较大系统的组件（图2.2）。

在这个例子中，如果已经证明了A和B是等价的，那么可以删除A和B，并解决一个更简单的问题，即证明C和D是等价的。在修改后的场景中C和D的输入不同，在下图中标记为“输入”。如果确定输入“应该是什么”具有挑战性，则保留一份接受输入并产生输入的A（或B）复制可能更方便。

通过使用分而治之的策略，通常可以对比使用FV工具进行本地验证更大的设计进行验证（图2.3）。

图中的顶部框是需求规范，底部框是实现规范，当两个规范具有同等的细节程度时，使用一个简单的检查器来比较输出流，能够验证这两种规范。

上图是一种形式等价验证（FEV），这两种规格并不完全相同。需求specification是implementation的抽象视图，省略了许多细节。

1. 影响锥（COI）

coi就是影响property结果的所有驱动（driver），追到PI或者undriver这样的free variable为止，中间出现的信号都属于coi。

如果单独考虑垂直（orthogonal ）需求，则可以降低验证复杂性。例如，如果设计包括加法和乘法硬件，则可以使用不同的仿真运行来关注不同的操作。

如果设计中有单独的单元执行这两个操作，则在仿真中仅包括验证目标操作所需的设计部分将更有效。通常创建一个验证环境比为每个操作创建一个更有效。

FV工具分析要验证的属性，从implementation中删除对属性描述的结果没有影响的任何逻辑，减少coi。如图2.4中所示，有几个框可以从设计中删除，因为它们在结果计算中不起作用。在大型设计中，这将大大减少所考虑的逻辑量。

三、形式操作定义

在需求或实现规范中，我对输入、输出和状态元素使用布尔变量，这些变量可能会随着时间的推移保持不同的值。最初假设这些变量可以采用二进制值（0或1），可以添加"x" 来表示不知道该值是0还是1。一般0也被解释为表示低/关/假，1被解释为代表高/开/真。值或值组合的操作可以用真值表来描述，结果（输出和下一状态）是激励参数（输入和当前状态）的函数。

1. 智能地构建真值表

正如前面自动售货机示例，可以利用实际数据的稀疏性来生成更紧凑的真值表表示，不需要重复表示相同或零结果的行，在实践中使用比naı¨ve指数计算所建议的更少的行。

2、添加顺序逻辑

真值表可以捕获具有序列逻辑的系统，模型可以通过添加输入激励和输出结果列来表示变量的当前和下一个状态，以存储随时间变化的状态信息。

使用了两个变量，可以为它们提供相同的名称，并在后续状态变量中添加后缀记号（'）。加法器在每个周期将新的输入值添加到其当前和（表2.4）。

四、布尔代数表示法

虽然可以使用真值表来指定组合多种操作的行为，但使用布尔代数将这些操作写成公式要方便得多。将用单字母名称表示变量，偶尔用下标表示。如上所述，当变量是状态变量时，可以使用记号（'）后缀来指示后续状态。

还将使用其他协议来最小化对符号和括号的需要。NOT操作具有最高优先级，然后是AND运算符。作为一个具体的例子，考虑下面的MUX实现（图2.5）：

引入中间变量a、b和c作为不同门的输出，并可以将实现描述为一组公式：

a == !y
b == x && y
c == a && z
result == b || c

上述四个公式均为真的全局声明，表示设计的实现。可以通过将中间变量的定义代入最终方程来简化连接：将a代入c（c==y&&z）的定义，然后将b和c的定义代入结果。这将整个公式简化为（表2.5）：

result == (x && y) || (!y && z)

(q0 && d0 && !d1 && !n0 && !n1 && !n2) ||
(q0 && !d0 && !d1 && !n0 && n1 && !n2) ||
(!q0 && d0 && d1 && n0 && !n1 && !n2) ||
(!q0 && !d0 && d1 && n0 && n1 && !n2) ||
(!q0 && d0 && !d1 && n0 && !n1 && n2) ||
(!q0 && !d0 && !d1 && n0 && n1 && n2)

上面这种结构的公式被称为disjunctive normal form （DNF）。

这种公式由一组“或”（disjunction）的子组组成，每个子组仅由一组“与”（conjunction）的变量或它的否组成。由于AND类似于乘法，OR类似于加法，所以也称为乘积和形式。

以这种方式从真值表构造公式可以很容易实现自动化，且对构建FV工具非常有用。但在进行此类重写时必须谨慎，因为生成的公式可能比计算所需结果更复杂。例如，图2.2中的小电路示例的结果定义为：

(x && y) || (!y && z)

但通过捕获真值表（表2.5）中求值为1的行来直接构建DNF时：

(!x && !y && z) || (x && !y && z) || (x && y && !z) || (x && y && z)

1、基本布尔代数定律

这些定律可以通过观察先前给出的真值表或编写新的真值来确认。FV引擎可以利用这些定律将布尔公式快速改写为更方便的形式进行分析（表2.6）。

2、比较规格

为了证明一个 implementation满足其要求，需要证明该implementation隐含了规格：

implementation-requirements

如果要求两者精确等价（对所有可能的输入序列产生相同的结果），那么也需要显示相反的情况：

requirements-implementation

使用基本的布尔代数规则，可以重写公式以表明两个implementation产生了等价的结果。例如，MUX的替代实现（图2.6）

可以用公式定义实现：!(!(x&&y)&&!(!x&&z) 。为了证明此implementation产生与原始implementation相同的结果，可以应用布尔代数规则将公式重写为等价公式，

• 应用德摩根定律，产生：!!(x&&y) || !!(!x&&z)

• 删除双NOT操作，产生：(x&&y)||(!x&&z)

!(!(x&&y)&&!(!x&&z) ==(x&&y)||(!x&&z) ，可以将其添加到重写规则列表中，以便将来进行简化。MUX2设计规范：

(x&&y) || (!x&&z)

与第一个MUX设计定义不同：

(x&&y) || (!y&&z)

这种差异可以进行一些关键观察。公式中的变量x、y和z实际上是计算中使用的实际输入值的占位符（或形式），使用更好的形式表示法使其更清晰，可以将MUX和MUX2重新表述为：

MUX(x,y,z) = (x&&y)||(!y&&z)
MUX2(y,x,z) = (x&&y)||(!x&&z)

作为占位符，可以重命名输入变量，而不影响函数计算的值。如果重命名每个公式中的第一个变量a和第二个变量b，并应用交换律，可以看到这两个定义确实匹配。

虽然两个implementation都可以执行相同的功能，如果没有正确连接输入，无法简单地用一个替换另一个，抖动（swizzling）输入位的错误可能难以检测。

在这个简单的MUX示例中，许多输入即使不能如上所述重新标记输入，在大多数情况下也会产生正确的结果。只有在两种输入激励模式下，才会检测到错误的连接（表2.7）。

自动重写过程（Automated rewriting procedures ）可用于小型数字电路问题，可以找到一系列变换以降低公式的复杂度，并可以用来证明两个公式是等价的。

对于大型问题，真值表和布尔代数公式对于自动化程序来说都变得很难处理，即使在人工指导下也很困难。

为了解决大型问题，后面会介绍BDDs和SAT公式。

五、BDDs

BDD提供了一种以二进制决策树的形式表示许多电路行为的紧凑方法。

在前面示例真值表中观察到的，通常存在大量冗余：35美分自动售货机真值表的许多行是0。BDD提供了一种结构：在保留原始设计行为的同时消除这种冗余。

如果应用一组标准化规则，将构造一个唯一的BDD，这样任何其他等效设计都具有相同的BDD表示，而无需任何重写。FV工具可以通过将两个公式转换为BDD形式并检查BDD是否相同，来测试两个公式之间的等价性。

图2.7是MUX的BDD示例，要查找特定输入模式的结果，如果变量在模式中为0，则跟随变量节点的左分支，如果变量为1，则跟随右分支。

在当前的形式中，并没有比真值表存在更大的存储优势，因为仍然在直接表示所有指数级的潜在执行路径。消除许多冗余可以最小化尺寸，因此删除底部行中所有冗余的0和1终端节点。（图2.8）

观察树左侧的两个z节点所做的决定是相同的，因此父y节点不会影响结果。同样在树的右侧，z节点是不必要的。可以合并这些节点集得到更紧凑的表示，如下所示（图2.9）：

BDD大小的关键是将变量添加到树中的顺序。原始MUX被方便地定义，以便提供合理的自然排序。

如果交换顺序，将变量添加到z，然后x，然后y，函数保持不变，会生成以下BDD（图2.10）。

新的BDD并不十分复杂（毕竟只是一个MUX），但添加了两个额外的节点（大小增加了66%）。对于更复杂的电路，BDD的大小可以根据变量的顺序呈指数增长。基于启发式的算法更善于找到更好的顺序（重新排序），以减少BDD的大小。

例如，在很多情况下，将变量的顺序与被分析电路的拓扑结构匹配是一种非常好的策略，可以利用电路关于逻辑密切相关节点的线索。

另一个通常强大的启发式方法是尝试为每个PI（ primary input）替换0和1值，并查看哪些情况显著减少了评估模型所需的总逻辑：这种情况指示应该接近BDD树顶部的变量。

BDD排序问题是NP完全的（ NP-complete ）。对于大型复杂操作，在最坏的情况下，找到一个好的BDD排序仍然需要指数时间。在实践中，有很多情况下FV工具可以有效地为很大的布尔函数构造BDD。

1、计算电路设计的BDD

如果有一个设计和规格的真值表，可以立即创建BDD，执行简化步骤，并证明设计和规格匹配。然而，很少有规格或设计被表达为真值表：特别是在芯片设计领域，更可能以RTL模型的形式呈现。

从一个电路开始，可以通过一次添加一个逻辑操作，模仿输入模型的结构来建立BDD。当电路被表示为一组布尔代数公式时，可以应用定律和定理来最小化其表达式。

表示AND、OR和NOT门的基本BDD（图2.11）。

为了从电路中创建BDD，可以使用这些通用形式来逐步构建更复杂的BDD，一次一个门。

例如，考虑公式（x&&y）||z，如图2.12所示

可以通过替换通用and BDD中a的x和b的y来构造电路的BDD，并移植其0和1弧来替换OR BDD的a节点弧，同时替换b的z。

下图左侧显示了移植，右侧显示了组成。这个过程可以迭代，直到电路中的所有门添加到BDD中（图2.13）。

如果比较组合逻辑的两种不同实现，可以评估当设计具有相等数量的输入和输出（包括状态）时，它们是否计算相同的结果。specification 往往更抽象，故不会有严格的等价性。而且specification通常根据系统在一段时间内的行为来描述系统，而不是逐步的行为。

2、模型检查（MODEL CHECKING ）

模型检查是FV工具用来分析一段时序系统行为的技术。给定一组定义为时序逻辑属性和有限状态系统的需求，模型检查算法搜索可能的状态并确定是否违反了属性。

搜索首先为初始态创建一个状态空间BDD，其中所有变量都可以是任何值，除非提供了显式约束。使用系统转换（编码为BDD），扩展状态空间BDD以包括所有可能的下一个状态。这个过程（称为reachability）可以重复，直到所有可能的状态都添加到BDD。

虽然无法预测该过程需要重复多少次，但当没有新状态添加到状态BDD时，就达到了一个固定点（fixed point ）。这已经分析了一组完整的可能行为：将转换进一步应用于任何现有状态都不会产生要添加的新状态。

在检测到反例时，模型检查器从反例阶段向后返回到初始条件，以创建如何达到不好的状态的具体示例。可能有许多不同的路径可以达到反例状态。模型检查器通常返回的最短路径，尽管有些可以提供多个路径或其他提示来帮助解决问题的根源。

模型检查器可以返回满足specification 的结果，返回反例或者由于计算爆炸而不提供结果，工具超时或生成BDD，会耗尽所有可用内存。

虽然BDD提供了一种全面检查设计是否符合其规范的方法，但在检查设计的大小方面存在实际限制。BDD模型可以随着每个额外的输入或状态元素呈指数增长。

通过对变量的仔细排序，BDD在许多情况下都可以被驯服。对于很大的设计，时间和空间的放大通常需要人工努力或使用更先进的启发式方法来应用案例分割（把规模很大的设计分割成比较小的、容易分析的多个部分）、假设保证推理或使用简化的假设来获得结果，这样的策略通常可以将指数增长转化为一组可以适应可用空间的小问题。

六、布尔可满足性

现在介绍新的技术：能为所有问题提供完全覆盖的保证，其好处是更快地提供反例，并以更自动化的方式适用于更大的设计。

大设计在最坏的情况下很难证明，但很多启发式方法通常可以在单元级设计的合理时间内解决SAT。

为了更好地理解SAT，希望以下规范能显示实现满足要求：

implementation = !(!a&&c || a&&!b)
requirement = !a&&!c || b&c

这可以表述为确定语句是否为冗余：在赘述中，对于任何输入，公式的计算结果都为真。

!(!a&&c || a&&!b) -> !a&&!c || b&c

使用蕴涵符的定义（p->q定义为！p||q）重写，此公式可以写成：

(!a&&c || a&&!b) || (!a&&!c || b&&c)

为了证明公式冗余，可以构造一个真值表。可以计算八种可能的输入模式中每一种的结果，任何0的行都将被标记为错误。为了快速发现bug，因此最好将解决方案重新集中在：搜索implementation不满足其要求的变量分配问题。

这是经典SAT问题的本质。对于寻找反例的具体目标，可以将目标表述为寻找变量赋值：

!(implementation -> specification)

如果找不到赋值，那么可以断定implementation 满足specification。

1、有界模型检查

基于BDD的技术逐步构建设计所有可能的下一个状态，直到结构包含所有可能的未来结果时，到达固定点。

算法可以计算在任何可到达状态中是否违反了要求。SAT检查通过迭代构建一个表达式来描述从设计状态开始的所有可能的执行路径，并同时检查每个步骤是否满足要求。最终要么找到反例，要么指数级增长，FV引擎无法再确定当前步骤是否满足要求。动态检查可以在指数膨胀成为问题之前尽早发现反例。

前面的需求定义的设计，修改了c变量是一个状态元素。使用未来值的启动符号，新设计可以用以下表达式表示：

c’ = !a&&!c || b&&c

在简化的（忽略寄存器计时）图2.14中。

为了扩展表达式以捕获可以在两个步骤中分配给变量的值，需要为下一个状态添加新版本的公式，其中包含a、b和c的新变量。新添加的表达式：

c’’ = !a’&&!c’ || b’&&c’

预处理变量a’和b’表示到达第二步的输入，c'’表示第二次计算后将存储的状态。

重复此过程，添加新的变量，直到SAT求解器耗尽时间或空间，并断言需求已满足特定的边界（bound），即最后一次成功扩展，或在某一点上确定产生目标公式反例。这个边界（bound）就是设计执行步骤的数量（这个步骤就是从给定的开始状态到满足需求的过程）。

如果SAT引擎达到n的边界，表示复位后n个周期内所有可能的设计的执行都已被分析，这相当于运行指数级的仿真。

每一步需要越来越多的时间来计算，因此通常使用最大边界参数来运行求解器。在证明达到指定的界限后，引擎认为它“足够好”并结束分析。所达到的界限是否足以满足验证要求是一个重要的问题，后面的章节会介绍。

SAT求解器比纯BDD引擎需要更少的内存，并且可以检查更大的模型。而且还不需要良好的BDD变量排序。SAT的缺点是：不能计算固定点来判断是否已经覆盖了所有可能的执行序列。在某些情况下，SAT技术可以涵盖所有可能的行为，但这不是常态。

在早期验证阶段的操作目标通常是快速发现错误或分析可能的行为，因此使用基于SAT的技术比使用BDD技术更好。

2、解决SAT问题

试图用尽可能少的计算找到一个变量赋值以产生反例的例子。为了使计算最小化，最好将问题划分为更简单的子问题来构造问题。

理想情况下，将其构造为多个项的AND，可以通过显示只有一个项求值为0，来确定变量赋值使整个公式为0。许多SAT算法使用这种方法，使它们能够快速确定一个大公式为0，而不必检查每个项。

给定一个conjunctive normal form 的布尔逻辑公式，SAT问题要求为每个变量找到一个赋值，从而使结果为1。如果存在这样的赋值，则公式是可满足的，如果不存在赋值，则该公式是不可满足的。

如果公式和子句（clauses ）结合，其中每个子句都是变量或变量反的OR，则公式为conjunctive normal form（CNF）。这种形式被称为和的乘积形式，再次将AND视为类乘法，将OR视为类加法。例如：

(a||b||!d)&&(!b||c)&&(a||c)

任何布尔逻辑公式都可以转换为CNF，尽管CNF公式可能大于原始公式。这种形式的优点是有很多项的“and”，这表示只需要显示有一个项为0就可以使其fail，如上所述。

从RTL形式构造CNF公式很简单，对于每个门需要定义输入和输出之间的关系。例如，考虑输入为a和b，输出为c的或门。对c的要求是，如果a或b为1，则c为1。此外，当a和b都为低时，c为0。这可以通过以下要求来实现：

a -> c
b -> c
!(a || b) -> !c

使用蕴含操作符的定义重写，得到CNF公式：

(!a||c)&&(!b||c)&&(a||b||!c)

电路定义可以通过为新的门添加额外的连接，并通过使用公共变量名将一个门的输出与下一个门输入相关联来构造。

为了找到变量的赋值，可以构造一个真值表并检查每个可能性。对于前面的示例，可以尝试分配以a = 0、b = 0、c = 0、d = 0开头的变量值。但这些赋值会产生一个0，依此类推。解决方案a = 0，b = 0，c = 0，d = 1也不起作用。故在找到解决方案之前，或在最坏的情况下，已经用尽了所有16（）种可能性。

随着变量数量的增加，解决问题所需的时间变得更长。坏消息是没有一种算法能够有效地为所有可能的公式提供解决方案。好消息是这个问题已经得到了很多关注，并且有许多已知的策略可以很好地解决相当大的问题。

好的SAT策略不是简单地列举和测试案例的指数数量，而是利用以下见解：

• 分而治之：尝试解决多个较小的问题.

• 从错误中吸取教训（或避免错误）：在后期利用早期失败中的信息.

• 优化重要内容：确定要解决的关键问题.

• 领域特定知识：使用现实RTL设计的已知特征

3、DAVIS-PUTNAM-SAT算法

与其为真值表中所有变量的每个可能赋值重复计算，更好的策略是仅评估一次每个变量的赋值，并衍生出两个子问题：一个是通过用值1替换变量而简化的公式，另一个是用值0替换变量。

对每个变量重复这个过程，如果在最后，一个子问题将公式求值为1，得到有一组赋值，表明公式是可满足的。如果所有子问题的公式求值结果为0，则公式不可满足。下面是算法的概述：

SATDivide&Conquer(formula)
If the formula evaluates to 1
{Return Success!}
If the formula evaluates to 0,
{Return Failure, hope another assignment works.}
Else
{split the problem on some variable, v.
SATDivide&Conquer (formula replacing v with 0)
SATDivide&Conquer (formula replacing v with 1)
}

在最坏的情况下，算法将重复执行，直到分配完所有变量，从而产生指数时间。然而每次拆分时，其中一项赋值都会删除其中一项子句（clause）。

例如，如果公式包含子句（a||!b||c），当a被赋值为1时，该子句的计算结果将为1，而无需为子句中的任何其他变量赋值（如果是FPV验证property会TrivT）；如果变量a在项中被否定，并且a被赋值为0，那么同样的减少也是可能的。

一旦任何一个conjunctive clauses （AND项）的值为0，整个公式的值将为0，因此算法可以放弃任何进一步的变量赋值。

搜索空间的这两种不同缩减可以在下面的搜索图中看到，该图可以找到公式(a||b||!d)&&(!b||c)&&(a||c) 的解。在这个搜索中，第一次分割选择变量a，然后是b、c，最后是d。与BDD一样，左子树标识变量分配给0的位置，右子树标识变量被分配给1的位置（图2.15）。

当算法从递归调用返回时，可以收集解决方案。在图中，可以通过从值为1的终端节点向上提升树并收集变量赋值来找到解决方案（例如，从最左侧的终端节点1:d = 0，c = 1，b = 0，a = 0）

注意，某些解决方案可能不会为所有变量提供赋值（上面的最右边的解决方案不会为d赋值）。在这些情况下，任何未赋值的变量都可以任意赋值0或1。

选择要拆分的变量会影响搜索的大小。在上面的示例中，以任意字母顺序选择变量。如果选择首先对变量b进行拆分，则需要少拆分一个。

更好的方法是让每个子问题选择自己的最优变量。如果选择a作为一个子问题，选择c作为另一个子问题将消除另一个分割。

对于这个简单的问题，一个做出正确选择的算法可能会缩短28%的运行时间，这不是一个糟糕的改进，特别是如果它扩展到更大的问题（同样，这不会适用于所有问题）。

在这种情况下，同时出现否定和不否定的变量（例如，b）可能是拆分的更好选择，因为当变量分配给值时，两个子问题都能够消除子句。这就是Davis-Putnam算法的关键所在。

Davis-Putnam算法通过使用resolution改进了这一基本技术。通过找到变量显示为正和负成对的子句来简化问题。在我们的示例中：

(a||b||!d) && (!b||c) && (a||c)

第一和第二子句中的b就是这样，解决方案将这两个子句合并为一个不带变量b的子句，并使其他子句不受影响。

(a||b||!d) && (!b||c) becomes (a||!d||c)

这产生了更简单的公式：

(a||!d||c)&&(a||c)

如果有其他带有变量b的子句，也可以解析成一个子句。这个过程重复寻找其他候选变量，直到没有其他可以解决的子句。一旦没有更多的子句需要解决，需要为简化公式找到一个变量赋值，然后将值插回原始问题中，以解决已解决的变量。在上面的示例中，会发现赋值a=1，d=0，c＝0。将这个部分解代入原始公式，发现b必须为0。

4、DAVIS-LOGEMANN-LOVELAND（DLL）SAT算法

Davis-Putnam算法可以通过观察单独出现在子子句（subclause ）中的变量赋值（可能是因为所有其他变量都赋值为0）来改进，而不需要拆分问题。每个子子句的计算值必须为1，因此变量值必须是1，除非出现在NOT公式中。可以用所需的值更快地替换所有子子句中的变量，拆分这些变量的性能成本很高。例如，对于子问题：

(b||!d)&&(!b||c)&&c

变量c是独立的，因此如果存在解，变量c必须是1。然后子问题简化为：

(b||!d)&&(!b)

然后，可以重复给b赋值0的过程（第二个子句需要）；将子问题简化为（d），需要给d赋值0。使用此方法，完全解决了SAT实例，不需要拆分或搜索！这种改进称为布尔约束传播（BCP）。DLL通常被称为DPLL，因为它是对Davis-Putnam算法的改进。

1）其他SAT算法改进

由于SAT公式的规模可能很大，即使是很小的效率改进也会对找到解决方案产生重大影响。这些改进可以是从搜索过程中的发现、本地化搜索技术以及改进的数据结构构建和处理工程中学习。

一种有效的学习技巧是跟踪冲突（conflict ）或冲突子句，这样做的目的是保存导致失败的变量集赋值的发现。利用这些信息，后续回溯可以避免重复错误的赋值，另一个有趣的算法（称为“Grasp "）表明，在添加第一次搜索时发现的一组冲突子句后，重新启动整个搜索可能会很有用。

良好的算法工程也可以大大提高性能，另一款成功的求解器（“Chaff”）采用了经常使用的操作非常高效的方法。通过优化BCP算法并优化速度和最近添加的子句的决策策略，求解器将速度提高了1-2个数量级。文章来源地址https://www.toymoban.com/news/detail-772145.html