昨天早上在准备省队集训，发现自己连2-SAT是什么都不知道，于是一早上都投身于2-SAT模板中，终于有个结果。
思路如下：
1.根据条件表达式建边；
2.缩环；
3.判断是否可行；
4.根据缩完环的图反向建边；
5.拓扑排序进行染色(1表示true,2表示false)。
时间复杂度：O(n+m)
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. "); 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 ",i); 174 else printf("%d:false ",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 }