2-SAT の共通部品

components/two_sat_core.hpp · GitHub で見る

共通ページ

TwoSAT の含意グラフを処理する内部部品です。通常は節を追加できる TwoSAT を使用し、符号付きリテラルの含意辺を直接用意する場合にこの部品を使います。

#include "lib/components/two_sat_core.hpp"
#include <cassert>
#include <utility>
#include <vector>

std::vector<std::pair<int, int>> edges{ {0, 2}, {3, 1}, {2, 3} };
std::vector<int> forced{3};
std::vector<bool> answer(2);
assert(two_sat_detail::solve(2, edges, forced, answer));
assert(answer[0] && answer[1]);

two_sat_detail::solve(variables, edges, forced, answer) は充足可能性を bool で返します。引数に既定値はありません。

引数	型・条件
variables	非負の int。変数の個数で、INT_MAX / 2 以下
edges	std::span<const std::pair<int,int>>。含意の始点・終点を並べる。辺数は INT_MAX 以下
forced	std::span<const int>。既存の単位節で真になるリテラルを並べる
answer	長さが variables の std::vector<bool>&。充足代入の出力先

変数 i の false 側のリテラルは 2*i、true 側は 2*i+1 とし、反対のリテラルは literal ^ 1 です。辺・固定リテラルの番号は全て [0,2*variables) としてください。

辺 u -> v は、u が真なら v が真であることを表します。対偶の辺 (v ^ 1) -> (u ^ 1) も用意する必要があります。単位節の辺 (literal ^ 1) -> literal は自身が対偶なので 1 本で構いません。重複する辺と自己辺も扱えます。対偶が揃っていることの検査は行いません。

forced は先に伝播できる単位節のリテラルを渡す補助入力です。各要素について、対応する辺 (literal ^ 1) -> literal を edges にも含めてください。別の制約を追加する引数ではありません。重複は許容し、空配列も指定できます。

返り値が true の場合は、answer を充足代入で更新します。代入例は一意ではありません。返り値が false の場合の answer の内容は未規定です。入力の edges・forced は更新しません。呼び出しごとに判定し、結果を保存しません。変数が 0 個の場合は、辺と固定リテラルも空とし、true と空の代入例を返します。

固定リテラル同士の矛盾を先に調べます。全変数が固定されている場合は、含意辺を直接検査して判定し、隣接表を構築しません。

初めは配列による連結隣接表を構築し、予算付きの伝播を行います。分岐の多いグラフで探索量が増えた場合は、辺の探索順を保ちながら同じ配列を CSR に変換して伝播を続けます。伝播で矛盾が生じた試行は取り消します。

処理予算を使い切った場合は、CSR を用いた 2-SAT 専用の反復 Tarjan 法へ移ります。出辺のない頂点は単独の強連結成分として扱い、探索スタックへ積みません。同じ成分に反対のリテラルが入れば充足不可能です。

変数数を \(n\)、含意辺数と forced の長さの和を \(m\) として、時間・追加空間は \(O(n+m)\) です。空の問題は \(O(1)\) 時間・空間です。

検証コード

• test/two_sat.test.cpp

コード

#ifndef TWO_SAT_CORE_HPP
#define TWO_SAT_CORE_HPP

#include <algorithm>
#include <cassert>
#include <cstddef>
#include <limits>
#include <span>
#include <utility>
#include <vector>

namespace two_sat_detail {
inline bool solve(int variables, std::span<const std::pair<int, int>> edges, std::span<const int> forced, std::vector<bool> &answer) {
	assert(0 <= variables && variables <= std::numeric_limits<int>::max() / 2);
	assert(edges.size() <= std::size_t(std::numeric_limits<int>::max()) && answer.size() == std::size_t(variables));
	int n = 2 * variables;
	std::vector<signed char> values(variables, -1);
	std::vector<int> trail;
	trail.reserve(variables);
	for (int literal : forced) {
		if (values[literal >> 1] < 0) {
			values[literal >> 1] = literal & 1;
			trail.push_back(literal);
		} else if (values[literal >> 1] != (literal & 1)) return false;
	}
	if (trail.size() == std::size_t(variables)) {
		for (auto [from, to] : edges) {
			if (values[from >> 1] == (from & 1) && values[to >> 1] != (to & 1)) return false;
		}
		for (int i = 0; i < variables; ++i) answer[i] = values[i];
		return true;
	}
	std::vector<int> offset(std::size_t(n) + 1, -1), adjacency(edges.size());
	std::size_t branching = 0;
	for (std::size_t i = 0; i < edges.size(); ++i) {
		auto [from, to] = edges[i];
		branching += offset[from] >= 0;
		adjacency[i] = offset[from];
		offset[from] = static_cast<int>(i);
	}
	bool compact = false;
	auto make_compact = [&] {
		std::fill(offset.begin(), offset.end(), 0);
		for (auto [from, to] : edges) ++offset[from];
		for (int v = 1; v < n; ++v) offset[v] += offset[v - 1];
		offset[n] = static_cast<int>(edges.size());
		for (auto [from, to] : edges) adjacency[--offset[from]] = to;
		compact = true;
	};
	if (variables >= 1024) {
		auto closure = [&]<bool Adaptive>() -> int {
			std::size_t budget = std::size_t(variables) + edges.size();
			if constexpr (!Adaptive) budget = (std::min)(budget, std::numeric_limits<std::size_t>::max() / 2) * 2;
			std::size_t switch_after = std::max<std::size_t>(1024, (std::size_t(variables) + edges.size()) / 16);
			std::size_t compact_budget = budget - std::min(budget, switch_after);
			auto propagate = [&] {
				for (std::size_t i = 0; i < trail.size(); ++i) {
					if (!budget) return -1;
					--budget;
					int v = trail[i];
					if constexpr (Adaptive) if (!compact && budget < compact_budget) make_compact();
					auto visit = [&](int to) {
						if (!budget) return -1;
						--budget;
						if (values[to >> 1] < 0) {
							values[to >> 1] = to & 1;
							trail.push_back(to);
						} else if (values[to >> 1] != (to & 1)) {
							for (int literal : trail) values[literal >> 1] = -1;
							return 0;
						}
						return 1;
					};
					if constexpr (Adaptive) if (compact) {
						for (int at = offset[v]; at < offset[v + 1]; ++at) {
							int status = visit(adjacency[at]);
							if (status != 1) return status;
						}
						continue;
					}
					for (int at = offset[v]; at >= 0; at = adjacency[at]) {
						int status = visit(edges[at].second);
						if (status != 1) return status;
					}
				}
				return 1;
			};
			auto empty = [&](int v) {
				if constexpr (Adaptive) if (compact) return offset[v] == offset[v + 1];
				return offset[v] < 0;
			};
			int status = propagate();
			if (!status) return 0;
			for (int i = 0; status > 0 && i < variables; ++i) if (values[i] < 0) {
				if (empty(2 * i)) values[i] = 0;
				else if (empty(2 * i + 1)) values[i] = 1;
				else {
					trail.assign(1, 2 * i);
					values[i] = 0;
					status = propagate();
					if (!status) {
						trail.assign(1, 2 * i + 1);
						values[i] = 1;
						status = propagate();
						if (!status) return 0;
					}
				}
			}
			return status;
		};
		int status = edges.size() >= std::size_t(variables) && branching > edges.size() / 32
			? closure.template operator()<true>() : closure.template operator()<false>();
		if (status >= 0) {
			if (status) for (int i = 0; i < variables; ++i) answer[i] = values[i];
			return status;
		}
	}
	if (!compact) make_compact();
	trail.clear();
	std::vector<int> order(n, -1);
	struct Frame { int vertex, next, low; };
	std::vector<Frame> stack;
	stack.reserve(n);
	int clock = 0, component = -2;
	auto enter = [&](int v) {
		order[v] = clock++;
		trail.push_back(v);
		stack.push_back({v, offset[v], order[v]});
	};
	for (int root = 0; root < n; ++root) if (order[root] == -1) {
		if (offset[root] == offset[root + 1]) { order[root] = component--; continue; }
		enter(root);
		while (!stack.empty()) {
			auto &frame = stack.back();
			int v = frame.vertex, next = frame.next, low = frame.low;
			for (; next < offset[v + 1]; ++next) {
				int to = adjacency[next];
				if (order[to] == -1) {
					if (offset[to] == offset[to + 1]) { order[to] = component--; continue; }
					break;
				}
				if (order[to] >= 0) low = std::min(low, order[to]);
			}
			frame.low = low;
			if (next < offset[v + 1]) {
				frame.next = next + 1;
				enter(adjacency[next]);
			} else {
				stack.pop_back();
				if (low == order[v]) {
					int u;
					do {
						u = trail.back();
						trail.pop_back();
						order[u] = component;
						if (order[u ^ 1] == component) return false;
					} while (u != v);
					--component;
				}
				if (!stack.empty()) stack.back().low = std::min(stack.back().low, low);
			}
		}
	}
	for (int i = 0; i < variables; ++i) answer[i] = order[2 * i] < order[2 * i + 1];
	return true;
}
}

#endif

Back to top page