2 SAT
unknown
c_cpp
4 years ago
1.5 kB
5
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...