CF641F Little Artem and 2-SAT解题报告

解题报告

CF641F Little Artem and 2-SAT解题报告：

更好的阅读体验

题意

给定两个 $n$ 个点的 2-SAT 模型（各 $m1,m2$ 条限制，型为 $\wedge_{i=1}^m (a_i\vee b_i)$ ），判断这两个模型的解集是否相同，如果不同，构造一组解使得一个有解一个无解。（$1\leqslant n\leqslant 1000,1\leqslant m\leqslant n^2$）

分析

憨憨题+经典题。

这道题告诉我们，2-SAT 不一定一定要用 tarjan 和 kosaraju，有时候 Floyd 也可以在 2-SAT 中有所应用。

事实上，我们用 Floyd 跑一遍传递闭包，然后再 dfs 一遍就可以解出 2-SAT 了。

首先建出来两个 2-SAT 模型，跑一遍，如果两个都无解就相似，如果一个有解一个无解就构造一组使某个模型有解。

否则有一些变量的取值是固定的，判一下是否有固定变量取值不同，或是有一个变量在一个模型确定，一个不确定，很容易构造出解。

此时两个模型的确定变量已经是相同的了，我们比较传递闭包的邻接矩阵是否相同，只要有一个不同的地方（设其为 $x\rightarrow y$）且 $x,y$ 在另一个模型内均没有确定取值，就可以钦定 $x=1,y=0$，然后跑一组解就好了。

时间复杂度：$O(\frac{n^3}{\omega}+m)$。

代码

2-SAT别写错，我写错了调了一个世纪 /ll 。

#include<stdio.h>
#include<bitset>
#define rev(x) (x>n? (x-n):(x+n))
using namespace std;
const int maxn=1005;
int n;
struct two_sat{
    int m,ok;
    int fixed[maxn<<1];
    bitset<maxn<<1>g[maxn<<1];
    void get(int x){
        fixed[x]=1,fixed[rev(x)]=0;
        for(int i=1;i<=2*n;i++)
            if(g[x][i]&&fixed[i]==-1)
                get(i);
    }
    void build(){
        for(int i=1;i<=2*n;i++)
            g[i].reset(),g[i][i]=1,fixed[i]=-1;
        for(int i=1;i<=m;i++){
            int x,y;
            scanf("%d%d",&x,&y),x=x>0? x:rev(-x),y=y>0? y:rev(-y);
            g[rev(x)][y]=1,g[rev(y)][x]=1;
        }
        for(int k=1;k<=2*n;k++)
            for(int i=1;i<=2*n;i++)
                if(g[i][k])
                    g[i]|=g[k];
        for(int i=1;i<=n;i++)
            if(g[i][n+i]&&g[n+i][i]){
                ok=0;
                return ;
            }
        ok=1;
        for(int i=1;i<=n;i++){
            if(fixed[i]==-1&&fixed[n+i]==-1&&g[i][n+i])
                get(n+i);
            if(fixed[i]==-1&&fixed[n+i]==-1&&g[n+i][i])
                get(i);
        }
    }
    void solve(){
        for(int i=1;i<=2*n;i++)
            if(fixed[i]==-1)
                get(i);
        for(int i=1;i<=n;i++)
            printf("%d%c",fixed[i],i==n? '\n':' ');
    }
}A,B;
int main(){
    scanf("%d%d%d",&n,&A.m,&B.m),A.build(),B.build();
    if(A.ok==0&&B.ok==0){
        puts("SIMILAR");
        return 0;
    }
    if(A.ok==0||B.ok==0){
        if(A.ok)
            A.solve();
        if(B.ok)
            B.solve();
        return 0;
    }
    for(int i=1;i<=2*n;i++){
        if(A.fixed[i]!=-1&&B.fixed[i]!=-1&&A.fixed[i]!=B.fixed[i]){
            A.solve();
            return 0;
        }
        if((A.fixed[i]==-1)+(B.fixed[i]==-1)==1){
            if(A.fixed[i]==-1)
                A.get(B.fixed[i]==0? i:rev(i)),A.solve();
            if(B.fixed[i]==-1)
                B.get(A.fixed[i]==0? i:rev(i)),B.solve();
            return 0;
        }
    }
    for(int i=1;i<=2*n;i++)
        for(int j=1;j<=2*n;j++){
            if(A.g[i][j]&&B.g[i][j]==0&&B.fixed[i]==-1&&B.fixed[i]==-1){
                B.get(i),B.get(rev(j)),B.solve();
                return 0;
            }
            if(B.g[i][j]&&A.g[i][j]==0&&A.fixed[i]==-1&&A.fixed[j]==-1){
                A.get(i),A.get(rev(j)),A.solve();
                return 0;
            }
        }
    puts("SIMILAR");
    return 0;
}