2-SAT问题（白书）

1. 定义

给定一个布尔方程，判断是否存在一组布尔变量的真值指派使整个方程为真的问题，被称为布尔方程的可满足性问题(SAT)。SAT问题是NP完全的，但对于满足一定限制条件的SAT问题，还是能够有效求解的。

如果合取范式的每一个子句中的文字个数不超过两个，那么对应的SAT问题可以称为2-SAT问题。

(a∨b)∧¬a$(a\vee b)\wedge \mathrm{\neg }a$ 令a为假而b为真，则可以满足
(a∨¬b)∧(b∨c)∧(¬c∨¬a)$(a\vee \mathrm{\neg }b)\wedge (b\vee c)\wedge (\mathrm{\neg }c\vee \mathrm{\neg }a)$ 令a和b为真，而c为假，则可以满足

利用强联通分量分解，可以在布尔公式子句数的线性时间内解决2-SAT问题

首先利用⇒$\Rightarrow$(蕴含）将每一个子句(a∨b)$(a\vee b)$ 改写成等价的(¬a⇒b)∧(¬b⇒a)$(\mathrm{\neg }a\Rightarrow b)\wedge (\mathrm{\neg }b\Rightarrow a)$
对于每个布尔变量x，构造两个顶点分别代表x和¬x$\mathrm{\neg }x$，以⇒$\Rightarrow$关系为有向边，建立有向图。此时，如果a点能够到达b点，就表示当a为真时b也为真。因此图中的同一个强联通分量中的所有布尔值均相同。

如果存在某个布尔变量x，x和¬x$x和\mathrm{\neg }x$均在同一个强联通分量中，则显然无法令整个布尔公式的值为真。反之，如果不存在这样的布尔变量，那么对于每个布尔变量x，让

x所在的强联通分量的拓扑序在¬x所在的强联通分量之后⇔x为真$x所在的强联通分量的拓扑序在\mathrm{\neg }x所在的强联通分量之后\iff x为真$

就是使得该公式的值为真的一组适合的布尔变量赋值。

2. 题目讲解

(1)POJ 3683