0w1

Template 2SAT

Referenced from here.

// O( V + E )
#include <bits/stdc++.h>
using namespace std;

typedef pair< int, int > pii;
typedef vector< pii > vp;
typedef vector< int > vi;
typedef vector< vi > vvi;

int MAXV;

int var_inv( int x ){ // 1 idx
    if( x <= MAXV ) return x + MAXV;
    return x - MAXV;
}

void kos_dfs1( const vvi &G, int u, vi &vis, vi &stk ){
    vis[ u ] = 1;
    for( int v : G[ u ] )
        if( not vis[ v ] )
            kos_dfs1( G, v, vis, stk );
    stk.push_back( u );
}

void kos_dfs2( const vvi &G, int u, vi &scc_id, int scc_no ){
    scc_id[ u ] = scc_no;
    for( int v : G[ u ] )
        if( not scc_id[ v ] )
            kos_dfs2( G, v, scc_id, scc_no );
}

void kosaraju( const vvi &G, vi &stk, vi &scc_id ){
    vi vis( G.size() );
    for( int i = 1; i < G.size(); ++i )
        if( not vis[ i ] )
            kos_dfs1( G, i, vis, stk );

    vvi rG( G.size() );
    for( int i = 1; i < G.size(); ++i )
        for( int j = 0; j < G[ i ].size(); ++j )
            rG[ G[ i ][ j ] ].push_back( i );

    for( int i = stk.size() - 1, scc_no = 0; i >= 0; --i )
        if( not scc_id[ stk[ i ] ] )
            kos_dfs2( rG, stk[ i ], scc_id, ++scc_no );
}

void solve(){
    int V, C; cin >> V >> C; // V : number of variables, C : number of clauses
    MAXV = V;

    vp constraint;
    for( int i = 0; i < C; ++i ){
        int u, v; cin >> u >> v; // negative denotes NOT
        if( u < 0 ) u = var_inv( -u ); // map NOT to +MAXV
        if( v < 0 ) v = var_inv( -v );
        constraint.push_back( pii( u, v ) );
    }

    vvi G( 2 * V + 1 );
    for( int i = 0; i < C; ++i ){
        int u = constraint[ i ].first;
        int v = constraint[ i ].second;
        if( var_inv( u ) == v ) continue; // NOT A or A -> either would work
        if( u == v ) // A or A -> must be A -> if NOT A should be chosen, we still have to choose A and cause a discrepancy
            G[ var_inv( u ) ].push_back( u );
        else // A or B -> if NOT A then B, if NOT B then A
            G[ var_inv( u ) ].push_back( v ),
            G[ var_inv( v ) ].push_back( u );
    }

    vi topo_stk, scc_id( 2 * V + 1 );
    kosaraju( G, topo_stk, scc_id ); // get topological order and SCC

    for( int i = 1; i <= V; ++i )
        if( scc_id[ i ] == scc_id[ var_inv( i ) ] ){ // if any A and NOT A should belong to the same SCC -> Unsatisfiable
            cout << "UNSATISFIABLE\n";
            return;
        }

    cout << "SATISFIABLE\n";

    vi sat( 2 * V + 1 );
    for( int i = 0; i < topo_stk.size(); ++i ) // topologically assign values
        if( not sat[ scc_id[ topo_stk[ i ] ] ] )
            sat[ scc_id[ topo_stk[ i ] ] ] = 1,
            sat[ scc_id[ var_inv( topo_stk[ i ] ) ] ] = 2;

    for( int i = 1; i <= V; ++i ){
        if( sat[ scc_id[ i ] ] == 1 )
            cout << i;
        else
            cout << -i;
        cout << " \n"[ i == V ];
    }
}

signed main(){
    ios::sync_with_stdio( false );
    solve();
    return 0;
}