【模板】2-SAT 问题

SAT以及2-SAT问题是啥以及定义我就不叨叨了，直接讲怎么求。

比如有一个条件：a || b，就是说a，b必须至少有一个为真。这个可以转化为（!a => b && !b => a），那么就可以连边建图了：首先把每一个点x拆成x和!x，那么对于上述条件，连两条边(!a -> b)和(!b -> a)。类似的，对于a和b的其他条件，我们也可以模仿着连边。

接下来怎么判断是否有可行解呢？可以用tarjan强连通分量缩点，对于属于一个强连通分量的点，他们的取值一定都是相同的（就是都是真或者都是假）。那么如果x和!x在一个强连通分量中，则必定无解，因为x为真和!x为真之可能满足一个。

那么接下来应该输出合法的一组解。一般2-SAT问题都有spj，所以任意一组就行。

要分两种情况：

1.如果x的拓扑序在!x前面，那么x一定是0.因为x一定有一条路径通向!x，如果x是1，一定能推出!x是1，也就是x是0，矛盾了。

2.如果x拓扑序在!x后面，那么x必定是1。仿照上述思想，如果!x为真，说明x = 0，能推出x为真，即x = 1，矛盾。如果x = 1,则!x为假，不一定能推出x。所以x必须是1。

不过tarjan缩完点后的拓扑序是反的，所以col[x] < col[x + n]说明x在!x后面；反之同理。

讲完了。

 1 #include<cstdio>
 2 #include<iostream>
 3 #include<algorithm>
 4 #include<cmath>
 5 #include<cstring>
 6 #include<cstdlib>
 7 #include<cctype>
 8 #include<stack>
 9 #include<queue>
10 #include<vector>
11 using namespace std;
12 #define enter puts("")
13 #define space putchar(' ')
14 #define Mem(a, x) memset(a, x, sizeof(a))
15 #define rg register
16 typedef long long ll;
17 typedef double db;
18 const int INF = 0x3f3f3f3f;
19 const db eps = 1e-8;
20 const int maxn = 1e6 + 5;
21 inline ll read()
22 {
23   ll ans = 0;
24   char ch = getchar(), las = ' ';
25   while(!isdigit(ch)) las = ch, ch = getchar();
26   while(isdigit(ch)) ans = ans * 10 + ch - '0', ch = getchar();
27   if(las == '-') ans = -ans;
28   return ans;
29 }
30 inline void write(ll x)
31 {
32   if(x < 0) putchar('-'), x = -x;
33   if(x >= 10) write(x / 10);
34   putchar(x % 10 + '0');
35 }
36 
37 int n, m;
38 struct Edge
39 {
40   int to, nxt;
41 }e[maxn << 1];
42 int head[maxn << 1], ecnt = 0;
43 void addEdge(int x, int y)
44 {
45   e[++ecnt].to = y;
46   e[ecnt].nxt = head[x];
47   head[x] = ecnt;
48 }
49 
50 stack<int> st;
51 bool in[maxn << 1];
52 int dfn[maxn << 1], low[maxn << 1], cnt = 0;
53 int col[maxn << 1], ccol = 0;
54 void tarjan(int now)
55 {
56   dfn[now] = low[now] = ++cnt;
57   st.push(now); in[now] = 1;
58   for(int i = head[now]; i; i = e[i].nxt)
59     {
60       if(!dfn[e[i].to])
61     {
62       tarjan(e[i].to);
63       low[now] = min(low[now], low[e[i].to]);
64     }
65       else if(in[e[i].to]) low[now] = min(low[now], dfn[e[i].to]);
66     }
67   if(dfn[now] == low[now])
68     {
69       int x; ++ccol;
70       do
71     {
72       x = st.top(); st.pop();
73       col[x] = ccol; in[x] = 0;
74     }while(x != now);
75     }
76 }
77 
78 int main()
79 {
80   n = read(); m = read();
81   for(int i = 1; i <= m; ++i)
82     {
83       int x = read(), flg1 = read(), y = read(), flg2 = read();
84       addEdge(x + flg1 * n, y + (flg2 ^ 1) * n);
85       addEdge(y + flg2 * n, x + (flg1 ^ 1) * n);
86     }
87   for(int i = 1; i <= (n << 1); ++i) if(!dfn[i]) tarjan(i);
88   for(int i = 1; i <= n; ++i) if(col[i] == col[n + i])
89       printf("IMPOSSIBLE
"); return 0;
90     }
91   printf("POSSIBLE
");
92   for(int i = 1; i <= n; ++i) write(col[i] < col[i + n]), space;
93   enter;
94   return 0;
95 }

View Code