Linear 2-SAT solver.

2sat.cpp

#include <list>
#include <vector>
#include <queue>
#include <iostream>

using namespace std;

typedef unsigned int uint;
typedef vector<list<uint>> adj_list;
typedef vector<int> vint;
typedef vector<bool> vbool;

#define NOT(n) (n & 1 ? ((n)-1) : ((n)+1))
#define ABS(n) ((n) & 1 ? ((n)-1) : (n))
#define VAR(n) (ABS(n)/2)
#define SGN(n) ((n) & 1 ? 0 : 1)

bool exists_contradiction_bfs(uint s, const adj_list& G) {
	queue<uint> Q;
	Q.push(s);
	vbool seen(Q.size());
	seen[s] = true;

	while(!Q.empty()) {
		uint v = Q.front();
		Q.pop();
		for(uint w : G[v]) {
			if(seen[w]) continue;
			if(VAR(w) == VAR(s)) return true;
			Q.push(w);
			seen[w] = true;
		}
	}
	return false;
}

void marking_bfs(uint s, const adj_list& G, vint& assignment) {
	queue<uint> Q;
	Q.push(s);
	assignment[VAR(s)] = SGN(s);

	while(!Q.empty()) {
		uint v = Q.front();
		Q.pop();

		for(uint x : G[v]) {
			if(assignment[VAR(x)] != -1) continue;
			assignment[VAR(x)] = SGN(x);
			Q.push(x);
		}
	}
}

int main() {
	int n;
	cin >> n;
	while(n--) {
		int m, terms;
		cin >> m >> terms;
		vint assignment(m, -1);
		vbool contradictions(2*m);
		adj_list G(2*m);
		char sgn, letter, sgn2, letter2;
		bool sat = true;

		while(terms--) {
			cin >> sgn >> letter >> sgn2 >> letter2;
			letter -= 'A';
			letter2 -= 'A';

			uint p, q;
			p = static_cast<uint>(letter*2);
			q = static_cast<uint>(letter2*2);

			if(sgn == '-') p++;
			if(sgn2 == '-') q++;

			G[NOT(p)].push_back(q);
			G[NOT(q)].push_back(p);
		}

		for(int i = 0; i < 2*m; i++) {
			contradictions[i] = exists_contradiction_bfs(i, G);
			if(contradictions[i] && contradictions[NOT(i)]) {
				sat = false;
				break;
			}
		}

		if(sat) {
			for(int i = 0; i < 2*m; i++) {
				if(!contradictions[i] && assignment[VAR(i)] == -1) marking_bfs(i, G, assignment);
			}

			cout << "Instance: ";
			for(int i = 0; i < m; i++) {
				if(assignment[i] == 0) cout << "-";
				cout << static_cast<char>('A' + i) << " ";
			}
			cout << endl;
		} else cout << "Instance is not satisfiable." << endl;
	}
}