2-SAT (two-statisfiability) 算法学习笔记

$2-SAT$问题指的是对于若干限制求出一组可行解的问题。

考虑对于$n$个值域为${0,1}$的变量$x_1 , x_2 ,...,x_n$ 满足若干限制：

若 $x_i = p$ 则 $x_j = q ( i,j\in[1,n],p,q \in \{0,1\})$

我们考虑对于每一个变量$x_i$开一个值域$x_{i,0} , x_{i,1}$表示第$i$个变量取值为$0/1$的点。

然后考虑每一组命题，若 $x_i = p$ 则 $x_j = q , i,j\in[1,n],p,q \in \{0,1\}$ ，

首先把$x_{i,p}$和$x_{j,q}$两个点连一条单向边。

并且由于这个命题非常特殊，值域大小只为2 ，其逆否命题也是限制（可以显然的反证）。

于是就把$x_{j,1-q}$和$x_{i,1-p}$ 连一条单向边。

然后对于上面的图跑tarjan找出scc，如果$x_{i,0}$和$x_{i,1}$在同一连通块中了，

说明下列命题成立： “若$x_i = 0$则$x_i = 1$ ” ，“若$x_i = 1$则$x_i = 0$ ” 所以此时答案无解。

如何构造出一组解呢，由于tarjan的dfs特性，

设$c_i$表示通过tarjan算法求出的连通块编号（这本身就是逆拓扑序的）。

$val_i = c_{x_{i,0}} > c_{x_{i,1}}$ 就构造出$val_i , i\in [1,n]$一组合法解了。

P4782 【模板】2-SAT 问题

设变量$x_i \in \{0,1\}$ ，给出若干组关系：$x_i = p $ 或者 $x_j = q$

如果$x_i ， (i\in [1,n])$有解,先输出"POSIBLE"然后输出一组合法解。

如果$x_i , (i\in [1,n])$无解，则输出"IMPOSIBLE"即可。

对于100%的数据$n,m\leq 10^6$

Sol：

$x_i$为$p$ 或 $x_j$为$q$ 可以拆成$2\times 2$对逻辑关系。

若$x_i$为$1-p$，则$x_j$为$q$ , 若$x_j$为$1-q$，则$x_i$为$p$
若$x_j$为$1-q$，则$x_i$为$p$ , 若$x_i$为$1-p,$ 则$x_j$为$q$

实现方面，只需：$[1,N]$为原来元素的$0$域，$[N+1，2N]$ 为原来元素的$1$域.

# include <bits/stdc++.h>

using namespace std;

const int N=2e6+,M=4e6+;

struct rec{ int pre,to;}a[M];

stack<int>s;

bool ins[N];

int cnt,tot,n,m,head[N],c[N],dfn[N],low[N],val[N];

void adde(int u,int v)

{

    a[++tot].pre=head[u];

    a[tot].to=v;

    head[u]=tot;

}

void tarjan(int u)

{

    dfn[u]=low[u]=++dfn[];

    s.push(u);ins[u]=;

    for (int i=head[u];i;i=a[i].pre){

        int v=a[i].to;

        if (!dfn[v]) {

            tarjan(v);

            low[u]=min(low[u],low[v]);

        } else if (ins[v]) low[u]=min(low[u],dfn[v]);

    }

    if (dfn[u]==low[u]) {

        cnt++; int v;

        do {

            v=s.top(); s.pop();

            ins[v]=; c[v]=cnt;

        } while (u!=v);

    }

}

int main()

{

    scanf("%d%d",&n,&m);

    for (int i=;i<=m;i++) {

        int s,ps,t,pt; scanf("%d%d%d%d",&s,&ps,&t,&pt);

        adde(s+(-ps)*n,t+pt*n); adde(t+(-pt)*n,s+ps*n);

        adde(t+(-pt)*n,s+ps*n); adde(s+(-ps)*n,t+pt*n);

    }

    for (int i=;i<=*n;i++) if (!dfn[i]) tarjan(i);

    for (int i=;i<=n;i++) if (c[i]==c[i+n]) {

        puts("IMPOSSIBLE"); return ;

    }

    for (int i=;i<=n;i++) val[i]=c[i]>c[n+i];

    puts("POSSIBLE");

    for (int i=;i<=n;i++) printf("%d ",val[i]); puts("");

    return ;

}

巴特西

2-SAT (two-statisfiability) 算法学习笔记

P4782 【模板】2-SAT 问题

最新文章

热门文章

巴特西

2-SAT (two-statisfiability) 算法 学习笔记

P4782 【模板】2-SAT 问题

最新文章

热门文章

2-SAT (two-statisfiability) 算法学习笔记