2-sat.cpp

#include <bits/stdc++.h>

using namespace std;

class two_sat{
	//p is +p, ~p is -p
	typedef pair<int, int> pii;
private:
	vector<vector<int>> adj;
	vector<int> comp;
	vector<int> num;
	vector<int> stk;
	vector<char> state;
	vector<bool> ans;
	int sz = 0;
	int curr_num = 1;
	int curr_comp = 1;
	bool solved = false;
	bool conds_solveable = false;
	int odd(int k){
		return (abs(k) << 1) - 1;
	}
	int even(int k){
		return (abs(k) << 1);
	}
	int dfs(int st){
		state[st] = 1;
		num[st] = curr_num++;
		int mnn = num[st];
		stk.push_back(st);
		for(auto x:adj[st]){
			if(state[x] == 0){
				mnn = min(dfs(x), mnn);
			} else if(state[x] == 1){
				mnn = min(mnn, num[x]);
			}
		}
		if(mnn == num[st]){
			bool seen = false;
			do{
				int v = stk.back(); stk.pop_back();
				comp[v] = curr_comp;
				state[v] = 2;
				seen |= v == st;
			}while(!seen);
			curr_comp++;
		}
		return mnn;
	}
public:
	two_sat(int mx, const vector<pii> &conds){
		sz = mx << 1;
		adj.resize(sz+1);
		num.resize(sz+1, 0);
		comp.resize(sz+1, 0);
		state.resize(sz+1, 0);
		for(auto x:conds){
			assert(x.first);
			assert(x.second);
			assert(even(x.first) <= sz);
			assert(even(x.second) <= sz);
			adj[x.first < 0?even(x.first):odd(x.first)].push_back(x.second < 0?odd(x.second):even(x.second));
			adj[x.second < 0?even(x.second):odd(x.second)].push_back(x.first < 0?odd(x.first):even(x.first));
		}
	}
	two_sat(const vector<pii> &conds){
		int mx = 0;
		for(auto x:conds){
			mx = max({mx, abs(x.first), abs(x.second)});
		}
		sz = mx << 1;
		adj.resize(sz+1);
		num.resize(sz+1, 0);
		comp.resize(sz+1, 0);
		state.resize(sz+1, 0);
		for(auto x:conds){
			assert(x.first);
			assert(x.second);
			assert(even(x.first) <= sz);
			assert(even(x.second) <= sz);
			adj[x.first < 0?even(x.first):odd(x.first)].push_back(x.second < 0?odd(x.second):even(x.second));
			adj[x.second < 0?even(x.second):odd(x.second)].push_back(x.first < 0?odd(x.first):even(x.first));
		}
	}
	two_sat(int mx){
		sz = mx << 1;
		adj.resize(sz+1);
		num.resize(sz+1, 0);
		comp.resize(sz+1, 0);
		state.resize(sz+1, 0);
	}
	two_sat(){
		sz = 0;
	}
	void add_condition(const pii &x){
		assert(!solved);
		int psz = sz;
		sz = max({sz, even(x.first), even(x.second)});
		if(sz != psz){
			if(psz == 0){
				adj.push_back({});
				num.push_back(0);
				comp.push_back(0);
				state.push_back(0);
			}
			while(psz != sz){
				adj.push_back({});
				num.push_back(0);
				comp.push_back(0);
				state.push_back(0);
				psz++;
			}
		}
		adj[x.first < 0?even(x.first):odd(x.first)].push_back(x.second < 0?odd(x.second):even(x.second));
		adj[x.second < 0?even(x.second):odd(x.second)].push_back(x.first < 0?odd(x.first):even(x.first));
	}
	bool solveable(){
		if(solved){
			return conds_solveable;
		}
		solved = true;
		for(int i = 1; i <= sz; i++){
			if(state[i] == 0){
				dfs(i);
			}
		}
		ans.resize(sz>>1, 0);
		for(int j = 1; j <= sz; j+= 2){
			if(comp[j] == comp[j+1]){
				ans.clear();
				conds_solveable = false;
				return false;
			}
			ans[j>>1] = comp[j] > comp[j+1]?1:0;
		}
		conds_solveable = true;
		return conds_solveable;
	}
	vector<bool> solve(){
		if(!solved){
			solveable();
		}
		return ans;
	}
};

int main(){
	two_sat ts;
	int n;
	scanf("%d", &n);
	for(int i = 0; i < n; i++){
		pair<int, int> a;
		scanf("%d%d", &a.first, &a.second);
		ts.add_condition(a);
	}
	if(!ts.solveable()){
		puts("No solution exists!");
	} else {
		puts("Here is an assignment that satisfies your conditions:");
		auto v = ts.solve();
		for(auto x:v){
			printf("%c", x+'0');
		}
		puts("");
	}
}