Cod sursa(job #3230185)

Utilizator horia_mercanHoria Mercan horia_mercan Data 19 mai 2024 20:36:41
Problema 2SAT Scor 80
Compilator cpp-64 Status done
Runda Arhiva educationala Marime 4.83 kb
/**
 * https://codeforces.com/blog/entry/16205
*/

#include <fstream>
#include <iostream>

#include <vector>
#include <stack>

using std::vector, std::stack;

class Graph2SAT {
 private:
    vector<vector<int>>neighbours_transpose;
    int nodes;
    int comp_cnt;
    int threshold_comp;
    
 public:

    vector<vector<int>>neighbours;
    Graph2SAT(int literals) {
        this->nodes = 2 * literals;
        neighbours.assign(2 * literals, vector<int>());
        neighbours_transpose.assign(2 * literals, vector<int>());
    }

    vector<int>comp; // component number
    static int pozitive_literal(int literal) { return (literal << 1); }
    static int negative_literal(int literal) { return (literal << 1) | 1; }

    void implies(int literal1, int literal2) {
        // std::cout << "add " << literal1 << " " << literal2 <<"\n";
        neighbours[literal1].push_back(literal2);
        neighbours_transpose[literal2].push_back(literal1);
        // std::cout << "done implies\n";
    }

    void dfs_util_topo_sort(int node, bool visited[], stack<int> &st) {
        visited[node] = true;

        for (const auto &x: neighbours[node]) {
            if (!visited[x]) {
                dfs_util_topo_sort(x, visited, st);
            }
        }
        st.push(node);
    }

    void dfs_util_kosaraju(int node, int _comp_cnt) {
        comp[node] = _comp_cnt;

        for (const auto &x: neighbours_transpose[node]) {
            if (comp[x] < 0) {
                dfs_util_kosaraju(x, _comp_cnt);
            }
        }
    }

    void strongly_connected_components() {
        stack<int>st;
        bool visited[nodes];
        for (int i = 0; i < nodes; i++)
            visited[i] = false;
        for (int i = 0; i < nodes; i++) {
            if (!visited[i]) {
                dfs_util_topo_sort(i, visited, st);
                // std::cout << "visited ";
                // for (int j = 0; j < nodes; j++) {
                //     std::cout << visited[j] << " ";
                // }
                // std::cout << "\n";
            }
        }

        std::cout << "after dfs util topo sort\n";

        comp.assign(nodes, -1);
        comp_cnt = 1;
        while (!st.empty()) {
            if (comp[st.top()] < 0) {
                dfs_util_kosaraju(st.top(), comp_cnt);
                comp_cnt++;
            }
            st.pop();
        }

    }

};

int main() {
    std::ifstream fin("2sat.in");
    std::ofstream fout("2sat.out");

    int N, M;
    fin >> N >> M;
    int x, y, c;

    Graph2SAT graph(N);
    for (int i = 0; i < M; i++) {
        fin >> x >> y;
        c=0;
        // x--;
        // y--;
        switch (c)
        {
        case 0:
            int literal1, literal2;
            if (x < 0) {
                literal1 = Graph2SAT::negative_literal(-x - 1);
            } else literal1 = Graph2SAT::pozitive_literal(x - 1);

            if (y < 0) {
                literal2 = Graph2SAT::negative_literal(-y - 1);
            } else literal2 = Graph2SAT::pozitive_literal(y - 1);
            // not (x) => y
            graph.implies(literal1 ^ 1, literal2);
            // not (y) => x
            graph.implies(literal2 ^ 1, literal1);
            break;
        case 1:
            // not(x) => not(y)
            graph.implies(Graph2SAT::negative_literal(x), Graph2SAT::negative_literal(y));
            break;
        case 2:
            // not(y) => not(x)
            graph.implies(Graph2SAT::negative_literal(y), Graph2SAT::negative_literal(x));
            break;
        case 3:
            // x => not(y)
            graph.implies(Graph2SAT::pozitive_literal(x), Graph2SAT::negative_literal(y));

            // y => not(x)
            graph.implies(Graph2SAT::pozitive_literal(y), Graph2SAT::negative_literal(x));
            break;
        default:
            break;
        }
    }

    // for (int i = 0; i < N; i++) {
    //     std::cout << "neighbours of pozitive " << i << "\t";
    //     for (const auto &x: graph.neighbours[2 * i]) {
    //         std::cout << x << " ";
    //     } 
    //     std::cout << "\n";
    //     std::cout << "neighbours of negative " << i << "\t";
    //     for (const auto &x: graph.neighbours[2 * i + 1]) {
    //         std::cout << x << " ";
    //     } 
    //     std::cout << "\n";
    // }
    // std::cout << "read done\n";
    graph.strongly_connected_components();

    // std::cout << "components:\t";

    // for (int i = 0; i < 2 * N; i++) {
    //     std::cout << graph.comp[i] << " ";
    // }
    // std::cout <<"\n";

    int cnt = 0;
    vector<int>literal_value(N);

    for (int i = 0; i < N; i++) {
        if (graph.comp[i * 2] > graph.comp[2 * i + 1]) {
            literal_value[i] = 1;
            cnt++;
        }
    }

    for (int i = 0; i < N; i++) {
        // if (literal_value[i]) {
            fout << literal_value[i] << " ";
        // }
    }
    std::cout << "finish\n";
    return 0;
}