2-SAT问题的解法（uva1146）

电玩女神 2022-08-08 12:44 82阅读 0赞

SAT：就是一些由布尔值组成的关系的集合。  
2-SAT：就是由两个布尔值组成的关系的集合。  
2-SAT问题：就是给出一些关系，然后问能不能满足这些所有的关系？  
现在比如说有n个国家，每个国家有两个代表，必须选出一个代表参加一个国际会议，但是有些代表之间有矛盾，现在给出这些矛盾的代表，问能不能选出满足条件的。  
4个国家，代表编号为2\*i，2 \*i-1  
这些代表有矛盾1和4，2和3，7和3  
这样的话肯定是能够满足条件的。  
这篇论文讲的很清晰

[点击][Link 1]

其中给出了两种解法，首先对于上面的例子，1和4有矛盾，很明显分别属于1和2国家，那么加入我要选1则必须选3，因为每个国家必须选一个，而1和4又是矛盾的！同样要选4必须选2，那么我可以给他们必选条件之间建一条有向边。  
那么对于上面样例可以得到这样一个图  
![这里写图片描述][20150517112622449]  
这样建图之后，能够得到一种很直观的解法。  
枚举所有的同一个国家的代表（2\*i 和 2 \*i-1）首先任选一个，推导出相关的，若不矛盾，则可行，否则选另一个，若也不可行，则无解。  
这个算法的时间负责度O（m\*n），在大多数情况下是可行的。

其实可以更优，首先我们发现图中存在很多环，对环缩点是对原图情况没有影响的，同样，在同一个环中的点必然是要么都选，要么都不选，那么如果存在在一个换中有同一个国家的两个代表的话，这样肯定是不可行的。  
那么就得到了一个基于对称性的算法，建图，缩点，缩在同一个环上的点判断是否是同一个国家，不在则无解。算法负责度O（m）

UVA1146这个题目是一个类似的题目，不过要求一个最大值，我们二分结果，然后用2-set判断是否可行。  
Tarjan算法：

#include <iostream>
    #include <cstdio>
    #include <cstring>
    #include <vector>
    #include <algorithm>
    #include <stack>
    using namespace std;
    const int N = 2200;
    int tim[N][3],dfs_clock,tpnum;
    stack<int> sta;
    struct TwoSet
    {
        vector<int> G[2*N];
        bool vis[2*N];
        int dfn[2*N],low[2*N],tp[2*N];
        void init(int n)
        {
            for(int i=0;i<=2*n;i++)
                G[i].clear();
            dfs_clock = tpnum = 0;
            memset(vis,false,sizeof(vis));
            memset(dfn,0,sizeof(dfn));
            memset(low,0,sizeof(low));
            memset(tp,0,sizeof(tp));
            while(!sta.empty())
                sta.pop();
    
        }
        void add_Node(int x,int valx,int y,int valy)
        {
            x = 2*x + valx;
            y = 2*y + valy;
            G[x^1].push_back(y);
            G[y^1].push_back(x);
        }
        void Tarjan(int x)
        {
            sta.push(x);
            vis[x] = true;
            dfn[x] = low[x] = ++dfs_clock;
            for(int i=0;i<G[x].size();i++)
            {
                int y = G[x][i];
                if(!dfn[y])
                {
                    Tarjan(y);
                    low[x] = min(low[x],low[y]);
                }
                else
                {
                    if(vis[y])
                        low[x] = min(low[x],dfn[y]);
                }
            }
            if(low[x] == dfn[x])
            {
                tpnum++;
                do
                {
                    x = sta.top();
                    sta.pop();
                    vis[x] = false;
                    tp[x] = tpnum;
                }while(low[x] != dfn[x]);
            }
        }
        bool yougth(int n)
        {
            for(int i=0;i<2*n;i++)
                if(!dfn[i])
                    Tarjan(i);
            for(int i=0;i<n;i++)
                if(tp[2*i]==tp[2*i+1])
                    return false;
            return true;
        }
    };
    TwoSet solver;
    bool test(int diff,int n)
    {
        solver.init(n);
        for(int i=0;i<n;i++)for(int a=0;a<2;a++)
            for(int j=i+1;j<n;j++)for(int b=0;b<2;b++)
                if(abs(tim[i][a]-tim[j][b])<diff)solver.add_Node(i,a^1,j,b^1);
        return solver.yougth(n);
    }
    int main()
    {
        //freopen("Input.txt","r",stdin);
        int n;
        while(~scanf("%d",&n))
        {
            int L = 0,R = 0;
            for(int i=0;i<n;i++)
            {
                for(int t=0;t<2;t++)
                {
                    scanf("%d",&tim[i][t]);
                    R = max(R,tim[i][t]);
                }
            }
            while(L<R)
            {
                int mid=L+(R-L+1)/2;
                if(test(mid,n))L=mid;
                else R=mid-1;
            }
            printf("%d\n",L);
        }
        return 0;
    }

直接暴力判断算法：

#include <iostream>
    #include <cstdio>
    #include <cstring>
    #include <vector>
    #include <algorithm>
    using namespace std;
    const int N = 2200;
    int tim[N][3];
    
    struct TwoSet
    {
        vector<int> G[2*N];
        bool vis[2*N];
        int s[2*N],c;
        void init(int n)
        {
            for(int i=0;i<=2*n;i++)
                G[i].clear();
            memset(vis,false,sizeof(vis));
        }
        void add_Node(int x,int valx,int y,int valy)
        {
            x = 2*x + valx;
            y = 2*y + valy;
            G[x^1].push_back(y);
            G[y^1].push_back(x);
        }
        bool dfs(int x)
        {
            if(vis[x^1])
                return false;
            if(vis[x])
                return true;
            vis[x] = true;
            s[c++] = x;
            for(int i=0;i<G[x].size();i++)
            {
                if(!dfs(G[x][i]))
                    return false;
            }
            return true;
        }
        bool yougth(int n)
        {
            for(int i = 0;i< 2*n;i+=2)
            {
                if(!vis[i] && !vis[i+1])
                {
                    c = 0;
                    if(!dfs(i))
                    {
                        while(c>0)
                            vis[ s[--c] ] = false;
                        if(!dfs(i+1))
                            return false;
                    }
                }
            }
            return true;
        }
    };
    TwoSet solver;
    bool test(int diff,int n)
    {
        solver.init(n);
        for(int i=0;i<n;i++)for(int a=0;a<2;a++)
            for(int j=i+1;j<n;j++)for(int b=0;b<2;b++)
                if(abs(tim[i][a]-tim[j][b])<diff)solver.add_Node(i,a^1,j,b^1);
        return solver.yougth(n);
    }
    int main()
    {
        //freopen("Input.txt","r",stdin);
        int n;
        while(~scanf("%d",&n))
        {
            int L = 0,R = 0;
            for(int i=0;i<n;i++)
            {
                for(int t=0;t<2;t++)
                {
                    scanf("%d",&tim[i][t]);
                    R = max(R,tim[i][t]);
                }
            }
            while(L<R)
            {
                int mid=L+(R-L+1)/2;
                if(test(mid,n))L=mid;
                else R=mid-1;
            }
            printf("%d\n",L);
        }
        return 0;
    }

[Link 1]: http://wenku.baidu.com/view/afd6c436a32d7375a41780f2.html
[20150517112622449]: /images/20220805/874cde80fec7422eb9ed6036c8c2c535.png