two_sat.hpp¶
追加二元析取约束，solve 每次从完整公式重新求解并返回独立布尔赋值；无解返回 nullopt，零变量返回有值的空数组。同变量恒真式不加边，单文字只加一条蕴含边，递归 Tarjan 直接比较逆拓扑分量编号。
Complexity: Time: \(O(V + C)\) per solve for \(V\) variables and \(C\) clauses; amortized \(O(1)\) per add_clause. Space: \(O(V + C)\), including \(O(V)\) call depth.
AC 记录：two_sat。
Implementation¶
当前头文件，省略 include guard；依赖见 #include。
/// @complexity Time: O(V + C) per solve for V variables and C clauses;
/// amortized O(1) per add_clause. Space: O(V + C), including O(V) call depth.
#include "atcoder/internal_csr.hpp"
#include <algorithm>
#include <cassert>
#include <limits>
#include <optional>
#include <utility>
#include <vector>
namespace noya {
/// @brief Append clauses (x_a == x) OR (x_b == y), then solve from scratch.
/// Variables are in [0,n); require 2*n and 2*clause_count to fit int.
/// Repeated solve() preserves the formula and returns an independent assignment.
/// Recursive Tarjan uses the repository's 512 MiB test stack budget.
class two_sat {
public:
explicit two_sat(int n) : n_(n) {
assert(0 <= n && n <= std::numeric_limits<int>::max() / 2);
}
void add_clause(int a, bool x, int b, bool y) {
assert(0 <= a && a < n_ && 0 <= b && b < n_);
assert(edges_.size() <= std::size_t(std::numeric_limits<int>::max()) - 2);
if (a == b) {
if (x == y) edges_.emplace_back(2 * a + !x, 2 * a + x);
return;
}
edges_.emplace_back(2 * a + !x, 2 * b + y);
edges_.emplace_back(2 * b + !y, 2 * a + x);
}
/// Return one satisfying assignment, or nullopt if none exists.
std::optional<std::vector<bool>> solve() {
int n = 2 * n_;
std::vector<int> ids(n);
{
atcoder::internal::csr<int> g(n, edges_);
std::vector<int> ord(n, -1), stack;
stack.reserve(n);
int now = 0, count = 0;
auto dfs = [&](auto &self, int v) -> int {
int low = ord[v] = now++;
stack.push_back(v);
for (int i = g.start[v]; i < g.start[v + 1]; ++i) {
int u = g.elist[i];
low = std::min(low, ord[u] == -1 ? self(self, u) : ord[u]);
}
if (low == ord[v]) {
while (true) {
int u = stack.back();
stack.pop_back();
ord[u] = n;
ids[u] = count;
if (u == v) break;
}
++count;
}
return low;
};
for (int v = 0; v < n; ++v)
if (ord[v] == -1) dfs(dfs, v);
}
std::vector<bool> answer(n_);
for (int v = 0; v < n_; ++v) {
if (ids[2 * v] == ids[2 * v + 1]) return std::nullopt;
// Components are numbered in reverse topological order.
answer[v] = ids[2 * v] > ids[2 * v + 1];
}
return answer;
}
int variable_count() const { return n_; }
private:
int n_;
std::vector<std::pair<int, int>> edges_;
};
} // namespace noya
// NOYA_TWO_SAT_HPP
#ifndef NOYA_TWO_SAT_HPP
#define NOYA_TWO_SAT_HPP 1
/// @complexity Time: O(V + C) per solve for V variables and C clauses;
/// amortized O(1) per add_clause. Space: O(V + C), including O(V) call depth.
#include "atcoder/internal_csr.hpp"
#include <algorithm>
#include <cassert>
#include <limits>
#include <optional>
#include <utility>
#include <vector>
namespace noya {
/// @brief Append clauses (x_a == x) OR (x_b == y), then solve from scratch.
/// Variables are in [0,n); require 2*n and 2*clause_count to fit int.
/// Repeated solve() preserves the formula and returns an independent assignment.
/// Recursive Tarjan uses the repository's 512 MiB test stack budget.
class two_sat {
public:
explicit two_sat(int n) : n_(n) {
assert(0 <= n && n <= std::numeric_limits<int>::max() / 2);
}
void add_clause(int a, bool x, int b, bool y) {
assert(0 <= a && a < n_ && 0 <= b && b < n_);
assert(edges_.size() <= std::size_t(std::numeric_limits<int>::max()) - 2);
if (a == b) {
if (x == y) edges_.emplace_back(2 * a + !x, 2 * a + x);
return;
}
edges_.emplace_back(2 * a + !x, 2 * b + y);
edges_.emplace_back(2 * b + !y, 2 * a + x);
}
/// Return one satisfying assignment, or nullopt if none exists.
std::optional<std::vector<bool>> solve() {
int n = 2 * n_;
std::vector<int> ids(n);
{
atcoder::internal::csr<int> g(n, edges_);
std::vector<int> ord(n, -1), stack;
stack.reserve(n);
int now = 0, count = 0;
auto dfs = [&](auto &self, int v) -> int {
int low = ord[v] = now++;
stack.push_back(v);
for (int i = g.start[v]; i < g.start[v + 1]; ++i) {
int u = g.elist[i];
low = std::min(low, ord[u] == -1 ? self(self, u) : ord[u]);
}
if (low == ord[v]) {
while (true) {
int u = stack.back();
stack.pop_back();
ord[u] = n;
ids[u] = count;
if (u == v) break;
}
++count;
}
return low;
};
for (int v = 0; v < n; ++v)
if (ord[v] == -1) dfs(dfs, v);
}
std::vector<bool> answer(n_);
for (int v = 0; v < n_; ++v) {
if (ids[2 * v] == ids[2 * v + 1]) return std::nullopt;
// Components are numbered in reverse topological order.
answer[v] = ids[2 * v] > ids[2 * v + 1];
}
return answer;
}
int variable_count() const { return n_; }
private:
int n_;
std::vector<std::pair<int, int>> edges_;
};
} // namespace noya
#endif // NOYA_TWO_SAT_HPP
/// @complexity Time: O(V + C) per solve for V variables and C clauses;
/// amortized O(1) per add_clause. Space: O(V + C), including O(V) call depth.
#include <algorithm>
#include <utility>
#include <vector>
namespace atcoder {
namespace internal {
template <class E> struct csr {
std::vector<int> start;
std::vector<E> elist;
explicit csr(int n, const std::vector<std::pair<int, E>>& edges)
: start(n + 1), elist(edges.size()) {
for (auto e : edges) {
start[e.first + 1]++;
}
for (int i = 1; i <= n; i++) {
start[i] += start[i - 1];
}
auto counter = start;
for (auto e : edges) {
elist[counter[e.first]++] = e.second;
}
}
};
} // namespace internal
} // namespace atcoder
#include <algorithm>
#include <cassert>
#include <limits>
#include <optional>
#include <utility>
#include <vector>
namespace noya {
/// @brief Append clauses (x_a == x) OR (x_b == y), then solve from scratch.
/// Variables are in [0,n); require 2*n and 2*clause_count to fit int.
/// Repeated solve() preserves the formula and returns an independent assignment.
/// Recursive Tarjan uses the repository's 512 MiB test stack budget.
class two_sat {
public:
explicit two_sat(int n) : n_(n) {
assert(0 <= n && n <= std::numeric_limits<int>::max() / 2);
}
void add_clause(int a, bool x, int b, bool y) {
assert(0 <= a && a < n_ && 0 <= b && b < n_);
assert(edges_.size() <= std::size_t(std::numeric_limits<int>::max()) - 2);
if (a == b) {
if (x == y) edges_.emplace_back(2 * a + !x, 2 * a + x);
return;
}
edges_.emplace_back(2 * a + !x, 2 * b + y);
edges_.emplace_back(2 * b + !y, 2 * a + x);
}
/// Return one satisfying assignment, or nullopt if none exists.
std::optional<std::vector<bool>> solve() {
int n = 2 * n_;
std::vector<int> ids(n);
{
atcoder::internal::csr<int> g(n, edges_);
std::vector<int> ord(n, -1), stack;
stack.reserve(n);
int now = 0, count = 0;
auto dfs = [&](auto &self, int v) -> int {
int low = ord[v] = now++;
stack.push_back(v);
for (int i = g.start[v]; i < g.start[v + 1]; ++i) {
int u = g.elist[i];
low = std::min(low, ord[u] == -1 ? self(self, u) : ord[u]);
}
if (low == ord[v]) {
while (true) {
int u = stack.back();
stack.pop_back();
ord[u] = n;
ids[u] = count;
if (u == v) break;
}
++count;
}
return low;
};
for (int v = 0; v < n; ++v)
if (ord[v] == -1) dfs(dfs, v);
}
std::vector<bool> answer(n_);
for (int v = 0; v < n_; ++v) {
if (ids[2 * v] == ids[2 * v + 1]) return std::nullopt;
// Components are numbered in reverse topological order.
answer[v] = ids[2 * v] > ids[2 * v + 1];
}
return answer;
}
int variable_count() const { return n_; }
private:
int n_;
std::vector<std::pair<int, int>> edges_;
};
} // namespace noya
// NOYA_TWO_SAT_HPP