2 SAT
unknown
c_cpp
3 years ago
1.5 kB
4
Indexable
void scc(vector<vector<int>>& g, int* idx) { int n = g.size(), ct = 0; int out[n]; vector<int> ginv[n]; memset(out, -1, sizeof out); memset(idx, -1, n * sizeof(int)); function<void(int)> dfs = [&](int cur) { out[cur] = INT_MAX; for(int v : g[cur]) { ginv[v].push_back(cur); if(out[v] == -1) dfs(v); } ct++; out[cur] = ct; }; vector<int> order; for(int i = 0; i < n; i++) { order.push_back(i); if(out[i] == -1) dfs(i); } sort(order.begin(), order.end(), [&](int& u, int& v) { return out[u] > out[v]; }); ct = 0; stack<int> s; auto dfs2 = [&](int start) { s.push(start); while(!s.empty()) { int cur = s.top(); s.pop(); idx[cur] = ct; for(int v : ginv[cur]) if(idx[v] == -1) s.push(v); } }; for(int v : order) { if(idx[v] == -1) { dfs2(v); ct++; } } } // 0 => impossible, 1 => possible pair<int,vector<int>> sat2(int n, vector<pair<int,int>>& clauses) { vector<int> ans(n); vector<vector<int>> g(2*n + 1); for(auto [x, y] : clauses) { x = x < 0 ? -x + n : x; y = y < 0 ? -y + n : y; int nx = x <= n ? x + n : x - n; int ny = y <= n ? y + n : y - n; g[nx].push_back(y); g[ny].push_back(x); } int idx[2*n + 1]; scc(g, idx); for(int i = 1; i <= n; i++) { if(idx[i] == idx[i + n]) return {0, {}}; ans[i - 1] = idx[i + n] < idx[i]; } return {1, ans}; }
Editor is loading...