test/yosupo/other/two_sat.test.cpp

View this file on GitHub
Last update: 2025-09-20 17:47:50+07:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#include <bits/stdc++.h>
using namespace std;

#include "other/two_sat.hpp"

int main() {
    cin.tie(nullptr)->sync_with_stdio(false);
    int n, m;
    string buf;
    cin >> buf >> buf >> n >> m;
    TwoSAT solver(n);
    while (m--) {
        int x, y;
        cin >> x >> y >> buf;
        x = x < 0 ? ~(-x - 1) : x - 1;
        y = y < 0 ? ~(-y - 1) : y - 1;
        solver.add_or(x, y);
    }
    auto assignment = solver.run();
    if (assignment.empty()) {
        cout << "s UNSATISFIABLE\n";
        return 0;
    }
    cout << "s SATISFIABLE\nv ";
    for (int i = 0; i < n; i++)
        cout << (assignment[i] ? 1 : -1) * (i + 1) << " ";
    cout << "0\n";
}

#line 1 "test/yosupo/other/two_sat.test.cpp"
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#include <bits/stdc++.h>
using namespace std;

#line 2 "other/two_sat.hpp"

#line 2 "graph/scc.hpp"

template<class G> auto find_scc(const G &g) {
    int n = (int)g.size();
    vector<int> val(n), z;
    vector<char> added(n);
    vector<basic_string<int>> scc;
    int time = 0;
    auto dfs = [&](auto &self, int v) -> int {
        int low = val[v] = time++;
        z.push_back(v);
        for (auto u : g[v])
            if (!added[u]) low = min(low, val[u] ?: self(self, u));
        if (low == val[v]) {
            scc.emplace_back();
            int x;
            do {
                x = z.back(), z.pop_back();
                added[x] = true;
                scc.back().push_back(x);
            } while (x != v);
        }
        return val[v] = low;
    };
    for (int i = 0; i < n; i++)
        if (!added[i]) dfs(dfs, i);
    reverse(begin(scc), end(scc));
    return scc;
}
template<class G> auto condense(const G &g) {
    auto scc = find_scc(g);
    int n = (int)scc.size();
    vector<int> rep(g.size());
    for (int i = 0; i < n; i++)
        for (auto v : scc[i]) rep[v] = i;
    vector<basic_string<int>> gd(n);
    for (int v = 0; v < g.size(); v++)
        for (auto u : g[v])
            if (rep[v] != rep[u]) gd[rep[v]].push_back(rep[u]);
    for (auto &v : gd) {
        sort(begin(v), end(v));
        v.erase(unique(begin(v), end(v)), end(v));
    }
    return make_tuple(move(scc), move(rep), move(gd));
}
#line 4 "other/two_sat.hpp"

struct TwoSAT {
    int n;
    vector<basic_string<int>> g;

    TwoSAT(int _n) : n(_n), g(2 * n) {}

    void add_if(int x, int y) { g[ev(x)] += ev(y), g[ev(~y)] += ev(~x); }
    void add_or(int x, int y) { add_if(~x, y); }
    void add_nand(int x, int y) { add_if(x, ~y); }
    void set_true(int x) { add_if(~x, x); }
    void set_false(int x) { add_if(x, ~x); }

    vector<bool> run() {
        vector<bool> res(n);
        auto [scc, rep, gd] = condense(g);
        for (int i = 0; i < n; i++) {
            if (rep[i] == rep[i + n]) return {};
            res[i] = rep[i] > rep[i + n];
        }
        return res;
    }

    int ev(int x) { return x < 0 ? ~x + n : x; }
};
#line 7 "test/yosupo/other/two_sat.test.cpp"

int main() {
    cin.tie(nullptr)->sync_with_stdio(false);
    int n, m;
    string buf;
    cin >> buf >> buf >> n >> m;
    TwoSAT solver(n);
    while (m--) {
        int x, y;
        cin >> x >> y >> buf;
        x = x < 0 ? ~(-x - 1) : x - 1;
        y = y < 0 ? ~(-y - 1) : y - 1;
        solver.add_or(x, y);
    }
    auto assignment = solver.run();
    if (assignment.empty()) {
        cout << "s UNSATISFIABLE\n";
        return 0;
    }
    cout << "s SATISFIABLE\nv ";
    for (int i = 0; i < n; i++)
        cout << (assignment[i] ? 1 : -1) * (i + 1) << " ";
    cout << "0\n";
}

Test cases

Env	Name	Status	Elapsed	Memory
g++	cycle_unsat_00	AC	197 ms	132 MB
g++	cycle_unsat_01	AC	176 ms	141 MB
g++	example_00	AC	5 ms	4 MB
g++	example_01	AC	4 ms	4 MB
g++	long_chain_00	AC	233 ms	195 MB
g++	long_chain_01	AC	185 ms	149 MB
g++	long_chain_02	AC	189 ms	149 MB
g++	long_chain_03	AC	195 ms	148 MB
g++	max_random_00	AC	280 ms	104 MB
g++	max_random_01	AC	274 ms	104 MB
g++	max_random_02	AC	288 ms	104 MB
g++	max_random_03	AC	284 ms	103 MB
g++	max_random_04	AC	276 ms	103 MB
g++	random_00	AC	179 ms	81 MB
g++	random_01	AC	234 ms	95 MB
g++	random_02	AC	96 ms	23 MB
g++	random_03	AC	78 ms	88 MB
g++	random_04	AC	79 ms	59 MB
clang++	cycle_unsat_00	AC	177 ms	132 MB
clang++	cycle_unsat_01	AC	181 ms	141 MB
clang++	example_00	AC	5 ms	4 MB
clang++	example_01	AC	4 ms	4 MB
clang++	long_chain_00	AC	240 ms	196 MB
clang++	long_chain_01	AC	196 ms	148 MB
clang++	long_chain_02	AC	196 ms	149 MB
clang++	long_chain_03	AC	198 ms	149 MB
clang++	max_random_00	AC	278 ms	103 MB
clang++	max_random_01	AC	264 ms	104 MB
clang++	max_random_02	AC	260 ms	104 MB
clang++	max_random_03	AC	259 ms	103 MB
clang++	max_random_04	AC	261 ms	104 MB
clang++	random_00	AC	179 ms	81 MB
clang++	random_01	AC	222 ms	96 MB
clang++	random_02	AC	94 ms	23 MB
clang++	random_03	AC	82 ms	87 MB
clang++	random_04	AC	82 ms	59 MB