Pagini recente » Cod sursa (job #1587602) | Cod sursa (job #1533739) | Cod sursa (job #2343208) | Cod sursa (job #1806831) | Cod sursa (job #3357118)
#include <cassert>
#include <fstream>
#include <vector>
using namespace std;
ifstream fin("2sat.in");
ofstream fout("2sat.out");
struct SCCDecomposer {
void dfs(int node, vector<vector<int>> &g, vector<int> &postOrder,
vector<bool> &visited) {
if (visited[node])
return;
visited[node] = true;
for (auto v : g[node]) {
if (!visited[v]) {
dfs(v, g, postOrder, visited);
}
}
postOrder.push_back(node);
}
vector<int> getPostOrder(vector<vector<int>> &g) {
vector<bool> visited(g.size());
vector<int> postOrder;
for (size_t node = 0; node < g.size(); node++) {
dfs(node, g, postOrder, visited);
}
return postOrder;
}
vector<vector<int>> getSCC(vector<vector<int>> &g) {
vector<int> postOrder = getPostOrder(g);
vector<vector<int>> gt(g.size());
for (size_t i{}; i < g.size(); i++) {
for (auto v : g[i]) {
gt[v].push_back(i);
}
}
vector<bool> visited(g.size());
vector<vector<int>> components;
for (size_t i{g.size()}; i--;) {
int node = postOrder[i];
vector<int> scc;
dfs(node, gt, scc, visited);
if (!scc.empty()) {
components.push_back(scc);
}
}
return components;
}
};
struct BoolTerm {
bool negated = false;
int id{};
};
struct SATSolver {
vector<bool> solve(vector<BoolTerm> equation, int n) {
vector<vector<int>> g(n * 2);
for (size_t i{}; i < equation.size(); i += 2) {
BoolTerm a = equation[i];
BoolTerm b = equation[i + 1];
int i1 = (a.id - 1) * 2 + a.negated;
int i2 = (b.id - 1) * 2 + b.negated;
assert(i1 < 2 * n);
assert(i2 < 2 * n);
g[i1 ^ 1].push_back(i2);
g[i2 ^ 1].push_back(i1);
}
SCCDecomposer decomposer;
vector<vector<int>> components = decomposer.getSCC(g);
for (size_t i{}; i < g.size(); i++) {
for (auto x : g[i]) {
int a = (i + 2) / 2 * (i % 2 ? -1 : 1);
int b = (x + 2) / 2 * (x % 2 ? -1 : 1);
}
}
vector<int> comp(n * 2, -1);
for (size_t i{}; i < (size_t)components.size(); i++) {
for (auto x : components[i]) {
int a = (x + 2) / 2 * (x % 2 ? -1 : 1);
comp[x] = i;
}
}
vector<bool> ans(n);
for (size_t i{}; i < (size_t)n * 2; i += 2) {
if (comp[i] == comp[i + 1] && comp[i] != -1) {
return {};
} else if (comp[i] < comp[i + 1]) {
ans[i / 2] = false;
} else {
ans[i / 2] = true;
}
}
return ans;
}
};
int main() {
int n, m;
fin >> n >> m;
vector<BoolTerm> equation;
for (size_t i{}; i < (size_t)m; i++) {
int a, b;
fin >> a >> b;
BoolTerm aTerm = {a < 0, abs(a)};
BoolTerm bTerm = {b < 0, abs(b)};
equation.push_back(aTerm);
equation.push_back(bTerm);
}
SATSolver solver;
vector<bool> ans = solver.solve(equation, n);
for (auto x : ans) {
fout << x << ' ';
}
if (ans.empty()) {
fout << -1 << '\n';
}
return 0;
}