2sat.cpp

// 2-SAT solver based on Kosaraju's algorithm.
// Variables are 0-based. Positive variables are stored in
// vertices 2n, corresponding negative variables in 2n+1
// TODO: This is quite slow (3x-4x slower than Gabow's
// algorithm)
struct TwoSat {
  int n;
  vector<vector<int>> adj, radj, scc;
  vector<int> sid, vis, val;
  stack<int> stk;
  int scnt;

  // n: number of variables, including negations
  TwoSat(int n)
      : n(n), adj(n), radj(n), sid(n), vis(n), val(n, -1) {}

  // adds an implication
  void impl(int x, int y) {
    adj[x].push_back(y);
    radj[y].push_back(x);
  }
  // adds a disjunction
  void vee(int x, int y) {
    impl(x ^ 1, y);
    impl(y ^ 1, x);
  }
  // forces variables to be equal
  void eq(int x, int y) {
    impl(x, y);
    impl(y, x);
    impl(x ^ 1, y ^ 1);
    impl(y ^ 1, x ^ 1);
  }
  // forces variable to be true
  void tru(int x) { impl(x ^ 1, x); }

  void dfs1(int x) {
    if (vis[x]++)
      return;
    for (int i = 0; i < adj[x].size(); i++) {
      dfs1(adj[x][i]);
    }
    stk.push(x);
  }

  void dfs2(int x) {
    if (!vis[x])
      return;
    vis[x] = 0;
    sid[x] = scnt;
    scc.back().push_back(x);
    for (int i = 0; i < radj[x].size(); i++) {
      dfs2(radj[x][i]);
    }
  }

  // returns true if satisfiable, false otherwise
  // on completion, val[x] is the assigned value of variable
  // x note, val[x] = 0 implies val[x^1] = 1
  bool two_sat() {
    scnt = 0;
    for (int i = 0; i < n; i++) {
      dfs1(i);
    }
    while (!stk.empty()) {
      int v = stk.top();
      stk.pop();
      if (vis[v]) {
        scc.push_back(vector<int>());
        dfs2(v);
        scnt++;
      }
    }
    for (int i = 0; i < n; i += 2) {
      if (sid[i] == sid[i + 1])
        return false;
    }
    vector<int> must(scnt);
    for (int i = 0; i < scnt; i++) {
      for (int j = 0; j < scc[i].size(); j++) {
        val[scc[i][j]] = must[i];
        must[sid[scc[i][j] ^ 1]] = !must[i];
      }
    }
    return true;
  }
};