POJ 3678 - Katu Puzzle 比较典型的构图2-sat...求是否有可行解

题意:

有N个Xi...又告诉M个位运算( AND OR XOR )结果..问是否有存在可行解

题解

每个Xi就两种情况..并且必须选择一个..符合2-sat的模型..那剩下就是根据运算式构造边了...这里要进一步理解2-sat中一条有向边的涵义是选了起点就必须选终点..那剩下的就好办了一个一个分析...

x,y代表当前的式子未知数..x0为x选0的点..x1为x选1的点...y0,y1同样..

2、x AND y = 0 ..表明x,y至少有一个为0...那么加边 ( x1,y0 ) , ( y1,x0 )

3、x OR y = 1 ...表明x,y至少有一个味1..那么加边 ( x0,y1 ) , ( y0,x1 )

4、x OR y = 0..表明x,y都为0...所以让选择x1,y1就直接自矛盾 ( x1,x0 ) , ( y1,y0 )

5、x XOR y = 1..表明x,y不同..那么加边 ( x0,y1 ) , ( x1,y0 ) ,( y0,x1 ) , ( y1,x0 )

6、x XOR y = 0..表明x,y是相同的..那么加边 ( x0,y0 ) , ( x1,y1 ) ,( y0,x0 ) , ( y1,x1 )

构造好边后...跑一边tarjan..判断是否有 x0,y1在一个强联通分量里..在就说明没得结果..没在说明是存在至少一组解的...

Program:

#include<iostream>
#include<stdio.h>
#include<string.h>
#include<cmath>
#include<queue>
#include<stack>
#include<set>
#include<algorithm>
#define ll long long
#define oo 1000000007
#define pi acos(-1.0)
#define MAXN 1005
#define MAXM 5000000
using namespace std;
struct node
{
       int x,y,next;
}line[MAXM];
int _next[MAXN],lnum,dfn[MAXN],low[MAXN],tp[MAXN],tpnum,DfsIndex;
bool instack[MAXN];
stack<int> mystack;
void addline(int x,int y)
{
       line[++lnum].next=_next[x],_next[x]=lnum;
       line[lnum].x=x,line[lnum].y=y;
}
void inputdata(int n,int m)
{
       int x,y,c,x0,x1,y0,y1;
       lnum=0;
       char s[5];
       while (m--)
       {
              scanf("%d%d%d%s",&x,&y,&c,s);
              x0=x<<1,x1=x0|1,y0=y<<1,y1=y0|1;
              if (s[0]=='A') // AND
              {
                    if (c) addline(x0,x1),addline(y0,y1);
                      else addline(y1,x0),addline(x1,y0);
              }else
              if (s[0]=='O') // OR
              {
                    if (c) addline(x0,y1),addline(y0,x1);
                      else addline(x1,x0),addline(y1,y0);
              }else
              if (s[0]=='X') // XOR
              {
                    if (c) addline(x0,y1),addline(x1,y0),addline(y0,x1),addline(y1,x0);
                      else addline(x0,x0),addline(x1,y1),addline(y0,y0),addline(y1,x1);
              }
       }
       return;
}
void tarjan(int x)
{
       int y,k;
       dfn[x]=low[x]=++DfsIndex;
       instack[x]=true;
       mystack.push(x);
       for (k=_next[x];k;k=line[k].next)
       {
               y=line[k].y;
               if (!dfn[y])
               {
                      tarjan(y);
                      low[x]=min(low[x],low[y]);
               }else
               if (instack[y])
                      low[x]=min(low[x],dfn[y]);
       }
       if (low[x]==dfn[x])
       {
               tpnum++;
               do
               {
                     x=mystack.top();
                     mystack.pop();
                     tp[x]=tpnum;
                     instack[x]=false;
               }while (low[x]!=dfn[x]);
       }
       return;
}
bool judge(int n)
{
       int i;
       for (i=0;i<n;i++)
          if (tp[i<<1]==tp[(i<<1)|1]) return false;
       return true;
}
int main()
{
       int n,m; 
       while (~scanf("%d%d",&n,&m))
       {
                memset(_next,0,sizeof(_next));
                inputdata(n,m);
                memset(dfn,0,sizeof(dfn));
                memset(instack,false,sizeof(instack));
                while (!mystack.empty()) mystack.pop();
                DfsIndex=tpnum=0;
                for (int i=0;i<(n<<1);i++)
                   if (!dfn[i]) tarjan(i);
                if (judge(n)) printf("YES\n");
                       else  printf("NO\n");
       }
       return 0;
}