2-SAT入门——UVALive - 3211

2-SAT解决的问题就是给m个bool 变量赋值，使得满足题目给出的所有要求。对于这类题建图之后，每一条边代表的意义是，若其中一个结点成立，这另一端对应结点也需要成立。

算法里巧用了异或运算，x和x^1分别表示了变量赋值为真和假的两种情况，对于每一对x和x^1只有一个能成立，当每一个成立的点通过边所连向的其他所有点都成立，即得到了2-SAT的解了。

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

bool dfs(int x){
if(mark[x^1])return false;//变量已经赋值为相反值了
if(mark[x])return true;
mark[x]=1;//变量赋值
s[c++]=x;//储存已赋值的点
for(int i=0;i<e[x].size();i++){
if(!dfs(e[x][i]))return false;
}
return true;
}

void init(int n){
this->n=n;
for(int i=0;i<n*2;i++){e[i].clear();}
memset(mark,0,sizeof(mark));
}
//要求x赋值为xval或y赋值为yval时
void add(int x,int xval,int y,int yval){
x=x*2+xval;
y=y*2+yval;
e[x^1].push_back(y);//y成立时x不成立
e[y^1].push_back(x);//x成立时y不成立
}

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]]=false;//清除赋值
if(!dfs(i+1))return false;//一个变量无法赋值为真也无法赋值为假
}
}
}
return true;
}

};

Now or later UVALive - 3211

飞机调度问题，每架飞机都可以选择早降落和晚降落，要求求出相邻着陆时间间隔最小值的最大值。

1.最大化最小值，问题用二分法解决，问题就变成了求当前间隔时间能否满足所有飞机的着陆间隔都大于等于该值。

2.若两架飞机早降落的时间间隔小于mid值，那么a飞机早降落时b飞机就不能早降落，b飞机早降落时，a飞机就只能晚降落，依靠这个依据为2-SAT建边，就可以求出是否有解。

#include<stdio.h>
#include<algorithm>
#include<string.h>
#include<iostream>
#include<stack>
#include<vector>
using namespace std;
const int maxn = 2005;
int n;
int t[maxn][2];
struct two_sat{
int n;
vector<int> e[maxn * 2];
bool mark[maxn * 2];
int s[maxn * 2], c;

bool dfs(int x){
if (mark[x ^ 1])return false;//变量已经赋值为相反值了
if (mark[x])return true;
mark[x] = 1;//变量赋值
s[c++] = x;//储存已赋值的点
for (int i = 0; i<e[x].size(); i++){
if (!dfs(e[x][i]))return false;
}
return true;
}

void init(int n){
this->n = n;
for (int i = 0; i<n * 2; i++){ e[i].clear(); }
memset(mark, 0, sizeof(mark));
}

void add(int x, int xval, int y, int yval){
x = x * 2 + xval;
y = y * 2 + yval;
e[x ^ 1].push_back(y);
e[y ^ 1].push_back(x);
}

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]] = false;//清除赋值
if (!dfs(i + 1))return false;//一个变量无法赋值为真也无法赋值为假
}
}
}
return true;
}

};
two_sat twosat;

bool test(int m){
twosat.init(n);
for (int i = 0; i<n; i++){
for (int j = i + 1; j<n; j++){
for (int a = 0; a<2; a++){
for (int b = 0; b<2; b++){
if (abs(t[i][a] - t[j][b])<m){
twosat.add(i, a, j, b);
}
}
}
}
}
return twosat.solve();
}

int main(){
while (scanf("%d", &n) == 1 && n){
int l = 0, r = 0;
for (int i = 0; i<n; i++){
scanf("%d%d", &t[i][0], &t[i][1]);
r = max(r, t[i][1]);
}
while (l<r){
int mid = l + (r - l + 1) / 2;
if (test(mid))l = mid;
else r = mid - 1;
}
printf("%d\n", l);
}
return 0;
}