2-sat

 1 #include <stack>
 2 #include <cstdio>
 3 #include <vector>
 4 #include <cstring>
 5 #include <algorithm>
 6 using namespace std;
 7 
 8 const int maxn = 2000 + 2;
 9 const int maxm = 4000000 + 2;
10 
11 stack<int> s;
12 bool in[maxn];
13 vector<int> G[maxn];
14 int n, m, scc, Index, dfn[maxn], low[maxn], belong[maxn];
15 
16 void tarjan(int now){
17     dfn[now] = low[now] = ++ Index;
18     in[now] = true, s.push(now);
19 
20     for (int i = 0, len = G[now].size(), to; i < len; i ++){
21         to = G[now][i];
22         if (!dfn[to]){
23             tarjan(to);
24             low[now] = min(low[now], low[to]);
25         }
26 
27         else if (in[to])
28             low[now] = min(low[now], dfn[to]);
29     }
30 
31     if (low[now] == dfn[now]){
32         ++ scc;    
33 
34         int u;
35         do {
36             u = s.top();
37             s.pop(), in[u] = false;
38             belong[u] = scc;
39         } while (u ^ now);
40     }
41 }
42 
43 inline void init(){
44     memset(low, 0, sizeof low);
45     memset(dfn, 0, sizeof dfn);
46     memset(in, false, sizeof in);
47     Index = scc = 0;
48     while (not s.empty())
49         s.pop();
50     for (int i = 0; i < 2 * n; i ++)
51         G[i].clear();
52 
53     for (int i = 0, a, b, x, y, g1, g2; i < m; i ++){
54         scanf("%d %d %d %d", &a, &b, &g1, &g2);
55 
56         x = a * 2 + 1 - g1, y = b * 2 + 1 - g2;
57         a = a * 2 + g1, b = b * 2 + g2;
58 
59         G[a].push_back(y), G[b].push_back(x);
60     }
61 }
62 
63 inline bool two_sat(){
64     init();
65     for (int i = 0; i < n * 2; i ++)
66         if (!dfn[i])
67             tarjan(i);
68 
69     for (int i = 0; i < n; i ++)
70         if (belong[i * 2] == belong[i * 2 + 1])
71             return false;
72 
73     return true;
74 }
75 
76 int main(){
77     while (scanf("%d %d", &n, &m) == 2)
78         puts(two_sat() ? "YES" : "NO");
79 }