test/math/two_sat.test.cpp

View this file on GitHub
Last update: 2023-05-26 21:39:22+09:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

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

#include "../../template/template.hpp"
#include "../../math/two_sat.hpp"

using namespace lib;

int main() {
    char p;
    std::string cnf;
    std::cin >> p >> cnf;
    int n, m;
    std::cin >> n >> m;
    two_sat ts(n);
    for (int i = 0; i < m; i++) {
        int a, b, c;
        std::cin >> a >> b >> c;
        ts.add_clause(std::abs(a) - 1, a > 0, std::abs(b) - 1, b > 0);
    }
    bool flag = ts.satisfiable();
    std::cout << "s " << (flag ? "SATISFIABLE" : "UNSATISFIABLE") << std::endl;
    if (flag) {
        std::cout << "v";
        auto ans = ts.ans();
        for (int i = 0; i < n; i++) {
            std::cout << " " << (ans[i] ? i + 1 : -(i + 1));
        }
        std::cout << " 0\n";
    }
}

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

#line 2 "template/template.hpp"

#include <bits/stdc++.h>

#define rep(i, s, n) for (int i = (int)(s); i < (int)(n); i++)
#define rrep(i, s, n) for (int i = (int)(n)-1; i >= (int)(s); i--)
#define all(v) v.begin(), v.end()

using ll = long long;
using ld = long double;
using ull = unsigned long long;

template <typename T> bool chmin(T &a, const T &b) {
    if (a <= b) return false;
    a = b;
    return true;
}
template <typename T> bool chmax(T &a, const T &b) {
    if (a >= b) return false;
    a = b;
    return true;
}

namespace lib {

using namespace std;

}  // namespace lib

// using namespace lib;
#line 2 "math/two_sat.hpp"

#line 2 "graph/scc_graph.hpp"

#line 4 "graph/scc_graph.hpp"

namespace lib {

struct scc_graph {
    vector<vector<int>> g, rg;
    int n, k;

    vector<int> vs, cmp;
    vector<int> seen;

    void dfs(int v) {
        seen[v] = 1;
        for (auto &nv : g[v]) {
            if (seen[nv] < 0) dfs(nv);
        }
        vs.emplace_back(v);
    }

    void rdfs(int v) {
        cmp[v] = k;
        for (auto nv : rg[v]) {
            if (cmp[nv] < 0) rdfs(nv);
        }
    }

    scc_graph(int n) : n(n) {
        g.resize(n);
        rg.resize(n);
    }

    void add_edge(int from, int to) {
        g[from].emplace_back(to);
        rg[to].emplace_back(from);
    }

    void scc() {
        seen.assign(n, -1);
        rep(i, 0, n) {
            if (seen[i] < 0) dfs(i);
        }
        reverse(all(vs));
        cmp.assign(n, -1);
        k = 0;
        for (auto &v : vs) {
            if (cmp[v] < 0) {
                rdfs(v);
                k++;
            }
        }
    }

    bool same(int u, int v) {
        return cmp[u] == cmp[v];
    }

    vector<int> scc_id() {
        return cmp;
    }

    vector<vector<int>> create_graph() {
        vector<vector<int>> t(k);
        rep(i, 0, n) {
            int v = cmp[i];
            for (auto to : g[i]) {
                int nv = cmp[to];
                if (v == nv) continue;
                t[v].emplace_back(nv);
            }
        }
        rep(i, 0, k) {
            sort(all(t[i]));
            t[i].erase(unique(all(t[i])), t[i].end());
        }
        return t;
    }
};

}
#line 5 "math/two_sat.hpp"

namespace lib {

struct two_sat {
    two_sat(int n) : n(n), scc(2 * n), _ans(n) {}

    void add_clause(int i, bool f, int j, bool g) {
        assert(0 <= i && i < n);
        assert(0 <= j && j < n);
        scc.add_edge(2 * i + (f ? 0 : 1), 2 * j + (g ? 1 : 0));
        scc.add_edge(2 * j + (g ? 0 : 1), 2 * i + (f ? 1 : 0));
    }

    bool satisfiable() {
        scc.scc();
        auto id = scc.scc_id();
        rep(i, 0, n) {
            if (scc.same(2 * i, 2 * i + 1)) return false;
            _ans[i] = id[2 * i] < id[2 * i + 1];
        }
        return true;
    }

    vector<bool> ans() {
        return _ans;
    }
    int n;
    scc_graph scc;
    vector<bool> _ans;
};

}  // namespace lib
#line 5 "test/math/two_sat.test.cpp"

using namespace lib;

int main() {
    char p;
    std::string cnf;
    std::cin >> p >> cnf;
    int n, m;
    std::cin >> n >> m;
    two_sat ts(n);
    for (int i = 0; i < m; i++) {
        int a, b, c;
        std::cin >> a >> b >> c;
        ts.add_clause(std::abs(a) - 1, a > 0, std::abs(b) - 1, b > 0);
    }
    bool flag = ts.satisfiable();
    std::cout << "s " << (flag ? "SATISFIABLE" : "UNSATISFIABLE") << std::endl;
    if (flag) {
        std::cout << "v";
        auto ans = ts.ans();
        for (int i = 0; i < n; i++) {
            std::cout << " " << (ans[i] ? i + 1 : -(i + 1));
        }
        std::cout << " 0\n";
    }
}