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消除的。重要的一点是整个算法没有回溯的过程，因为过去确定的值肯定是符合题意的，而已确定的值不会对现在的决策产生影响。

此题代码如下

#include<cstdio>
#include<iostream>
#include<cstring>
#include<vector>
#define maxn 100009
#define rep(i,j,k) for(int i = j; i <= k; i++)
using namespace std;

int n, m, a[maxn] = {0}, s[maxn][2] = {0};
double po;

int read()
{
int s = 0, t = 1; char c = getchar();
while( !isdigit(c) ){
if( c == '-' ) t = -1; c = getchar();
}
while( isdigit(c) ){
s = s * 10 + c - '0'; c = getchar();
}
return s * t;
}

struct TWO_SAT{
int n;
vector<int> q[maxn*2];
int s[maxn*2], c;
bool mark[maxn*2];

void init(int n){
this-> n = n;
rep(i,0,n*2-1) q[i].clear();
memset(mark,0,sizeof(mark));
}

bool dfs(int x)
{
if( mark[x^1] ) return false;
if( mark[x] ) return true;
s[c++] = x;
mark[x] = 1;
int s = q[x].size();
rep(i,0,s-1){
if( !dfs(q[x][i] )) return false;
}
return true;
}

bool solve()
{
for(int i = 0; i < n*2; i += 2)
{
if( !mark[i] && !mark[i^1] ){
c = 0;
if( !dfs(i) ){
while( c > 0 ) mark[s[--c]] = 0;
if( !dfs(i+1) ) return false;
}
}
}
return true;
}
};

TWO_SAT solver;

bool test()
{
solver.init(n);
rep(i,0,m-1){
if( (a[s[i][0]] < po && a[s[i][1]] < po) || (a[s[i][0]] >= po && a[s[i][1]] >= po ) )
{
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);
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);

}
else {
solver.q[s[i][0]*2+1].push_back(s[i][1]*2);
solver.q[s[i][1]*2+1].push_back(s[i][0]*2);
}
}

bool ok = solver.solve();
if( ok ){
rep(i,0,n-1){
if( a[i] < po ){
if( solver.mark[i*2] ) printf("B\n");
else printf("C\n");
}
else {
if( solver.mark[i*2] ) printf("A\n");
else printf("C\n");
}
}
}
return ok;
}

int main()
{
while( scanf("%d%d", &n,&m) == 2 && n && m ){
int sum = 0;
rep(i,0,n-1) {
a[i] = read();
sum += a[i];
}
po = 1.0 * sum / n;
rep(i,0,m-1){
rep(j,0,1)
s[i][j] = read(), s[i][j]--;
}
if( !test() ) {
cout<<"No solution\n";
}
}
return 0;
}