public
Last active

Linear 2-SAT solver.

  • Download Gist
2sat.cpp
C++
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
#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;
}
}

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.