2-SAT
(math/two_sat.hpp)

• View this file on GitHub
• Last update: 2025-03-09 11:05:50+09:00
• Include: #include "math/two_sat.hpp"

Depends on

• グラフ構造体 (graph/graph_template.hpp)
• 強連結成分分解(SCC) (graph/scc.hpp)

Verified with

• test/library-checker/math/two-sat.test.cpp

Code

#pragma once

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

template<class Cost = int>
class TwoSat {
public:
    TwoSat() = default;
    explicit TwoSat(int N): N(N), scc(N * 2), ans(N), called_satisfiable(false) {}

    void add_clause(int i, bool f_i, int j, bool f_j) {
        if(!f_i) i = NOT(i);
        if(!f_j) j = NOT(j);
        scc.add_directed_edge(i, NOT(j));
        scc.add_directed_edge(j, NOT(i));
    }
    bool satisfiable() {
        scc.build();
        for(int i = 0; i < N; i++) {
            if(scc[i] == scc[NOT(i)]) return false;
            ans[i] = (scc[i] < scc[NOT(i)]);
        }
        called_satisfiable = true;
        return true;
    }
    std::vector<bool> get_answer() const {
        assert(called_satisfiable);
        return ans;
    }

private:
    int N;
    SCC<Cost> scc;
    std::vector<bool> ans;
    bool called_satisfiable;

    inline int NOT(int i) { return i + (i < N ? N : -N); }
};

#line 2 "math/two_sat.hpp"

#line 2 "graph/scc.hpp"

#include <algorithm>
#include <cassert>
#include <vector>

#line 2 "graph/graph_template.hpp"

#line 5 "graph/graph_template.hpp"

template <typename Cost = int> struct Edge {
    int from, to;
    Cost cost;
    int id;
    Edge() = default;
    explicit Edge(int from, int to, Cost cost = 1, int id = -1)
        : from(from), to(to), cost(cost), id(id) {}
    operator int() const { return to; }
};

template <typename Cost = int> class Graph {
  public:
    Graph() = default;
    explicit Graph(int N) : N(N), M(0), G(N) {}

    inline void add_directed_edge(int from, int to, Cost cost = 1) {
        assert(0 <= from && from < N);
        assert(0 <= to && to < N);
        G[from].emplace_back(from, to, cost, M++);
    }

    inline void add_undirected_edge(int from, int to, Cost cost = 1) {
        assert(0 <= from && from < N);
        assert(0 <= to && to < N);
        G[from].emplace_back(from, to, cost, M);
        G[to].emplace_back(to, from, cost, M++);
    }

    inline size_t size() const { return G.size(); }
    inline std::vector<Edge<Cost>> &operator[](const int &i) { return G[i]; }
    inline const std::vector<Edge<Cost>> &operator[](const int &i) const {
        return G[i];
    }

  protected:
    int N, M;
    std::vector<std::vector<Edge<Cost>>> G;
};

template <class Cost = int> using Edges = std::vector<Edge<Cost>>;
#line 8 "graph/scc.hpp"

template <typename Cost = int> class SCC {
  public:
    explicit SCC(int N)
        : G(N), G_rev(N), comp(N, -1), seen(N, false), isBuilt(false) {}
    explicit SCC(const Graph<Cost> &g)
        : G(g), G_rev(g.size()), comp(g.size(), -1), seen(g.size(), false), isBuilt(false) {
        for(int i = 0; i < (int)g.size(); i++) {
            for(const auto &e : g[i]) G_rev.add_directed_edge(e.to, i);
        }
        build();
    }
    inline void add_directed_edge(int from, int to) {
        assert(!isBuilt &&
               "This scc_graph is already built, but you tried to add edge.");
        G.add_directed_edge(from, to);
        G_rev.add_directed_edge(to, from);
    }
    void build() {
        assert(!isBuilt && "This scc_graph is already built.");
        for(int i = 0; i < (int)G.size(); i++) {
            if(!seen[i]) dfs(i);
        }
        std::reverse(vs.begin(), vs.end());
        count = 0;
        for(const int v : vs) {
            if(comp[v] == -1) {
                dfs_rev(v, count);
                count++;
            }
        }
        isBuilt = true;
    }
    Graph<Cost> get_contracted_graph() {
        assert(isBuilt && "This scc_graph is not yet built.");
        Graph<Cost> new_g(count);
        for(int i = 0; i < (int)G.size(); i++) {
            for(const auto &e : G[i]) {
                int from = comp[i];
                int to = comp[e.to];
                if(from != to) new_g.add_directed_edge(from, to, e.cost);
            }
        }
        return new_g;
    }
    int operator[](const int &k) const {
        assert(isBuilt && "This scc_graph is not yet built.");
        return comp[k];
    }
    size_t size() { return (size_t)count; }

  private:
    Graph<Cost> G, G_rev;
    std::vector<int> vs, comp;
    std::vector<bool> seen;
    int count;
    bool isBuilt;

    void dfs(int u) {
        seen[u] = true;
        for(const auto &e : G[u]) {
            if(!seen[e.to]) dfs(e.to);
        }
        vs.push_back(u);
    }
    void dfs_rev(int u, int idx) {
        comp[u] = idx;
        for(const auto &e : G_rev[u]) {
            if(comp[e.to] == -1) dfs_rev(e.to, idx);
        }
    }
};
#line 4 "math/two_sat.hpp"

template<class Cost = int>
class TwoSat {
public:
    TwoSat() = default;
    explicit TwoSat(int N): N(N), scc(N * 2), ans(N), called_satisfiable(false) {}

    void add_clause(int i, bool f_i, int j, bool f_j) {
        if(!f_i) i = NOT(i);
        if(!f_j) j = NOT(j);
        scc.add_directed_edge(i, NOT(j));
        scc.add_directed_edge(j, NOT(i));
    }
    bool satisfiable() {
        scc.build();
        for(int i = 0; i < N; i++) {
            if(scc[i] == scc[NOT(i)]) return false;
            ans[i] = (scc[i] < scc[NOT(i)]);
        }
        called_satisfiable = true;
        return true;
    }
    std::vector<bool> get_answer() const {
        assert(called_satisfiable);
        return ans;
    }

private:
    int N;
    SCC<Cost> scc;
    std::vector<bool> ans;
    bool called_satisfiable;

    inline int NOT(int i) { return i + (i < N ? N : -N); }
};

Back to top page