2SAT学习笔记

算法&模板

算法

应用的问题

当有一堆的非黑即白的关系，且关系两两间存在一定的限制

此时可以运用2-SAT算法来求出可行解或者判断无解

引入

存在n个点，要求对点进行黑白染色，有m条限制形如：\((u,f_1,v,f_2)\)
表示 [ \(u\) 号点为 \(f_1\) 或 \(v\) 号点为 \(f_2\) ] ,求一组可行解

考虑将"或" 这种比较模糊的条件限制给固定住
即: 对于\((u,f_1,v,f_2)\)
有:

• \(u\) 号点不为 \(f_1\)时, \(v\) 号点为 \(f_2\)
• \(v\) 号点不为 \(f_2\)时, \(u\) 号点为 \(f_1\)

那么我们可以从u和v的部分取值中确切的推出对方的取值了
但此处是部分取值,那么考虑拆点,将每个点 \(u\) 拆成两个点,分别代表 \(u\) 选白和 \(u\)选黑
然后按照上面列出的限制,将每个点的状态向可推出的其他点的相应状态连边即可

连边后发现若发现点u的黑点与白点同处一个环内,则代表限制存在矛盾

否则,对于每个原先的点将它的缩点拓扑序较大的新点作为答案

code

建图

	
for(int i=1;i<=n;++i) id[0][i]=i+n, id[1][i]=i;
for(int i=1;i<=m;++i)
{
     int u=read(), x=read(), v=read(), y=read();
     add(id[1^x][u],id[y][v]);
     add(id[1^y][v],id[x][u]);
}
	

tarjan缩点

int col[_<<1], st[_<<1], top, dfn[_<<1], low[_<<1], cnt, num, id[2][_];
void tarjan(int u)
{
    low[u]=dfn[u]=++cnt, st[++top]=u;
    for(int i=h[u];i;i=e[i].ne)
    {
        int v=e[i].to;
        if(dfn[v] && !col[v]) low[u]=min(low[u], dfn[v]);
        else if(!dfn[v]) { tarjan(v); low[u]=min(low[u],low[v]);}
    }
    if(dfn[u]!=low[u]) return;
    col[u]=++num; while(st[top]!=u) col[st[top]]=num, top--; top--;
}

check&getans

for(re int i=1;i<=n;++i) if(col[i]==col[n+i]) {puts("IMPOSSIBLE"); return 0;}
puts("POSSIBLE");
for(re int i=1;i<=n;++i) printf("%d ", (col[i]<col[i+n]));

例题

此坑待填