2-SAT

struct SAT_2 {
    int n;
    vector<vector<int>> g, grev;

    SAT_2(int n = 0) : n(n) {
        g.assign(2 * n, {});
        grev.assign(2 * n, {});
    };

    void add_clause(bool positive_x, int x, bool positive_y, int y) { // (x v !y) -> (true, x, false, y)
        assert(0 <= x && x < n);
        assert(0 <= y && y < n);
        int vx = 2 * x + (positive_x ? 0 : 1);
        int vy = 2 * y + (positive_y ? 0 : 1);
        g[vx ^ 1].push_back(vy);
        grev[vy].push_back(vx ^ 1);
        g[vy ^ 1].push_back(vx);
        grev[vx].push_back(vy ^ 1);
    }

    vector<int> solve() { // return.empty() -> no solution, o/w -> x_i = bool(return[i])
        vector<int> used(2 * n, 0), topsort;
        function<void(int)> dfs_topsort = [&](int v) {
            used[v] = 1;
            for (int u : g[v]) {
                if (!used[u]) {
                    dfs_topsort(u);
                }
            }
            topsort.push_back(v);
        };
        for (int v = 0; v < 2 * n; v++) {
            if (!used[v]) {
                dfs_topsort(v);
            }
        }
        reverse(topsort.begin(), topsort.end());
        vector<int> cols(2 * n, -1);
        function<void(int, int)> dfs_color = [&](int v, int color) {
            cols[v] = color;
            for (int u : grev[v]) {
                if (cols[u] == -1) {
                    dfs_color(u, color);
                }
            }
        };
        int curcol = 0;
        for (int v : topsort) {
            if (cols[v] == -1) {
                dfs_color(v, curcol++);
            }
        }
        for (int v = 0; v < 2 * n; v += 2) {
            if (cols[v] == cols[v + 1]) {
                return {};
            }
        }
        vector<int> solution(n, 0);
        for (int v = 0; v < 2 * n; v += 2) {
            solution[v >> 1] = (cols[v] > cols[v + 1] ? 1 : 0);
        }
        return solution;
    }
};