问题描述
SAT(satisfiabality) 是适应性的缩写，一般称 k 的适应性问题为
k-SAT。适应性问题指有 \(n\) 个布尔变量
\(\{x_i\}\)，加入一些限制然后求限制内的解的问题。
因为 \(k>2\) 的 k-SAT 问题是 NP
完全问题（没有一定的算法和正解），我们只讨论 2-SAT 问题。
Tarjan
一般来讲，我们会想到把变量 \(x_i\)
的两种状态（比如选和不选，记为 \(x_{i0},x_{i1}\)）抽象成两个点，将限制条件转化为有向边，然后通过求强联通分量求解。连边
\(a\rightarrow b\) 表示条件为满足 \(a\) 必须满足 \(b\)。
如果有条件 \(a_0\rightarrow
b_0\)，\(b_0\rightarrow
a_1\)，\(a_1\rightarrow
b_1\)，\(b_1\rightarrow
a_0\)，我们把它想成一个图进行连边，发现 \(a_0\) 和 \(a_1\)
在同一个强联通分量里。也就是说要符合条件必须同时选 \(a_0,a_1\)，即 \(a\)
变量同时选且不选，这显然是不可能的，所以本例无解。
那么我们就可以得到普遍解法，即求强联通分量：若存在一个元素的两种状态在同一个强联通分量里，此题无解；否则有解。
得到一个解的方法为：选一个未被确定的变量，可随便指定其为一个状态，将所有与之相连的变量状态确定，重复此过程直到所有变量都确定。
模版
P4782洛谷模板
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
| #include<iostream>
#include<cstdio>
#include<cstring>
#include<vector>
#include<algorithm>
#include<stack>
using namespace std;
inline int read()
{
int x=0,w=0;char c=getchar();
while(!isdigit(c))w|=c=='-',c=getchar();
while(isdigit(c))x=(x<<3)+(x<<1)+(c^48),c=getchar();
return w?-x:x;
}
const int maxn=2e6+10;
int n,m;
int ecnt,dfn[maxn],low[maxn],head[maxn],to[maxn],nxt[maxn],cnt,_n,belong[maxn];
vector<int> g[maxn];
stack <int> st;
bool vis[maxn];
void tarjan(int x)
{
dfn[x]=low[x]=++cnt;
st.push(x);vis[x]=1;
for (int i=0;i<g[x].size();i++)
{
int u=g[x][i];
if(!dfn[u])
{
tarjan(u);
low[x]=min(low[x],low[u]);
}else if(vis[u])
low[x]=min(low[x],dfn[u]);
}
if(low[x]==dfn[x])
{
++_n;
do{
belong[x]=_n;
x=st.top();st.pop();
vis[x]=0;
}while(dfn[x]!=low[x]);
}
}
int main()
{
n=read(),m=read();
for(int x,y,x1,y1,i=1;i<=m;i++)
{
x=read(),x1=read(),y=read(),y1=read();
g[x+n*x1].push_back(y+n*(y1^1));
g[y+n*y1].push_back(x+n*(x1^1));
}
for(int i=1;i<=(n<<1);i++)
if(!dfn[i])tarjan(i);
for(int i=1;i<=n;i++)
if(belong[i]==belong[i+n]){
printf("IMPOSSIBLE\n");
return 0;
}
printf("POSSIBLE\n");
for(int i=1;i<=n;i++)
printf("%d ",belong[i]<belong[i+n]);
printf("\n");
return 0;
}
|
例题
洛谷P5782
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
| #include<iostream>
#include<cstdio>
#include<vector>
#include<cstring>
#include<algorithm>
using namespace std;
const int maxn=10005;
int n,m;
vector<int> g[maxn*2];
bool mark[maxn*2];
int sta[maxn*2],top;
bool dfs(int x)
{
if(mark[x^1])return false;
if(mark[x])return true;
mark[x]=1;
sta[top++]=x;
for(int i=0;i<g[x].size();i++)
if(!dfs(g[x][i]))return false;
return true;
}
inline bool TwoSAT()
{
memset(mark,0,sizeof mark);
for(int i=0;i<n;i+=2){
if(!mark[i] and !mark[i^1]){
top=0;
if(!dfs(i))
{
while(top)mark[sta[--top]]=0;
if(!dfs(i^1))return false;
}
}
}
return true;
}
int main()
{
int u,v;
scanf("%d%d",&n,&m);
n*=2;
for(int i=0;i<m;i++){
scanf("%d%d",&u,&v);
u--,v--;
g[u].push_back(v^1);
g[v].push_back(u^1);
}
if(TwoSAT()){
for(int i=0;i<n;i+=2)
if(mark[i])printf("%d\n",i+1);
else printf("%d\n",(i^1)+1);
}else printf("NIE\n");
return 0;
}
|
