所谓2-SAT就是2元可满足性问题。首先，作为众所周知的，任何布尔表达式，都可以化为合取范式的形式，即化为：   () and () and () ...and () 其中括号里面的是用析取符号or 连接的变量或者变量的非的形式。我们一般称，变量或者变量的非为“文字”,而括号里的叫做子句。可满足性问题是要给所有的变量一个赋值（真或假）使得表达式值为真。而2元可满足性问题，就是化为合取范式后，每个子句最多有两个文字的可满足性问题。

 

      cook定理已经说明，一般地可满足性问题是NPC的。但是值得注意的是，2-SAT却是P的。简单分析一下2-SAT: 它要求每个子句的值都是真。考虑一个子句，a or b ，显然如果a取false，则b一定取true，反之亦然。先给出算法：

 

      假设2-SAT问题中有N个变量，则构造一个有向图包含2n个节点。每个节点代表一个变量或者变量的非（即代表一个文字）。对每个子句a or b,在途中加2条有向边 (~a,b)和(~b,a)  (其中~表示变量的非)。然后对这个有向图求强连通分量，把每个强连通分量看作一个点（缩点），这样新的有向图是无环的（无环有向图又叫DAG）。

如果一个强连通分量里同时包含了同一个变量以及它的非，则原问题是不可满足的。否则，我们可以构造解，对这个DAG可以进行拓扑排序，按照节点的拓扑排序顺序的倒序进行如下操作：找到此顺序中第一个没有标记的节点，把此节点标记成true，并且把和此节点矛盾的节点（一个节点包含了a，另外一个节点包含了~a，则称它们是矛盾的），以及祖先标记成false，直到所有节点都有标记，结束。这些标记也对应着变量的取值。

 

     大概不严谨地证明一下，首先同一个强连通分量里的文字是等价的。因为对一个子句a or b，按照一个取假，另外一个一定取真的意思，连的边表示逻辑中的“蕴含”关系，即有~a->b  ，~b->a。这样一个强连通分量里的文字互相蕴含，所以是等价的。于是，当存在a->~a->a时，显然原问题不可满足。

 

     第二，因为每标记一个true，立刻把与它矛盾的并且“反向蕴含”的点都设置为false，所以，这样的赋值不会产生矛盾。

 

      第三，不会把一个变量和它的非都设置为false。

 

    这是因为，考虑设置变量为false时，假设设置a为true，沿着“反向蕴含链”把x设置为false了，这说明有x->~a,由于对称性，有a->~x  （这里的->表示有路相连，并不一定是一条边），按照算法流程必须要先考虑~x （拓扑排序的逆序），可见这时~x应该已经被设置为true了，因为否则的话，如果~x=false，则会沿着“反向蕴含链”把a也设置为false的，根本不会到考虑a为true的这一步骤了。于是，设置false是安全的。

 

    综上所述，该算法可以找到一组2-SAT的可行解，或者判断无解。该算法的复杂度：求强连通分量、拓扑排序、以及遍历图都是O(m)的，其中m是边数。