【学习笔记】2-SAT
主要参考https://anguei.blog.luogu.org/solution-p4782
前言
SAT描述的是一类如何使得一些（一些布尔变量的|）的&为真的问题
据说已被证明是NP完全问题只能暴力，而2-SAT则是对这个问题进行限制
只考虑如何使得一些（2个布尔变量的|）的&为真的问题
正文
暴力不提
第一次思维跳跃
我们可以对布尔变量x建x点表示使x为真，和-x点表示使x为假
显然，要求((-x)|(-x))&(x|x)是显然无解的
那么我们考虑什么情况下无解，我们怎么确认它无解
第二次思维跳跃
我们可以用“=>“表示推知，那么根据题给约束，我们可以将推知建成有向边
也就是当题目要求(x&y)时，-x=>y且-y=>x所以我们可以-x向y建边-y向x建边
那么，这样做有什么用（事实上，先讲建边再讲怎么用相当于铺平了道路往下走，在实际教授中不可以这样）
那我们重新来，请忽略这一部分
第二次思维跳跃
我们想要确认它无解，也就是()&()两者不能同时成立
那么什么时候不会同时成立呢？
我们其实已经有了一组冲突条件，显然x为真-x就不为真
所以我们不可以既让x为真又让-x为假
可是从题目给的约束中得到这些并不容易
其实yjx已经想到过一种写法，如果有(x|y)&(-x|z)&(y|(-z))这样的条件
我们先假设x成立，那么-x一定不成立，那么z一定就成立，如果z成立，那-z就不成立，所以y一定成立（如果觉得绕就多想一想）
这时我们如果略去什么x成立-x就不成立这种已知的约束条件
就直接是假设x成立，则z成立，则y成立
我们知道这个衔接部分（如-x不成立，z就一定成立）的约束是题目所给（即(-x|z)）
那么我们要做的就是略去已知条件，高效地将题给条件转化为这种我们所需要的推导过程（由(-x|z)推知x成立，z就一定成立）
那么如何转化为推导过程已经很明显了
对于（x&y）我们可以得到（“=>”表示推知）-x=>y且-y=>x
在编程实现的过程中我们可以把推知转化为边来思考，那么对于每个布尔变量x都要建它的x点和-x点
那我们再次回到刚刚的问题“我们怎么确认一个2-SAT问题无解”或者说“我们怎么确认题给条件有冲突”
第三次思维跳跃
首先我们可以明确一点，题给条件是一种约束，而冲突是我们布尔变量定义决定的当x成立，-x就不成立
无解即是x成立，而约束使得-x也得成立
如果我们尝试用建边将=>推知表现出来，那么当x=>a=>b=>…=>-x时，x不能为真，但是注意，这不足以判断无解，无解还需要-x=>c=>d=>…=>x
也就是假设x成立，约束使得-x也得成立，再假设-x成立，约束使得x也得成立
这时一定无解，再简要概括就是建边后x能连到-x，-x也能连到x，那么这个判断怎么实现呢
第四次思维跳跃
暴力就不提了，我们可以想到的是，当有向图中x能连到-x，-x也能连到x，x和-x处于同一强连通分量里面，那么判断问题无解也就转换为了判断每个布尔变量的x和-x在不在同一强连通分量里
具体实现自然用tarjan求有向图强连通分量
那么如果问题有解，我们应该如何找出某个可行解呢（说可行解是因为可能有多解）
第五次思维跳跃
思考一下，问题有解可能是哪几种情况。。。
我们是不是可以将问题有解分为对于一个布尔变量x
1.约束条件使x=>a=>b=>…=>-x，x只能为false
2.约束条件使-x=>c=>d=>…=>x，x只能为true
3.约束条件没有使x和-x相连（或者根本没约束x），x可以为true/false
那么除了暴力假设x成立，再跑一边看看有没有x=>a=>b=>…=>-x，我们能不能从图的性质上想出解决的高效方法
3比较好处理，关键是怎么快速判断有没有1/2
也就是？
看x在-x前面/后面
有向图中的前面后面的表现是什么？
第六次思维跳跃
拓扑序
如果x的拓扑序小于-x的，那么就可能存在x=>a=>b=>…=>-x（可能的意思是也可能是x与-x不相连，但跑出来的拓扑序x的小)就令x为false，否则可能存在-x=>c=>d=>…=>x，令x为true
不用判断3是因为3的情况出现时x为true/false都可以，但只要有x=>a=>b=>…=>-x，x的拓扑序就一定小于-x，只要有-x=>c=>d=>…=>x，-x的拓扑序就一定小于x的，那么可以想到上面这样做没有问题
那为什么用拓扑序就不算暴力了？不要再跑一遍图？还有环怎么办？
第七次思维跳跃
注意思考问题，拓扑序能够由dfs的顺序提供吗？
比如我们是不是可以对于x=>a=>b=>…=>-x，x的dfs序小于-x的，那么x为false
但是，有环情况下我们可能可以举出反例吗？
好像环也没有问题？
但是我想到一个问题，如果对于x=>a=>b=>-x我们先dfs了a->b->-x，再dfs了x,那么x的dfs序不是更大，但是显然x的拓扑序小啊
嗯本文是一遍看题解一遍思考的，然后我看到了这句话
但是，对于一组布尔方程，可能会有多组解同时成立。要怎样判断给每个布尔变量赋的值是否恰好构成一组解呢？
这个很简单，只需要 当 x 所在的强连通分量的拓扑序在¬x所在的强连通分量的拓扑序之后取 x 为真 就可以了。在使用 Tarjan 算法缩点找强连通分量的过程中，已经为每组强连通分量标记好顺序了——不过是反着的拓扑序。所以一定要写成 color[x] < color[-x] 。
来自 «https://www.luogu.org/problemnew/solution/P4782»
然后我就懵逼了，tarjan也可能跑出刚刚dfs跑出的顺序啊，那可能按题解所说的color[a]=1,color[b]=2,color[-x]=3,color[x]=4，欸好像x是false
但我也可以先tarjanx再到a再到b再到-x啊。。
我一开始还以为是他令x为i号点，-x为i+n号点，然后for1~2n跑tarjan规定顺序的原因
现在我甚至怀疑我可以hack
好的我去请教一下Ebola大佬
好的我想我知道我的思路错在哪里了
问题就在tarjan是在跑完某个点之后对这个点进行dfn[x]==low[x]的判断然后再加入scc（强连通分量）
所以tarjan对于x=>a=>b=>-x，假设先tarjan到a,应该是tarjan(a)->tarjan(b)->tarjan(-x),scc[-x]=1,scc[b]=2,scc[a]=3,再tarjan到x，scc[x]=4，所以可以发现无论先tarjan到x还是-x，scc里面都会存下拓扑的逆序
所以问题解决了，我们可以用scc来判断是x=>a=>b=>…=>-x还是-x=>c=>d=>…=>x
上代码
#include<bits/stdc++.h>
using namespace std;
const int N=1000005;
int n,m;
int sum,h[N<<1];
struct Edge{int v,nxt;}e[N<<1];
void adde(int x,int y)
{
sum++;
e[sum].v=y;
e[sum].nxt=h[x];
h[x]=sum;
}
int cnt,dfn[N<<1],low[N<<1];
int totscc,scc[N<<1];
stack<int> sta;
void tarjan(int x)
{
cnt++;
dfn[x]=low[x]=cnt;
sta.push(x);
for(int i=h[x];i;i=e[i].nxt)
{
int y=e[i].v;
if(!dfn[y])
{
tarjan(y);
low[x]=min(low[x],low[y]);
}
else if(!scc[y]) low[x]=min(low[x],dfn[y]);
}
if(dfn[x]==low[x])
{
int z;
totscc++;
do{
z=sta.top();
sta.pop();
scc[z]=totscc;
}while(z!=x);
}
}
int main()
{
scanf("%d%d",&n,&m);
int a,b,c,d;
for(int i=1;i<=m;i++)
{
scanf("%d%d%d%d",&a,&b,&c,&d);
adde(2*a-(!b),2*c-d);
adde(2*c-(!d),2*a-b);
}
for(int i=1;i<=2*n;i++)
if(!dfn[i])
tarjan(i);
for(int i=1;i<=n;i++)
if(scc[2*i-1]==scc[2*i])
{printf("IMPOSSIBLE\n");return 0;}
printf("POSSIBLE\n");
for(int i=1;i<=n;i++)
printf("%d ",scc[2*i-1]<scc[2*i]);
return 0;
}
本人太菜QAQ，如果有错误请指出哦QAQ
2019.5.1