Test/TwoSat.test.cpp

View this file on GitHub
Last update: 2021-03-18 15:32:11+09:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

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

#include "Mathematics/TwoSat.hpp"

#include <iostream>
#include <string>
#include <cmath>

int main() {
	std::ios::sync_with_stdio(false);
	std::cin.tie(0);
	
	std::string dummy; std::cin >> dummy >> dummy;
	
	int N, M;
	std::cin >> N >> M;
	
	TwoSat sat(N);
	
	while (M--) {
		int a, b, t;
		std::cin >> a >> b >> t;
		sat.add_clause(std::abs(a) - 1, a > 0, std::abs(b) - 1, b > 0);
	}
	
	if (!sat.build()) std::cout << "s UNSATISFIABLE" << std::endl;
	else {
		std::cout << "s SATISFIABLE" << std::endl;
		std::cout << "v";
		for (int i = 0; i < N; ++i) std::cout << " " << (sat.get(i) ? i + 1 : -(i + 1));
		std::cout << " 0" << std::endl;
	}
}

#line 1 "Test/TwoSat.test.cpp"
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#line 1 "Mathematics/TwoSat.hpp"



#line 1 "GraphTheory/StronglyConnectedComponents.hpp"



#include <vector>
#include <cassert>
#include <algorithm>

/**
 * @brief https://tkmst201.github.io/Library/GraphTheory/StronglyConnectedComponents.hpp
 */
struct StronglyConnectedComponents {
	using Graph = std::vector<std::vector<int>>;
	
private:
	int n;
	std::vector<int> rank_;
	std::vector<std::vector<int>> rank_list_;
	
public:
	explicit StronglyConnectedComponents(const Graph & g) : n(g.size()) {
		Graph rg(n);
		for (int i = 0; i < n; ++i) {
			for (int j : g[i]) {
				assert(0 <= j && j < n);
				rg[j].emplace_back(i);
			}
		}
		std::vector<bool> visited(n, false);
		std::vector<int> num;
		auto dfs = [&](auto self, int u) -> void {
			visited[u] = true;
			for (int v : g[u]) if (!visited[v]) self(self, v);
			num.emplace_back(u);
		};
		for (int i = 0; i < n; ++i) if (!visited[i]) dfs(dfs, i);
		int cnt = 0;
		visited.assign(n, false);
		rank_.assign(n, -1);
		auto rdfs = [&](auto self, int u) -> void {
			visited[u] = true;
			rank_[u] = cnt;
			for (int v : rg[u]) if (!visited[v]) self(self, v);
		};
		for (int i = n - 1; i >= 0; --i) if (!visited[num[i]]) rdfs(rdfs, num[i]), ++cnt;
		rank_list_.assign(cnt, {});
		for (int i = 0; i < n; ++i) rank_list_[rank_[i]].emplace_back(i);
	}
	
	int size() const noexcept {
		return n;
	}
	
	int scc_size() const noexcept {
		return rank_list_.size();
	}
	
	int scc_size(int k) const noexcept {
		assert(0 <= k && k < scc_size());
		return rank_list_[k].size();
	}
	
	int rank(int u) const noexcept {
		assert(0 <= u && u < size());
		return rank_[u];
	}
	
	const std::vector<int> & rank_list(int k) const noexcept {
		assert(0 <= k && k < scc_size());
		return rank_list_[k];
	}
	
	Graph get_graph(const Graph & g) const {
		Graph res(scc_size());
		for (int i = 0; i < scc_size(); ++i) {
			for (int j : rank_list_[i]) for (int v : g[j]) if (rank(v) != i) res[i].emplace_back(rank(v));
			std::sort(begin(res[i]), end(res[i]));
			res[i].erase(unique(begin(res[i]), end(res[i])), end(res[i]));
		}
		return res;
	}
};


#line 5 "Mathematics/TwoSat.hpp"

#line 8 "Mathematics/TwoSat.hpp"

/**
 * @brief https://tkmst201.github.io/Library/Mathematics/TwoSat.hpp
 */
struct TwoSat {
	using scc_type = StronglyConnectedComponents;
	
private:
	int n;
	typename scc_type::Graph g;
	std::vector<bool> ans;
	bool satisfiability = false;
	
public:
	explicit TwoSat(int n) : n(n), g(2 * n) {}
	
	int size() const noexcept {
		return n;
	}
	
	void add_clause(int x, bool xb, int y, bool yb) {
		assert(0 <= x && x < n);
		assert(0 <= y && y < n);
		g[x + (xb ? n : 0)].emplace_back(y + (yb ? 0 : n));
		g[y + (yb ? n : 0)].emplace_back(x + (xb ? 0 : n));
		satisfiability = false;
	}
	
	void add_clause(int x, bool xb) {
		assert(0 <= x && x < n);
		g[x + (xb ? n : 0)].emplace_back(x + (xb ? 0 : n));
		satisfiability = false;
	}
	
	bool build() {
		scc_type scc(g);
		ans.assign(n, false);
		satisfiability = false;
		for (int i = 0; i < n; ++i) {
			if (scc.rank(i) == scc.rank(i + n)) return false;
			if (scc.rank(i) > scc.rank(i + n)) ans[i] = true;
		}
		satisfiability = true;
		return true;
	}
	
	const std::vector<bool> & ans_list() const noexcept {
		assert(satisfiability);
		return ans;
	}
	
	bool get(int i) const noexcept {
		assert(satisfiability);
		assert(0 <= i && i < n);
		return ans[i];
	}
};


#line 4 "Test/TwoSat.test.cpp"

#include <iostream>
#include <string>
#include <cmath>

int main() {
	std::ios::sync_with_stdio(false);
	std::cin.tie(0);
	
	std::string dummy; std::cin >> dummy >> dummy;
	
	int N, M;
	std::cin >> N >> M;
	
	TwoSat sat(N);
	
	while (M--) {
		int a, b, t;
		std::cin >> a >> b >> t;
		sat.add_clause(std::abs(a) - 1, a > 0, std::abs(b) - 1, b > 0);
	}
	
	if (!sat.build()) std::cout << "s UNSATISFIABLE" << std::endl;
	else {
		std::cout << "s SATISFIABLE" << std::endl;
		std::cout << "v";
		for (int i = 0; i < N; ++i) std::cout << " " << (sat.get(i) ? i + 1 : -(i + 1));
		std::cout << " 0" << std::endl;
	}
}