首页 / 算法 / 「算法笔记」2-SAT 问题
「算法笔记」2-SAT 问题
内容导读
互联网集市收集整理的这篇技术教程文章主要介绍了「算法笔记」2-SAT 问题，小编现在分享给大家，供广大互联网技能从业者学习和参考。文章包含3109字，纯文字阅读大概需要5分钟。
内容图文
一、定义
k-SAT（Satisfiability）问题的形式如下：
-
有 \(n\) 个 01 变量 \(x_1,x_2,\cdots,x_n\)，另有 \(m\) 个变量取值需要满足的限制。
-
每个限制是一个 \(k\) 元组 \((x_{p_1},x_{p_2},\cdots,x_{p_k})\)，满足 \(x_{p_1}\oplus x_{p_2}\oplus\cdots\oplus x_{p_k}=a\)。其中 \(a\) 为 \(0\) 或 \(1\)，\(\oplus\) 是某种二元 bool 运算（如 或运算 \(\vee\)、与运算 \(\wedge\)）。
-
要求构造一种满足所有限制的变量的赋值方案。
当 \(k>2\) 时该问题为 NP 完全的，只能暴力求解。因此一般讨论的是 \(k=2\) 的情况，即 2-SAT 问题。
二、基本思想
以 Luogu P4782 【模板】2-SAT 问题 为例，建立图论模型。
\(m\) 个限制，每个限制的形式都是 「\(x_i\) 为 真/假 或 \(x_j\) 为 真/假」。
对于变量 \(x_i\)，建立两个点 \(i\) 与 \(i+n\)，分别表示 \(x_i\) 为真、\(\neg x_i\) 为真。
若 \(x\) 为真，则 \(\neg x\) 为假；若 \(\neg x\) 为假，则 \(x\) 为真。反之亦然。显然 \(x\) 和 \(\neg x\) 是互斥的。即，点 \(i\) 与 \(i+n\) 分别表示 \(x_i\) 为真或假。
对变量关系建有向图。有向边 \(u\to v\) 表示，若 \(u\) 为真，则 \(v\) 一定为真。
具体地，对于每个限制 \((a\vee b)\)（变量 \(a,b\) 至少满足一个），可将其转化为 \(\neg a\rightarrow b\wedge\neg b\rightarrow a\)（\(a\) 为假则 \(b\) 一定为真；\(b\) 为假则 \(a\) 一定为真）。即节点 \(\neg a\) 向节点 \(b\) 连边，从节点 \(\neg b\) 向节点 \(a\) 连边。
考虑节点 \(i\) 与 \(i+n\) 在图中的关系。若它们 互相可达，即在 同一个强连通分量 中，则说明在赋值限制下，它们代表的一对互斥取值会同时被取到。则不存在一组合法的赋值方案。
否则，说明有解，考虑如何构造一组合法解。
首先，对建出的图进行缩点得到一个 DAG。考虑节点 \(i\) 与 \(i+n\) 所在强连通分量的 拓扑关系。若两分量不连通，则 \(x_i\) 取任意值（真或假）。否则只能取属于拓扑序较大的分量的值。因为若取拓扑序较小的值，可以根据逻辑关系推出取另一个值也是同时发生的。
三、具体实现
以 Luogu P4782 【模板】2-SAT 问题 为例。
-
对于每个限制 \((a\vee b)\)（变量 \(a,b\) 至少满足一个），节点 \(\neg a\) 向节点 \(b\) 连边，从节点 \(\neg b\) 向节点 \(a\) 连边。
-
用 Tarjan 算法对建出的图缩点。
-
对于 \(i\in [1,n]\)，若 \(i\) 与 \(i+n\) 在同一个强连通分量中，则不存在一组合法的赋值方案。
-
否则，根据 Tarjan 求得的强连通分量的标号为拓扑逆序，即反向的拓扑序 ，可以得到 \(x_i\) 的值（取 \(i\) 与 \(i+n\) 所在强连通分量拓扑序较大的点的值）。
#include<bits/stdc++.h>
#define int long long
using namespace std;
const int N=2e6+5;
int n,m,x,a,y,b,cnt,hd[N],to[N<<1],nxt[N<<1],tot,c[N],top,s[N],num,dfn[N],low[N];
void add(int x,int y){
to[++cnt]=y,nxt[cnt]=hd[x],hd[x]=cnt;
}
void tarjan(int x){
dfn[x]=low[x]=++num,s[++top]=x;
for(int i=hd[x];i;i=nxt[i]){
int y=to[i];
if(!dfn[y]) tarjan(y),low[x]=min(low[x],low[y]);
else if(!c[y]) low[x]=min(low[x],dfn[y]);
}
if(low[x]==dfn[x]){
c[x]=++tot;
while(s[top]!=x) c[s[top--]]=tot;
--top;
}
}
signed main(){
scanf("%lld%lld",&n,&m);
for(int i=1;i<=m;i++){
scanf("%lld%lld%lld%lld",&x,&a,&y,&b);
if(a&&b) add(x+n,y),add(y+n,x);
if(!a&&b) add(x,y),add(y+n,x+n);
if(a&&!b) add(x+n,y+n),add(y,x);
if(!a&&!b) add(x,y+n),add(y,x+n);
}
for(int i=1;i<=2*n;i++)
if(!dfn[i]) tarjan(i);
for(int i=1;i<=n;i++)
if(c[i]==c[i+n]) puts("IMPOSSIBLE"),exit(0);
puts("POSSIBLE");
for(int i=1;i<=n;i++)
printf("%d%c",c[i]<c[i+n],i==n?'\n':' '); //Tarjan 求得的强连通分量的标号为拓扑逆序，即反向的拓扑序
return 0;
}
内容总结
以上是互联网集市为您收集整理的「算法笔记」2-SAT 问题全部内容，希望文章能够帮你解决「算法笔记」2-SAT 问题所遇到的程序开发问题。 如果觉得互联网集市技术教程内容还不错，欢迎将互联网集市网站推荐给程序员好友。
内容备注
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 gblab@vip.qq.com 举报，一经查实，本站将立刻删除。
内容手机端
扫描二维码推送至手机访问。