SAT问题是“布尔逻辑可满足性问题（boolean SATisfiability problem）”的简称，指给定一个合取范式公式f，判断其是否可满足，即找出布尔变量真值赋值，使得公式f为真。

一，SAT问题

1，基本概念

布尔变量（Boolean variables）：取值为真值 {0，1}的变量，x₁，x₂，…… x_n，

文字（Literals） : x₁, ¬x₁, x₂, ¬x₂, …

子句（Disjunctive clause）：一个或多个文字的析取式：x₁∨¬x₂∨x₃

合取范式公式（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的四个解：

二，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