| 10 | void add_or(int x, int y) { |
| 11 | V[n-x].adj.push_back(n+y), V[n-y].adj.push_back(n+x); } |
| 12 | int dfs(int u) { |
| 13 | int br = 2, res; |
| 14 | S.push_back(u), V[u].num = V[u].lo = at++; |
| 15 | iter(v,V[u].adj) { |
| 16 | if (V[*v].num == -1) { |
| 17 | if (!(res = dfs(*v))) return 0; |
| 18 | br |= res, V[u].lo = min(V[u].lo, V[*v].lo); |
| 19 | } else if (!V[*v].done) |
| 20 | V[u].lo = min(V[u].lo, V[*v].num); |
| 21 | br |= !V[*v].val; } |
| 22 | res = br - 3; |
| 23 | if (V[u].num == V[u].lo) rep(i,res+1,2) { |
| 24 | for (int j = (int)size(S)-1; ; j--) { |
| 25 | int v = S[j]; |
| 26 | if (i) { |
| 27 | if (!put(v-n, res)) return 0; |
| 28 | V[v].done = true, S.pop_back(); |
| 29 | } else res &= V[v].val; |
| 30 | if (v == u) break; } |
| 31 | res &= 1; } |
| 32 | return br | !res; } |
| 33 | bool sat() { |
| 34 | rep(i,0,2*n+1) |
| 35 | if (i != n && V[i].num == -1 && !dfs(i)) return false; |