2-SAT问题
国家队论文下载
1. 赵爽 2-sat解法浅析（pdf）
2. 伍昱 由对称性解2-sat问题(ppt)
SAT问题
先看什么是SAT问题。适定性（Satisfiability）问题
给定 $n$个还未赋值的布尔变量 $x_1…x_n$。
现在有 $m$ 个条件，每个条件的形式为$x_i为a或x_j为b或…$ ,每个条件都是满足一些限制，2-SAT就是每个条件都是二个限制就是2-SAT问题。只有2-SAT问题是多项式时间复杂度，其他的都是幂次方级时间复杂度。2-sat不仅仅是元素个数最多的集合含有2个元素，而是每个集合都含有2个元素，且这2个元素不允许同时取出。
2-SAT问题
这里总结下来有三种情况
-
$a || b \Leftrightarrow \neg a \to b \Leftrightarrow \neg b \to a$
-
$a \to b \Leftrightarrow \neg a || b$
-
$a \Leftrightarrow a || a \Leftrightarrow \neg a \to a $
模型一：两者（A，B）不能同时取($\neg(A || B)$)，那么选择了A就只能选择B’，选择了B就只能选择A’，连边A→B’，B→A’
模型二：两者（A，B）不能同时不取(A || B)(两个里面至少有一个是真的)，那么选择了A’就只能选择B，选择了B’就只能选择A，连边A’→B，B’→A
模型三：两者（A，B）要么都取，要么都不取，那么选择了A，就只能选择B，选择了B就只能选择A，选择了A’就只能选择B’，选择了B’就只能选择A’,连边A→B，B→A，A’→B’，B’→A’
模型四：两者（A，A’）必取A，那么连边A’→A ，如果时不能取A，那么连边A $\to$ A’
模板说明
我们将每个位置选取拆点，由于每个位置只会选0或1，那么我们把选0记作$x_i$,选1记作$y_i$,那么就拆分成为两倍的点。
当我们安装上述方式建图之后，可以使用tarjan强连联通分量算法，如果拆出的点$x_0,y_1$都在一个强连通分量中，那么我们认为无解，因为可以从$x_0$推出$y_0$也可以从$y_0$推出$x_0$，显然矛盾。如果一个元素拆成的两个点在同一个强连通分量里，即强连通分量编号相同，那么整个序列无解。
那么所有当拆出的两个点不在同一个强连通分量中时，方案我们取缩点后拓补后的点，就是$x_i$的拓补排序比$y_i$更靠后，就选取$x_i$，那么就是i选取0。Tarjan后同一元素拆点强连通分量编号小的点是合法点
如果一个元素拆成的两个点之间没有任何路径相连，即使是有向路径，那么这两点都可以成为合法点，这两点的分量编号不同，选小的即可。
有向无环图的情况下，合法点的拓扑序比非法点大。
上面的输出方案是随意输出一种即可，但是要是要求输出字典序最小的答案呢？也是很好解决的，dfs即可
点从$1 \to 2n$枚举，如果这个点能选，就将ta相连的点都选上，就将ta相连的点的相连的点都选上，就将…
如果某个点发生冲突了（对立点被选了），这个点就不能选，与ta相连的点不能选，与ta相连的点的相连点不能选，与ta…
这样最后被选中的点就是这字典序最小的解了，复杂度： $O(nm)$
const int N = 2e6 + 100 , M = N ;
int n,m ;
int h[N],e[M],ne[M],idx ;
int dfn[N],low[N],timestamp ; // tarjan求强连通分量的辅助数组
int stk[N],id[N],top,id_cnt;
bool ins[N] ;
void add(int a,int b){
e[idx] = b,ne[idx] = h[a],h[a] = idx ++ ;
}
void tarjan(int u){
dfn[u] = low[u] = ++ timestamp ; // 记录时间戳
stk[++top] = u ,ins[u] = 1 ; // 加入栈中
for(int i = h[u] ;~i ; i = ne[i]){
int j = e[i] ;
if(!dfn[j]){
tarjan(j) ;
low[u] = min(low[u],low[j]) ;
}
else if(ins[j]) low[u] = min(low[u],dfn[j]) ;
}
if(low[u] == dfn[u]){
int y ;
id_cnt ++ ;
do{
y = stk[top--],ins[y] = 0 ,id[y] = id_cnt ;
}while(y != u) ;
}
}
int main(){
scanf("%d%d",&n,&m) ;
memset(h,-1,sizeof h) ;
while(m--){
int i,j,a,b ;
scanf("%d%d%d%d",&i,&a,&j,&b) ;
i -- ,j -- ;
add(2 * i + !a,2 * j + b); // 将非a连接b
add(2 * j + !b,2 * i + a); // 将非b连接a
}
for(int i = 0 ; i < 2 * n ; i++){
if(!dfn[i])
tarjan(i) ;
}
for(int i = 0 ; i < n ; i ++){
if(id[2 * i] == id[2 * i + 1]){
puts("IMPOSSIBLE") ;
return 0 ;
}
}
puts("POSSIBLE") ;
for(int i = 0 ; i < n ; i++){
if(id[2 * i] < id[2 * i + 1]) printf("0 ") ;
else printf("1 ") ;
}
return 0;
}
优化建边
对一个集合进行处理，当题目要求这个集合只能选出一个点时候，优化思路是进行前缀和优化，就是再多建一些点，这些点是前缀和点，表示前面是否是1，这里我么用$\neg a$表示取0，$a$表示取1。那么我们思考有前缀的时候，这个点与前缀的关系，这里的单向箭头都指条件。
$$
\begin{eqnarray}
a_i \\
\downarrow \\
pre_{a_i-1} \to pre_{a_i} \\
\end{eqnarray}
$$
然后$a_i$与$pre_{a_i-1}$的关系是当$a_i$是1，那么$pre_{a_i-1}$是0（因为$a_i$这时候是1，代表之前没出现过1），当$pre_{a_i-1}$是1，那么$a_i$是0，(因为之前出现过1，那么这个就不能是1),所以最后就是 $a_i \to \neg pre_{a_i-1}和pre_{a_i-1} \to \neg a_i$
所以这里多建的边是$a_i \to pre_{a_i} ,\neg pre_{a_i} \to \neg a_i,pre_{a_i-1} \to pre_{a_i},\neg pre_{a_i} \to \neg pre_{a_i-1},和a_i \to \neg pre_{a_i-1}和pre_{a_i-1} \to \neg a_i$
2-SAT与二分的结合
感觉什么算法与二分结合都是结合在check函数这里，当发现问题的单调性之后，使用这种算法来进行check函数的检验。
poj2723那么这道题就是给了n对钥匙，选其中一个钥匙对应的钥匙就会消失，然后有m对门，每个门两个钥匙任意一个都可开启此门，门从上到下。由题目分析可得到，当可以开开i个门，那么一定可以开开i-1个门，那么说开门数量是具有单调性的，由于具有单调性，所以可以使用二分来解决。
typedef pair<int,int> pii ;
const int N = 4100 , M = 2 * N ;
// http://poj.org/problem?id=2723
// 由题目分析可得到，当可以开开i个门，那么一定可以开开i-1个门，那么说开门数量是具有单调性的
// 由于具有单调性，所以可以使用二分来解决
// 那么是二分的话，据需要写一个合适的检查函数
// 那么检查函数需要找到选前mid个门能否成立
// 那么这就转化为一个2-SAT问题，是否成立了。
// 每对钥匙a,b是选了 a -> !b ,b -> !a ;
// 每对门a,b是a || b, !a - > b,!b - > a;
int n,m ;
int h[N],e[M],ne[M],idx ;
int dfn[N],low[N],timestamp ;
int stk[N],id[N],top,id_cnt ;
bool ins[N] ;
pii key[N],q[N] ;
void init(){
idx = timestamp = id_cnt = 0 ;
memset(h,-1,sizeof h) ;
memset(dfn,0,sizeof dfn) ;
}
void add(int a,int b){
e[idx] = b,ne[idx] = h[a],h[a] = idx ++ ;
}
void tarjan(int u){
dfn[u] = low[u] = ++ timestamp ;
stk[++top] = u ,ins[u] = 1 ;
for(int i = h[u] ; ~ i ; i = ne[i]){
int j = e[i] ;
if(!dfn[j]){
tarjan(j) ;
low[u] = min(low[u],low[j]) ;
}
else if(ins[j]) low[u] = min(low[u],dfn[j]) ;
}
if(low[u] == dfn[u]){
int y ;
id_cnt ++ ;
do{
y =stk[top--],ins[y] = 0,id[y] = id_cnt ;
}while(y != u) ;
}
}
bool check(int m){
init() ;
for(int i = 0 ; i < n ; i++){
add(key[i].x,key[i].y + 2 * n),add(key[i].y ,key[i].x + 2 * n) ;
}
for(int i = 0 ; i < m; i++){
add(q[i].x + 2 * n,q[i].y),add(q[i].y + 2 * n,q[i].x) ;
}
for(int i = 0 ; i < 4 * n ; i++){
if(!dfn[i])
tarjan(i) ;
}
for(int i = 0 ; i < 2 * n ; i++){
if(id[i] == id[i + 2 * n]){
return 0 ;
}
}
return 1 ;
}
int main(){
while(scanf("%d%d",&n,&m),n || m){
for(int i = 0 ; i < n ; i ++) scanf("%d%d",&key[i].x,&key[i].y) ;
for(int i = 0 ; i < m ; i++) scanf("%d%d",&q[i].x,&q[i].y) ;
int l = 1 , r = m ;
while(l < r){
int mid = l + r + 1 >> 1 ;
if(check(mid)) l = mid ;
else r = mid - 1;
}
printf("%d\n",l) ;
}
return 0;
}
参考博客： 【研究总结】2-sat问题
2-SAT略解
2-SAT学习笔记
