（转）2-SAT小结
Posted enceladus-return0
tags:
篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了（转）2-SAT小结相关的知识，希望对你有一定的参考价值。
2-sat小结
原文作者：老K
原文传送门
2-sat是什么
一类问题是这样的：
（两个符号的意思 (lor or,land and)）
有n个布尔变量，现在对它们做出限制，比如(a_i=1,a_i lor a_j=1)，求一组可行的解。
假设限制元素最多的限制限制了k个元素，这个问题就被称为k-sat问题。
可以证明（然而我不会），(k>2)时是NPC的。
基础想法
把每个变量(a_i)拆成2个点(i_0,i_1)，表示它为1或0
每个变量就变成了一个集合。要求在每个集合里选一个元素，满足所有限制。
然后有向边(<u,v>)表示若选u则选v。
(a_i=1)型限制
连(<i_0,i_1>)。
(a_i=0)则反过来。
(a_i=a_j)限制
连(<i_0,j_0><j_0,i_0><i_1,j_1><j_1,i_1>)
(a_i ot=a_j)限制
连(<i_0,j_1><j_0,i_1><i_1,j_0><j_1,i_0>)
(a_ilor a_j=1)或者(a_iland a_j =0)限制
对于前者，连(<i_0,j_1><j_0,i_1>)
后者显然是交换0,1
(a_ilor a_j=0)或者(a_iland a_j =1) 限制
拆开，转化为(a_i=1)型限制
其实都很显然是吧。
算法1
有一个很显然的结论:设(u')表示u所在集合的另一个元素。
如果存在(<u,v>)则一定存在(<v',u'>)（对称性）
那么我们可以按照顺序枚举每一个布尔变量。
假设它是0，然后沿着单向边计算它影响的元素，如果没有问题就是0,并且计算它影响的元素的值。
否则假设它是1，如果没问题就是1，并且计算它影响元素的值。
否则无解。
由于对称性以及边是单向的，可以证明这个算法的正确性。（或者感性理解）
时间复杂度(O(nm))其中n是点数m是边数。
当然0,1的顺序是可以交换的。
这个算法可以求出字典序最小的解。
在算之前，按照每个变量0,1编号较小值从小到大排序。
然后枚举要先枚举每个变量编号较小的那个点。
算法2
有没有更快的算法呢？
当然是有的。
我们可以先tarjan 强连通分量缩点。
那么同一个强连通分量里，点的选择情况是一样的（选则都选，不选则都不选）。
由对称性可知如果(u,v)在同一个强连通分量里，那么(u',v')也在同一个强连通分量里。
如果(u,u')在同一个强连通分量里，那么无解。
否则考虑，缩完点后得到了一个DAG，由两个边相反的DAG组成。
我们可以通过拓扑排序，每次找一个没有出边的分量，如果它里面点的对称点没有被选择，那么执行如下操作：
选择它里面的所有点。
把它扔掉。（把所有到它的边断掉）
可以发现是对的。
时间复杂度(O(n+m))，通常用来计算可行解或者判断可行性。
算法3（黑科技）
不难发现，在缩完点后，如果u能到达v，那么在tarjan 中，u一定在v之后被找到。
于是我们可以在拓扑排序中，每次取能取的，编号最小的分量，
显然，如果一个分量(u)和分量(v)是对称的，那么如果(u<v)，会选择u，否则会选择v。
那么就不用重建图拓扑排序了。
常数优化/代码量优化效果还是很明显的。
例题
满汉全席
模板题。
NOI 2017 Day2T1 游戏
之所以用UOJ是因为ex test巨强无比。
发现有一些地图是X，3种都可以，但是个数不超过8.
我们可以把X转化为A或B。
枚举每个X转化为A还是B，跑2-SAT就可以了。
/*
Authlor: CNYALI_LK
LANG: C++
PROG: 317.cpp
Mail: [email protected]
*/
#include<bits/stdc++.h>
#define debug(...) fprintf(stderr,__VA_ARGS__)
#define DEBUG printf("Passing [%s] in LINE %d
",__FUNCTION__,__LINE__)
#define Debug debug("Passing [%s] in LINE %d
",__FUNCTION__,__LINE__)
#define all(x) x.begin(),x.end()
using namespace std;
const double eps=1e-8;
const double pi=acos(-1.0);
typedef long long ll;
typedef pair<int,int> pii;
template<class T>int chkmin(T &a,T b){return a>b?a=b,1:0;}
template<class T>int chkmax(T &a,T b){return a<b?a=b,1:0;}
template<class T>T sqr(T a){return a*a;}
template<class T>T mmin(T a,T b){return a<b?a:b;}
template<class T>T mmax(T a,T b){return a>b?a:b;}
template<class T>T aabs(T a){return a<0?-a:a;}
#define min mmin
#define max mmax
#define abs aabs
int read(){
int s=0,base=1;
char c;
while(!isdigit(c=getchar()))if(c=='-')base=-base;
while(isdigit(c)){s=s*10+(c^48);c=getchar();}
return s*base;
}
char rc(){
char c;
while(!isalpha(c=getchar()));
return c;
}
void rs(char *s){
while(!isalpha(*s=getchar()))++s;
while(isalpha(*s))*(++s)=getchar();
*s=0;
}
char WriteIntBuffer[1024];
template<class T>void write(T a,char end){
int cnt=0,fu=1;
if(a<0){putchar('-');fu=-1;}
do{WriteIntBuffer[++cnt]=fu*(a%10)+'0';a/=10;}while(a);
while(cnt){putchar(WriteIntBuffer[cnt]);--cnt;}
putchar(end);
}
struct _limit{
int a,b,ax,bx;
};
_limit a[102424];
char s[102424];
_limit limit(){
_limit x;
x.a=read()-1;
x.ax=rc();
x.b=read()-1;
x.bx=rc();
return x;
}
int h[102424];
int beg[102424],to[233333],lst[233333],dfn[102423],low[102423],no[102423];
int blocks,e,t;
void add(int u,int v){
to[++e]=v;
lst[e]=beg[u];
beg[u]=e;
}
int stk[102424],*top=stk;
void dfs(int x){
dfn[x]=low[x]=++t;
*(++top)=x;
flor(int i=beg[x];i;i=lst[i])
if(dfn[to[i]]){
if(!no[to[i]])
chkmin(low[x],dfn[to[i]]);
}else{
dfs(to[i]);
chkmin(low[x],low[to[i]]);
}
if(dfn[x]==low[x]){
++blocks;
do{
no[*(--top+1)]=blocks;
}while(*(top+1)!=x);
}
}
int main(){
#ifdef cnyali_lk
freopen("317.in","r",stdin);
freopen("317.out","w",stdout);
#endif
int n,d,m;
n=read();
d=read();
rs(s);
int xs=0;
flor(int i=0;i<n;++i){
if(s[i]=='x'){h[xs]=i;++xs;}
}
m=read();
flor(int i=1;i<=m;++i){
a[i]=limit();
}
int un=1<<d,u,v;
flor(int j=0;j<un;++j){
flor(int i=0;i<d;++i)s[h[i]]='a'+!!(j&(1<<i));
flor(int i=0;i<n+n;++i)beg[i]=dfn[i]=low[i]=no[i]=0;
blocks=e=t=0;
flor(int i=1;i<=m;++i){
if(a[i].ax-'A'==s[a[i].a]-'a')continue;
if(a[i].bx-'A'==s[a[i].b]-'a'){
int u=a[i].a*2+(a[i].ax-'A'-(a[i].ax-'A'>=s[a[i].a]-'a'));
add(u,u^1);
}
else{
int u=a[i].a*2+(a[i].ax-'A'-(a[i].ax-'A'>=s[a[i].a]-'a'));
int v=a[i].b*2+(a[i].bx-'A'-(a[i].bx-'A'>=s[a[i].b]-'a'));
add(u,v);
add(v^1,u^1);
}
}
flor(int i=0;i<n+n;++i)if(!dfn[i])dfs(i);
int ok=1;
flor(int i=0;i<n;++i)if(no[i<<1]==no[i<<1|1])ok=0;
if(ok){
flor(int i=0;i<n;++i){
int ans=(no[i<<1]>no[i<<1|1]);
ans+=(ans>=s[i]-'a');
putchar(ans+'A');
}
return 0;
}
}
printf("-1
");
return 0;
}
({Hugecolor{Gold}{老K太强了QAQ}})
以上是关于（转）2-SAT小结的主要内容，如果未能解决你的问题，请参考以下文章