Cod sursa(job #2845145)

Utilizator Cosmin2004_InfoMoldoveanu Cosmin Cosmin2004_Info Data 7 februarie 2022 16:05:49
Problema 2SAT Scor 40
Compilator cpp-64 Status done
Runda Arhiva educationala Marime 2.29 kb
#include <bits/stdc++.h>

using namespace std;
class SAT2 {
    int n;
    vector <bool> exp;
    vector <vector <int>> g;
    int getnode(int expr) { if(expr < 0) return n - expr; return expr; }
    int timer;
    vector <int> id, low, colour;
    vector <bool> inst;
    stack <int> st;
    vector <vector <int>> sccs;
    void dfs(int u) {
        low[u] = id[u] = ++timer;
        st.push(u); inst[u] = true;
        for(int v : g[u]) {
            if(!id[v]) {
                dfs(v);
                low[u] = min(low[u], low[v]);
            } else if(inst[v]) low[u] = min(low[u], id[v]);
        }
        if(low[u] == id[u]) {
            sccs.push_back({u});
            while(st.top() != u) {
                colour[st.top()] = sccs.size();
                sccs.back().push_back(st.top());
                inst[st.top()] = false;
                st.pop();
            }
            colour[u] = sccs.size();
            inst[u] = false;
            st.pop();
        }
    }
public:
    SAT2(int _n) : n(_n), exp(2 * _n + 1, false), g(2 * _n + 1), timer(0), id(2 * _n + 1, 0), low(2 * _n + 1, 0), colour(2 * _n + 1), inst(2 * _n + 1, 0) {}
    void add_expr(int x, int y) {
        g[getnode(-x)].push_back(getnode(y));
        g[getnode(-y)].push_back(getnode(x));
    }
    void scc() {
        for(int i = 1; i <= 2 * n; i++) if(!id[i])
            dfs(i);
    }
    inline bool solve() {
        scc();
        for(int i = 1; i <= n; i++)
            if(colour[i] == colour[i + n])
                return false;
        int k = sccs.size();
        for(auto it = sccs.begin(); it != (sccs.begin() + (k / 2)); it++)
            for(auto node = it -> begin(); node != it -> end(); node++)
                exp[*node] = true;
        return true;
    }
    vector <bool> get_solution() {
        exp.resize(n + 1);
        exp.erase(exp.begin());
        return exp;
    }
};

int main()
{
    ifstream cin("2sat.in");
    ofstream cout("2sat.out");
    int n, m, x, y;
    cin >> n >> m;
    SAT2 S(n);
    for(int i = 1; i <= m; i++)
        cin >> x >> y,
        S.add_expr(x, y);
    if(!S.solve()) cout << "-1";
    else {
        vector <bool> sol = S.get_solution();
        for(bool x : sol)
            cout << x << " ";
    }
    return 0;
}