#line 1 "test/yosupo-judge/two_sat/main.test.cpp"
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"
#include <iostream>
#include <string>
#include <vector>
#line 2 "Mylib/Graph/two_sat.cpp"
#include <cassert>
#include <optional>
#line 2 "Mylib/Graph/GraphUtils/strongly_connected_components.cpp"
#include <algorithm>
#line 4 "Mylib/Graph/Template/graph.cpp"
namespace haar_lib {
template <typename T>
struct edge {
int from, to;
T cost;
int index = -1;
edge() {}
edge(int from, int to, T cost) : from(from), to(to), cost(cost) {}
edge(int from, int to, T cost, int index) : from(from), to(to), cost(cost), index(index) {}
};
template <typename T>
struct graph {
using weight_type = T;
using edge_type = edge<T>;
std::vector<std::vector<edge<T>>> data;
auto& operator[](size_t i) { return data[i]; }
const auto& operator[](size_t i) const { return data[i]; }
auto begin() const { return data.begin(); }
auto end() const { return data.end(); }
graph() {}
graph(int N) : data(N) {}
bool empty() const { return data.empty(); }
int size() const { return data.size(); }
void add_edge(int i, int j, T w, int index = -1) {
data[i].emplace_back(i, j, w, index);
}
void add_undirected(int i, int j, T w, int index = -1) {
add_edge(i, j, w, index);
add_edge(j, i, w, index);
}
template <size_t I, bool DIRECTED = true, bool WEIGHTED = true>
void read(int M) {
for (int i = 0; i < M; ++i) {
int u, v;
std::cin >> u >> v;
u -= I;
v -= I;
T w = 1;
if (WEIGHTED) std::cin >> w;
if (DIRECTED)
add_edge(u, v, w, i);
else
add_undirected(u, v, w, i);
}
}
};
template <typename T>
using tree = graph<T>;
} // namespace haar_lib
#line 5 "Mylib/Graph/GraphUtils/strongly_connected_components.cpp"
namespace haar_lib {
template <typename T>
auto strongly_connected_components(const graph<T> &g) {
const int n = g.size();
std::vector<int> ret(n), low(n, -1), ord(n, -1), S;
std::vector<bool> check(n);
S.reserve(n);
int t = 0;
int k = 0;
auto dfs =
[&](auto &dfs, int cur) -> void {
low[cur] = ord[cur] = t++;
S.push_back(cur);
check[cur] = true;
for (auto &e : g[cur]) {
if (ord[e.to] == -1) {
dfs(dfs, e.to);
low[cur] = std::min(low[cur], low[e.to]);
} else if (check[e.to]) {
low[cur] = std::min(low[cur], low[e.to]);
}
}
if (low[cur] == ord[cur]) {
while (true) {
int u = S.back();
S.pop_back();
check[u] = false;
ret[u] = k;
if (cur == u) break;
}
++k;
}
};
for (int i = 0; i < n; ++i) {
if (ord[i] == -1) {
t = 0;
dfs(dfs, i);
}
}
for (auto &x : ret) x = k - 1 - x;
return std::make_pair(ret, k);
}
} // namespace haar_lib
#line 7 "Mylib/Graph/two_sat.cpp"
namespace haar_lib {
class two_sat {
int n_;
graph<int> g_;
int f(int i) {
assert(i != 0);
assert(std::abs(i) <= n_);
if (i > 0)
return i - 1;
else
return std::abs(i) - 1 + n_;
}
public:
two_sat() {}
two_sat(int n) : n_(n), g_(2 * n) {}
/**
* @note a→bを導入する
*/
void add_if(int a, int b) {
g_.add_edge(f(a), f(b), 1);
}
/**
* @note a∨bを導入する
* @note a ∨ b <=> (!a => b) ∧ (!b => a)
*/
void add_or(int a, int b) {
add_if(-a, b);
add_if(-b, a);
}
/**
* @note ¬(a∧b)を導入する
* @note !(A ∧ B) <=> (!A ∨ !B)
*/
void not_coexist(int a, int b) {
add_or(-a, -b);
}
public:
std::optional<std::vector<bool>> solve() const {
auto [scc, m] = strongly_connected_components(g_);
for (int i = 0; i < n_; ++i) {
if (scc[i] == scc[i + n_]) return std::nullopt;
}
std::vector<bool> ret(n_);
for (int i = 0; i < n_; ++i) ret[i] = scc[i] > scc[i + n_];
return ret;
}
};
} // namespace haar_lib
#line 2 "Mylib/IO/input_tuples.cpp"
#include <initializer_list>
#line 4 "Mylib/IO/input_tuples.cpp"
#include <tuple>
#include <utility>
#line 6 "Mylib/IO/input_tuple.cpp"
namespace haar_lib {
template <typename T, size_t... I>
static void input_tuple_helper(std::istream &s, T &val, std::index_sequence<I...>) {
(void) std::initializer_list<int>{(void(s >> std::get<I>(val)), 0)...};
}
template <typename T, typename U>
std::istream &operator>>(std::istream &s, std::pair<T, U> &value) {
s >> value.first >> value.second;
return s;
}
template <typename... Args>
std::istream &operator>>(std::istream &s, std::tuple<Args...> &value) {
input_tuple_helper(s, value, std::make_index_sequence<sizeof...(Args)>());
return s;
}
} // namespace haar_lib
#line 8 "Mylib/IO/input_tuples.cpp"
namespace haar_lib {
template <typename... Args>
class InputTuples {
struct iter {
using value_type = std::tuple<Args...>;
value_type value;
bool fetched = false;
int N, c = 0;
value_type operator*() {
if (not fetched) {
std::cin >> value;
}
return value;
}
void operator++() {
++c;
fetched = false;
}
bool operator!=(iter &) const {
return c < N;
}
iter(int N) : N(N) {}
};
int N;
public:
InputTuples(int N) : N(N) {}
iter begin() const { return iter(N); }
iter end() const { return iter(N); }
};
template <typename... Args>
auto input_tuples(int N) {
return InputTuples<Args...>(N);
}
} // namespace haar_lib
#line 3 "Mylib/IO/join.cpp"
#include <sstream>
#line 5 "Mylib/IO/join.cpp"
namespace haar_lib {
template <typename Iter>
std::string join(Iter first, Iter last, std::string delim = " ") {
std::stringstream s;
for (auto it = first; it != last; ++it) {
if (it != first) s << delim;
s << *it;
}
return s.str();
}
} // namespace haar_lib
#line 9 "test/yosupo-judge/two_sat/main.test.cpp"
namespace hl = haar_lib;
int main() {
std::string p, cnf;
int N, M;
std::cin >> p >> cnf >> N >> M;
hl::two_sat sat(N);
for (auto [a, b, c] : hl::input_tuples<int, int, int>(M)) {
sat.add_or(a, b);
}
if (auto res = sat.solve(); res) {
std::vector<int> ans(N);
for (int i = 0; i < N; ++i) ans[i] = (*res)[i] ? i + 1 : -(i + 1);
std::cout
<< "s SATISFIABLE" << std::endl
<< "v " << hl::join(ans.begin(), ans.end()) << " " << 0 << std::endl;
} else {
std::cout << "s UNSATISFIABLE" << std::endl;
}
return 0;
}
test/yosupo-judge/two_sat/main.test.cpp
Basic graph
(Mylib/Graph/Template/graph.cpp)