2-SAT

graph/two_sat.hpp · GitHub で見る

共通ページ

#include "lib/graph/two_sat.hpp"
#include <cassert>

TwoSAT sat(3);
sat.add_clause(0, true, 1, false); // x[0] または !x[1]
sat.add_clause(1, true, 2, true);
assert(sat.satisfiable());
auto answer = sat.answer(); // std::vector<bool>
assert(answer[0] || !answer[1]);
assert(answer[1] || answer[2]);

sat.add_clause(0, false, 0, false);
assert(sat.satisfiable());
assert(!sat.answer()[0]);

TwoSAT(n = 0) で 0 始まりの n 個の bool 変数を作ります。

操作	内容・返り値
size()	変数の個数を int で返す
reserve(m)	m 節分の含意辺の格納容量を予約する。返り値は void
add_clause(i,f,j,g)	(x[i] == f) || (x[j] == g) を追加する。返り値は void
satisfiable()	充足可能なら true、充足不可能なら false を bool で返す
answer()	直前に求めた充足代入のコピーを std::vector<bool> で返す

f・g は bool 値です。answer() は、直前の satisfiable() が true で、以後に節を追加していない場合だけ呼べます。返す配列の長さは size()、各要素は対応する変数の値です。代入例は一意ではありません。

同じ変数を両辺に指定できます。add_clause(i,f,i,f) は変数の固定、add_clause(i,true,i,false) は恒真節です。恒真節では辺を追加せず、固定節では含意と対偶が同じ辺になるため 1 本だけ追加します。重複する節も指定できます。

変数数は 0 <= n <= INT_MAX / 2、i・j は [0,n)、実際に格納する含意辺は INT_MAX 以下である必要があります。予約する節数 m は std::size_t で、INT_MAX / 2 以下です。これらの範囲は assert の前提です。TwoSAT(0) は充足可能で、代入例は空配列です。節がなければ、全変数が false の代入例を返します。

充足可能・充足不可能のどちらの判定結果も保存します。節を追加せずに satisfiable() を再度呼ぶと、保存した結果を返します。add_clause は恒真節の場合も保存結果を無効にするため、追加後は再び satisfiable() を呼んでください。reserve は保存結果を無効にしません。コピーは節・保存結果とも独立します。

参考: Nyaan’s Library、maspypy library。

変数数を \(n\)、節数を \(m\) として、構築は \(O(n)\)、節追加は償却 \(O(1)\)、初回または節追加後の判定は \(O(n+m)\)、変更のない問題の再判定は \(O(1)\)、代入例のコピーは \(O(n)\)、保持・作業空間は \(O(n+m)\) です。空の問題は \(O(1)\) 時間・空間です。

依存ライブラリ

• 2-SAT の共通部品

検証コード

• test/two_sat.test.cpp

コード

#ifndef TWO_SAT_HPP
#define TWO_SAT_HPP

#include "../components/two_sat_core.hpp"

class TwoSAT {
	int n_;
	std::vector<std::pair<int, int>> edges_;
	std::vector<int> forced_;
	std::vector<bool> answer_;
	bool valid_ = false, solved_ = false;
	static int vertices(int n) {
		assert(0 <= n && n <= std::numeric_limits<int>::max() / 2);
		return n * 2;
	}

  public:
	explicit TwoSAT(int n = 0) : n_(n), answer_(vertices(n) / 2) {}
	int size() const { return n_; }
	void reserve(std::size_t clauses) {
		assert(clauses <= std::size_t(std::numeric_limits<int>::max() / 2));
		edges_.reserve(clauses * 2);
	}
	void add_clause(int i, bool f, int j, bool g) {
		assert(0 <= i && i < n_ && 0 <= j && j < n_);
		valid_ = solved_ = false;
		if (i == j && f != g) return;
		assert(edges_.size() <= std::size_t(std::numeric_limits<int>::max() - 1 - int(i != j)));
		edges_.emplace_back(2 * i + !f, 2 * j + g);
		if (i == j) forced_.push_back(2 * i + f);
		if (i != j) edges_.emplace_back(2 * j + !g, 2 * i + f);
	}
	bool satisfiable() {
		if (solved_) return valid_;
		valid_ = false;
		if (edges_.empty()) std::fill(answer_.begin(), answer_.end(), false), valid_ = true;
		else valid_ = two_sat_detail::solve(n_, edges_, forced_, answer_);
		solved_ = true;
		return valid_;
	}
	std::vector<bool> answer() const { assert(valid_); return answer_; }
};

#endif

Back to top page