POJ 3678 2SAT基础题

题目大意：

　　有一个大小为N的集合={x1,x2..xn}，xi=0或1，现在给出它们之间的一些逻辑运算的结果(比如x1 and x2=1)，逻辑运算有AND OR XOR三种，问是否存在一种满足所有条件的取值方案。

分析：

　　（这题开始我构图出错了，叫lin神看了下，他提出一个观点，如果类似 u，v，1 AND这样的数据，说明u，v的1必须都选，那么就把u的0连向u的1,v的0连向v的1，这样的目的是使得推出矛盾）

　　由于集合中的每个元素只有两种选择，要么为0，要么为1，所以可以将这个问题转化成一个2-sat判定问题。对于集合中的每个元素，看做两个点:i和i+n。i表示这个元素取0，i+n表示这个元素取1。那么，剩下的问题就是如何构图了。

　　首先，理解清楚求解2-sat的方法是很必要的。求解2-sat的方法是，构造出一个图，图中的有向边<x,y>表示选x时必须选y。只有这个图满足这个条件，并且所有的边都是对称的（假如原问题能转化成2-sat判定，那么图中的边必然是对称的），那么就可以利用求强连通分量缩点的方法来验证2-sat问题。

对于本题，我们逐个考虑每个逻辑运算：

1、A AND B=0.这要求A和B不同时为1。既然不同时为1，那么A取1时，B必须取0；B取1时，A必须取0.所以，要连得边便是A+n->B, B+n->A。

2、A AND B=1.这要求A和B同时为1。换句话说，A和B不能是0.那要怎么样体现在图中呢？我们知道，判断一个2-sat问题是否存在合法方案的方法是，缩点后判断有没有两个同组点属于同一个连通分量。我们需要A和B都必须是1，那么我们就让A和B必须选0时无解即可。也就是说，连边A->A+n, B->B+n。这样的话，假如构图完成后，A必须取0，那么由于存在边A->A+n，所以A也必须取1，那么就不可能是一个合法方案。所以，这两条边能保证，有合法方案的话，一定是A取1（选A+n节点）的情况。

3、A OR B=0.这要求A和B同时为0.方法和2类似，方向变一下而已，理由同上。

4、A XOR B=0.这要求A=B。所以，A为0时，B必须为0，同理B为0时，A必须为0.所以添加边：A->B,B->A,A+n->B+n,B+n->A+n。

以上的分析过程是摘自上面的链接博客，自己必须深刻体会，并在今后中会应用，尤其是第2点和第3点，而其他的就是要注意有什么限制就连什么边，不能多连，也不能少连。。

代码：

poj3678

  1 /*3678    Accepted    488K    141MS    C++    3238B    2012-04-25 13:26:00*/
  2 #include <cstdio>
  3 #include <cstring>
  4 #include <cmath>
  5 #include <iostream>
  6 #include <algorithm>
  7 #include <vector>
  8 using namespace std;
  9 
 10 #define mpair make_pair
 11 #define pii pair<int,int>
 12 #define MM(a,b) memset(a,b,sizeof(a));
 13 typedef long long lld;
 14 typedef unsigned long long u64;
 15 template<class T> bool up_max(T& a,const T& b){return b>a? a=b,1 : 0;}
 16 template<class T> bool up_min(T& a,const T& b){return b<a? a=b,1 : 0;}
 17 #define maxn 2020
 18 
 19 int n,m;
 20 vector<int> adj[maxn];
 21 
 22 int Bcnt, Index, Top;
 23 int low[maxn], dfn[maxn];
 24 bool instack[maxn];
 25 int belong[maxn],stack[maxn];
 26 void Tarjan(int u){
 27     low[u]= dfn[u]= ++Index;
 28     stack[++Top]= u;
 29     instack[u]= 1;
 30     for(int i=0;i<adj[u].size();++i){
 31         int v= adj[u][i];
 32         if( !dfn[v] ){
 33             Tarjan( v );
 34             up_min( low[u], low[v] );
 35         }
 36         else if( instack[v] )
 37             up_min( low[u], dfn[v] );
 38     }
 39     if( low[u] == dfn[u] ){
 40         ++Bcnt;
 41         int v;
 42         do{
 43             v= stack[Top--];
 44             instack[v]= 0;
 45             belong[v]= Bcnt;
 46         }while( u!=v );
 47     }
 48 }
 49 
 50 int main()
 51 {
 52     while( cin>>n>>m ){
 53         for(int i=1;i<=n+n;++i) adj[i].clear();
 54         for(int i=1;i<=m;++i){
 55             int u,v,w; char ch[10];
 56             scanf("%d%d%d%s", &u, &v, &w, ch);
 57             ++u, ++v;
 58             /// u+u-1: 0;  u+u: 1;
 59             if( *ch == 'A' ){
 60                 if( 1==w ){
 61                     adj[u+u].push_back( v+v );
 62                     adj[v+v].push_back( u+u );
 63                     adj[u+u-1].push_back( u+u );
 64                     adj[v+v-1].push_back( v+v );
 65                 }
 66                 else{
 67                     adj[u+u].push_back( v+v-1 );
 68                     adj[v+v].push_back( u+u-1 );
 69                 }
 70             }
 71             else if( *ch == 'O' ){
 72                 if( 1==w ){
 73                     adj[u+u-1].push_back( v+v );
 74                     adj[v+v-1].push_back( u+u );
 75                 }
 76                 else{
 77                     adj[u+u-1].push_back( v+v-1 );
 78                     adj[v+v-1].push_back( u+u-1 );
 79                     adj[u+u].push_back( u+u-1 );
 80                     adj[v+v].push_back( v+v-1 );
 81                 }
 82             }
 83             else if( *ch == 'X' ){
 84                 if( 1==w ){
 85                     adj[u+u].push_back( v+v-1 );
 86                     adj[v+v].push_back( u+u-1 );
 87                     adj[u+u-1].push_back( v+v );
 88                     adj[v+v-1].push_back( u+u );
 89                 }
 90                 else{
 91                     adj[u+u].push_back( v+v );
 92                     adj[v+v].push_back( u+u );
 93                     adj[u+u-1].push_back( v+v-1 );
 94                     adj[v+v-1].push_back( u+u-1 );
 95                 }
 96             }
 97         }
 98 
 99         Bcnt= Index= Top= 0;
100         for(int i=1;i<=n+n;++i) low[i]= dfn[i]= instack[i]= 0;
101         for(int i=1;i<=n+n;++i)
102             if( !dfn[i] )
103                 Tarjan( i );
104         for(int i=1;i<=n;++i){
105             if( belong[i+i-1] == belong[i+i] ){
106                 puts("NO"); break;
107             }
108             if( i==n ) puts("YES");
109         }
110     }
111 }

一毛原创作品，转载请注明出处。