程序验证（二）：SAT问题

概念：Satisfiability Problem

SAT问题：给定一个命题公式 F F F，决定是否存在一个解释 I I I使得 I ⊨ F I\models F I⊨F.
3SAT问题是首个被确定的NP完全问题。
大多数重要逻辑问题可以归约为SAT：

• 永真性
• 蕴含
• 等价性

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

CNF详解

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

集合表示

一个公式(formula)可以视为子句(clause)的集合：
C 1 ∧ . . . ∧ C n C_1\wedge ... \wedge C_n C1​∧...∧Cn​
可以表示为：
{ C 1 , . . . , C n } \{C_1 , ... , C_n \} {C1​,...,Cn​}
同样，子句可以视为文字(literal)的集合：
( P ∨ Q ) ∧ ( Q → ¬ P ) (P\vee Q)\wedge (Q\to \neg P) (P∨Q)∧(Q→¬P)
可以表示为：
{ { P , Q } , { ¬ Q , ¬ P } } \{\{P,Q\},\{\neg Q,\neg P\}\} {{P,Q},{¬Q,¬P}}
一些通用的表示方法：

• 公式 formula: F F F
• 子句 clause: C C C
• 变量 variable: P , Q , R , . . . P, Q, R, ... P,Q,R,...

一些方便的表达方式：

• C i { P ↦ F } C_i\{P\mapsto F\} Ci​{P↦F}: 在子句 C i C_i Ci​中使用 F F F替代 P P P
• C i [ P ] C_i[P] Ci​[P]: 变量 P P P在子句 C i C_i Ci​中是不取非的，也就是 C i = { . . . , P , . . . } C_i = \{... , P , ...\} Ci​={...,P,...}
• C i [ ¬ P ] C_i[\neg P] Ci​[¬P]: 变量 P P P在 C i C_i Ci​中是取非的，也就是 C i = { . . . , ¬ P , . . . } C_i = \{... , \neg P , ...\} Ci​={...,¬P,...}

在这种符号体系下，会有以下命题成立（有点绕，需要多看几遍）：
以 F F F表示公式， C C C表示子句，基于CNF公式的集合表示，有：

• C i ∨ C j C_i\vee C_j Ci​∨Cj​: union of C i C_i Ci​ and C j C_j Cj​, C i ∪ C j C_i\cup C_j Ci​∪Cj​
• F i ∧ F j F_i\wedge F_j Fi​∧Fj​: union of F i F_i Fi​ and F j F_j Fj​, F i ∪ F j F_i\cup F_j Fi​∪Fj​

归结(resolution)

只有一条规则：
C 1 [ P ]   C 2 [ ¬ P ] C 1 { P ↦ ⊥ } ∨ C 2 { ¬ P ↦ ⊥ } \frac{C_1[P]~C_2[\neg P]}{C_1\{P\mapsto \bot\}\vee C_2\{\neg P\mapsto \bot\}} C1​{P↦⊥}∨C2​{¬P↦⊥}C1​[P] C2​[¬P]​
给定两个具有相同变量 P P P，但是对于 P P P取非情况不同的两个子句，那么：

• 如果 P P P为真，那么 C 2 C_2 C2​中的其它文字必然为真
• 如果 P P P为假，那么 C 1 C_1 C1​中的其它文字必然为假
• 因此，可以在两个子句中都移除 P P P，也就是归结
• C 1 { P ↦ ⊥ } ∨ C 2 { ¬ P ↦ ⊥ } C_1\{P\mapsto \bot\}\vee C_2\{\neg P\mapsto\bot\} C1​{P↦⊥}∨C2​{¬P↦⊥}叫做归结式(resolvent)
  这个归结式可以作为一个合取子句加入到原公式，这样得到的新公式与原公式等价。
  而如果 C 1 { p ↦ ⊥ } ∨ C 2 { ¬ P ↦ ⊥ } = ⊥ ∨ ⊥ = ⊥ C_1\{p\mapsto \bot\}\vee C_2\{\neg P\mapsto\bot\}=\bot\vee\bot=\bot C1​{p↦⊥}∨C2​{¬P↦⊥}=⊥∨⊥=⊥：
• 那么 C 1 ∧ C 2 C_1\wedge C_2 C1​∧C2​是不可满足的
• 任何包括 { C 1 , C 2 } \{C_1,C_2\} {C1​,C2​}在内的CNF都是不可满足的
  举例：
  A ∨ B ∨ C A\vee B\vee C A∨B∨C与 ¬ A ∨ B ∨ D \neg A\vee B\vee D ¬A∨B∨D的归结子句是 B ∨ C ∨ D B\vee C\vee D B∨C∨D

归结法求解SAT

归结算法

• F ′ F' F′是所有归结式的集合
• 每一轮迭代，更新 F F F以包含以产生的归结式
• 每一轮迭代，计算所有可能的归结式
• 在更新后的 F F F上重复归结过程
• 终止条件：1.出现 ⊥ \bot ⊥归结式 2.无法再更新 F F F（此时所有的可归结的子句都已经被归结了）
  举例：
  ( P ∨ Q ) ∧ ( P → R ) ∧ ( Q → R ) ∧ ¬ R (P\vee Q)\wedge (P\to R)\wedge (Q\to R)\wedge \neg R (P∨Q)∧(P→R)∧(Q→R)∧¬R

归结算法的评价

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

基于搜索的方法

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

部分解释

在实现策略上更加灵活
如果 I I I是一个部分解释，文字 ℓ \ell ℓ可以为 t r u e true true, f a l s e false false, u n d e f undef undef:

• t r u e true true(satisfied): I ⊨ ℓ I\models \ell I⊨ℓ
• f a l s e false false(conflicting): I ⊭ ℓ I\not\models\ell I​⊨ℓ
• u n d e f undef undef: v a r ( ℓ ) ∉ I var(\ell)\not\in I var(ℓ)​∈I
  给定一个子句 C C C和解释 I I I：
• C is t r u e true true under I I I iff I ⊨ C I\models C I⊨C
• C is f a l s e false false under I I I iff I ⊭ C I\not\models C I​⊨C
• C is u n i t unit unit under I I I iff C = C ′ ∨ ℓ , I ⊭ C ′ C=C' \vee \ell, I\not\models C' C=C′∨ℓ,I​⊨C′, ℓ \ell ℓ is u n d e f undef undef
• Otherwise it is u n d e f undef undef

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

举例：
令 I = { P 1 ↦ 1 , P 2 ↦ 0 , P 4 ↦ 1 } I=\{P_1\mapsto 1,P_2\mapsto 0,P_4\mapsto 1\} I={P1​↦1,P2​↦0,P4​↦1}，那么有：

• P 1 ∨ P 3 ∨ ¬ P 4 P_1\vee P_3\vee\neg P_4 P1​∨P3​∨¬P4​ is t r u e true true
• ¬ P 1 ∨ P 2 \neg P_1\vee P_2 ¬P1​∨P2​ is f a l s e false false
• ¬ P 1 ∨ ¬ P 4 ∨ P 3 \neg P_1\vee\neg P_4 \vee P_3 ¬P1​∨¬P4​∨P3​ is u n i t unit unit
• ¬ P 1 ∨ P 3 ∨ P 5 \neg P_1\vee P_3 \vee P_5 ¬P1​∨P3​∨P5​ is u n d e f undef undef

搜索程序：一个状态机

• 每一个状态都记录了部分解释与当前的公式
• 状态之间的转化由转化规则决定
  程序的状态包括：
• s a t sat sat
• u n s a t unsat unsat
• [ I ] ∥ F [I] \lVert F [I]∥F, 这里的 [ I ] [I] [I]是一个解释， F F F是一个CNF
  初始状态： [ Φ ] ∥ F [\Phi]\lVert F [Φ]∥F
  结束状态： s a t sat sat, u n s a t unsat unsat
  中间状态：
• [ Φ ] ∥ F 1 [\Phi]\lVert F_1 [Φ]∥F1​, C C C: 解释为空， F = F 1 ∧ C F=F_1\wedge C F=F1​∧C
• [ I 1 , P ˉ , I 2 ] ∥ F [I_1,\bar{P},I_2]\lVert F [I1​,Pˉ,I2​]∥F: 解释先置为 I 1 I_1 I1​，然后 P ↦ 0 P\mapsto 0 P↦0, 然后解释为 I 2 I_2 I2​

搜索规则

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

1. 判定规则(Decision Rule)
   [ I ] ∥ F ↪ [ I , P ∘ ] ∥ F   i f { P   o c c u r s   i n   F P   u n a s s i g n e d   i n   I [I]\lVert F \hookrightarrow [I,P^{\circ}]\lVert F~if \begin{cases}P~occurs~in~F\\P~unassigned~in~I\end{cases} [I]∥F↪[I,P∘]∥F if{P occurs in FP unassigned in I​
2. 回退规则(Backtrack Rule)
   [ I 1 , P ∘ , I 2 ] ∥ F ↪ [ I 1 , P ˉ ] ∥ F   i f { [ I 1 , P , I 2 ] ⊭ F P   l a s t   d e c i s i o n   i n   i n t e r p . [I_1,P^{\circ},I_2]\lVert F\hookrightarrow [I_1,\bar{P}]\lVert F~if \begin{cases}[I_1,P,I_2]\not\models 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 ] ∥ F ↪ s a t   i f   [ I ] ⊨ F [I]\lVert F\hookrightarrow sat~if~[I]\models F [I]∥F↪sat if [I]⊨F
4. 不可满足规则(Unsat Rule)
   [ I ] ∥ F ↪ u n s a t   i f { I ⊭ F N o   d e c i s i o n s   i n   I [I]\lVert F\hookrightarrow unsat~if \begin{cases}I\not\models F\\No~decisions~in~I\end{cases} [I]∥F↪unsat if{I​⊨FNo decisions in I​
   以上四条规则足以构建一个基本的sat求解器
   我们可以进一步优化。比如在 u n i t unit unit子句中，对于解释 I I I与子句 C C C，有

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

1. 单元传播规则(Unit Propagation Rule)
   [ I ] ∥ F , C ∨ P ↪ [ I , P ] ∥ F , C ∨ P [I]\lVert F, C\vee P\hookrightarrow[I,P]\lVert F,C\vee P [I]∥F,C∨P↪[I,P]∥F,C∨P
   [ I ] ∥ F , C ∨ ¬ P ↪ [ I , P ˉ ] ∥ F , C ∨ ¬ P [I]\lVert F,C\vee \neg P\hookrightarrow [I,\bar{P}]\lVert F,C\vee \neg P [I]∥F,C∨¬P↪[I,Pˉ]∥F,C∨¬P
   条件是
   I ⊭ C , a n d   P   u n d e f i n e d   i n   I I\not\models C, and~P~undefined~in~I I​⊨C,and P undefined in I

高级回退&子句学习

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

• 它总是回退到最近确定的解释
• 它不保留子句冲突的信息
  引入回跳规则(BackJump Rule):
  [ I 1 , P ∘ , I 2 ] ∥ F ↪ [ I 1 , ℓ ] ∥ F , ( C → l )   i f { [ I 1 , P ∘ , I 2 ] ⊭ F E x i s t s   C   s . t . : F ⇒ ( C → l ) I 1 ⊨ C v a r ( ℓ )   u n d e f .   i n   I 1 v a r ( ℓ )   a p p e a r s   i n   F [I_1,P^{\circ},I_2]\lVert F\hookrightarrow [I_1,\ell]\lVert F, (C\to l)~if \begin{cases}[I_1,P^{\circ},I_2]\not\models F\\ Exists~C~s.t.:F\Rightarrow (C\to l)\\ I_1\models C\\ var(\ell)~undef.~in~I_1\\ var(\ell)~appears~in~F\end{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​
  这里 C → l C\to l C→l就叫做冲突子句，我们只要避免冲突子句就可以进一步寻找解。
  那么，如何找到冲突子句呢？
  构造一个蕴含图(implication graph) G = ( V , E ) G=(V,E) G=(V,E):
• V V V对于解释 I I I中每一个判定文字都有一个节点，用这个文字的值和它的判定等级来标记（说白了就是这个文字是你所判定的第几个文字）
• 对于每个子句 C = ℓ 1 ∨ . . . ∨ ℓ n ∨ ℓ C=\ell_1\vee ... \vee\ell_n \vee \ell C=ℓ1​∨...∨ℓn​∨ℓ，其中 ℓ 1 , . . . , ℓ n \ell_1, ... ,\ell_n ℓ1​,...,ℓn​被赋值为假，首先为 ℓ \ell ℓ添加一个节点，它的判定等级就是它进入到 I I I的顺序，然后添加边 ( ℓ i , ℓ ) (\ell_i, \ell) (ℓi​,ℓ)到 E E E，其中 1 ≤ i ≤ n 1\le i\le n 1≤i≤n
• 添加一个冲突节点 Λ \Lambda Λ。对于所有标记为 P P P与 ¬ P \neg P ¬P的冲突变元，在 E E E中添加从这些节点到 Λ \Lambda Λ的边。
• 将每条边都标记上导致这个蕴含关系的子句
  例如：
  
  冲突图：只有一个冲突变元，且所有节点都具有通往 Λ \Lambda Λ的路径的蕴含图
  例如：
  
  获得冲突子句：
  考虑一个冲突图 G G G

1. 在 G G G中切一刀，使得：

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

1. 在“原因”一侧中，选出所有与被切割的边相连的节点 K K K
2. K K K中的节点即为冲突的原因
3. 相应的文字的非生成了冲突子句
   例如：
   
   图中， ¬ P 5 ∨ ¬ P 2 \neg P_5\vee\neg P_2 ¬P5​∨¬P2​和 ¬ P 5 ∨ P 6 \neg P_5\vee P_6 ¬P5​∨P6​可以作为冲突子句

DPLL & CDCL

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