博文
SAT问题简介
||
SAT问题是“布尔逻辑可满足性问题（boolean SATisfiability problem）”的简称，指给定一个合取范式公式f，判断其是否可满足，即找出布尔变量真值赋值，使得公式f为真。
一，SAT问题
1，基本概念
布尔变量（Boolean variables）：取值为真值 {0，1}的变量，x1，x2，…… xn，
文字（Literals） : x1, ¬x1, x2, ¬x2, …
子句（Disjunctive clause）：一个或多个文字的析取式：x1∨¬x2∨x3
合取范式公式（Formula Conjunctive Normal Form， CNF)：一个或多个子句的合取式
2，合取范式公式的3个重要参数
每个子句中的变元数；
变元数；
子句数。
3，3SAT与2SAT
二类SAT问题：
- 3SAT问题：子句只有3个变元的SAT问题。
- 2SAT问题：子句只有2个变元的SAT问题。
4，例子
3SAT例子：
f1 = (x1 ∨x2 ∨x3)∧(x1 ∨x2 ∨¬x3)∧(¬x1 ∨¬x2 ∨ x3) ∧ (¬x1 ∨ x2 ∨ x3)
f1是可满足，有四个解：
x1 =0, x2=1, x3=0;
x1 =0, x2=1, x3=1;
x1 =1, x2=0, x3=1;
x1 =1, x2=1, x3=1
用真值表图示f1的四个解：
x1 | x2 | x3 | x1∨x2∨x3 | x1∨x2∨¬x3 | ¬x1∨¬x2∨x3 | ¬x1∨x2∨x3 | f1 |
0 | 0 | 0 | 0 | 1 | 1 | 1 | 0 |
0 | 0 | 1 | 1 | 0 | 1 | 1 | 0 |
0 | 1 | 0 | 1 | 1 | 1 | 1 | 1 |
0 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
1 | 0 | 0 | 1 | 1 | 1 | 0 | 0 |
1 | 0 | 1 | 1 | 1 | 1 | 1 | 1 |
1 | 1 | 0 | 1 | 1 | 0 | 1 | 0 |
1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
二，SAT问题的实例的标准表示
实例f1的标准表示
将变元编号：
x1: 1; x2: 2 x3: 3
¬x1: -1; ¬x2: -2 ¬x3: -3
p cnf 3（变元数） 4（子句数）
1 2 3 0
1 2 -3 0
-1 -2 3 0
-1 2 3 0
更多的例子可以参考SAT问题例子库：
https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
比如：uf-20-02文件
p cnf 20 91
-10 -16 5 0
16 -6 5 0
-17 -14 -18 0
-10 -15 19 0
-1 -9 -18 0
3 7 -6 0
-13 1 6 0
-2 -16 -20 0
7 8 18 0
-7 10 -20 0
2 -14 -17 0
2 1 19 0
7 -20 -1 0
-11 1 -17 0
3 -12 19 0
-3 -13 6 0
-13 3 -12 0
5 -7 -12 0
20 8 -16 0
-13 -6 19 0
-5 1 14 0
9 -5 18 0
-12 -17 -1 0
-20 -16 19 0
12 10 -11 0
6 -7 -2 0
13 -10 17 0
-20 8 -16 0
-10 -1 -8 0
-7 -3 19 0
19 -1 -6 0
19 -2 13 0
-2 20 -9 0
-8 -20 16 0
-13 -1 11 0
15 -12 -6 0
-17 -19 9 0
19 -18 16 0
7 -8 -19 0
-3 -7 -1 0
7 -17 -16 0
-2 -14 1 0
-18 -10 -8 0
-16 5 8 0
4 8 10 0
-20 -11 -19 0
8 -16 -6 0
18 12 8 0
-5 -20 -10 0
16 17 3 0
7 -1 -17 0
17 -4 7 0
20 -9 -13 0
13 18 16 0
-16 -6 5 0
5 17 7 0
-12 -17 -6 0
-20 19 -5 0
9 -19 16 0
-13 -16 11 0
-4 -19 -18 0
-13 10 -15 0
16 -7 -14 0
-19 -7 -18 0
-20 5 13 0
12 -6 4 0
7 9 -13 0
16 3 7 0
9 -1 12 0
-3 14 7 0
1 15 14 0
-8 -11 18 0
19 -9 7 0
-10 6 2 0
14 18 -11 0
-9 -16 14 0
1 11 -20 0
11 12 -4 0
13 -11 -14 0
17 -12 9 0
14 9 1 0
8 19 4 0
6 -13 -20 0
-2 -13 11 0
14 -13 17 0
9 -11 18 0
-13 -6 5 0
5 19 -18 0
-4 10 11 0
-18 -19 -20 0
3 -9 8 0
%
0
https://wap.sciencenet.cn/blog-2322490-1403730.html
上一篇：SAT问题与乔治-布尔
下一篇：笛卡尔的“良知（bon sens）”与王阳明与“致良知”
