约简算法解决 SAT 问题

terry 2年前 (2023-09-27) 阅读数 64 #数据结构与算法

概念：可满足性问题

SAT 问题：给定一个命题公式 F F F，判断是否存在解释 I I I 使得 I ⊨ F I\models F I⊨F.
第一个问题3被认为是一个NP完全问题。
最重要的逻辑问题可以归结为SAT：

SAT解题能力的培养：
重点：搜索与推理相结合，提高效率

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

SAT中有详细解释※C一般是CNF。为了便于讨论，这里引入 CNF 集的表示。

原则体现了

该公式可以被视为一组子句：
C 1 ∧ 。。。 ∧ C n C_1\wedge ... \wedge C_n C1∧.. .∧Cn
可以描述为：
{ C 1, . 。。 , C n } \{C_1 , ... , C_n \} {C1,...,Cn}
类似地，子句可以看作字母的集合：
( P ∨ Q ) ∧ ( Q → Ø P ) (P\vee Q)\楔形 (Q\to \neg P) (P∨Q) ∧(Q→ØP)
可以描述为：
{ { P , Q } , { Ø Q , Ø P } } \{\{P,Q\},\{\neg Q,\neg P\}\} {{P,Q},{ØQ,ØP}}
常见的一些表达方式：

公式：F F F
子句：C C C
变量变量：P , Q , R , . 。。 P, Q, R, ... P,Q,R,...

一些方便的表达式：

C i { P ↦ F } C_i\ {P\mapsto F\} Ci{P↦ F }：使用 F F F 代替 P P P
C i [ P ] C_i[P] Ci[P]：子句 C i C_i Ci中的变量 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 ：联盟C i C_i Ci和 C j C_j Cj的 n，C i ∪ C j C_i\cup C_j Ci∪Cj
F i ∧ F j F_i\wedge F_j Fi∧Fj：F i 的并集F_i Fi 和 F j F_j Fj，F i ∪ F j F_i\cup F_j Fi∪Fj

分辨率

只有一条规则：
C 1 [ P ] C 2 ] 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 为 true，则 C 2 C_2 C2中的其他文字一定为 true
如果 P P P 为 false，则 C 1 C_1 C1中的其他文字一定为 false
因此 P P P 可以从两个子句中省略，即
C 1 { P ↦ ⊥ } ∨ C 2 { Ø P ↦ ⊥ } C_1\ {P\mapto \bot\}\ C_2\{\neg P\mapsto\ bot\} C1{ P↦⊥}∨C2{ØP↦⊥}称为溶剂
，该溶剂可以作为连接子句添加到原始公式中，因此如果生成的新公式与原来的公式
如果 C 1 { p ↦ ⊥ } ∨ C 2 { Ø P ↦ ⊥ } = ⊥ ∨ ⊥ = ⊥ C_1\{p\mapsto \bot\}\vee C_2\{\neg P\mapsto }=\ bot\vee\bot=\bot C1{p↦⊥}∨C2{ØP↦⊥}=⊥∨⊥=⊥：
则 C 1 ∧ C 2 C_1\楔形 C_2 C1∧ C2 否满足
任何 CNF 包括 { C 1 , C 2 } \{C_1,C_2\} {C1,C2} 不满足
示例：
A ∨ A\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 的方法归约算法

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 )\楔形 (P\to R)\楔形 (Q\to R)\楔形 \neg R(P∨Q)∧(P→R ) ∧(Q→R)∧ØR

步骤	子句	描述
1	p ∧ Q p\Q Q p∧ -
2	P ∨ R \neg P\ vee R ØP∨R	-
3	Ø Q ∨ R \neg Q\vee R ØQ∨R❀-❀ \neg R ØR	-
5	Q ∨ R Q\ vee R Q∨R	1&2
6	R R R	3&5
7	3&5♶

算法简化评估

解决较大问题时效率低下基于搜索的方法

总体思路：从空的解释（解释）开始，一次增加一个变量的值 ❀ 部分解释 in实现策略比较灵活
如果 I I I 是部分解释，则文本 ℓ \ell ℓ 可以为 true，如果为 false， u n d e f undef undef:

t r u e true Ⓞ satisfy: ⓐ satisfies \model \ell I ⊨ℓ
f a l s e false false(冲突): I ⊭ ℓ I\ not\models\ell I⊨ℓ
u n d e f undef undef: var ( ≓ )( ≓ ) \ora\ing I var(ℓ) εI
给定子句 C C C 和解释 I I I：
C is true true under I I I if I ⊨ C I\models C I⊨C a l false under I I I if I ⊭ C I\not\models C I ⊨C
C 是 I I I 下的 u n i 单位单位，如果 C = C ′ ∨ ℓ , I ⊭ C ′ C=C' \vee \ell, I\ not \models C' C=C′∨ℓ,I ⊨C′, ℓ \ell ℓ 是 u n d e f undef undef
否则是 u n d e f undef undef

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

示例： ❀ 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 为真
Ø P 1
Ø P 1 。 \vee P_2 ØP1∨P2 是 false false false
Ø P 1 ∨ Ø P 4 ∨ P 3 \neg P_1\vee\neg P_4 \vee P_3 ØP1∨ØP4∨P3 是 u n i t 单位单位
Ø P 1 ∨ P 3 ∨ P 5 \neg P_1\vee P_3 \vee P_5 ØP1∨P3 是 u n d e f undef

搜索程序：状态机

每个状态记录部分解释和当前公式
状态之间的变换由变换规则决定
：程序状态
s a t sat sat
u n s a t unsat un sat
[ I ] ∥ F [I] \lVert F [I]∥F，其中 [ I ] [I] [F] 是解释， F [I] CNF
初始状态：[ Φ ] ∥ F [\ Phi]\lVert F [Φ]∥F
最终状态：s a t 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

搜索规则

用外行人的话说，最深的搜索优化了几种算法中的回溯策略。

决策规则（决策规则）
[ I ] ∥ F ↪ [ I , P ∘ ] ∥ F i f { P o c c u r s in F P u n a s ign e ]\l circ; ]\lVert F~if \begin{case}P~发生~in~F\\P~未分配~in~I\end{case} [I]∥F↪[I,P∘]∥F if { P 是在 FP 中未在 I
回溯规则
[I 1, P ∘, I 2 ] ∥ F ↪ [ I 1 , P ˉ ] ∥ F i f { [ I 1 , P ] n 为 2 F是 nterp 。 [I_1,P^{\circ},I_2]\lVert F\hookrightarrow [I_1,\bar{P}]\lVert F~if \begin{case}[I_1 ,P,I_2]\not\models F\\ P~end~decision~in~interp.\end{case}[I1,P∘,I2]∥F↪[I1,Pˉ]∥F if { [I1,P,I2]⊨ FP 在 interp 中的最终决定。
Rule Sat (Rule Sat)
[ I ] ∥ F ↪ s a t i f [ I ] ⊨ F [I]\lVert F\hookrightarrow sat~if~[I]\models I] ∥F↪sit if [I]⊨F
规则不饱和（规则不饱和）
[ I ] ∥ F ↪ u n s a t i f { I ⊨ ̸ F No d e c i n I on n i o [rrow F ] begin {case}I\not \models F\\No~decisions~in~I\end{cases} [I]∥F↪unsat if{I⊨FNo Decisions in I
以上四个规则足以构建 sat 求解器的基础
我们可以进一步优化例如，在单元子句 u n i t 中，对于描述 I I I 和子句 C C C，存在

I I I 不满足 C C C
C C 存在且 C 中只有一个文字设置为 false
得出结论原理包括：

Unit Propagation Rule（单位传播规则）
[ I ] ∥ F , C ∨ P ↪ [ I , P ] ∥ F , C ∨ P [I]\lVert \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 , and P u n d e f i n e d i n I I\not\~ models C, undefined~ in~I I⊨C, I 中未定义和 P

高级回滚和子句学习

相对“愚蠢”的基本回滚规则：

它总是返回到最近定义的解释它不存储有关子句冲突的信息
介绍BackJump 规则：
[I 1 , P ∘ , I 2 ] ∥ F ↪ [ I 1 , ∥ → l ] , ( ∥ F ] ) [ I 1 , P ∘ , I 2 ] ⊭ F E x i s t s C s 。 t。 : F ⇒ ( C → l ) I 1 ⊨ C var ( ℓ ) un def 。 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]\no\models F\\ Ana~C~\Rightarrow (C\to l)\\ I_1\models C\\ var(\ell)~undef.~in~I_1\\ var(\ell)~visible~in~F\结束 {case} [I1,P∘,I2]∥F↪[I1,ℓ]∥F,(C→l) if⎩⎪⎪⎪⎪⎪⎪⎨⎪⎪⎪⎪⎪⎪⎧[I1 ,P∘,I2]⊨Fexis C s.t.:F⇒(C→l)I1⊨Cvar(ℓ) undef. I1var(ℓ) 出现在 F
中，这里 C → l C \to l C→l 称为冲突子句。只要避免冲突条款，就能找到更多解决方案
那么，我们如何找到冲突条款呢？
创建蕴涵图（implication graph） G = ( V , E ) G=(V,E) G=(V,E):
V V V 定义 I 中的每个规则词都有一个 I 节点，标记为带有这个文本的值和惩罚级别（说白了，这个文本就是你使用的文本）
对于每个子句 C = ℓ 1 ∨ 。。。 ∨ ℓ n ∨ ℓ C=\ell_1\vee ... \vee\ell_n \vee \ell C=ℓ1∨...∨ℓn∨ℓ，其中 ℓ 1 , . 。。 . ) (\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

修剪 G G G，以便：

所有决策节点都位于一侧（“原因”）
至少有一个冲突文本位于另一侧（“”）

在“原因”上侧，选择与切边相连的所有节点 K K K
K K K K 中的节点是冲突原因
未创建的冲突子句对应的文本❀ :

图中, Ø P 5 ∨ Ø P 2 \neg P_5\vee\neg P_2 ØP5∨ØP2 和 Ø P 5 ∨ P 6 \neg P_5 ØP5 P6 P6 可以用作冲突子句。