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; }