2-SAT
(lib/graph/two_sat.hpp)

• View this file on GitHub
• Last update: 2024-11-25 23:39:35+09:00
• Include: #include "lib/graph/two_sat.hpp"
• Link: https://noshi91.hatenablog.com/entry/2019/10/03/184812
• Link: https://zenn.dev/magurofly/articles/9d8417a17231db

Depends on

• Strongly Connected Component (強連結成分分解) (lib/graph/scc.hpp)

Verified with

• test/library_checker/other/two_sat.test.cpp

Code

#pragma once

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

#include "../graph/scc.hpp"

#include <vector>
#include <cassert>

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 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
 */

#include <vector>
#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;
    }
};

Back to top page