Cod sursa(job #2654446)

Utilizator TincaMateiTinca Matei TincaMatei Data 30 septembrie 2020 23:06:10
Problema 2SAT Scor 100
Compilator cpp-64 Status done
Runda Arhiva educationala Marime 3.39 kb
#include <bits/stdc++.h>

const int MAX_N = 100000;

struct SATSolver {
private:
    int low[2*MAX_N], id[2*MAX_N], tarjan_stack[2*MAX_N], top, lastid;
    bool instack[2*MAX_N], fixed[2*MAX_N];

    void tarjan(int nod) {
        id[nod] = low[nod] = lastid++;
        tarjan_stack[top++] = nod;
        instack[nod] = true;

        for(auto it: graph[nod]) {
            if(id[it] == -1) {
                tarjan(it);
                low[nod] = std::min(low[nod], low[it]);
            } else if(instack[it])
                low[nod] = std::min(low[nod], low[it]);
        }

        if(id[nod] == low[nod]) {
            std::vector<int> ctc;
            do {
                int extr = tarjan_stack[--top];
                ctc.push_back(extr);
                instack[extr] = false;
            } while(tarjan_stack[top] != nod);
            
            bool var_false = false, var_true = false;
            for(auto it: ctc)
                if(fixed[it] && res[it])
                    var_true = true;
                else if(fixed[it])
                    var_false = true;
        
            if(var_false && var_true)
                error = true;
            if(!var_false && !var_true)
                var_true = true;

            for(auto it: ctc) {
                if(!fixed[it]) {
                    fixed[it] = true;
                    res[it] = var_true;
                } else if(res[it] != var_true)
                    error = true;
            
                if(!fixed[neg[it]]) {
                    fixed[neg[it]] = true;
                    res[neg[it]] = 1 - var_true;
                } else if(res[neg[it]] != 1 - var_true)
                    error = true;
            }
        }
    }
public:
    int N;
    bool res[MAX_N * 2];
    int neg[MAX_N * 2];

    std::vector<int> graph[2*MAX_N];
    
    bool error;

    SATSolver(int _N) {
        N = _N;
        for(int i = 0; i < N; ++i) {
            neg[i] = i + N;
            neg[i + N] = i;
        }
        reset();
    }

    void reset() {
        error = false;
        lastid = top = 0;
        for(int i = 0; i < 2 * N; ++i) {
            low[i] = id[i] = -1;
            instack[i] = fixed[i] = res[i] = false;
        }
    }

    void add_or(int a, int b) {
        graph[neg[a]].push_back(b);
        graph[neg[b]].push_back(a);
    }

    void add_xor(int a, int b) {
        graph[a].push_back(neg[b]);
        graph[b].push_back(neg[a]);
        graph[neg[a]].push_back(b);
        graph[neg[b]].push_back(a);
    }

    void solve_system() {
        for(int i = 0; i < 2 * N; ++i)
            if(id[i] == -1)
                tarjan(i);
        for(int i = 0; i < N; ++i)
            if(res[i] == res[neg[i]])
                error = true;
    }
};

int main() {
    int n, m;
	FILE *fin = fopen("2sat.in", "r");
    fscanf(fin, "%d%d", &n, &m);
    SATSolver *sat;
    
    sat = new SATSolver(n);

    for(int i = 0; i < m; ++i) {
        int x, y;
        fscanf(fin, "%d%d", &x, &y);
        
        if(x < 0)
            x = sat->neg[-x - 1];
        else
            x = x - 1;

        if(y < 0)
            y = sat->neg[-y - 1];
        else
            y = y - 1;
        sat->add_or(x, y);
    }


    fclose(fin);
    sat->solve_system();

    FILE *fout = fopen("2sat.out", "w");
    if(sat->error)
        fprintf(fout, "-1");
    else
        for(int i = 0; i < n; ++i)
            fprintf(fout, "%d ", sat->res[i]);
    fclose(fout);
    
    return 0;
}