2-SAT
(Mathematics/TwoSat.hpp)

View this file on GitHub
Last update: 2021-03-18 15:32:11+09:00
Include: #include "Mathematics/TwoSat.hpp"
Link: https://tkmst201.github.io/Library/Mathematics/TwoSat.hpp

概要

論理変数 $x_0, \ldots, x_{N-1}$ に対して $(x_0 \lor x_1) \land (\lnot x_0 \lor x_2) \land (x_3 \lor x_0) \land (x_5) \land (x_2 \lor x_{N-1})$ のような形式の論理式を満たす真偽の組み合わせを求めます。
より具体的には、クロージャ(括弧) の積で表されていて各クロージャ内は 2 つ以下のリテラルの和で表されているような論理式を解きます。

TwoSat(int n)
- $\Theta(n)$ $n$ 個の論理変数で初期化
int size()
- $\Theta(1)$ 論理変数の個数 $N$ を返す
void add_clause(int x, bool xb, int y, bool yb)
- ならし $\Theta(1)$ クロージャ $x = xb \lor y = yb$ を追加
void add_clause(int x, bool xb)
- ならし $\Theta(1)$ クロージャ $x = xb$ を追加
bool build()
- $\Theta(N)$ 論理式を満たすような論理値の割り当てを求める
const vector<bool> & ans_list
- $\Theta(1)$ 論理式を満たすような論理値の割り当てを返す
bool get(int i)
- $\Theta(1)$ 論理式を満たすような論理値の割り当てで $x_i$ の真偽値を返す

コンストラクタ

TwoSat(int n)

$n$ 個の論理変数で初期化します。

制約

$0 \leq n$

計算量

$\Theta(n)$

メンバ関数

以下、論理変数の個数を $N$ とし、それぞれ $x_0, \ldots, x_{N-1}$ とします。

int size()

論理変数の個数 $N$ を返します。

計算量

$\Theta(1)$

void add_clause(int x, bool xb, int y, bool yb)

クロージャ $x = xb \lor y = yb$ を追加します。

制約

$0 \leq x, y < N$
$xb, yb$ はそれぞれ $true, false$ のいずれか

計算量

ならし $\Theta(1)$

void add_clause(int x, bool xb)

クロージャ $x = xb$ を追加します。

制約

$0 \leq x < N$
$xb$ は $true, false$ のいずれか

計算量

ならし $\Theta(1)$

bool build()

論理式を満たすような論理値の割り当てを求めます。割り当てることができた場合は $true$ を、割り当てが存在しない場合は $false$ を返します。

計算量

$\Theta(N)$

const vector & ans_list

論理式を満たすような論理値の割り当てを返します。
$[i] := x_i$ の論理値

制約

論理式を満たすような論理値の割り当てが存在する

計算量

$\Theta(1)$

bool get(int i)

論理式を満たすような論理値の割り当てで $x_i$ の真偽値を返します。

制約

論理式を満たすような論理値の割り当てが存在する
$0 \leq i < N$

計算量

$\Theta(1)$

使用例

#include <bits/stdc++.h>
#include "Mathematics/TwoSat.hpp"
using namespace std;

int main() {
	TwoSat sat(5);
	cout << "sat.size() = " << sat.size() << endl; // 5
	sat.add_clause(0, true, 1, false);
	sat.add_clause(1, false, 2, false);
	
	sat.build();
	// true true false true true
	for (bool b : sat.ans_list()) cout << boolalpha << b << " "; cout << '\n';
	for (int i = 0; i < sat.size(); ++i) cout << boolalpha << sat.get(i) << " "; cout << '\n';
	
	sat.add_clause(0, false);
	sat.add_clause(1, false);
	sat.build();
	// false false false true true
	for (bool b : sat.ans_list()) cout << boolalpha << b << " "; cout << '\n';
	
	sat.add_clause(0, true, 1, true);
	bool f = sat.build();
	cout << boolalpha << f << endl; // false
}

参考

2021/03/18: https://noshi91.hatenablog.com/entry/2019/10/03/184812
2021/03/18: https://www.slideshare.net/yoshiokatsuneo/2sat-72370606
2020/09/10: AC Library

Depends on

強連結成分分解 (SCC) (GraphTheory/StronglyConnectedComponents.hpp)

Verified with

Test/TwoSat.test.cpp

Code

#ifndef INCLUDE_GUARD_TWO_SAT_HPP
#define INCLUDE_GUARD_TWO_SAT_HPP

#include "GraphTheory/StronglyConnectedComponents.hpp"

#include <vector>
#include <cassert>

/**
 * @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];
	}
};

#endif // INCLUDE_GUARD_TWO_SAT_HPP

#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];
	}
};

2-SAT (Mathematics/TwoSat.hpp)

概要

コンストラクタ

TwoSat(int n)

メンバ関数

int size()

void add_clause(int x, bool xb, int y, bool yb)

void add_clause(int x, bool xb)

bool build()

const vector & ans_list

bool get(int i)

使用例

参考

Depends on

Verified with

Code

2-SAT
(Mathematics/TwoSat.hpp)