每条约束至多两个文字

文字是变量或变量的否定。2-CNF公式例如(p∨q)∧(¬p∨r)∧(¬r∨q),要求三个析取子句同时为真;“2”限制每个子句的宽度,不是限制整个公式只有两个变量。单文字约束p也可写成p∨p,不超出这个范围。

子句a∨b与¬a→b、¬b→a同时成立等价。因此,每个变量建立正、负两个顶点,再为每个子句加入这两条有向边。沿路径连续推出的文字,必须与起点的真值选择相容。

参考:[1]

强连通分量中的矛盾

若p和¬p处于同一个强连通分量,就既有从p到¬p的路径,也有反向路径。把其中任一方设真,都会迫使它的否定也真,因此公式不可满足。只有一个方向的路径并不足以判定矛盾,不能把任何相连的正负文字都当成冲突。

反过来,若每个变量的两种文字分属不同分量,就能沿分量凝聚图的拓扑次序构造赋值。按逆拓扑顺序选尚未赋值的分量设真,并把其对偶分量设假;如此避免把已为真的文字引向假文字。这个构造说明检查条件也是充分的。

参考:[1]

线性界限取决于约束形式

若有n个变量、m个至多双文字子句,图只有2n个顶点和至多2m条边。使用线性时间的强连通分量算法,构图、检查和构造解合计O(n+m)。这项结论按显式输入计量,不包含把别的问题强行编码时可能产生的额外规模。

允许每个子句至多三个文字,问题便包含NP完全的3-SAT。2-SAT的图条件不适用于任意长子句;也不能把一个三选一约束随意拆成若干双文字约束而声称保持原问题。公式结构本身是可高效求解的重要前提。

参考:[1] [2]