[蒟蒻修炼计划][模板] 2-SAT

Posted 2020-07-27 Aireen Ye

昨天早上在准备省队集训，发现自己连2-SAT是什么都不知道，于是一早上都投身于2-SAT模板中，终于有个结果。

思路如下：

1.根据条件表达式建边；

2.缩环；

3.判断是否可行；

4.根据缩完环的图反向建边；

5.拓扑排序进行染色(1表示true,2表示false)。

  1 /*假设输入是无空格无括号的的c++条件表达式且未知数用编号代替*/
  2 #include<set> 
  3 #include<cmath>
  4 #include<ctime>
  5 #include<queue>
  6 #include<stack>
  7 #include<cstdio>
  8 #include<vector>
  9 #include<cstring>
 10 #include<cstdlib>
 11 #include<iostream>
 12 #include<algorithm>
 13 #define L 11
 14 #define N 100001
 15 #define M 1000001
 16 using namespace std;
 17 struct graph{
 18     int nxt,to;
 19 }e[M],gra[M];
 20 int sol[N],col[N];
 21 int f[N],dfn[N],low[N],sta[N];
 22 int g[N],go[N],to[N],n,m,nn,cnt;
 23 bool ins[N];char c[L];queue<int> q;
 24 inline addedge(int x,int y){
 25     e[++cnt].nxt=g[x];g[x]=cnt;e[cnt].to=y;
 26 }
 27 inline adde(int x,int y){
 28     gra[++cnt].nxt=go[x];go[x]=cnt;gra[cnt].to=y;
 29 }
 30 inline void type(){
 31     int l=strlen(c),i=0,x=0,y=0;
 32     bool flag1=true,flag2=true;
 33     if(c[i]==‘!‘){
 34         flag1=false;i++;
 35     }
 36     while(i<l&&c[i]>=‘0‘&&c[i]<=‘9‘)
 37         x=x*10+c[i++]-‘0‘;
 38     if(i==l){
 39         if(flag1) addedge(x+n,x);
 40         else addedge(x,x+n);
 41         return;
 42     }
 43     char cha=c[i];i++;
 44     if(c[i]==‘!‘){
 45         flag2=false;i++;
 46     }
 47     while(i<l&&c[i]>=‘0‘&&c[i]<=‘9‘)
 48         y=y*10+c[i++]-‘0‘;
 49     if(cha==‘&‘){
 50         if(flag1&&flag2){
 51             addedge(x+n,x);
 52             addedge(y+n,y);
 53         }
 54         else if(flag1){
 55             addedge(x+n,x);
 56             addedge(y,y+n);
 57         }
 58         else if(flag2){
 59             addedge(x,x+n);
 60             addedge(y+n,y);
 61         }
 62         else{
 63             addedge(x,x+n);
 64             addedge(y,y+n);
 65         }
 66     }
 67     else if(cha==‘|‘){
 68         if(flag1&&flag2){
 69             addedge(x+n,y);
 70             addedge(x,y+n);
 71         }
 72         else if(flag1){
 73             addedge(x+n,y+n);
 74             addedge(y,x);
 75         }
 76         else if(flag2){
 77             addedge(x,y);
 78             addedge(y+n,x+n);
 79         }
 80         else{
 81             addedge(x,y+n);
 82             addedge(y,x+n);
 83         }
 84     }
 85     else if(cha==‘^‘){
 86         if(flag1&&flag2){
 87             addedge(x,y+n);
 88             addedge(x+n,y);
 89             addedge(y,x+n);
 90             addedge(y+n,x);
 91         }
 92         else if(flag1){
 93             addedge(x,y);
 94             addedge(x+n,y+n);
 95             addedge(y,x);
 96             addedge(y+n,x+n);
 97         }
 98         else if(flag2){
 99             addedge(x,y);
100             addedge(x+n,y+n);
101             addedge(y,x);
102             addedge(y+n,x+n);
103         }
104         else{
105             addedge(x,y+n);
106             addedge(x+n,y);
107             addedge(y,x+n);
108             addedge(y+n,x);
109         }
110     }
111 }
112 inline void tarjan(int u){
113     dfn[u]=low[u]=++cnt;
114     sta[++sta[0]]=u;ins[u]=true;
115     for(int i=g[u];i;i=e[i].nxt)
116         if(!dfn[e[i].to]){
117             tarjan(e[i].to);
118             low[u]=min(low[u],low[e[i].to]);
119         }
120         else if(ins[e[i].to])
121             low[u]=min(low[u],low[e[i].to]);
122     if(dfn[u]==low[u]){
123         while(sta[sta[0]+1]!=u){
124             f[sta[sta[0]]]=u;
125             ins[sta[0]--]=false;
126         }
127     }
128 }
129 inline bool chk(){
130     for(int i=1;i<=n;i++)
131         if(f[i]==f[i+n]) return false;
132     return true;
133 }
134 inline void build(){
135     cnt=0;
136     for(int i=1;i<=nn;i++)
137         for(int j=g[i];j;j=e[j].nxt){
138             if(f[i]!=f[e[j].to]){
139                 adde(f[e[j].to],f[i]);to[i]++;
140             }
141         }
142 }
143 inline void toposort(){
144     for(int i=1;i<=nn;i++)
145         if(f[i]==i&&!to[i]) q.push(i);
146     while(!q.empty()){
147         int u=q.front();q.pop();
148         if(!col[u]){
149             col[u]=1;col[u+n]=-1;
150         }
151         for(int i=go[u];i;i=gra[i].nxt)
152             if(!(--to[gra[i].to]))
153                 q.push(gra[i].to);
154     }
155 }
156 inline void init(){
157     scanf("%d%d",&n,&m);
158     for(int i=1;i<=m;i++){
159         scanf("%s",&c);type();
160     }
161     nn=n<<1;cnt=0;
162     for(int i=1;i<=nn;i++)
163         if(!dfn[i]) tarjan(i);
164     if(!chk()){
165         printf("No solution.\n");
166         return;
167     }
168     build();
169     toposort();
170     for(int i=1;i<=n;i++)
171         col[i]=col[f[i]];
172     for(int i=1;i<=n;i++)
173         if(col[i]>0) printf("%d:true\n",i);
174         else printf("%d:false\n",i);
175 }
176 int main(){
177     freopen("2sat.in","r",stdin);
178     freopen("2sat.out","w",stdout);
179     init();
180     fclose(stdin);
181     fclose(stdout);
182     return 0;
183 }