2-SAT问题

2-SAT

SAT(satisfiabality)是适应性的缩写，一般称K的适应性问题为k-SAT

适应性问题就是有x1-n和y1-n的布尔变量，加入一些限制然后求限制内的解得问题（自己理解）

因为k>2的k-SAT问题是DP完全问题（没有一定的算法和正解）（好吧就是暴力），我们只讨论2-SAT问题。

我们先看一道洛谷的紫题。

注意下面的Two-SAT函数并不是2-SAT的标程，这是一种便于理解的（我写的时候只会的）方法。

洛谷P5782

#include<iostream>
#include<cstdio>
#include<vector>
#include<cstring>
#include<algorithm>
using namespace std;
const int maxn=10005;
int n,m;
vector<int> g[maxn*2];
bool mark[maxn*2];
int sta[maxn*2],top;
bool dfs(int x)
{
    if(mark[x^1])return false;
    if(mark[x])return true;
    mark[x]=1;
    sta[top++]=x;
    for(int i=0;i<g[x].size();i++)
        if(!dfs(g[x][i]))return false;
    return true;
}
inline bool TwoSAT()
{
    memset(mark,0,sizeof mark);
    for(int i=0;i<n;i+=2){
        if(!mark[i] and !mark[i^1]){
            top=0;
            if(!dfs(i))
            {
                while(top)mark[sta[--top]]=0;
                if(!dfs(i^1))return false;
            }
        }
    }
    return true;
}
int main()
{
    int u,v;
    scanf("%d%d",&n,&m);
        n*=2;
        for(int i=0;i<m;i++){
            scanf("%d%d",&u,&v);
            u--,v--;
            g[u].push_back(v^1);//建边 
            g[v].push_back(u^1);
        }
        if(TwoSAT()){
            for(int i=0;i<n;i+=2)
            if(mark[i])printf("%d
",i+1);
            else printf("%d
",(i^1)+1);
        }else printf("NIE
");
    return 0;
}

 然而这并不是2-SAT的普遍解法。一般来讲，我们会想到把所有元素的两种状态分别写出来，也就是把一个元素分为两个，然后通过求强联通分量求解。

怎么理解？

eg:给出条件，“a->b”表示满足a必须满足b（因为这些条件都是要满足的所以可以理解为下列条件都要满足）

条件：a -> -b , -b -> -a , -a -> b

我们把它想成一个图，发现b和-b在同一个强联通分量里，也就是说要符合条件必须满足b同事取b和-b，这显然是不可能的，所以本例无解。

那么我们就可以得到通俗解法，即求强联通分量：若一个元素的两种状态在同一个强联通分量里，此题无解;否则有解。

P4782洛谷模板

#include<iostream>
#include<cstdio>
#include<cstring>
#include<vector>
#include<algorithm>
#include<stack>
using namespace std;
inline int read()
{
    int x=0,w=0;char c=getchar();
    while(!isdigit(c))w|=c=='-',c=getchar();
    while(isdigit(c))x=(x<<3)+(x<<1)+(c^48),c=getchar();
    return w?-x:x;
}
const int maxn=2e6+10;
int n,m;
int ecnt,dfn[maxn],low[maxn],head[maxn],to[maxn],nxt[maxn],cnt,_n,belong[maxn];
vector<int> g[maxn];
//inline void addedge(int from,int too)
//{
//    to[++ecnt]=too;nxt[ecnt]=head[from];head[from]=ecnt;
//    to[++ecnt]=from;nxt[ecnt]=head[too];head[too]=ecnt;
//}
stack <int> st;
bool vis[maxn];
void tarjan(int x)
{
    dfn[x]=low[x]=++cnt;
    st.push(x);vis[x]=1;
    for (int i=0;i<g[x].size();i++)
    {
        int u=g[x][i];
        if(!dfn[u])
        {
            tarjan(u);
            low[x]=min(low[x],low[u]);
        }else if(vis[u])
            low[x]=min(low[x],dfn[u]);
    }
    
    if(low[x]==dfn[x])
    {
        ++_n;
        do{
            belong[x]=_n;
            x=st.top();st.pop();
            vis[x]=0;
        }while(dfn[x]!=low[x]);
    }
}
int main()
{
    n=read(),m=read();
    for(int x,y,x1,y1,i=1;i<=m;i++)
    {
        x=read(),x1=read(),y=read(),y1=read();
//        addedge(x+n*(x1&1),y+n*(y1^1));addedge(y+n*(y1&1),x+n*(x1^1));
        g[x+n*x1].push_back(y+n*(y1^1));
        g[y+n*y1].push_back(x+n*(x1^1));
    }
    for(int i=1;i<=(n<<1);i++)
    if(!dfn[i])tarjan(i);
    for(int i=1;i<=n;i++)
    if(belong[i]==belong[i+n]){
        printf("IMPOSSIBLE
");
        return 0;
    }
    printf("POSSIBLE
");
    for(int i=1;i<=n;i++)
        printf("%d ",belong[i]<belong[i+n]);
    printf("
");
    return 0;
}

//x1 1 0
//2 0 1 1

看到被我注释掉的前向星了吗？没错我因为这调了一下午

似乎有一个名为Kosaraju的算法也可以解决2SAT问题