Uva 1391 （LA 3713） Astronauts （2-SAT问题）

今天学了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 }