Graph/two_sat.hpp

View this file on GitHub
Last update: 2020-11-05 12:15:41+09:00
Include: #include "Graph/two_sat.hpp"

Depends on

Verified with

Verify/two_sat.test.cpp

Code

#pragma once

#include "strongly_connected_component.hpp"

struct TwoSat {
    int vnum;
    Graph<> graph;
    std::vector<bool> assign;

    explicit TwoSat(int n) : vnum(n), graph(n * 2), assign(n) {}

    int enc(int x, bool t) { return x + (t ? vnum : 0); }

    // (v_x = tx) or (v_y = ty)
    void add(int x, bool tx, int y, bool ty) {
        graph.span(true, enc(x, !tx), enc(y, ty));
        graph.span(true, enc(y, !ty), enc(x, tx));
    }

    // assign is also updated
    bool judge() {
        StronglyConnectedComponents scc(graph);

        for (int x = 0; x < vnum; ++x) {
            int fid = scc.id[enc(x, false)],
                tid = scc.id[enc(x, true)];

            if (fid == tid) {
                return false;
            } else {
                assign[x] = (fid < tid);
            }
        }
        return true;
    }
};

#line 2 "Graph/two_sat.hpp"

#line 2 "Graph/strongly_connected_component.hpp"

#line 2 "Graph/graph.hpp"

#include <vector>

template <class Cost = int>
struct Edge {
    int src, dst;
    Cost cost;

    Edge() = default;
    Edge(int src, int dst, Cost cost = 1)
        : src(src), dst(dst), cost(cost){};

    bool operator<(const Edge<Cost>& e) const { return cost < e.cost; }
    bool operator>(const Edge<Cost>& e) const { return cost > e.cost; }
};

template <class Cost = int>
struct Graph : public std::vector<std::vector<Edge<Cost>>> {
    using std::vector<std::vector<Edge<Cost>>>::vector;

    void span(bool direct, int src, int dst, Cost cost = 1) {
        (*this)[src].emplace_back(src, dst, cost);
        if (!direct) (*this)[dst].emplace_back(dst, src, cost);
    }
};
#line 4 "Graph/strongly_connected_component.hpp"

#line 6 "Graph/strongly_connected_component.hpp"

template <class Cost = int>
struct StronglyConnectedComponents {
    Graph<Cost> graph, rgraph;
    std::vector<bool> visited;
    std::vector<int> stk;

    // id[v] = 頂点vはgroups[id[v]]に属する
    std::vector<int> id;
    std::vector<std::vector<int>> groups;

    explicit StronglyConnectedComponents(const Graph<Cost>& g)
        : graph(g), visited(graph.size(), false), id(graph.size(), -1) {
        revinit();

        for (int v = 0; v < (int)graph.size(); ++v) dfs(v);

        while (!stk.empty()) {
            int v = stk.back();
            stk.pop_back();
            if (id[v] < 0) {
                groups.emplace_back();
                rdfs(v);
            }
        }
    }

    void revinit() {
        rgraph = Graph<Cost>(graph.size());
        for (int v = 0; v < (int)graph.size(); ++v) {
            for (const auto& e : graph[v]) {
                rgraph[e.dst].emplace_back(e.dst, v, e.cost);
            }
        }
    }

    void dfs(int v) {
        if (visited[v]) return;
        visited[v] = true;
        for (const auto& e : graph[v]) dfs(e.dst);
        stk.push_back(v);
    }

    void rdfs(int v) {
        if (id[v] >= 0) return;
        id[v] = groups.size() - 1;
        groups.back().push_back(v);
        for (const auto& e : rgraph[v]) rdfs(e.dst);
    }
};
#line 4 "Graph/two_sat.hpp"

struct TwoSat {
    int vnum;
    Graph<> graph;
    std::vector<bool> assign;

    explicit TwoSat(int n) : vnum(n), graph(n * 2), assign(n) {}

    int enc(int x, bool t) { return x + (t ? vnum : 0); }

    // (v_x = tx) or (v_y = ty)
    void add(int x, bool tx, int y, bool ty) {
        graph.span(true, enc(x, !tx), enc(y, ty));
        graph.span(true, enc(y, !ty), enc(x, tx));
    }

    // assign is also updated
    bool judge() {
        StronglyConnectedComponents scc(graph);

        for (int x = 0; x < vnum; ++x) {
            int fid = scc.id[enc(x, false)],
                tid = scc.id[enc(x, true)];

            if (fid == tid) {
                return false;
            } else {
                assign[x] = (fid < tid);
            }
        }
        return true;
    }
};