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

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

(a∨b)∧¬a" role="presentation" style="position: relative;">(a∨b)∧¬a(a∨b)∧¬a 令a为假而b为真，则可以满足

(a∨¬b)∧(b∨c)∧(¬c∨¬a)" role="presentation" style="position: relative;">(a∨¬b)∧(b∨c)∧(¬c∨¬a)(a∨¬b)∧(b∨c)∧(¬c∨¬a) 令a和b为真，而c为假，则可以满足

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

首先利用⇒" role="presentation" style="position: relative;">⇒⇒(蕴含）将每一个子句(a∨b)" role="presentation" style="position: relative;">(a∨b)(a∨b) 改写成等价的(¬a⇒b)∧(¬b⇒a)" role="presentation" style="position: relative;">(¬a⇒b)∧(¬b⇒a)(¬a⇒b)∧(¬b⇒a)

对于每个布尔变量x，构造两个顶点分别代表x和¬x" role="presentation" style="position: relative;">¬x¬x，以⇒" role="presentation" style="position: relative;">⇒⇒关系为有向边，建立有向图。此时，如果a点能够到达b点，就表示当a为真时b也为真。因此图中的同一个强联通分量中的所有布尔值均相同。

如果存在某个布尔变量x，x和¬x" role="presentation" style="position: relative;">x和¬xx和¬x均在同一个强联通分量中，则显然无法令整个布尔公式的值为真。反之，如果不存在这样的布尔变量，那么对于每个布尔变量x，让

x所在的强联通分量的拓扑序在¬x所在的强联通分量之后⇔x为真" role="presentation" style="position: relative;">x所在的强联通分量的拓扑序在¬x所在的强联通分量之后⇔x为真x所在的强联通分量的拓扑序在¬x所在的强联通分量之后⇔x为真

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

(1)POJ 3683