tests/2_Sat.test.cpp

View this file on GitHub
Last update: 2025-11-28 02:09:51+07:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#include "../misc/macros.h"
#include "../graph/2SAT.h"

void solve() {
  string rid;
  cin >> rid >> rid;
  int n, m;
  cin >> n >> m;
  TwoSat ts(n);
  for (int i = 0; i < m; ++i) {
    int a, b, rid;
    cin >> a >> b >> rid;
    if (a < 0)
      a = ~(-a - 1);
    else
      --a;
    if (b < 0)
      b = ~(-b - 1);
    else
      --b;
    ts.either(a, b);
  }
  if (ts.solve()) {
    cout << "s SATISFIABLE\n";
    cout << "v ";
    for (int i = 0; i < n; ++i) cout << (ts.values[i] ? i + 1 : -i - 1) << " ";
    cout << "0\n";
  } else {
    cout << "s UNSATISFIABLE\n";
  }
}

int main() {
  cin.tie(0)->sync_with_stdio(0);
  cin.exceptions(cin.failbit);
  int tc = 1;
  // cin >> tc;
  for (int i = 1; i <= tc; ++i) {
    solve();
  }
}

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

#line 1 "misc/macros.h"
// #pragma GCC optimize("Ofast,unroll-loops")       // unroll long, simple loops
// #pragma GCC target("avx2,fma")                   // vectorizing code
// #pragma GCC target("lzcnt,popcnt,abm,bmi,bmi2")  // for fast bitset operation

#include <bits/extc++.h>
#include <tr2/dynamic_bitset>

using namespace std;
using namespace __gnu_pbds;  // ordered_set, gp_hash_table
// using namespace __gnu_cxx; // rope

// for templates to work
#define all(x) (x).begin(), (x).end()
#define sz(x) (int) (x).size()
#define pb push_back
#define eb emplace_back
using i32 = int32_t;
using u32 = uint32_t;
using i64 = int64_t;
using u64 = uint64_t;
using i128 = __int128_t;
using u128 = __uint128_t;
using ld = long double;
using pii = pair<i32, i32>;
using vi = vector<i32>;

// fast map
const int RANDOM = chrono::high_resolution_clock::now().time_since_epoch().count();
struct chash {  // customize hash function for gp_hash_table
  int operator()(int x) const { return x ^ RANDOM; }
};
gp_hash_table<int, int, chash> table;

/* ordered set
    find_by_order(k): returns an iterator to the k-th element (0-based)
    order_of_key(k): returns the number of elements in the set that are strictly less than k
*/
template <class T>
using ordered_set = tree<T, null_type, less<T>, rb_tree_tag, tree_order_statistics_node_update>;

/*  rope
    rope <int> cur = v.substr(l, r - l + 1);
    v.erase(l, r - l + 1);
    v.insert(v.mutable_begin(), cur);
*/
#line 1 "graph/2SAT.h"
/**
 * Usage: TwoSat ts(number of boolean variables);
 *  ts.either(0, ~3); // Var 0 is true or var 3 is false
 *  ts.setValue(2); // Var 2 is true
 *  ts.atMostOne({0,~1,2}); // <= 1 of vars 0, ~1 and 2 are true
 *  ts.solve(); // Returns true iff it is solvable
 *  ts.values[0..N-1] holds the assigned values to the vars
 */
struct TwoSat {
  int N;
  vector<vi> gr;
  vi values;  // 0 = false, 1 = true
  TwoSat(int n = 0) : N(n), gr(2 * n) {}
  int addVar() {  // (optional)
    gr.eb(), gr.eb();
    return N++;
  }
  void either(int f, int j) {
    f = max(2 * f, -1 - 2 * f), j = max(2 * j, -1 - 2 * j);
    gr[f].eb(j ^ 1), gr[j].eb(f ^ 1);
  }
  void setValue(int x) { either(x, x); }
  void atMostOne(const vi& li) {  // (optional)
    if (sz(li) <= 1) return;
    int cur = ~li[0];
    for (int i = 2; i < sz(li); ++i) {
      int next = addVar();
      either(cur, ~li[i]), either(cur, next), either(~li[i], next);
      cur = ~next;
    }
    either(cur, ~li[1]);
  }
  vi val, comp, z;
  int time = 0;
  int dfs(int i) {
    int low = val[i] = ++time, x;
    z.push_back(i);
    for (int e : gr[i]) {
      if (!comp[e]) low = min(low, val[e] ?: dfs(e));
    }
    if (low == val[i]) {
      do {
        x = z.back(), z.pop_back(), comp[x] = low;
        if (values[x >> 1] == -1) values[x >> 1] = x & 1;
      } while (x != i);
    }
    return val[i] = low;
  }
  bool solve() {
    values.assign(N, -1);
    val.assign(2 * N, 0);
    comp = val;
    for (int i = 0; i < 2 * N; ++i)
      if (!comp[i]) dfs(i);
    for (int i = 0; i < N; ++i)
      if (comp[2 * i] == comp[2 * i + 1]) return 0;
    return 1;
  }
};
#line 5 "tests/2_Sat.test.cpp"

void solve() {
  string rid;
  cin >> rid >> rid;
  int n, m;
  cin >> n >> m;
  TwoSat ts(n);
  for (int i = 0; i < m; ++i) {
    int a, b, rid;
    cin >> a >> b >> rid;
    if (a < 0)
      a = ~(-a - 1);
    else
      --a;
    if (b < 0)
      b = ~(-b - 1);
    else
      --b;
    ts.either(a, b);
  }
  if (ts.solve()) {
    cout << "s SATISFIABLE\n";
    cout << "v ";
    for (int i = 0; i < n; ++i) cout << (ts.values[i] ? i + 1 : -i - 1) << " ";
    cout << "0\n";
  } else {
    cout << "s UNSATISFIABLE\n";
  }
}

int main() {
  cin.tie(0)->sync_with_stdio(0);
  cin.exceptions(cin.failbit);
  int tc = 1;
  // cin >> tc;
  for (int i = 1; i <= tc; ++i) {
    solve();
  }
}