test/library_checker/other/two_sat.test.cpp

View this file on GitHub
Last update: 2024-11-25 23:39:35+09:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"
#include <iostream>
#include <vector>

#include "../../../lib/graph/two_sat.hpp"

using namespace std;

int main(){
    ios::sync_with_stdio(false);
    cin.tie(nullptr);

    string p, cnf; cin >> p >> cnf;
    int n, m; cin >> n >> m;
    TwoSAT SAT(n);
    for(int i = 0; i < m; i++){
        int a, b, c; cin >> a >> b >> c;
        SAT.add_clause(abs(a) - 1, a > 0, abs(b) - 1, b > 0);
    }
    SAT.build();
    vector<bool> ans = SAT.getAnswer();
    if(ans.empty()){
        cout << "s UNSATISFIABLE" << '\n';
    }else{
        cout << "s SATISFIABLE" << '\n';
        cout << "v ";
        for(int i = 0; i < n; i++){
            if(i) cout << ' ';
            cout << (ans[i] ? i + 1 : -i - 1);
        }
        cout << " 0" << '\n';
    }
    return 0;
}

#line 1 "test/library_checker/other/two_sat.test.cpp"

#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"
#include <iostream>
#include <vector>

#line 2 "lib/graph/two_sat.hpp"

/**
 * @brief 2-SAT
 * @see https://zenn.dev/magurofly/articles/9d8417a17231db https://noshi91.hatenablog.com/entry/2019/10/03/184812
 */

#line 2 "lib/graph/scc.hpp"

/**
 * @brief Strongly Connected Component (強連結成分分解)
 * @docs docs/graph/scc.md
 */

#line 9 "lib/graph/scc.hpp"
#include <cassert>
#include <algorithm>

struct SCC{
    int siz;
    std::vector<std::vector<int>> G, G_reverse, G_compress;
    std::vector<bool> check;
    std::vector<int> memo, id;
    std::vector<int> s;
    std::vector<std::vector<int>> result;

    SCC(const int N) : siz(N), G(N), G_reverse(N), check(N), id(N){ }

    void add_edge(int u, int v){
        assert(0 <= u && u < siz);
        assert(0 <= v && v < siz);
        G[u].emplace_back(v);
    }

    void build(){
        for(int i = 0; i < siz; ++i){
            for(const auto &x : G[i]){
                G_reverse[x].emplace_back(i);
            }
        }

        for(int i = 0; i < siz; ++i){
            if(!check[i]){
                dfs(G, i);
            }
        }
        reverse(memo.begin(), memo.end());

        for(int i = 0; i < siz; ++i) check[i] = false;
        for(const auto &x : memo){
            if(!check[x]){
                s = {};
                dfs2(G_reverse, x);
                for(const auto &y : s){
                    id[y] = (int) result.size();
                }
                result.emplace_back(s);
            }
        }

        G_compress.resize(result.size());
        for(int i = 0; i < siz; ++i){
            for(const auto &x : G[i]){
                if(id[i] != id[x]){
                    G_compress[id[i]].emplace_back(id[x]);
                }
            }
        }
    }

    void dfs(const std::vector<std::vector<int>> &G, int curr){
        check[curr] = true;
        for(const auto &x : G[curr]){
            if(check[x]){
                continue;
            }
            dfs(G, x);
        }
        memo.emplace_back(curr);
    }

    void dfs2(const std::vector<std::vector<int>> &G, int curr){
        s.emplace_back(curr);
        check[curr] = true;
        for(const auto &x : G[curr]){
            if(check[x]){
                continue;
            }
            dfs2(G, x);
        }
    }

    std::vector<std::vector<int>> get() const {
        return result;
    }

    std::vector<std::vector<int>> getCompressed() const {
        return G_compress;
    }

    int getId(int x) const {
        return id[x];
    }
};
#line 9 "lib/graph/two_sat.hpp"

#line 12 "lib/graph/two_sat.hpp"

struct TwoSAT{
    int N;
    SCC scc;
    std::vector<bool> ans;
    TwoSAT(const int N) : N(N), scc(2 * N){ }

    // ((x = f) or (y = g))
    void add_clause(int x, bool f, int y, bool g){
        assert(0 <= x && x < N);
        assert(0 <= y && y < N);
        int px = x * 2 + f, py = y * 2 + g;
        int nx = x * 2 + !f, ny = y * 2 + !g;
        scc.add_edge(nx, py);
        scc.add_edge(ny, px);
    }

    void build(){
        scc.build();
        for(int i = 0; i < N; i++){
            // x -> !x と !x -> x のパスが存在する場合は解なし
            if(scc.getId(i * 2) == scc.getId(i * 2 + 1)){
                return;
            }
        }
        ans.resize(N);
        for(int i = 0; i < N; i++){
            // !x -> x のパスが存在する可能性があるなら 真 を割り当てる
            ans[i] = scc.getId(i * 2) < scc.getId(i * 2 + 1);
        }
    }

    std::vector<bool> getAnswer() const {
        return ans;
    }
};
#line 7 "test/library_checker/other/two_sat.test.cpp"

using namespace std;

int main(){
    ios::sync_with_stdio(false);
    cin.tie(nullptr);

    string p, cnf; cin >> p >> cnf;
    int n, m; cin >> n >> m;
    TwoSAT SAT(n);
    for(int i = 0; i < m; i++){
        int a, b, c; cin >> a >> b >> c;
        SAT.add_clause(abs(a) - 1, a > 0, abs(b) - 1, b > 0);
    }
    SAT.build();
    vector<bool> ans = SAT.getAnswer();
    if(ans.empty()){
        cout << "s UNSATISFIABLE" << '\n';
    }else{
        cout << "s SATISFIABLE" << '\n';
        cout << "v ";
        for(int i = 0; i < n; i++){
            if(i) cout << ' ';
            cout << (ans[i] ? i + 1 : -i - 1);
        }
        cout << " 0" << '\n';
    }
    return 0;
}