2-SAT (other/two_sat.hpp)

Description

2-SAT solver using strongly connected components. Variables are represented as integers $0$ to $n-1$, with bitwise not representing negation (~x is $\neg x$).

Operations

TwoSAT(int n)
- Constructs 2-SAT instance with n variables
- Time complexity: $\mathcal O(1)$
void add_if(int x, int y)
- Adds constraint: if $x$ then $y$ (equivalent to $\neg x \lor y$)
- Time complexity: $\mathcal O(1)$
void add_or(int x, int y)
- Adds constraint: $x \lor y$
- Time complexity: $\mathcal O(1)$
void add_nand(int x, int y)
- Adds constraint: $\neg(x \land y)$ (equivalent to $\neg x \lor \neg y$)
- Time complexity: $\mathcal O(1)$
void set_true(int x)
- Forces variable $x$ to be true
- Time complexity: $\mathcal O(1)$
void set_false(int x)
- Forces variable $x$ to be false
- Time complexity: $\mathcal O(1)$
vector<bool> run()
- Solves the 2-SAT instance
- Returns a satisfying assignment if one exists, empty vector otherwise
- Time complexity: $\mathcal O(V + E)$ where $V = 2n$ and $E$ is the number of constraints

Depends on

Strongly Connected Components (graph/scc.hpp)

Verified with

test/yosupo/other/two_sat.test.cpp

Code

#pragma once

#include "../graph/scc.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 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; }
};