2_SAT问题小结

先写写最近生活的一点感想，唉。。。今天真是失败的一天呐，算是知道了自己的一个定位，高中的时候觉得自己无所不能，现在才明白自己其实没有什么事情是能够做得好的。。。以前一直自嘲是穷屌，现在应该算是明白了自己确实是个穷屌，不能够奢望做很多事情，只希望能把目前最爱的ACM继续努力地做下去，不管别人说什么。。。

2_SAT虽然只写了两道水题，但是还是写写总结吧，加深一点理解吧。感觉2_SAT问题，讲的就是一个“v”的关系。对于每一个节点：对应着两种状态，我们可以假定这个节点为xi，那么用xi=true，代表一种状态，相应的xi=false是另一种状态。题目给出节点与节点之间的关系，用'v'的关系表示出来。比如：xi v xj ，这种状态表示xi = true && xj = true时符合，xi = false && xj = true 符合，xi = true && xj = false符合。这样的话如果xi
= false，那么我们可以确定 xj = true，那么我们就建立一条有向边 (xi = false) -> (xj = true)，同理这条语句还表明了另外一条有向边(xj = false) -> (xi = true)。我们不可能用节点的状态来表示一种有向边，所以我们把一个节点分成两个比如 xi 节点分成了 i*2,i*2+1，这两个节点，用哪一个点标记了代表这个节点当前的状态，所以很容易明白，如果i*2和i*2+1同时被标记了，证明题目所给出的所以关系不能同时被满足。(好像2_SAT讲完了。。。)，总的来说，2_SAT问题就是题目给出一张有向图，然后进行点标记,i*2，i*2+1两个点中能且只能标记一个点，问能不能按照条件把所有节点标记完（2*i,2*i+1代表i节点）。

下面是白皮上面的两道水题。。。

LA_3211：二分答案+2_SAT，

LA_3713：一条语句可能对应两个v关系式（其实想了一下，其实如果这道题乱搞的话，直接在填边的时候乱搞一个，意思也就是直接找出地推关系，就不需要两个式子了。。。好像是差不多。。。）。

下面附上我的两道题的代码：

LA_3211

#include <iostream>
#include <cstdio>
#include <cstring>
#include <cmath>
#include <algorithm>
#include <vector>
#define FOR(i,x,y)  for(int i = x;i < y;i ++)

using namespace std;

const int MAXN = 2222;
int e[MAXN],l[MAXN];
const int INF = 1e7+1;

struct TwoSAT{
int n;
vector <int> G[MAXN<<1];
bool mark[MAXN<<1];
int S[MAXN<<1],c;

bool dfs(int x){
if(mark[x^1])   return false;
if(mark[x])     return true;
mark[x] = true;
S[c++] = x;
for(int i = 0;i < G[x].size();i ++){
if(!dfs(G[x][i]))   return false;
}
return true;
}

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

void add_clause(int x,int xval,int y,int yval){
x = (x<<1) + xval;
y = (y<<1) + yval;
G[x^1].push_back(y);
G[y^1].push_back(x);
}

bool solve(){
for(int i = 0;i < (n<<1);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;
}
};

int main()
{
//freopen("test.in","r",stdin);
int n;
while(~scanf("%d",&n)){
int ll=0,rr=0,p;
FOR(i,0,n)  {scanf("%d%d",&e[i],&l[i]);rr = max(rr,l[i]);}
TwoSAT q;
while(ll+1 < rr){
p = (ll+rr)>>1;
q.init(n);
FOR(i,0,n){
FOR(j,i+1,n){
if(abs(e[i]-e[j]) < p)  q.add_clause(i,0,j,0);
if(abs(e[i]-l[j]) < p)  q.add_clause(i,0,j,1);
if(abs(l[i]-e[j]) < p)  q.add_clause(i,1,j,0);
if(abs(l[i]-l[j]) < p)  q.add_clause(i,1,j,1);
}
}
if(q.solve()){
ll = p;
}
else rr = p;
}
printf("%d\n",ll);
}
return 0;
}

LA_3713

#include <iostream>
#include <cstdio>
#include <cstring>
#include <cmath>
#include <algorithm>
#include <vector>
#define FOR(i,x,y)  for(int i = x;i < y;i ++)

using namespace std;

const int MAXN = 1e6+5;
int n,m,ave,a[MAXN];

struct TwoSAT{
int n;
vector <int> G[MAXN<<1];
bool mark[MAXN<<1];
int S[MAXN<<1],c;

bool dfs(int x){
if(mark[x^1])   return false;
if(mark[x])     return true;
mark[x] = true;
S[c++] = x;
for(int i = 0;i < G[x].size();i ++){
if(!dfs(G[x][i]))   return false;
}
return true;
}

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

void add_clause(int x,int xval,int y,int yval){
x = (x<<1) + xval;
y = (y<<1) + yval;
G[x^1].push_back(y);
G[y^1].push_back(x);
}

bool solve(){
for(int i = 0;i < (n<<1);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;
}
};

TwoSAT q;

int main(){
//freopen("test.in","r",stdin);
int x,y;
while(~scanf("%d%d",&n,&m) && (n || m)){
int ans = 0;
q.init(n);
FOR(i,0,n){
scanf("%d",&a[i]);
ans += a[i];
}
if(ans % n){
ave = (ans/n)+1;
}
else ave = (ans/n);
FOR(i,0,m){
scanf("%d%d",&x,&y);
if((a[x-1] < ave && a[y-1] < ave) || (a[x-1] >= ave && a[y-1] >= ave)){
q.add_clause(x-1,0,y-1,0);
q.add_clause(x-1,1,y-1,1);
}
else{
q.add_clause(x-1,1,y-1,1);
}
}
if(q.solve()){
FOR(i,0,n){
if(q.mark[i<<1]){
printf("C\n");
}
else {
if(a[i] < ave)
printf("B\n");
else printf("A\n");
}
}
}
else
printf("No solution.\n");
}
return 0;
}