初始2-SAT那时还是在研一时上了一门叫做计算复杂性的课，教材是一本英文的书，很难。当时，第一次接触了不可判定的问题，疯狂地看了很多东西。又系统地学习了复杂度类P,NP(C)，受益颇多。3-SAT就是NPC了，而2-SAT确是P的。

 

       所谓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是边数。

 

    从网上找了段2-SAT的C++类的代码，修改了一下：

 

 

 

 

 

 

#include

 

#include

 

#include

 

#include

 

using namespace std;

 

 

 

const int N = 5050; //最大人数

 

const int inf=6000001;

 

class SAT

 

{

 

 private:

 

  vector g[N]; //原图边连接情况

 

  int n, M, h[N], id[N]; //id[]表示原图中每个点都属于哪个强连通分量

 

  int cnt, scnt, dfn[N], low[N], cur[N];

 

  int stack[N], top, est[N], etop;

 

  vector tree[N]; //有向无环图的边连接情况(新图)

 

  vector contain[N]; //新图中每个点都包含原图中的哪些点

 

  void dfs(int);

 

  void tsDfs(int);

 

  void topologicalSort();

 

  void colorDfs(int);

 

  void color();

 

  void tagAnswer();

 

  void printAnswer();

 

  void getOneAnswer();

 

  void buildGraph();

 

 public:

 

  void scR();

 

  void build(int);

 

  bool judge();

 

  bool solve();

 

  void make(int,int);

 

  

 

};

 

/*

 

函数build是对原图初始化(根据实际输入情况做相应的更改)

 

*/

 

void SAT::make(int x,int y) { // x || y      负数表示非 1<=|x| , |y| <=M   注意从1开始

 

int x1,x2,y1,y2;

 

 if (x > 0) {

 

  x1 = x - 1;

 

  x2 = x1 + M;

 

 }

 

 else {

 

  x2 = -x - 1;

 

  x1 = x2 + M;

 

 }

 

 if (y > 0 ) {

 

  y1 = y - 1;

 

  y2 = y1 + M;

 

 }

 

 else {

 

  y2 = -y - 1;

 

  y1 = y2 + M;

 

 }

 

 g[x2].push_back(y1);

 

 g[y2].push_back(x1);

 

}

 

 

void SAT::build(int num)   //变量个数

 

{

 

 int i;

 

 M = num;

 

 n = M << 1;

 

 for (i = 0 ; i < n ; ++i) {

 

  g[i].clear();

 

 }

 

 

 

}

 

void SAT::dfs(int src)

 

{

 

 etop = top = 0;

 

 stack[top++] = src;

 

 while(top != 0)

 

 {

 

  int c = stack[top-1];

 

  if(dfn[c] == -1)

 

  {

 

   h[c] = dfn[c] = low[c] = cnt++;

 

   est[etop++] = c;

 

  }

 

  for(; cur[c] >= 0; cur[c]--)

 

  {

 

   int no = g[c][cur[c]];

 

   if(dfn[no] == -1)

 

   {

 

    stack[top++] = no;

 

    break;

 

   }

 

   if (h[c]>low[no]) {

 

    h[c] = low[no];

 

   }

 

  

 

  }

 

  if(cur[c] >= 0)

 

   continue;

 

  top--;

 

  int k;

 

  if(h[c] != low[c])

 

  {

 

   low[c] = h[c];

 

   continue;

 

  }

 

  do

 

  {

 

   k = est[--etop];

 

   id[k] = scnt; low[k] = N;

 

  } while(k != c);

 

  scnt++;

 

 }

 

}

 

/*

 

函数scR和dfs是求原图的强连通分量(代码由wywcgs原创)

 

*/

 

void SAT::scR()

 

{

 

 int i;

 

 memset(dfn, 0xff, sizeof(dfn));

 

 cnt = scnt = 0;

 

 for(i = 0; i < n; i++)

 

 {

 

  cur[i] = g[i].size()-1;

 

  contain[i].clear();

 

 }

 

 for(i = 0; i < n; i++)

 

  if(dfn[i] == -1)

 

   dfs(i);

 

 

 

 /*

 

 统计每个强连通分量都包含哪些点，为后面求可行方案做准备。如果不求可行解，可注释掉。

 

 */

 

 for ( i=0;i