2-SAT入门 poj2749 Building roads hdu4421 Bit Magic

poj2749 Building roads

http://poj.org/problem?id=2749

二分答案，以后构造布尔表达式。

　　相互讨厌是!((a and b)or(!a and !b) 化简得 (!a or !b)and(a or b)

　　相互喜欢是!(a and !b)or(!a and b) 化简得 (!a or b)and(a or !b)

　　然后枚举点对讨论一个点对和S1，S2相连会不会超过lim来添加限制。

　　　　一共有四种情况都差不多，比如都连到S1会超过lim，就添加!(!a and !b) 化简得 (a or b)

构造表达式的时候可以从三个层次考虑，一个是直接写!()描述不允许出现的情况，然后化简。也可以考虑要排除什么情况，从什么变量取值使得子句为假出发，直接构造得到化简后的表达式。也可以从图上考虑，不通过dd_clause将子句化成蕴含的形式，直接考虑，谁向谁连边。比如相互喜欢就是四条边<a真,b真> <b假,a假><a假,b假><b真,a真>。

我觉得第一种比较好。

#include <iostream>
#include <cstdio>
#include <algorithm>
#include <vector>
#include <cstring>
using namespace std;

typedef pair<int,int> Point;
//点的标号从0开始到2n-1
const int maxn = 500 + 10 ;
const int maxm = 1000 + 10 ;
struct TwoSAT
{
    int n;
    vector<int> G[maxn*2];
    bool mark[maxn*2];
    int S[maxn*2],c;

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

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

    // x = xval or y = yval
    void add_clause(int x,int xval,int y,int yval){
        x = x * 2 + xval;
        y = y * 2 + yval;
        G[x^1].push_back(y);
        G[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]] = 0;
                    if(!dfs(i+1))
                        return 0;
                }
            }
        return 1;
    }
};

TwoSAT TSAT;
Point S[3],P[maxn];
pair<int,int> hate[maxm],like[maxm];

int N,A,B,SS;

int dis(Point P,Point Q){return abs(P.first-Q.first)+abs(P.second-Q.second);}

bool ok(int lim){
    TSAT.init(N);
    for (int i = 0; i < A; ++i){
        TSAT.add_clause(hate[i].first,0,hate[i].second,0);
        TSAT.add_clause(hate[i].first,1,hate[i].second,1);
    }
    for (int i = 0; i < B; ++i){
        TSAT.add_clause(like[i].first,0,like[i].second,1);
        TSAT.add_clause(like[i].first,1,like[i].second,0);
    }
    for (int i = 0; i < N; ++i)
        for (int j = i+1; j < N; ++j){
            int i0 = dis(P[i],S[0]),
                i1 = dis(P[i],S[1]),
                j0 = dis(P[j],S[0]),
                j1 = dis(P[j],S[1]);
            if(i0+j0>lim)
                TSAT.add_clause(i,1,j,1);
            if(i1+j1>lim)
                TSAT.add_clause(i,0,j,0);
            if(i0+SS+j1>lim)
                TSAT.add_clause(i,1,j,0);
            if(i1+SS+j0>lim)
                TSAT.add_clause(i,0,j,1);
        }
    return TSAT.solve();
}

int main()
{

    Point S1,S2;
    while(cin>>N>>A>>B){
        cin>>S[0].first>>S[0].second>>S[1].first>>S[1].second;
        SS=dis(S[0],S[1]);
        for (int i = 0; i < N; ++i)
            cin>>P[i].first>>P[i].second;

        for (int i = 0; i < A; ++i){
            cin>>hate[i].first>>hate[i].second;
            hate[i].first--;
            hate[i].second--;
        }
        for (int i = 0; i < B; ++i){
            cin>>like[i].first>>like[i].second;
            like[i].first--;
            like[i].second--;
        }

        if(!ok(4000000)){
            cout<<-1<<endl;
            continue;
        }

        int l=0,r=4000000,mid=(l+r)>>1;
        for(;l<r-1;mid=(l+r)>>1)
            if(ok(mid))
                r=mid;
            else
                l=mid;

        cout<<r<<endl;
    }
    return 0;
}

hdu4421 Bit Magic

http://acm.hdu.edu.cn/showproblem.php?pid=4421

按位做，变成32个问题。把题目给的逻辑函数（i ope j equal bval）对应的最大项表达式找到。需要注意的是，出现(i && j)可以处理成(i||i)&&(j||j)。

#include <cstdio>
#include <cstring>
#include <iostream>

using namespace std;

inline int min(int a,int b) { return a<b? a: b ; }
const int maxn =  4000 +10  ;
const int maxm =  4000000 + 10;
struct  TwoSAT {
    int col[maxn],dfn[maxn],low[maxn],s[maxn],cnt,scnt, stop,n;
    int pre[maxm],ad[maxn],v[maxm], tot ;

    void init()
    {
        tot=0 ;
        memset(ad,0,sizeof(ad));
    }
    void add(int x,int y)
    {
        pre[++tot] = ad[x];
        ad[x] = tot ;
        v[tot] = y; 
    }
    void add_clause(int x, int xval, int y, int yval)
    {
        add(x+xval*n,y+(!yval)*n);
        add(y+yval*n,x+(!xval)*n);
    }
    void dfs(int u) {
        dfn[u]=low[u]=++cnt ;
        s[++stop]=u;
        for (int j=ad[u];j;j=pre[j]){
            if (!dfn[v[j]]){
                dfs(v[j]);
                low[u] = min(low[u],low[v[j]]) ;
            }
            else if (!col[v[j]]) 
                low[u] = min(low[u] , dfn[v[j]]); 
        }
        if(low[u]==dfn[u]){
            ++scnt; 
            while(1){
                int x=s[stop--];
                col[x]=scnt; 
                if(x==u)break; 
            }
        }
    }
    bool slove()
    {
        memset(dfn,0,sizeof(dfn));
        memset(col,0,sizeof(col));
        cnt=scnt=stop= 0 ; 
        for (int i=0; i<2*n; ++i)
            if (!dfn[i])
                dfs(i);
        for(int i=0;i<n;++i)
            if (col[i] ==col[i+n])
                return 0;
        return 1;
    }
};

TwoSAT TSAT; 

int b[600][600]; 
int main()
{
    int n ; 
    while (scanf("%d",&n)!=EOF) {
        for (int i=0; i<n; ++i) 
            for (int j=0; j<n; ++j) 
                scanf("%d",&b[i][j]) ; 
        TSAT.n=n;
        int flag = 1; 
        for (int k=0; k<31; ++k) {
            TSAT.init() ; 
            for (int i=0; i<n; ++i) 
                for (int j=i; j<n; ++j)
                if (i==j)
                    continue; 
                else if (i %2 ==1 && j%2 ==1) {
                    if (b[i][j] & (1<<k)){
                        TSAT.add_clause(i,1,j,1);
                    }
                    else{
                        TSAT.add_clause(i,0,i,0);
                        TSAT.add_clause(j,0,j,0);
                    }
                }
                else if (i%2==0 && j%2==0) {
                    if (b[i][j] & (1<<k)){
                        TSAT.add_clause(i,1,i,1);
                        TSAT.add_clause(j,1,j,1);
                    }
                    else {
                        TSAT.add_clause(i,0,j,0);
                    }
                } 
                else {
                    if (b[i][j] & (1<<k)) {
                        TSAT.add_clause(i,0,j,0);
                        TSAT.add_clause(i,1,j,1);
                    }
                    else {
                        TSAT.add_clause(i,0,j,1);
                        TSAT.add_clause(i,1,j,0);
                    }
                }
                flag = TSAT.slove();
            //printf("%d %d
",k,flag); 
            if (!flag) break ; 
        }
        if (flag) puts("YES"); else puts("NO"); 
    }
}