Cod sursa(job #3357118)

Utilizator andreiarama2Arama Andrei Robert andreiarama2 Data 6 iunie 2026 14:58:14
Problema 2SAT Scor 100
Compilator cpp-64 Status done
Runda Arhiva educationala Marime 2.71 kb
#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;
}