test/math/two-sat/yosupo-2-Sat.test.cpp

View this file on GitHub
Last update: 2023-12-03 13:41:56+08:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#include <iostream>

#include "../../../library/math/two-sat.hpp"

using namespace std;
using namespace felix;

int main() {
	ios::sync_with_stdio(false);
	cin.tie(0);
	string s;
	int n, m;
	cin >> s >> s >> n >> m;
	two_sat ts(n);
	for(int i = 0; i < m; ++i) {
		int u, v;
		cin >> u >> v >> s;
		bool x = u > 0;
		bool y = v > 0;
		u = abs(u) - 1;
		v = abs(v) - 1;
		ts.add_or_clause(u, x, v, y);
	}
	if(ts.satisfiable()) {
		cout << "s SATISFIABLE\nv ";
		auto ans = ts.answer();
		for(int i = 0; i < n; ++i) {
			cout << (i + 1) * (ans[i] ? +1 : -1) << " ";
		}
		cout << "0\n";
	} else {
		cout << "s UNSATISFIABLE\n";
	}
	return 0;
}

#line 1 "test/math/two-sat/yosupo-2-Sat.test.cpp"
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#include <iostream>

#line 2 "library/math/two-sat.hpp"
#include <vector>
#line 3 "library/graph/scc.hpp"
#include <cassert>
#include <algorithm>
#include <functional>

namespace felix {

struct SCC {
public:
	std::vector<int> id;

	SCC() : n(0) {}
	explicit SCC(int _n) : id(_n), n(_n), g(_n), h(_n) {}

	void add_edge(int u, int v) {
		assert(0 <= u && u < n);
		assert(0 <= v && v < n);
		g[u].push_back(v);
		h[v].push_back(u);
	}

	void build() {
		std::vector<int> top;
		top.reserve(n);
		std::function<void(int)> dfs1 = [&](int u) {
			id[u] = 1;
			for(auto v : g[u]) {
				if(id[v] == 0) {
					dfs1(v);
				}
			}
			top.push_back(u);
		};
		for(int i = 0; i < n; i++) {
			if(id[i] == 0) {
				dfs1(i);
			}
		}
		std::fill(id.begin(), id.end(), -1);
		std::function<void(int, int)> dfs2 = [&](int u, int x) {
			id[u] = x;
			for(auto v : h[u]) {
				if(id[v] == -1) {
					dfs2(v, x);
				}
			}
		};
		for(int i = n - 1, cnt = 0; i >= 0; i--) {
			int u = top[i];
			if(id[u] == -1) {
				dfs2(u, cnt);
				cnt++;
			}
		}
	}

	std::vector<std::vector<int>> compress() {
		int sz = *std::max_element(id.begin(), id.end()) + 1;
		std::vector<std::vector<int>> new_g(sz);
		for(int u = 0; u < n; u++) {
			for(auto v : g[u]) {
				if(id[u] == id[v]) {
					continue;
				}
				new_g[id[u]].push_back(id[v]);
			}
		}
		for(int i = 0; i < sz; ++i) {
			std::sort(new_g[i].begin(), new_g[i].end());
			new_g[i].erase(std::unique(new_g[i].begin(), new_g[i].end()), new_g[i].end());
		}
		return new_g;
	}

private:
	int n;
	std::vector<std::vector<int>> g, h;
};

} // namespace felix
#line 4 "library/math/two-sat.hpp"

namespace felix {

struct two_sat {
public:
	two_sat() : n(0) {}
	explicit two_sat(int _n) : n(_n), g(_n * 2), ans(_n) {}

	void add_implies_clause(int u, bool x, int v, bool y) {
		g.add_edge(2 * u + x, 2 * v + y);
		g.add_edge(2 * v + !y, 2 * u + !x);
	}

	void add_or_clause(int u, bool x, int v, bool y) {
		g.add_edge(2 * u + !x, 2 * v + y);
		g.add_edge(2 * v + !y, 2 * u + x);
	}

	void add_xor_clause(int u, bool x, int v, bool y) {
		add_or_clause(u, x, v, y);
		add_or_clause(u, !x, v, !y);
	}

	void add_equal_clause(int u, bool x, int v, bool y) {
		add_implies_clause(u, x, v, y);
		add_implies_clause(u, !x, v, !y);
	}

	void add_unequal_clause(int u, bool x, int v, bool y) {
		add_implies_clause(u, x, v, !y);
		add_implies_clause(u, !x, v, y);
	}

	void set_value(int u, bool x) {
		g.add_edge(2 * u + !x, 2 * u + x);
	}

	bool satisfiable() {
		built = true;
		g.build();
		for(int i = 0; i < n; ++i) {
			if(g.id[2 * i] == g.id[2 * i + 1]) {
				return false;
			}
			ans[i] = (g.id[2 * i] < g.id[2 * i + 1]);
		}
		return true;
	}

	std::vector<bool> answer() {
		if(!built) {
			satisfiable();
		}
		return ans;
	}

private:
	int n;
	SCC g;
	bool built = false;
	std::vector<bool> ans;
};

} // namespace felix
#line 5 "test/math/two-sat/yosupo-2-Sat.test.cpp"
using namespace std;
using namespace felix;

int main() {
	ios::sync_with_stdio(false);
	cin.tie(0);
	string s;
	int n, m;
	cin >> s >> s >> n >> m;
	two_sat ts(n);
	for(int i = 0; i < m; ++i) {
		int u, v;
		cin >> u >> v >> s;
		bool x = u > 0;
		bool y = v > 0;
		u = abs(u) - 1;
		v = abs(v) - 1;
		ts.add_or_clause(u, x, v, y);
	}
	if(ts.satisfiable()) {
		cout << "s SATISFIABLE\nv ";
		auto ans = ts.answer();
		for(int i = 0; i < n; ++i) {
			cout << (i + 1) * (ans[i] ? +1 : -1) << " ";
		}
		cout << "0\n";
	} else {
		cout << "s UNSATISFIABLE\n";
	}
	return 0;
}