归结算法求解SAT问题

2020年6月5日10:55:40 发表评论 310 views

概念: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 DB∨C∨D

归结法求解SAT

归结算法

归结算法求解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
步骤子句备注
1p ∧ Q p\wedge Q p∧Q-
2¬ P ∨ R \neg P\vee R ¬P∨R-
3¬ Q ∨ R \neg Q\vee R ¬Q∨R-
4¬ R \neg R ¬R-
5Q ∨ R Q\vee R Q∨R1&2
6R R R3&5
7⊥ \bot ⊥4&6

归结算法的评价

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

基于搜索的方法

大致思路:从一个空的解释(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~\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 Λ的边。
  • 将每条边都标记上导致这个蕴含关系的子句
    例如:
    归结算法求解SAT问题
    冲突图:只有一个冲突变元,且所有节点都具有通往 Λ \Lambda Λ的路径的蕴含图
    例如:
    归结算法求解SAT问题
    获得冲突子句:
    考虑一个冲突图 G G G
  1. 在 G G G中切一刀,使得:
  • 所有的判定节点在一侧(“原因”)
  • 至少一个冲突文字在另一侧(“结果”)
  1. 在“原因”一侧中,选出所有与被切割的边相连的节点 K K K
  2. K K K中的节点即为冲突的原因
  3. 相应的文字的非生成了冲突子句
    例如:
    归结算法求解SAT问题
    图中, ¬ 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求解器主要采用的方法。

发表评论

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: