「problems」【转】(一) SAT problem 介绍

problems

Boolean Satisfiability Problem

什么是SAT?

Boolean satisfiability problem 简称SAT，简单说就是用来判断一组给定的布林函数，是否可以找到一组变数赋值能使其为真。

# a, b, c 任一为true 该式都为true，也就是找的到解

# satisfiable

(a ∨ b ∨ c)

# a 不论为true 或false 该式都为false，即找不到能使该式为true 的assign 方式

# unsatisfiable

(a ∧ ¬a)

SAT 的重要性

SAT是第一个NP-Complete problem
在应用的角度只要知道NP-Complete problem很难，没办法有效率找到最佳解(但可能可以有效率的找到近似最佳解)，以及NP-Complete problem可以在多项式时间内互相转换(就是说你可以拿一个NP-Complete problem来解另外一个)，这样就够了。
解SAT的方法发展的很好
SAT做为最古老且知名的NP-Complete problem，已经有许多演算法跟技巧被发明出来解它，目前最好的那些SAT solver可以解到上万个变数，我们知道NP-Complete problem可以在多项式时间内互转，而SAT solver的效率又不错，那么SAT自然是很有实用性的。

SAT 的应用

SAT 被应用在如EDA 领域的测试、验证，ai 领域如自动定理证明，网路上还查的到很多，但一时间看不懂所以然的我就不列了，以下举几个例子。

Circuit satisfiability problem
给出一个电路，是否有input能让output为true

# 考虑下列AND gate

C = A . B

# 有对应如下的boolean function

(¬a ∨ ¬b ∨ c)∧(a ∨ ¬c)∧(b ∨ ¬c)

# 思考拼凑一下可以发现能让它satisfiable 的值就是AND gate output true 的值

如果运用这种方法，就可以堆积出复杂电路的boolean function，可以测试一个电路能不能output true，也就是说能知道它会不会是无用的电路(可以化简)。

这种方法叫做Tseitin transformation，有兴趣可参考wiki: https://en.wikipedia.org/wiki/Tseytin_transformation

四色问题
如果地图上相邻的两个区域不能画相同的颜色，那不管这张地图多复杂，最少都可以用四种颜色画出它。

# 考虑区域1跟2相邻

# 下列四个变数代表区域1能被画的颜色

R1 B1 G1 Y1

# R1 B1 G1 Y1 只能有一个为true

(¬R1 ∨ ¬B1)∧

(¬R1 ∨ ¬G1)∧

(¬R1 ∨ ¬Y1)∧

(¬B1 ∨ ¬G1)∧

(¬B1 ∨ ¬Y1)∧

(¬G1 ∨ ¬Y1)

# 区域2相同

R2 B2 G2 Y2

(¬R2 ∨ ¬B2)∧

(¬R2 ∨ ¬G2)∧

(¬R2 ∨ ¬Y2)∧

(¬B2 ∨ ¬G2)∧

(¬B2 ∨ ¬Y2)∧

(¬G2 ∨ ¬Y2)

# 区域1跟区域2不能同颜色

(¬R1 ∨ ¬R2)∧(¬B1 ∨ ¬B2)∧(¬G1 ∨ ¬G2)∧(¬Y1 ∨ ¬Y2)

# 将全部AND 起来，就能得到一个boolean function，

# 一定找的到true 的赋值方式，而且区域1,2不同色，就

# 算区域更多也不会用超过四种颜色。

不过我们知道一张地图的区域最少能用几种颜色画，让相邻的区域不同颜色，这样的事情要干嘛? 当然是有用处的。

例如很多地方都盖了基地台，但只要是相邻的基地台使用相同的频率，就会相互干扰导致收讯不良。因此对应到四色问题，我们知道最少用四种频率的基地台就能解决干扰了。

reference

一个介绍SAT的英文文章

http://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-Python.html

【转】(一) SAT problem 介绍

problems

Boolean Satisfiability Problem

什么是SAT?

SAT 的重要性

SAT 的应用

reference

相关阅读

栏目导航

推荐阅读

热门阅读