test/graph/twosat.test.cpp

View this file on GitHub
Last update: 2025-10-17 22:12:07+08:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

// competitive-verifier: PROBLEM https://judge.yosupo.jp/problem/two_sat
#include <bits/stdc++.h>
#define PUSHB push_back
using namespace std;
using ll = long long;

#include "../../src/graph/twosat.hpp"
#include "../../src/misc/read.hpp"

int main() {
  cin.tie(nullptr)->sync_with_stdio(false);
  for (int _ = 0; _ < 6; _++) getchar();
  int n = read(), m = read();
  TwoSat ts(n);
  for (int _ = 0; _ < m; _++) {
    int a = read(), b = read(), unused = read();
    ts.adde(abs(a) - 1, a > 0, abs(b) - 1, b > 0);
  }
  auto resp = ts.work();
  if (resp) {
    cout << "s SATISFIABLE\n";
    cout << "v";
    for (int i = 0; i < n; i++) {
      cout << " " << (ts.ans[i] ? 1 : -1) * (i + 1);
    }
    cout << " 0\n";
  } else {
    cout << "s UNSATISFIABLE\n";
  }
  return 0;
}

#line 1 "test/graph/twosat.test.cpp"
// competitive-verifier: PROBLEM https://judge.yosupo.jp/problem/two_sat
#include <bits/stdc++.h>
#define PUSHB push_back
using namespace std;
using ll = long long;

#line 1 "src/graph/twosat.hpp"
// 2-SAT 问题: 给定 $n$ 个布尔变量, 与 $m$ 个形式为 $(x_i = f) \lor (x_j = g)$ 的条件.
// 如果有解答案构造在 `ans` 中.
#line 1 "src/graph/scc.hpp"
// 有向图的强连通分量. 返回强联通分量个数, 点对应的强连通分量编号在 `sccid` 中.
struct SCC {
  int n, cur_dfn, cur_scc;
  stack<int> stk;
  vector<int> dfn, low, sccid;
  vector<vector<int>> G;
  SCC(int n) : n(n), dfn(n, -1), low(n), sccid(n, -1), G(n) {}
  void adde(int u, int v) { G[u].PUSHB(v); }
  int work() {
    cur_dfn = cur_scc = 0;
    for (int i = 0; i < n; i++)
      if (dfn[i] == -1) tarjan(i);
    assert(stk.empty());
    return cur_scc;
  }

 private:
  void tarjan(int u) {
    dfn[u] = low[u] = cur_dfn++, stk.push(u);
    for (int v : G[u]) {
      if (dfn[v] == -1) {
        tarjan(v), low[u] = min(low[u], low[v]);
      } else if (sccid[v] == -1) {
        low[u] = min(low[u], dfn[v]);
      }
    }
    if (dfn[u] == low[u]) {
      int v;
      do {
        v = stk.top(), stk.pop(), sccid[v] = cur_scc;
      } while (v != u);
      cur_scc++;
    }
  }
};
#line 4 "src/graph/twosat.hpp"
struct TwoSat {
  int n;
  vector<char> ans;
  SCC scc;
  TwoSat(int n) : n(n), ans(n), scc(2 * n) {}
  void adde(int i, bool f, int j, bool g) {
    scc.adde(2 * i + !f, 2 * j + g), scc.adde(2 * j + !g, 2 * i + f);
  }
  bool work() {
    scc.work();
    const auto& sccid = scc.sccid;
    for (int i = 0; i < n; i++) {
      if (sccid[2 * i] == sccid[2 * i + 1]) return false;
      ans[i] = sccid[2 * i] > sccid[2 * i + 1];
    }
    return true;
  }
};
#line 1 "src/misc/read.hpp"
#define GC ch = getchar_unlocked()
ll read() {
  ll x = 0, f = 1, GC;
  while (ch < '0' || ch > '9') ch == '-' ? f = -1, GC : GC;
  while (ch >= '0' && ch <= '9') x = x * 10 + ch - '0', GC;
  return x * f;
}
#undef GC
#line 9 "test/graph/twosat.test.cpp"

int main() {
  cin.tie(nullptr)->sync_with_stdio(false);
  for (int _ = 0; _ < 6; _++) getchar();
  int n = read(), m = read();
  TwoSat ts(n);
  for (int _ = 0; _ < m; _++) {
    int a = read(), b = read(), unused = read();
    ts.adde(abs(a) - 1, a > 0, abs(b) - 1, b > 0);
  }
  auto resp = ts.work();
  if (resp) {
    cout << "s SATISFIABLE\n";
    cout << "v";
    for (int i = 0; i < n; i++) {
      cout << " " << (ts.ans[i] ? 1 : -1) * (i + 1);
    }
    cout << " 0\n";
  } else {
    cout << "s UNSATISFIABLE\n";
  }
  return 0;
}

Test cases

Env	Name	Status	Elapsed	Memory
g++	cycle_unsat_00	AC	144 ms	146 MB
g++	cycle_unsat_01	AC	146 ms	150 MB
g++	example_00	AC	5 ms	4 MB
g++	example_01	AC	5 ms	4 MB
g++	long_chain_00	AC	171 ms	152 MB
g++	long_chain_01	AC	182 ms	152 MB
g++	long_chain_02	AC	148 ms	111 MB
g++	long_chain_03	AC	147 ms	111 MB
g++	max_random_00	AC	391 ms	59 MB
g++	max_random_01	AC	384 ms	59 MB
g++	max_random_02	AC	377 ms	59 MB
g++	max_random_03	AC	403 ms	59 MB
g++	max_random_04	AC	385 ms	59 MB
g++	random_00	AC	283 ms	47 MB
g++	random_01	AC	311 ms	53 MB
g++	random_02	AC	77 ms	21 MB
g++	random_03	AC	58 ms	35 MB
g++	random_04	AC	89 ms	28 MB