Skip to content

Instantly share code, notes, and snippets.

@fedelebron
Created October 3, 2011 05:42
Show Gist options
  • Save fedelebron/1258506 to your computer and use it in GitHub Desktop.
Save fedelebron/1258506 to your computer and use it in GitHub Desktop.
Linear 2-SAT solver.
#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;
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment