graph/test/2_Sat.test.cpp

View this file on GitHub
Last update: 2023-07-25 00:50: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;

using ll = long long;

#include "../2sat.hpp"

void solve(int ith) {
  int n, m;
  string rid;
  cin >> rid >> rid >> n >> m;
  twosat ts(n);
  for (int i = 0; i < m; ++i) {
    int x, y;
    cin >> x >> y >> rid;
    ts.add_clause(x > 0, abs(x) - 1, y > 0, abs(y) - 1);
  }
  auto res = ts.solve();
  if (res.first) {
    cout << "s SATISFIABLE\n";
    cout << "v ";
    for (int i = 0; i < n; ++i) {
      cout << (res.second[i] ? i + 1 : -(i + 1)) << ' ';
    }
    cout << 0;
  } else
    cout << "s UNSATISFIABLE";
}

signed main() {
  ios::sync_with_stdio(false);
  cin.tie(nullptr), cin.exceptions(cin.failbit);
  int tc = 1;
  // cin >> tc;
  for (int i = 1; i <= tc; ++i) solve(i);
}

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

#include <bits/stdc++.h>

using namespace std;

using ll = long long;

#line 2 "graph/scc.hpp"

struct scc {
  vector<vector<int>> g;
  int n;
  vector<int> num, low, current, S;
  int counter;
  vector<int> id;
  vector<vector<int>> scc_list;

  scc(int n)
      : g(n),
        n(n),
        num(n, -1),
        low(n, 0),
        current(n, 0),
        counter(0),
        id(n, -1) {}

  void add_edge(int u, int v) { g[u].push_back(v); }

  void dfs(int u) {
    low[u] = num[u] = counter++;
    S.push_back(u);
    current[u] = 1;
    for (auto v : g[u]) {
      if (num[v] == -1) dfs(v);
      if (current[v]) low[u] = min(low[u], low[v]);
    }
    if (low[u] == num[u]) {
      scc_list.push_back(vector<int>());
      while (1) {
        int v = S.back();
        S.pop_back();
        current[v] = 0;
        scc_list.back().push_back(v);
        id[v] = (int)scc_list.size() - 1;
        if (u == v) break;
      }
    }
  }

  // build scc_list
  void build() {
    for (int i = 0; i < n; i++) {
      if (num[i] == -1) dfs(i);
    }
    reverse(begin(scc_list), end(scc_list));
  }

  // build DAG of strongly connected components
  // Returns: adjacency list of DAG, and root vertices (in-degree
  // = 0)
  pair<vector<vector<int>>, vector<int>> condense() {
    vector<vector<int>> dag(scc_list.size());
    vector<int> roots, in(scc_list.size());
    for (int u = 0; u < n; ++u) {
      int x = id[u];
      for (int v : g[u]) {
        int y = id[v];
        if (x != y) {
          dag[x].push_back(y);
          ++in[y];
        }
      }
    }
    for (int u = 0; u < (int)dag.size(); ++u)
      if (in[u] == 0) roots.push_back(u);
    return {dag, roots};
  }
};
#line 2 "graph/2sat.hpp"

struct twosat : scc {
  int n;
  twosat(int n) : scc(2 * n), n(n) {}

  // add 2-SAT clause
  void add_clause(bool is_x_true, int x, bool is_y_true, int y) {
    assert(x >= 0 && x < n);
    assert(y >= 0 && y < n);
    if (!is_x_true) x += n;
    if (!is_y_true) y += n;
    // x || y
    // !x -> y
    // !y -> x
    add_edge((x + n) % (2 * n), y);
    add_edge((y + n) % (2 * n), x);
  }

  // Returns:
  // If no sol -> returns {false, {}}
  // If has sol -> returns {true, sol}
  //    where |sol| = n, sol = true / false
  pair<bool, vector<bool>> solve() {
    build();
    vector<bool> sol(n);
    for (int i = 0; i < n; i++) {
      if (id[i] == id[i + n]) {
        return {false, {}};
      }
      sol[i] = id[i] < id[i + n];
    }
    return {true, sol};
  }
};
#line 10 "graph/test/2_Sat.test.cpp"

void solve(int ith) {
  int n, m;
  string rid;
  cin >> rid >> rid >> n >> m;
  twosat ts(n);
  for (int i = 0; i < m; ++i) {
    int x, y;
    cin >> x >> y >> rid;
    ts.add_clause(x > 0, abs(x) - 1, y > 0, abs(y) - 1);
  }
  auto res = ts.solve();
  if (res.first) {
    cout << "s SATISFIABLE\n";
    cout << "v ";
    for (int i = 0; i < n; ++i) {
      cout << (res.second[i] ? i + 1 : -(i + 1)) << ' ';
    }
    cout << 0;
  } else
    cout << "s UNSATISFIABLE";
}

signed main() {
  ios::sync_with_stdio(false);
  cin.tie(nullptr), cin.exceptions(cin.failbit);
  int tc = 1;
  // cin >> tc;
  for (int i = 1; i <= tc; ++i) solve(i);
}