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
",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
");
                }
                else {
                    if(a[i] < ave)
                        printf("B
");
                    else printf("A
");
                }
            }
        }
        else
            printf("No solution.
");
    }
    return 0;
}