SAT问题.

Presentation on theme: "SAT问题."— Presentation transcript:

1 SAT问题

2 内容 什么是SAT问题 SAT问题的重要性 DPLL算法

3 SAT问题 布尔变量是值域只有两个元素0和1的变量 一个只由布尔变量形成的CSP问题又称为SAT问题
可以将SAT问题看做是一类特殊的CSP问题，不过因为SAT是一类重要的问题，在现实中和理论上有着重要的意义，因此我们将重新给出SAT问题的定义

4 SAT问题的相关定义 一般来说，SAT问题是判定一个命题公式是否可满足的问题，通常这个命题公式是CNF公式。相关定义如下：
文字：布尔变量x和布尔变量的非﹁x称为文字，前者为正文字，后者为负文字 子句：l1∨… ∨ lk形式的式子称为子句，其中∨是逻辑上的析取连接词， li是文字；子句也常被表示为文字的集合 CNF公式：C1 ∧… ∧ Cm为CNF公式，其中∧是逻辑上的合取连接词，Ci是子句； CNF公式也常被表示为子句的集合

5 SAT问题的相关定义 赋值t：变量到{0,1}的映射 对于文字l： t(l) = 1当且仅当： l为正文字x且t(x) = 1
对于子句C=l1∨… ∨ lk： t(C)=1当且仅当 对于某个li有t(li) = 1 对于公式F= C1 ∧… ∧ Cm：t(F)=1当且仅当 对于所有的Ci有t(Ci) = 1

6 SAT问题的相关定义 这样一个SAT问题就是： 给定一个CNF公式F，判定它是否存在一个赋值t，使得t(F)=1

7 SAT问题的重要性 SAT问题是一个重要的问题，它是最早被证明为NP完全的问题之一；目前SAT问题还被用于编码一些实际应用问题，比如人工智能问题，形式验证问题等 现在的SAT求解器能求解的问题的规模：百万个变量，千万个子句

8 SAT的理论意义 [Cook 70] 中指出SAT 是NPC的

9 图染色问题 每个节点染且仅染一种颜色，相邻的节点颜色不同 图是否能2染色? 图是否能3染色? 图是否能K（k>3）染色?
Decidable in P. 图是否能3染色? NP-complete. 图是否能K（k>3）染色?

10 SAT问题的实践意义 SAT 问题在实践中主要应用于: 验证和测试电路图案 两个电路的等价性检测 软件的可达性分析 程序的形式验证 ……

11 求解SAT 尝试所有的赋值可能 应用一些启发式策略来生成比较可能满足布尔公式的赋值 当有 n 个变量时，需要尝试 2n 个可能的组合
指数爆炸 应用一些启发式策略来生成比较可能满足布尔公式的赋值

12 SAT求解器 SAT求解器是求解SAT问题的算法，它以一个CNF公式作为输入，以0,1作为输出，表示该公式是否可满足。有的求解器还可以给出满足的解，或者不满足的原因 SAT求解器分为完全求解器和不完全求解器两种

13 完全求解器 穷尽搜索空间 只要有足够的时间，一定能够给出答案 适用于实际应用中的问题

14 不完全求解器 大多采用局部搜索方法 当问题可满足的时候，有可能给出答案，也有可能给不出答案 当问题不可满足的时候，无法给出答案
适用于随机产生的CNF公式

15 DPLL SAT 求解器 Davis-Putnam-Logemann-Loveland 算法(1960,1962). 最近的一些途径
它提供了一个结构化的方法来枚举可能的赋值。 Chronological backtracking 最近的一些途径 Conflict analysis & learning Non-chronological backtracking Search space pruning

16 DPLL算法简述 它是一个回溯搜索算法 它的基本思想是每次选中一个未被赋值的变量进行赋值，然后判断该赋值是否满足整个公式： 满足：结束搜索；
导致冲突（某个子句为0）：回溯； 否则：对下一个变量进行赋值

17 DPLL算法的例子

18 DPLL算法的例子 上图是一个典型的DPLL算法过程，是一个树状结构
分别给变量a,b,c赋值，给变量赋值为1用变量本身表示，赋值为0用变量的非表示 当给变量a,b,c分别赋值为1,1,0的时候，遇到了冲突，这时需要回溯到b，重新给b赋值

19 DPLL 算法 decide-next-branch() deduce() – 单元值传播（unit propagation）:
选择一个没有被赋值的变量，并给定一个赋值 deduce() – 单元值传播（unit propagation）: 如果有一个没有赋值的变量，给它一个赋值，从这个赋值出发做BCP (Boolean Constraint Propagation). BCP 反复的应用单子句规则（当有一个子句变成单子句的时候触发） BCP 也可能应用其它的规则 如果没有发现冲突，选择下一个没有被赋值的变量；反之，回溯。 analyze-conflict() 找出导致冲突（一个变量既被赋值为真又被赋值为假 ）的原因，有的时候还会添加一些新的子句来约束后面的搜索。 backtrack() 回溯，取消一些赋值和他们诱导出的赋值。

20 DPLL 算法详解

21 例子 f = a (b + c + d) (b’ + c) (b’ + d) (x’ + y’) (x + z’) (x’ + b’ + y) (x + b’ + z) (c + d + y’ + z’). a = 1. f = (b + c + d) (b’ + c) (b’ + d) (x’ + y’) (x + z’) (x’ + b’ + y) (x + b’ + z) (c + d + y’ + z’). 决策(分支)变量: b = 1. f = c d (x’ + y’) (x + z’) (x’ + y) (x + z) (c + d + y’ + z’). c = 1, d = 1. f = (x’ + y’) (x + z’) (x’ + y) (x + z). 决策变量: x = 1. f = y’ y . 冲突

22 例子（续） f可满足 f = (x’ + y’) (x + z’) (x’ + y) (x + z). f = z’ z.
翻转最近的决策变量赋值，i.e., x = 0. f = z’ z. 还是冲突，翻转再上一个决策变量赋值， i.e., b = 0. f = (c + d) (x’ + y’) (x + z’) (c + d + y’ + z’). 决策变量: x = 1. f = (c + d) y’ (c + d + y’ + z’). y = 0. f = (c + d). 决策变量: c = 1. f = 1. f可满足

23 ZChaff: 优化BCP BCP占据了求解的大量时间（大概80%） BCP没有必要检查所有的子句是否变成了单子句。
每一个子句选择2个文字作为观察文字（watching literals ），仅当有一个观察文字都为假的时候这个子句才可能变成单子句。 一个赋值 (x = 1) 仅可能将包括x’的子句变成单子句，类似的性质对 (x = 0)也成立。 需要一个高效的数据结构

24 ZChaff: 启发式分支策略 分支决策变量的选取显著的影响了搜索树的深度 搜索应该局部化
出现频繁的文字似乎是自然的选择 搜索应该局部化 即，冲突分析后，应该选择那些导致冲突的文字做为决策文字 每一个变量都分配一个计数器，子句中出现一次变量，该变量就累加一。我们可以选择没有赋值的变量中，该值最高的变量做为决策变量。 由于冲突分析会引入lemma子句加入，这个策略会使得搜索倾向于局部化。

25 ZChaff: 有效的冲突分析 当冲突分析的时候，我们还应该添加一些子句来避免重复的子空间搜索。
例，如果按照a, b, c, d, e的顺序搜索，那么如果冲突分析得出是a导致的冲突，那么我们不需要按照年代顺序一步步回溯回去，直接跳到a即可，这样就避免了重复的子空间搜索。

26 ZChaff:有效的冲突分析（续） 假设有两个互相冲突的单子句P和Q。 考虑P和Q中那些导致他们成为单子句的变量。
如果那些变量是a, b, c (他们的赋值为1）和d, e, f (他们的赋值为0)，那么我们将添加子句 (a’ + b’ + c’ + d + e + f)。

27 x1’ +x9+x10+x11

28 Unique Implication Point
UIP = 当前决策层上，决策变量到冲突的路径都经过的点 x1 is UIP (decision variable causing is always a UIP) x4 is UIP

29 Limiting Learned Clauses
保留较短的子句（较少的文字） zChaff 推荐仅保留最靠近冲突的UIP lemma[Zhang et al., ICCAD2001] 类似cache的处理，周期性的舍弃一部分lemma 用活跃性统计来保留最有用的子句 [minisat 1.2] CALTECH CS137 Fall DeHon