2-SAT 问题

2-SAT(2-satisfiability,二元可满足性)是布尔可满足性问题的一个重要特例,其中每个约束子句恰好由两个文字通过或运算连接。与一般 SAT 属于 NP 完全不同,2-SAT 存在线性时间的高效算法,既能判定是否存在满足所有子句的变量赋值,也能在有解时构造出具体方案。

概述

2-SAT 问题把每个布尔变量拆成真、假两个节点,每个二元子句都等价于两条蕴含关系。将全部蕴含关系建成有向图后,一个变量的真、假节点是否处于同一强连通分量,就决定了问题是否有解。它是竞赛与实际工程中处理二值约束的利器。

核心原理

• 建图:子句 a 或 b 等价于两条蕴含边,即非 a 推出 b,非 b 推出 a,共同构成蕴含图。
• 矛盾判定:若某变量的真节点与假节点落在同一个强连通分量中,说明存在无法调和的矛盾,问题无解。
• 求解构造:对图求强连通分量并缩点得到有向无环图,按拓扑逆序为每个变量选择所在分量更靠后的取值,即可得到一组合法解。
• 复杂度:建图与求强连通分量均为线性,整体时间与变量和子句数量成正比。

应用场景

2-SAT 常用于处理成对的二值选择约束,如排班中的互斥安排、平面图元素的左右放置、区间的取舍冲突、开关电路的一致性检验等。凡是每条约束都能表述为两个二元选项之间蕴含关系的问题,都可尝试转化为 2-SAT 求解。

常见问题

问:为什么 2-SAT 能高效而一般 SAT 不能?答:二元子句可精确转化为蕴含关系并用图论工具刻画,而三元及以上子句无法简化为这种成对蕴含结构,一般 SAT 因此保持 NP 完全。

问:求强连通分量常用什么算法?答:通常使用 Tarjan 算法或 Kosaraju 算法,二者都能在线性时间内完成强连通分量的划分。