library/math/two-sat.hpp

• View this file on GitHub
• Last update: 2023-12-03 13:41:56+08:00
• Include: #include "library/math/two-sat.hpp"

Depends on

• library/graph/scc.hpp

Verified with

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

Code

#pragma once
#include <vector>
#include "../graph/scc.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 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

Back to top page