| 1 | struct { vi adj; int val, num, lo; bool done; } V[2*1000+100]; |
| 2 | struct TwoSat { |
| 3 | int n, at = 0; vi S; |
| 4 | TwoSat(int _n) : n(_n) { |
| 5 | rep(i,0,2*n+1) |
| 6 | V[i].adj.clear(), |
| 7 | V[i].val = V[i].num = -1, V[i].done = false; } |
| 8 | bool put(int x, int v) { |
| 9 | return (V[n+x].val &= v) != (V[n-x].val &= 1-v); } |
| 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; |
| 36 | return true; } }; |
| 37 | // vim: cc=60 ts=2 sts=2 sw=2: |
nothing calls this directly
no outgoing calls
no test coverage detected