首页 > 代码库 > 2-SAT入门 poj2749 Building roads

2-SAT入门 poj2749 Building roads

2024-07-12 03:12:43   223人阅读

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-1const 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;}

 


联系
我们