sotanishy's code snippets for competitive programming
View the Project on GitHub sotanishy/cp-library-cpp
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat" #include "../../sat/twosat.hpp" #include <bits/stdc++.h> using namespace std; using ll = long long; int main() { string _p, _cnf; int N, M; cin >> _p >> _cnf >> N >> M; vector<tuple<int, bool, int, bool>> clauses; for (int i = 0; i < M; i++) { int a, b, _c; cin >> a >> b >> _c; clauses.push_back({abs(a) - 1, (a > 0), abs(b) - 1, (b > 0)}); } auto ans = two_sat(N, clauses); if (!ans.empty()) { cout << "s SATISFIABLE\nv"; for (int i = 0; i < N; i++) { cout << " " << (ans[i] ? 1 : -1) * (i + 1); } cout << " 0\n"; } else { cout << "s UNSATISFIABLE\n"; } }
#line 1 "test/yosupo/two_sat.test.cpp" #define PROBLEM "https://judge.yosupo.jp/problem/two_sat" #line 2 "sat/twosat.hpp" #include <vector> #line 2 "graph/scc.hpp" #include <algorithm> #include <ranges> #line 5 "graph/scc.hpp" std::vector<int> scc(const std::vector<std::vector<int>>& G) { const int n = G.size(); std::vector<std::vector<int>> G_rev(n); for (int u = 0; u < n; ++u) { for (int v : G[u]) G_rev[v].push_back(u); } std::vector<int> comp(n, -1), order(n); std::vector<bool> visited(n); auto dfs = [&](const auto& dfs, int u) -> void { if (visited[u]) return; visited[u] = true; for (int v : G[u]) dfs(dfs, v); order.push_back(u); }; for (int v = 0; v < n; ++v) dfs(dfs, v); int c = 0; auto rdfs = [&](const auto& rdfs, int u, int c) -> void { if (comp[u] != -1) return; comp[u] = c; for (int v : G_rev[u]) rdfs(rdfs, v, c); }; for (int v : order | std::views::reverse) { if (comp[v] == -1) rdfs(rdfs, v, c++); } return comp; } std::vector<std::vector<int>> contract(const std::vector<std::vector<int>>& G, const std::vector<int>& comp) { const int n = *std::ranges::max_element(comp) + 1; std::vector<std::vector<int>> G2(n); for (int i = 0; i < (int)G.size(); ++i) { for (int j : G[i]) { if (comp[i] != comp[j]) { G2[comp[i]].push_back(comp[j]); } } } for (int i = 0; i < n; ++i) { std::ranges::sort(G2[i]); G2[i].erase(std::ranges::unique(G2[i]).begin(), G2[i].end()); } return G2; } #line 5 "sat/twosat.hpp" std::vector<bool> two_sat( int n, const std::vector<std::tuple<int, bool, int, bool>>& clauses) { std::vector<std::vector<int>> G(2 * n); std::vector<bool> val(n); for (auto& [i, f, j, g] : clauses) { G[n * f + i].push_back(n * (!g) + j); G[n * g + j].push_back(n * (!f) + i); } auto comp = scc(G); for (int i = 0; i < n; ++i) { if (comp[i] == comp[n + i]) { // not satisfiable return {}; } val[i] = comp[i] > comp[n + i]; } return val; } #line 4 "test/yosupo/two_sat.test.cpp" #include <bits/stdc++.h> using namespace std; using ll = long long; int main() { string _p, _cnf; int N, M; cin >> _p >> _cnf >> N >> M; vector<tuple<int, bool, int, bool>> clauses; for (int i = 0; i < M; i++) { int a, b, _c; cin >> a >> b >> _c; clauses.push_back({abs(a) - 1, (a > 0), abs(b) - 1, (b > 0)}); } auto ans = two_sat(N, clauses); if (!ans.empty()) { cout << "s SATISFIABLE\nv"; for (int i = 0; i < N; i++) { cout << " " << (ans[i] ? 1 : -1) * (i + 1); } cout << " 0\n"; } else { cout << "s UNSATISFIABLE\n"; } }