[学习笔记]2-SAT 问题
(本文语言不通,细节省略较多,不适合初学者学习)
解决一类简单的sat问题。
每个变量有0/1两种取值,m个限制条件都可以转化成形如:若x为0/1则y为0/1等等(x可以等于y)
具体:
每个变量拆成i,i+n两个点,表示取0和取1
对于x为0,y为1的情况,从x向y+n连接一条边,
发现有逆命题:若y为0,则x一定为1,从y向x+n连接一条边。
可以发现,这形成了一个有向图。
可以tarjan
无解的条件是:一个变量的i,i+n在同一个scc里。这样这个变量不论取哪个值,都必须取另外一个值。
至于怎么输出方案?
方法一:
tarjan启发缩点。同一个scc一个值确定,其他的值就都确定了。
现在是DAG,就要拓扑咯。
如果正常拓扑的话,入度为0的点,出度影响的是一大片。随便赋值很可能就错了。
0出度点比较温顺,不会影响别人的取值。
就建一个反向DAG。然后拓扑
自底向上,不断选择零出度点。
具体流程:
c[i]表示i属于的scc
2-SAT点的对称的,边的连法也是对称的,所以其实一个scc也是对称的。设opp[c[i]]=c[i+n],opp[c[i+n]]=c[i]
由于对称,对于一个scc中的任何点i,opp[c[i]]都是c[i+n]。
val[2*n]表示scc的赋值。
初始-1
1.队列开始的scc,编号k
如果val[k]=-1,则val[k]=0,val[opp[k]]=1 (前提条件:i是0,i+n是1)
val[k]=0表示选择这个scc的赋值可以取到自己。
否则跳过。
2.topo结束后,for(i=1,i<=n,i++)
如果val[c[i]]=0,表示,c[i]可以取到。那么i的值就是0
如果val[c[i]]=1,表示,我们先topo到了val[c[i+n]],val[c[i+n]]=0,可以取。0就不可取了。
合并一下,恰好,i的实际值就是val[c[i]]
正确性:
一个链其实是一个块,证明时可以分别考虑。
因为图是对称的,根据bfs性质,如果先推到i,一定i+n会在i后面才推到。所以,其实整个链是连续的scc都取自己,即val[k]=0的。不存在i的一个后继没有选上,却选上了的情况
所以,
1.如果不存在一个i,满足i,i+n都在链上,一个链上的scc其实是同时取或者同时不取,一定满足条件。
2.如果存在一个i,i+n都在链上。先访问到的会选择上。假设i指向i+n,由于反向建图,会先访问i+n,变量i会赋值为1,代表0的i点没有选择自己,条件的假设本身就不满足了。这显然合法。
复杂度:线性。
方法二:
方法一好麻烦啊。还要缩点还要topo
发现一个性质:
tarjan本质是DFS
最先赋值的是底层的scc
本来就要自底向上topo,所以,干脆就把scc和opp[scc]的大小作为val好了。
即,c[i]>opp[c[i]]的话,那么意味着,tarjan的时候,先dfs出opp[c[i]],对应topo中先把opp[c[i]]入队。
(由于刚才说了,topo实际上把一条链上的scc都选择自己,或者都不选择自己,和dfs先搜完一个子树再回溯如出一辙。整个子树scc缩点之后就是一条链,这条链的scc值都比对称的链scc小。即先赋值。)
所以,i就赋值为对面的1
反之就是0
发现,恰好,i的赋值就是c[i]>c[i+n]
仔细想想,其实我已经证明了方法二和方法一本质是一致的。
两者正确性的证明都是上面写的那个。
(upda2019.4.3:
这个证明和上面的不一样
发现两条链不是简单对称,而是“DNA双螺旋结构!”
也就是,反向对称的
而且发现,对于一条链,后继一定比前驱的编号小
不妨从1~n那排点考虑,所以,如果一个点被选择了,意味着c[i]<c[i+n]
由于反向对称,而i的后继对应的是i+n的前驱,所以编号一定也更小,一定也会被选择上。
所以正确。
)
方法二显然简单。
甚至不用缩点,tarjan完了,直接输出。
模板:
#include<bits/stdc++.h>
#define numb (ch^'0')
using namespace std;
typedef long long ll;
const int N=1e6+;
void rd(int &x){
x=;char ch;
while(!isdigit(ch=getchar()));
for(x=numb;isdigit(ch=getchar());x=(x<<)+(x<<)+numb);
}
int n,m;
struct node{
int nxt,to;
}e[*N];
int hd[*N],cnt;
void add(int x,int y){
e[++cnt].nxt=hd[x];
e[cnt].to=y;
hd[x]=cnt;
}
int sta[*N],top;
bool in[*N];
int c[*N],scc;
int dfn[*N],low[*N];
int df;
void tarjan(int x){
//cout<<" x "<<x<<endl;
dfn[x]=low[x]=++df;
in[x]=;
sta[++top]=x;
for(int i=hd[x];i;i=e[i].nxt){
int y=e[i].to;
//cout<<y<<endl;
if(!dfn[y]){
tarjan(y);low[x]=min(low[x],low[y]);
}
else if(in[y]) low[x]=min(low[x],dfn[y]);
}
if(dfn[x]==low[x]){
scc++;int z;
do{
z=sta[top--];in[z]=;c[z]=scc;
}while(z!=x);
}
}
int main(){
rd(n);rd(m);
int x,y,p,q;
for(int i=;i<=m;i++){
rd(x),rd(p),rd(y),rd(q);
add(x+(-p)*n,y+q*n);
add(y+(-q)*n,x+p*n);
}
for(int i=;i<=*n;i++){
if(!dfn[i]) tarjan(i);
top=;
}
for(int i=;i<=n;i++){
if(c[i]==c[i+n]){
printf("IMPOSSIBLE");return ;
}
}
printf("POSSIBLE\n");
for(int i=;i<=n;i++){
printf("%d ",c[i]>c[i+n]);
}
return ;
}
最新文章
- js正则表达式校验非零的正整数:^[1-9]\d*$ 或 ^([1-9][0-9]*){1,3}$ 或 ^\+?[1-9][0-9]*$
- Web 前端开发精华文章集锦(jQuery、HTML5、CSS3)【系列十八】
- 在Main中定义student的结构体,进行年龄从大到小依次排序录入学生信息。(结构体的用法以及冒泡排序)
- Java基础之写文件——使用Formatter对象加载缓冲区(UsingAFormatter)
- Django搭建及源码分析(二)
- jquery的each()函数用法
- Swift标识符和关键字
- Java发送post请求
- select默认选择的实现方法
- 武汉科技大学ACM :1007: 华科版C语言程序设计教程(第二版)习题7.10
- 关于Qt信号与槽机制的传递方向性研究(结论其实是错误的,但是可以看看分析过程)
- Canvas旋转图片--保持相同大小的算法
- Mysql笔记3数据库基本操作
- java集合(3)- Java中的equals和hashCode方法详解
- django drf 开发 ~ models基础学习
- PostgreSQL自学笔记:7 插入、更新与删除数据
- MySQL中的sort_buffer_size参数大小的设置问题
- T-SQL:Varchar和Nvarchar区别(八)
- poj3070_斐波那契数列(Fibonacci)
- Java EE之Hibernate异常总结【5】java.lang.StackOverflowError[栈溢出]
热门文章
- selenium--driver.switchTo()
- FU-A方式分包
- Linux搭建mysql、apache、php服务总结
- Spring Cloud(五):Hystrix 监控面板【Finchley 版】
- 正式放弃Edge,重新拥抱Chrome
- AC 自动机——多模式串匹配
- solidity事件详解
- 2019-1-7Xiaomi Mi5 刷全球版MIUI教程
- 上层应用与wpa_supplicant,wpa_supplicant与kernel 相关socket创建交互分析
- UML建模语言入门 -- 静态图详解 类图 对象图 包图 静态图建模实战