程序验证（二）：SAT问题

概念：Satisfiability Problem

SAT问题：给定一个命题公式
$F$

F，决定是否存在一个解释
$I$

I使得
$Imodels F$

I⊨F.
3SAT问题是首个被确定的NP完全问题。
大多数重要逻辑问题可以归约为SAT：

• 永真性
• 蕴含
• 等价性

SAT求解能力的发展：
关键：将搜索与推理结合以提高效率

CNF详解

SAT求解器的输入一般是CNF，这里为便于讨论，引入关于CNF的集合表示。

集合表示

一个公式(formula)可以视为子句(clause)的集合：

$C_1wedge … wedge C_n$

C1​∧...∧Cn​
可以表示为：

${C_1 , … , C_n }$

{C1​,...,Cn​}
同样，子句可以视为文字(literal)的集合：

$(Pvee Q)wedge (Qto neg P)$

(P∨Q)∧(Q→¬P)
可以表示为：

${{P,Q},{neg Q,neg P}}$

{{P,Q},{¬Q,¬P}}
一些通用的表示方法：

• 公式 formula:
  $F$

  F

• 子句 clause:
  $C$

  C

• 变量 variable:
  $P, Q, R, …$

  P,Q,R,...

一些方便的表达方式：

• 
  $C_i{Pmapsto F}$

  Ci​{P↦F}: 在子句
  $C_i$

  Ci​中使用
  $F$

  F替代
  $P$

  P

• 
  $C_i[P]$

  Ci​[P]: 变量
  $P$

  P在子句
  $C_i$

  Ci​中是不取非的，也就是
  $C_i = {… , P , …}$

  Ci​={...,P,...}

• 
  $C_i[neg P]$

  Ci​[¬P]: 变量
  $P$

  P在
  $C_i$

  Ci​中是取非的，也就是
  $C_i = {… , neg P , …}$

  Ci​={...,¬P,...}

在这种符号体系下，会有以下命题成立（有点绕，需要多看几遍）：
以
$F$

F表示公式，
$C$

C表示子句，基于CNF公式的集合表示，有：

• 
  $C_ivee C_j$

  Ci​∨Cj​: union of
  $C_i$

  Ci​ and
  $C_j$

  Cj​,
  $C_icup C_j$

  Ci​∪Cj​

• 
  $F_iwedge F_j$

  Fi​∧Fj​: union of
  $F_i$

  Fi​ and
  $F_j$

  Fj​,
  $F_icup F_j$

  Fi​∪Fj​

归结(resolution)

只有一条规则：

$frac{C_1[P]~C_2[neg P]}{C_1{Pmapsto bot}vee C_2{neg Pmapsto bot}}$

C1​{P↦⊥}∨C2​{¬P↦⊥}C1​[P] C2​[¬P]​
给定两个具有相同变量
$P$

P，但是对于
$P$

P取非情况不同的两个子句，那么：

• 如果
  $P$

  P为真，那么
  $C_2$

  C2​中的其它文字必然为真

• 如果
  $P$

  P为假，那么
  $C_1$

  C1​中的其它文字必然为假

• 因此，可以在两个子句中都移除
  $P$

  P，也就是归结

• 
  $C_1{Pmapsto bot}vee C_2{neg Pmapstobot}$

  C1​{P↦⊥}∨C2​{¬P↦⊥}叫做归结式(resolvent)
  这个归结式可以作为一个合取子句加入到原公式，这样得到的新公式与原公式等价。
  而如果
  $C_1{pmapsto bot}vee C_2{neg Pmapstobot}=botveebot=bot$

  C1​{p↦⊥}∨C2​{¬P↦⊥}=⊥∨⊥=⊥：

• 那么
  $C_1wedge C_2$

  C1​∧C2​是不可满足的

• 任何包括
  ${C_1,C_2}$

  {C1​,C2​}在内的CNF都是不可满足的
  举例：
  
  $Avee Bvee C$

  A∨B∨C与
  $neg Avee Bvee D$

  ¬A∨B∨D的归结子句是
  $Bvee Cvee D$

  B∨C∨D

归结法求解SAT

归结算法

• 
  $F’$

  F′是所有归结式的集合

• 每一轮迭代，更新
  $F$

  F以包含以产生的归结式

• 每一轮迭代，计算所有可能的归结式
• 在更新后的
  $F$

  F上重复归结过程

• 终止条件：1.出现
  $bot$

  ⊥归结式 2.无法再更新
  $F$

  F（此时所有的可归结的子句都已经被归结了）
  举例：
  
  $(Pvee Q)wedge (Pto R)wedge (Qto R)wedge neg R$

  (P∨Q)∧(P→R)∧(Q→R)∧¬R

归结算法的评价

解决较大规模问题的效率低下

基于搜索的方法

大致思路：从一个空的解释(interpretation)出发，每次扩展一个变量的取值

部分解释

在实现策略上更加灵活
如果
$I$

I是一个部分解释，文字
$ell$

ℓ可以为
$true$

true,
$false$

false,
$undef$

undef:

• 
  $true$

  true(satisfied):
  $Imodels ell$

  I⊨ℓ

• 
  $false$

  false(conflicting):
  $Inotmodelsell$

  I​⊨ℓ

• 
  $undef$

  undef:
  $var(ell)notin I$

  var(ℓ)​∈I
  给定一个子句
  $C$

  C和解释
  $I$

  I：

• C is
  $true$

  true under
  $I$

  I iff
  $Imodels C$

  I⊨C

• C is
  $false$

  false under
  $I$

  I iff
  $Inotmodels C$

  I​⊨C

• C is
  $unit$

  unit under
  $I$

  I iff
  $C=C’ vee ell, Inotmodels C’$

  C=C′∨ℓ,I​⊨C′,
  $ell$

  ℓ is
  $undef$

  undef

• Otherwise it is
  $undef$

  undef

iff: if and only if，当且仅当 unit: 单元，一个新引入的概念 

举例：
令
$I={P_1mapsto 1,P_2mapsto 0,P_4mapsto 1}$

I={P1​↦1,P2​↦0,P4​↦1}，那么有：

• 
  $P_1vee P_3veeneg P_4$

  P1​∨P3​∨¬P4​ is
  $true$

  true

• 
  $neg P_1vee P_2$

  ¬P1​∨P2​ is
  $false$

  false

• 
  $neg P_1veeneg P_4 vee P_3$

  ¬P1​∨¬P4​∨P3​ is
  $unit$

  unit

• 
  $neg P_1vee P_3 vee P_5$

  ¬P1​∨P3​∨P5​ is
  $undef$

  undef

搜索程序：一个状态机

• 每一个状态都记录了部分解释与当前的公式
• 状态之间的转化由转化规则决定
  程序的状态包括：
• 
  $sat$

  sat

• 
  $unsat$

  unsat

• 
  $[I] lVert F$

  [I]∥F, 这里的
  $[I]$

  [I]是一个解释，
  $F$

  F是一个CNF
  初始状态：
  $[Phi]lVert F$

  [Φ]∥F
  结束状态：
  $sat$

  sat,
  $unsat$

  unsat
  中间状态：

• 
  $[Phi]lVert F_1$

  [Φ]∥F1​,
  $C$

  C: 解释为空，
  $F=F_1wedge C$

  F=F1​∧C

• 
  $[I_1,bar{P},I_2]lVert F$

  [I1​,Pˉ,I2​]∥F: 解释先置为
  $I_1$

  I1​，然后
  $Pmapsto 0$

  P↦0, 然后解释为
  $I_2$

  I2​

搜索规则

通俗的说，就是深度优先搜索。在某些算法中优化了回退策略。

1. 判定规则(Decision Rule)
   
   $[I]lVert F hookrightarrow [I,P^{circ}]lVert F~if begin{cases}P~occurs~in~F\P~unassigned~in~Iend{cases}$

   [I]∥F↪[I,P∘]∥F if{P occurs in FP unassigned in I​

2. 回退规则(Backtrack Rule)
   
   $[I_1,P^{circ},I_2]lVert Fhookrightarrow [I_1,bar{P}]lVert F~if begin{cases}[I_1,P,I_2]notmodels F\P~last~decision~in~interp.end{cases}$

   [I1​,P∘,I2​]∥F↪[I1​,Pˉ]∥F if{[I1​,P,I2​]​⊨FP last decision in interp.​

3. 可满足规则(Sat Rule)
   
   $[I]lVert Fhookrightarrow sat~if~[I]models F$

   [I]∥F↪sat if [I]⊨F

4. 不可满足规则(Unsat Rule)
   
   $[I]lVert Fhookrightarrow unsat~if begin{cases}Inotmodels F\No~decisions~in~Iend{cases}$

   [I]∥F↪unsat if{I​⊨FNo decisions in I​
   以上四条规则足以构建一个基本的sat求解器
   我们可以进一步优化。比如在
   $unit$

   unit子句中，对于解释
   $I$

   I与子句
   $C$

   C，有

• 
  $I$

  I不满足
  $C$

  C

• 
  $C$

  C中有且只有一个文字被置为假
  那么根据归结原理，有：

5. 单元传播规则(Unit Propagation Rule)
   
   $[I]lVert F, Cvee Phookrightarrow[I,P]lVert F,Cvee P$

   [I]∥F,C∨P↪[I,P]∥F,C∨P
   
   $[I]lVert F,Cvee neg Phookrightarrow [I,bar{P}]lVert F,Cvee neg P$

   [I]∥F,C∨¬P↪[I,Pˉ]∥F,C∨¬P
   条件是
   
   $Inotmodels C, and~P~undefined~in~I$

   I​⊨C,and P undefined in I

高级回退&子句学习

基础的回退规则比较“笨”：

• 它总是回退到最近确定的解释
• 它不保留子句冲突的信息
  引入回跳规则(BackJump Rule):
  
  $[I_1,P^{circ},I_2]lVert Fhookrightarrow [I_1,ell]lVert F, (Cto l)~if begin{cases}[I_1,P^{circ},I_2]notmodels F\ Exists~C~s.t.:FRightarrow (Cto l)\ I_1models C\ var(ell)~undef.~in~I_1\ var(ell)~appears~in~Fend{cases}$

  [I1​,P∘,I2​]∥F↪[I1​,ℓ]∥F,(C→l) if⎩⎪⎪⎪⎪⎪⎪⎨⎪⎪⎪⎪⎪⎪⎧​[I1​,P∘,I2​]​⊨FExists C s.t.:F⇒(C→l)I1​⊨Cvar(ℓ) undef. in I1​var(ℓ) appears in F​
  这里
  $Cto l$

  C→l就叫做冲突子句，我们只要避免冲突子句就可以进一步寻找解。
  那么，如何找到冲突子句呢？
  构造一个蕴含图(implication graph)
  $G=(V,E)$

  G=(V,E):

• 
  $V$

  V对于解释
  $I$

  I中每一个判定文字都有一个节点，用这个文字的值和它的判定等级来标记（说白了就是这个文字是你所判定的第几个文字）

• 对于每个子句
  $C=ell_1vee … veeell_n vee ell$

  C=ℓ1​∨...∨ℓn​∨ℓ，其中
  $ell_1, … ,ell_n$

  ℓ1​,...,ℓn​被赋值为假，首先为
  $ell$

  ℓ添加一个节点，它的判定等级就是它进入到
  $I$

  I的顺序，然后添加边
  $(ell_i, ell)$

  (ℓi​,ℓ)到
  $E$

  E，其中
  $1le ile n$

  1≤i≤n

• 添加一个冲突节点
  $Lambda$

  Λ。对于所有标记为
  $P$

  P与
  $neg P$

  ¬P的冲突变元，在
  $E$

  E中添加从这些节点到
  $Lambda$

  Λ的边。

• 将每条边都标记上导致这个蕴含关系的子句
  例如：
  
  冲突图：只有一个冲突变元，且所有节点都具有通往
  $Lambda$

  Λ的路径的蕴含图
  例如：
  
  获得冲突子句：
  考虑一个冲突图
  $G$

  G

1. 在
   $G$

   G中切一刀，使得：

• 所有的判定节点在一侧（“原因”）
• 至少一个冲突文字在另一侧（“结果”）

2. 在“原因”一侧中，选出所有与被切割的边相连的节点
   $K$

   K

3. 
   $K$

   K中的节点即为冲突的原因

4. 相应的文字的非生成了冲突子句
   例如：
   
   图中，
   $neg P_5veeneg P_2$

   ¬P5​∨¬P2​和
   $neg P_5vee P_6$

   ¬P5​∨P6​可以作为冲突子句

DPLL & CDCL

DPLL见DPLL
CDCL即为(Conflict-Driven Clause Learning)，是目前SAT求解器主要采用的方法。