SAT问题的定义
SAT是Satisfiability（可满足性）的缩写，而k-SAT问题就是说你有(n)个未知的bool变量(a_i)，有(m)个对这些变量的限制，每个限制有(k)个元素，设每个元素为(x)，要求 (x)或(
eg x) 的 (lor)（或）或者(land)（和）的值（如3-SAT中，形如(a or b or !c) 或 a and !b and !c 的条件）为true，或定义某一个未知数为true/false的一种解法。
很容易想到(O(2^nm))暴力做法，即枚举每一个bool未知数的值，判断是否合法。而对于(k geq 3)而言的k-SAT已经被证明是NP完全问题（即没有多项式复杂度的问题），而我们研究的2-SAT则有一个多项式解法。
2-SAT问题的解法
定义对于任何一个单字母bool变量(a)为true。
我们通过建一些特殊的图来实现：我们令编号从(1)到(n)的点为未知变量(a_i)取true的情况，(n+1)到(2 imes n)的点为(a_i)取false的情况。连边方面，我们令从(a)连向(b)表示由(a)能推到(b)，则(aland b)可以变为(a
ightarrow b, b
ightarrow a)，即由(a)为真可以推出(b)为真，由(b)为真可以推出(a)为真；(a lor b)可以变为(
eg a
ightarrow b,
eg b
ightarrow a)，即若(a)为假则(b)为真；(a = x (xin { true, false}))可以变为(
eg a
ightarrow a)，这个我们之后再说为什么，先当这种情况不存在。可以发现所有情况都可以化为刚才三种情况之一。
然后我们对于这样一个特殊的图跑一边强连通分量，如果存在( eg a)和(a)只有同存在于同一个强连通分量中，则一定无解，因为这一意味着你可以从( eg a)推到(a)，而很明显这是矛盾的。
于是我们得到了一张拓扑图。有一个性质，就是在有解的情况下，一个未知数的两个取值是有前后推导关系的，也就是一个取值直接或间接的指向了另一个取值时，我们取后者是一定有解的。实际实现上，输出的时候，输出对于每一个点拆除的true和false中，拓扑序较大的那一个，则一定有一个解。然而由于我们跑了Tarjan，那么我们可以附带着求一个反向的拓扑序，那么这就拓扑序也求得了。
从刚才这一角度来说，对于刚才建图中的第三种情况，我们连( eg a ightarrow a)可以让(a)的拓扑序必定大于( eg a)，即最后输出的时候一定会输出开始时给它的定义。
很明显复杂度瓶颈在Tarjan跑强连通分量上，其复杂度为(O(n+m))，所以总复杂度为(O(n+m))
例题
例题1 P4782 【模板】2-SAT 问题
一道模板题，甚至连赋值操作都没有。可以看到这里输入的时候用了一些小技巧来压了一下输入的行，其他就没什么难以理解的了。
#include <iostream>
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <vector>
namespace ztd{
using namespace std;
typedef long long ll;
const int mod = 998244353;
const int inf = 2147483647;
template<typename T> inline T read(T& t) {//fast read
t=0;short f=1;char ch=getchar();double d = 0.1;
while (ch<'0'||ch>'9') {if (ch=='-') f=-f;ch=getchar();}
while (ch>='0'&&ch<='9') t=t*10+ch-'0',ch=getchar();
if(ch=='.'){ch=getchar();while(ch<='9'&&ch>='0') t+=d*(ch^48),d*=0.1,ch=getchar();}
t*=f;
return t;
}
}
using namespace ztd;
const int maxn = 2e6+7, maxm = 2e6+7;
int n, m;
int last[maxn], ecnt;
struct edge{int y, gg;}e[maxm];
inline void addedge(int x, int y){
e[++ecnt] = {y, last[x]};
last[x] = ecnt;
}
int dfn[maxn], low[maxn], pcnt, st[maxn], top, gang[maxn], gtot;
bool instack[maxn];
void Tarjan(int x){
dfn[x] = low[x] = ++pcnt;
st[++top] = x; instack[x] = 1;
for(int i = last[x], y = e[i].y; i; i = e[i].gg, y = e[i].y){
if(!dfn[y]){
Tarjan(y);
low[x] = min(low[x], low[y]);
}else if(instack[y]) low[x] = min(low[x], dfn[y]);
}
if(low[x] == dfn[x]){
int now; ++gtot;
do{
now = st[top--]; instack[now] = 0;
gang[now] = (gtot);
}while(now ^ x);
}
}
int main(){
read(n); read(m);
int xx, yy, hmx, hmy;
for(int i = 1; i <= m; ++i){
read(xx); read(hmx); read(yy); read(hmy);
addedge(xx+(1-hmx)*n, yy+hmy*n);
addedge(yy+(1-hmy)*n, xx+hmx*n);
}
for(int i = 1; i <= n*2; ++i) if(!dfn[i]) Tarjan(i);
for(int i = 1; i <= n; ++i){
if(gang[i] == gang[i+n]){
puts("IMPOSSIBLE");
return 0;
}
}
puts("POSSIBLE");
for(int i = 1; i <= n; ++i){
cout << ((int)(gang[i] > gang[i+n])) << " ";
}
cout << '
';
return 0;
}
例题2 P4171 [JSOI2010]满汉全席
同样也是一道模板题。
#include <iostream>
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <vector>
namespace ztd{
using namespace std;
typedef long long ll;
const int mod = 998244353;
const int inf = 2147483647;
template<typename T> inline T read(T& t) {//fast read
t=0;short f=1;char ch=getchar();double d = 0.1; short hm=-1;
while (ch<'0'||ch>'9') {if (ch=='-') f=-f; if(ch=='h')hm=1; if(ch=='m')hm=0; ch=getchar();}
while (ch>='0'&&ch<='9') t=t*10+ch-'0',ch=getchar();
if(ch=='.'){ch=getchar();while(ch<='9'&&ch>='0') t+=d*(ch^48),d*=0.1,ch=getchar();}
t*=f;
return hm;
}
}
using namespace ztd;
const int maxn = 407, maxm = 4007;
int n, m, Eastward_Red_Sun_Rise_up_China_got_with_a_LKY;
int last[maxn], ecnt;
struct edge{int y, gg;}e[maxm];
inline void addedge(int x, int y){
e[++ecnt] = {y, last[x]};
last[x] = ecnt;
}
int dfn[maxn], low[maxn], pcnt, st[maxn], top, gang[maxn], gtot;
bool instack[maxn];
void Tarjan(int x, int fa){
dfn[x] = low[x] = ++pcnt;
st[++top] = x; instack[x] = 1;
for(int i = last[x], y = e[i].y; i; i = e[i].gg, y = e[i].y){
if(!dfn[y]){
Tarjan(y,x);
low[x] = min(low[x], low[y]);
}else if(instack[y]) low[x] = min(low[x], dfn[y]);
}
if(low[x] == dfn[x]){
int now; ++gtot;
do{
now = st[top--]; instack[now] = 0;
gang[now] = (gtot);
}while(now ^ x);
}
}
inline void init(){
n = m = gtot = top = pcnt = ecnt = 0;
memset(last, 0, sizeof(last));
memset(dfn, 0, sizeof(dfn));
memset(gang, 0, sizeof(gang));
memset(low, 0, sizeof(low));
memset(instack, 0, sizeof(instack));
}
inline void Main(){
init();
read(n); read(m);
int xx, yy, hmx, hmy;
for(int i = 1; i <= m; ++i){
hmx = read(xx); hmy = read(yy);
addedge(xx+(1-hmx)*n, yy+hmy*n);
addedge(yy+(1-hmy)*n, xx+hmx*n);
}
for(int i = 1; i <= n*2; ++i) if(!dfn[i]) Tarjan(i, -1);
for(int i = 1; i <= n; ++i){
if(gang[i] == gang[i+n]){
puts("BAD");
return;
}
}
puts("GOOD");
}
int main(){
// freopen("P4171_1.in","r",stdin);
int T; read(T);
while(T--) Main();
return 0;
}
例题3 P3825 [NOI2017]游戏
这道题中在不考虑 三个都可以选的地图 的情况下，也是一道2-SAT模板题：对于每一个输入(i h_i j h_j)，令(x = [ ext{第i个位置能不能选}h_i])，(y = [ ext{第j个位置能不能选}h_j])，依次考虑：
- 若(x)为
false，则关系不可能成立，continue即可； - 若(y)为
false，则(x)为假，连(x ightarrow eg x)； - 否则则连(x ightarrow y, eg x ightarrow eg y)
然后就是常规的2-SAT了。
我们再考虑进去 三个都可以选的地图(x)， 我们可以暴力枚举每一个(x)不能选哪一个，则复杂度为(O((n+m)3^n))，过不了。考虑优化。我们想到我们只要正确的(x)的解存在于我们考虑过的集合就可以这个性质，所以说当我们令(x)为(A)和(B)的时候，他能选的集合就已经为({a,b,c})三种所有的可能了，则时间复杂度优化到(O((n+m)2^n))了，可过。
#include <iostream>
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <vector>
namespace ztd{
using namespace std;
typedef long long ll;
const int mod = 998244353;
const int inf = 2147483647;
template<typename T> inline T read(T& t) {//fast read
t=0;short f=1;char ch=getchar();double d = 0.1;
while (ch<'0'||ch>'9') {if (ch=='-') f=-f;ch=getchar();}
while (ch>='0'&&ch<='9') t=t*10+ch-'0',ch=getchar();
if(ch=='.'){ch=getchar();while(ch<='9'&&ch>='0') t+=d*(ch^48),d*=0.1,ch=getchar();}
t*=f;
return t;
}
}
using namespace ztd;
const int maxn = 1e5+7, maxm = 4e5+7;
int n, m, d, Dongfang_hong, Taiyang_Sheng, Zhongguo_Chulege_LKY, X[maxn], a1[maxm], b1[maxm];
char s[maxn], a2[maxm], b2[maxm];
int last[maxn], ecnt;
struct edge{int y, gg;}e[maxm];
inline void addedge(int x, int y){
e[++ecnt] = {y, last[x]};
last[x] = ecnt;
}
int dfn[maxn], low[maxn], pcnt, st[maxn], top, gang[maxn], gtot;
bool instack[maxn];
void Tarjan(int x){
dfn[x] = low[x] = ++pcnt;
st[++top] = x; instack[x] = 1;
for(int i = last[x], y = e[i].y; i; i = e[i].gg, y = e[i].y){
if(!dfn[y]){
Tarjan(y);
low[x] = min(low[x], low[y]);
}else if(instack[y]) low[x] = min(low[x], dfn[y]);
}
if(low[x] == dfn[x]){
int now; ++gtot;
do{
now = st[top--]; instack[now] = 0;
gang[now] = (gtot);
}while(now ^ x);
}
}
inline void init(){
ecnt = pcnt = top = 0;
memset(dfn, 0, sizeof(dfn));
memset(low, 0, sizeof(low));
memset(gang, 0, sizeof(gang));
memset(instack, 0, sizeof(instack));
memset(last, 0, sizeof(last));
}
char sol[maxn];
inline bool check(){
for(int i = 1; i <= n*2; ++i) if(!dfn[i]) Tarjan(i);
for(int i = 1; i <= n; ++i){
if(gang[i] == gang[i+n]) return 0;
else if(gang[i] < gang[i+n]) sol[i] = ((s[i] == 'A') ? 'B' : 'A');
else sol[i] = ((s[i] == 'C') ? 'B' : 'C');
}
for(int i = 1; i <= n; ++i) cout << sol[i];
return 1;
}
inline bool work(){
init();
for(int i = 1; i <= m; ++i){
if(a2[i] == s[a1[i]]) continue;
if(b2[i] == s[b1[i]]){
if(a2[i] == 'C' || (a2[i] == 'B' && s[a1[i]] == 'C')) addedge(a1[i]+n, a1[i]);
else addedge(a1[i], a1[i]+n);
continue;
}
int add1, add2;
if(a2[i] == 'C' || (a2[i] == 'B' && s[a1[i]] == 'C')) add1 = n; else add1 = 0;
if(b2[i] == 'C' || (b2[i] == 'B' && s[b1[i]] == 'C')) add2 = n; else add2 = 0;
addedge(a1[i]+add1, b1[i]+add2); addedge( b1[i]-add2+n, a1[i]-add1+n);
}
return check();
}
void dfs(int x){
if(x == d+1){
if(work()) exit(0);
else return;
}
s[X[x]] = 'A'; dfs(x+1);
s[X[x]] = 'B'; dfs(x+1);
}
int main(){
read(n); read(Zhongguo_Chulege_LKY); scanf("%s", s+1); read(m);
for(int i = 1; i <= n; ++i) s[i] -= ('a'-'A');
for(int i = 1; i <= n; ++i) if(s[i] == 'X') X[++d] = i;
for(int i = 1; i <= m; ++i) scanf("%d %c %d %c",&a1[i], &a2[i], &b1[i], &b2[i]);
dfs(1);
puts("-1");
return 0;
}