Cod sursa(job #3296956)

Utilizator OvidRata Ovidiu Ovid Data 19 mai 2025 12:56:04
Problema 2SAT Scor 0
Compilator cpp-64 Status done
Runda Arhiva educationala Marime 6.61 kb
#include<bits/stdc++.h>
using namespace std;

//#pragma GCC optimize("O3,unroll-loops")
//#pragma GCC target("avx2,bmi,bmi2,lzcnt,popcnt")


string numeFisier="ctc";
ifstream fin(numeFisier+".in"); ofstream fout(numeFisier+".out");
#define cin fin
#define cout fout


#define INIT  ios_base :: sync_with_stdio(false); cin.tie(NULL); cout.tie(NULL);mt19937 rng(chrono::steady_clock::now().time_since_epoch().count());
#define mp make_pair
#define pb push_back
#define ft first
#define sc second
#define ll long long
#define pii pair<int, int>
#define count_bits __builtin_popcount
#define int ll






// An instance of this struct must be instantiated manually 
struct StronglyConnectedComponents{

    int n,m;
    vector< vector<int> > g;


    int indexArray0=0;
    vector<int> indexArray;
    vector<int> lowlink;

    vector<bool> onStack;
    stack<int> st;

    vector< vector<int> > componentOfRepresentative;
    vector<int> representative;


    //Strongly connected components in reverse topological order
    vector< vector<int> > stronglyConnectedComponents;


    //CondensationGraph
    vector< vector<int> > condensationGraph;


    void getNM(int N, int M){
        n =N;
        m = M;
        g.assign(n+10, {});
        indexArray.assign(n+10, 0);
        lowlink.assign(n+10, 0);
        onStack.assign(n+10, 0);
    }

    void strongConnected(int u){
        
        indexArray0++;
        indexArray[u] =indexArray0;
        lowlink[u] = indexArray0;

        st.push(u);
        onStack[u]=true;

        for(int v:g[u]){
            if(!indexArray[v]){
                strongConnected(v);
                lowlink[u]=min(lowlink[u], lowlink[v]);
            }
            else{
                if( onStack[v] ){
                    lowlink[u] = min(lowlink[u], lowlink[v]);
                }
            }
        }
        if( lowlink[u]==indexArray[u] ){
            stronglyConnectedComponents.pb({});
            
            while(st.top()!=u ){
                onStack[st.top()]=false;
                stronglyConnectedComponents.back().pb(st.top());
                st.pop();
            }

            stronglyConnectedComponents.back().pb(u);
            st.pop();
            onStack[u]=false;

        }
    }



    void buildStronglyConnectedComponents(){
        if(!stronglyConnectedComponents.empty()){
            return;
        }
        for(int i=1; i<=n; i++){
            if(indexArray[i]==0){
                strongConnected(i);
            }
        }
    }


    vector<int> verified;
    void buildCondensationGraph(){
        buildStronglyConnectedComponents();
        if( !condensationGraph.empty() ){
            return;
        }   
        representative.assign(n+10, 0);
        componentOfRepresentative.assign(n+10, {});
        
        for(auto component: stronglyConnectedComponents){
            int repr = component[0];
            for(auto u : component){
                representative[u]=repr;
            }
            componentOfRepresentative[repr]=component;
        }

        

        condensationGraph.assign(n+10, {});
        verified.assign(n+10, 0);
    
        for(auto component:stronglyConnectedComponents){
            int repr = component[0];
            for(int u : component){
                for(int v: g[u]){
                    int repr2 = representative[u];
                    if( repr!=repr2 ){
                        if(!verified[repr2]){
                            verified[ repr2 ]=1;
                            condensationGraph[ repr ].pb(repr2);
                        }
                    }
                }
            }
            for(int u : component){
                for(int v: g[u]){
                    int repr2 = representative[u];
                    if( repr!=repr2 ){
                        verified[repr2]=0;
                    }
                }
            }
        }

    };

};


struct SAT2{

    int numberOfVariables, numberOfClauses;

    vector<vector<int>> clauses;

    //the actual solution
    //if is not satisfiable, will be {-1}
    vector<int> assignment;

    int getNodeFromVariable(int u){
        u+=numberOfVariables;
        if(u<numberOfVariables){
            u++;
        }
        return u;
    }

    int getVariableFromNode(int u){
        if(u<=numberOfVariables){
            return u-numberOfVariables-1;
        }
        else{
            return u-numberOfVariables;
        }
    }

    void assign(int u, bool truth){
        if( u<0 ){
            truth = !truth;
            u = -u;
        }
        assignment[u] = ((int)truth);
    }

    void satisfy(){
        StronglyConnectedComponents implications;
        implications.getNM(numberOfVariables*2, numberOfClauses*2);



        for(auto clause : clauses){
            int u = clause[0];
            int v = clause[1];
            int notU = getNodeFromVariable(-u);
            int notV = getNodeFromVariable(-v);
            u = getNodeFromVariable(u);
            v = getNodeFromVariable(v);

            implications.g[ notU ].pb( v );
            implications.g[notV].pb(u);
        }
        implications.buildCondensationGraph();

        
        
        assignment.assign(numberOfVariables+10, -1);
        

        for( auto component : implications.stronglyConnectedComponents ){
            int repr = implications.representative[component[0]];
            int notRepr = implications.representative[getNodeFromVariable( -getVariableFromNode(repr) )];
            
            if(repr == notRepr){
                assignment={-1};
                return;
            }

            for (auto u : component){
                
                int varU = getVariableFromNode(u);
                int varNotU = -varU;
                if( assignment[ abs( varU ) ]!=-1 ){
                    continue;
                }
                assign( varU, true );
                assign(varNotU, false);
            }

        }

    }

} sat2;


void input(){
    
    cin>>sat2.numberOfVariables>>sat2.numberOfClauses;
    for(int i=1, u, v; i<=sat2.numberOfClauses; i++){
        cin>>u>>v;
        sat2.clauses.pb({u,v});
    }

}


void solve(){
    sat2.satisfy();
}


void output(){
    if(((int)sat2.assignment.size())==1){
        cout<<"-1";
        return;
    }
    for(int i = 1; i<=sat2.numberOfVariables; i++){
        cout<<sat2.assignment[i]<<" ";
    }
}

int32_t main(){
    INIT

    input();

    solve();

    output();


    return 0;
}