标签：
今天学了2-SAT问题，就找了这道例题，敲了一下，还好过了。
2-SAT问题应该是把一些布尔变量之间的逻辑关系反映到一个无向图（有时可能是有向图）上来。通过推导的形式在这个有向图里面补边。再通过确定一些变量的值，使所有的变量都能符合题意中逻辑关系。补边方式 即如果Xi = true && Xj = false 不符合题意，那么如果Xi == true ，那么就在 Xi = true 和 Xj = true之间连一条边， 使得当Xi = true 时能马上确定 Xj = true。 在实际操作上总把一个点 Xi 拆成两个点 Xi*2 和 Xi*2+1， 其中 Xi*2 表示当 Xi 为假时， Xi*2+1 表示 当 Xi*2+1 为真时。 同时为了实现判别 Xi 的真假性的确定，以及 Xi 的值是否已确定。 用一个布尔数组mark来判断。若 mark[Xi*2] == 1 则 Xi 的值为假，mark[Xi*2+1] == 1 则 Xi 的值为真。 若 mark[Xi*2] == 1 && mark[Xi*2+1] == 1 则说明之前确定的变量是错误的。 若mark[Xi*2] == 0 && mark[Xi*2+1] == 0， 则需开始确定变量的值。确定变量的值时先假定其为假，若失败，再假定其为真。若再失败，则退出。成功则寻找下一个没确定的变量。当然，在失败之后，是需要把这期间的mark消除的。
此题代码如下
1 #include<cstdio> 2 #include<iostream> 3 #include<cstring> 4 #include<vector> 5 #define maxn 100009 6 #define rep(i,j,k) for(int i = j; i <= k; i++) 7 using namespace std; 8 9 int n, m, a[maxn] = {0}, s[maxn][2] = {0}; 10 double po; 11 12 int read() 13 { 14 int s = 0, t = 1; char c = getchar(); 15 while( !isdigit(c) ){ 16 if( c == ‘-‘ ) t = -1; c = getchar(); 17 } 18 while( isdigit(c) ){ 19 s = s * 10 + c - ‘0‘; c = getchar(); 20 } 21 return s * t; 22 } 23 24 struct TWO_SAT{ 25 int n; 26 vector<int> q[maxn*2]; 27 int s[maxn*2], c; 28 bool mark[maxn*2]; 29 30 void init(int n){ 31 this-> n = n; 32 rep(i,0,n*2-1) q[i].clear(); 33 memset(mark,0,sizeof(mark)); 34 } 35 36 bool dfs(int x) 37 { 38 if( mark[x^1] ) return false; 39 if( mark[x] ) return true; 40 s[c++] = x; 41 mark[x] = 1; 42 int s = q[x].size(); 43 rep(i,0,s-1){ 44 if( !dfs(q[x][i] )) return false; 45 } 46 return true; 47 } 48 49 bool solve() 50 { 51 for(int i = 0; i < n*2; i += 2) 52 { 53 if( !mark[i] && !mark[i^1] ){ 54 c = 0; 55 if( !dfs(i) ){ 56 while( c > 0 ) mark[s[--c]] = 0; 57 if( !dfs(i+1) ) return false; 58 } 59 } 60 } 61 return true; 62 } 63 }; 64 65 TWO_SAT solver; 66 67 bool test() 68 { 69 solver.init(n); 70 rep(i,0,m-1){ 71 if( (a[s[i][0]] < po && a[s[i][1]] < po) || (a[s[i][0]] >= po && a[s[i][1]] >= po ) ) 72 { 73 solver.q[s[i][0]*2].push_back(s[i][1]*2+1);solver.q[s[i][0]*2+1].push_back(s[i][1]*2); 74 solver.q[s[i][1]*2].push_back(s[i][0]*2+1);solver.q[s[i][1]*2+1].push_back(s[i][0]*2); 75 76 } 77 else { 78 solver.q[s[i][0]*2+1].push_back(s[i][1]*2); 79 solver.q[s[i][1]*2+1].push_back(s[i][0]*2); 80 } 81 } 82 83 bool ok = solver.solve(); 84 if( ok ){ 85 rep(i,0,n-1){ 86 if( a[i] < po ){ 87 if( solver.mark[i*2] ) printf("B\n"); 88 else printf("C\n"); 89 } 90 else { 91 if( solver.mark[i*2] ) printf("A\n"); 92 else printf("C\n"); 93 } 94 } 95 } 96 return ok; 97 } 98 99 int main() 100 { 101 while( scanf("%d%d", &n,&m) == 2 && n && m ){ 102 int sum = 0; 103 rep(i,0,n-1) { 104 a[i] = read(); 105 sum += a[i]; 106 } 107 po = 1.0 * sum / n; 108 rep(i,0,m-1){ 109 rep(j,0,1) 110 s[i][j] = read(), s[i][j]--; 111 } 112 if( !test() ) { 113 cout<<"No solution\n"; 114 } 115 } 116 return 0; 117 }
Uva 1391 （LA 3713） Astronauts （2-SAT问题）
标签：
原文地址：http://www.cnblogs.com/83131yyl/p/5037474.html
