Verify/two_sat.test.cpp

View this file on GitHub
Last update: 2020-11-05 12:15:41+09:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

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

#include "../Graph/two_sat.hpp"

#include <iostream>
#include <string>

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

    std::string tmp;
    int n, m;
    std::cin >> tmp >> tmp >> n >> m;

    TwoSat ts(n);
    while (m--) {
        int x, y;
        std::cin >> x >> y >> tmp;
        ts.add(std::abs(x) - 1, x > 0, std::abs(y) - 1, y > 0);
    }

    if (!ts.judge()) {
        std::cout << "s UNSATISFIABLE\n";
    } else {
        std::cout << "s SATISFIABLE\n";

        std::cout << "v ";
        for (int x = 1; x <= n; ++x) {
            std::cout << (ts.assign[x - 1] ? x : -x) << " ";
        }
        std::cout << "0\n";
    }

    return 0;
}

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

#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;
    }
};
#line 4 "Verify/two_sat.test.cpp"

#include <iostream>
#include <string>

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

    std::string tmp;
    int n, m;
    std::cin >> tmp >> tmp >> n >> m;

    TwoSat ts(n);
    while (m--) {
        int x, y;
        std::cin >> x >> y >> tmp;
        ts.add(std::abs(x) - 1, x > 0, std::abs(y) - 1, y > 0);
    }

    if (!ts.judge()) {
        std::cout << "s UNSATISFIABLE\n";
    } else {
        std::cout << "s SATISFIABLE\n";

        std::cout << "v ";
        for (int x = 1; x <= n; ++x) {
            std::cout << (ts.assign[x - 1] ? x : -x) << " ";
        }
        std::cout << "0\n";
    }

    return 0;
}