2-SAT 问题
$\mathtt{SAT=Satisfiability}$
2-SAT 问题，就是求一类 在多个只有两个元素的集合里面选择元素，每个集合里面只能选一个，并满足给定的约束条件 的问题，处理这类约束条件的思路有点像 差分约束系统，即建立有向图来表示限制条件，这类问题的一般形式其实是 K-SAT 问题，即每个元素里面有 K 个元素，2-SAT 只是其中的一个情况
由于 2-SAT 问题不好系统地解释，下面用一个例题结合起来总结：
Description
某国有n个党派，每个党派在议会中恰有2个代表。现在要成立和平委员会 ，该委员会必须满足：
1、每个党派在和平委员会中有且只有一个代表 。
2、如果某两个代表不和，则他们不能都属于委员会 。
代表的编号从 1 到 2n，编号为 2a-1、2a 的代表属于第a个党派，求和平委员会是否能创立。若能，求一种构成方式。
PS：有n个组，第i个组里有两个节点Ai, Ai” 。需要从每个组中选出一个。而某些点不可以同时选出（称之为不相容）。任务是保证选出的n个点都能两两相容。这类型的问题我们称之为2-SAT问题。
第一行包含两个整数 n 和 m ，分别表示党派数量和 m 对不和的关系。 接下来 m 行每行两个整数 a,b，表示编号为 a 和 b 的代表不和
Output
如果能成立，则输出构成委员会的代表的编号，输出字典序最小的方案。如果不能成立，则输出”NIE”。
Sample Output
Hint
1≤n≤8000，0≤m ≤20000 。
例题分析
典型的模板题，每个党派是一个集合，两个代表是元素，只能选一个代表进入和平委员会而且还要保证避开代表的冲突关系，也就是不同集合元素间的约束关系，下面总结了两种方法解决 2-SAT 问题，分别是 强连通分量法 和 染色法
建立有向图（重点）
无论是 强连通分量法 还是 染色法 都要求在建好的有向图上进行操作，建立有向图的原则是 如果选择 $i$ 就必须选择 $j$，那么就连接 $i\to j$，以输入样例作为例子：
3 个集合分别是 ${1,\;2}$，${3\;4}$，${5,\;6}$，其中代表 1 和代表 3 冲突，那么意味着选择了 1 就只能选 4，这时连接 $1\to 4$，同理选了 3 就只能选 2，连接 $3\to 2$，代表 2 和 4 发生冲突就连接 $2\to 3$，$4\to 1$ 即可
强连通分量法
顾名思义，对这张有向图跑一个 Tarjan 或者 Kosaraju 跑完后所有的强连通分量里的点就是必选的点，由于一个集合里面只能选择一个代表，只要两个元素 $i_1,\;i_2$ 出现在同一个强连通分量里就说明矛盾，那么就是无解的情况
由于写过强连通分量的板子，就不再此放出代码了
染色法（重点）
枚举每个集合，从代表 1 出发，递归地把必选的点都染上颜色，如果染色过程中发现有有同一集合的两个元素都被染色就铁定是无解，这时需要把之前染过的色清除掉，并从代表 2 开始新的一轮染色，如果代表 2 也返回了无解的结果，才判定整张图是无解的状态
染色法的思路和二分图判定相似，但是要注意，每次判断局部无解时，一遇到染色失败的情况可以直接返回无解，但是染色成功时却不能直接返回有解（想想应该能明白……）
最后的选择方案就是所有染色点的编号，并且这是字典序最小的选择方案
例题代码
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
| #include <cstdio>
#include <cstring>
#include <queue>
#include <iostream>
#include <vector>
#include <cmath>
#include <algorithm>
#define maxn 8001*2
#define maxm 20001*4
int to[maxm],nxt[maxm],head[maxn];
int tot,n,m,other[maxn],stk[maxn];
bool color[maxn];
using namespace std;
template<typename t>inline void fcin(t &x){
int sign=1; x=0; char op=getchar();
while(op<'0'||op>'9'){if(op=='-') sign=-1;op=getchar();}
while(op>='0'&&op<='9'){x=x*10+(op-48);op=getchar();}
x*=sign;
}
inline void Eadd(int u,int v){
to[++tot]=v; nxt[tot]=head[u];
head[u]=tot;
}
bool DFS(int u){
if(color[u]) return true;
if(color[other[u]]) return false;
color[u]=1; stk[++stk[0]]=u;
for(int i=head[u];i;i=nxt[i])
if(!DFS(to[i])) return false;
return true;
}
bool twoSAT(){
for(int i=1;i<=n;i++){
if(color[2*i-1] && color[2*i]) continue;
stk[0]=0;
if(!DFS(2*i-1)){
while(stk[0]) color[stk[stk[0]]]=0,stk[0]--;
if(!DFS(2*i)) return false;
}
}
return true;
}
inline void init(){
fcin(n);fcin(m); int x,y;
for(int i=1;i<=2*n;i++){
if(i&1) other[i]=i+1;
else other[i]=i-1;
}
for(int i=1;i<=m;i++){
fcin(x);fcin(y);
Eadd(x,other[y]); Eadd(y,other[x]);
}
}
int main(){
#ifndef ONLINE_JUDGE
freopen("testin.txt","r",stdin);
freopen("testout.txt","w",stdout);
#endif
init();
if(!twoSAT()) printf("NIE");
else
for(int i=1;i<=2*n;i++) if(color[i]) printf("%d\n",i);
return 0;
}
|
Description
有n个布尔变量x1x_1x1~xnx_nxn，另有m个需要满足的条件，每个条件的形式都是“xi为true/false或xj为true/false”。比如“x1为真或x3为假”、“x7为假或x2为假”。2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足。
第一行两个整数n和m，意义如体面所述。
接下来m行每行4个整数 i a j b，表示“xi为a或xj为b”(a,b∈{0,1})
Output
如无解，输出“IMPOSSIBLE”（不带引号）; 否则输出”POSSIBLE”（不带引号),下
一行n个整数x1~xn（xi∈{0,1}），表示构造出的解。
Sample Output
1
2
3
4
| POSSIBLE
0 0 0
// ANOTHER POSSIBLE RESULT:
// 1 1 0
|
Hint
1<=n,m<=1e6 , 前3个点卡小错误，后面5个点卡效率，由于数据随机生成，可能会含有（ 10 0 10 0）之类的坑，但按照最常规写法的写的标程没有出错，各个数据点卡什么的提示在标程里。
分析
刚开始没看到 或 导致刚了半个小时出来全 WA……，一道 2-SAT 模板题，题意大致是给定 m 组条件，给 n 个变量赋值使得每组条件中至少一个得到满足，那么假设 条件1 已经不满足了，则必须满足条件2，反之亦然，于是对于样例 1 1 3 0 ，假设 $2i-1$ 和 $2i$ 分别表示第$i$ 个变量是 1 和 0 的情况，连接的有向边（必选边）就是 $4\to6$ 和 $5\to 1$
最后按照染色方案输出就可以了
Codes
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
| #include <cstdio>
#include <cstring>
#include <queue>
#include <iostream>
#include <vector>
#include <cmath>
#include <algorithm>
#define maxn 1000001*2
#define maxm 1000001*4
int to[maxm],nxt[maxm],head[maxn];
int tot,n,m,other[maxn],stk[maxn];
bool color[maxn];
using namespace std;
template<typename t>inline void fcin(t &x){
int sign=1; x=0; char op=getchar();
while(op<'0'||op>'9'){if(op=='-') sign=-1;op=getchar();}
while(op>='0'&&op<='9'){x=x*10+(op-48);op=getchar();}
x*=sign;
}
inline void Eadd(int u,int v){
to[++tot]=v; nxt[tot]=head[u];
head[u]=tot;
}
bool DFS(int u){
if(color[u]) return true;
if(color[other[u]]) return false;
color[u]=1; stk[++stk[0]]=u;
for(int i=head[u];i;i=nxt[i])
if(!DFS(to[i])) return false;
return true;
}
bool twoSAT(){
for(int i=1;i<=n;i++){
if(color[2*i-1] && color[2*i]) continue;
stk[0]=0;
if(!DFS(2*i-1)){
while(stk[0]) color[stk[stk[0]]]=0,stk[0]--;
if(!DFS(2*i)) return false;
}
}
return true;
}
inline void init(){
fcin(n);fcin(m); int x,y,z,w;
for(int i=1;i<=2*n;i++){
if(i&1) other[i]=i+1;
else other[i]=i-1;
}
for(int i=1;i<=m;i++){
fcin(x);fcin(y);fcin(z);fcin(w);
x=y?2*x-1:2*x; z=w?2*z-1:2*z;
Eadd(other[x],z); Eadd(other[z],x);
}
}
int main(){
#ifndef ONLINE_JUDGE
freopen("testin.txt","r",stdin);
freopen("testout.txt","w",stdout);
#endif
init();
if(!twoSAT()) printf("IMPOSSIBLE");
else{
printf("POSSIBLE\n");
for(int i=1;i<=n;i++)
if(color[2*i-1]) printf("1 ");
else printf("0 ");
}
return 0;
}
|
Description
给n对平面上的点，你可以在每对点中选择一个放置炸弹（不能同时都放），炸弹爆炸后所摧毁的区域是一个圆，且每个炸弹的摧毁区域的半径都一样。当然作为游戏者，你可以控制这个半径的大小。
现在请你确定这个半径的最大值，使得放完n个炸弹后，没有任何两个炸弹有重合的部分（注意相接不算相交）。
第一行一个整数n，表示有n对顶点。接下来的n行，第i行表示第i对顶点的横纵坐标。
Output
一个保留两位小数的实数，表示炸弹爆炸的半径的最大值。
Sample Output #1
Sample Output #2
Hint
2 <= n < 1000坐标为[-10000,10000]内的实数。
分析
做法：二分答案 + 2-SAT 验证可行性
二分半径 R 之后，每次都跑 2-SAT 来判断当前半径 R 是否可取，可取则缩小 R 的范围，不可取则扩大 R 的范围直到 L 和 R 的差值可以忽略
建图的时候，考虑每两组之间的约束关系，用 A1，A2，B1，B2 表示两组中的四个炸弹，如果 A1 和 B1 爆炸范围相交（超过 $2\times R$）则只能选 B2，连接 $A_1\to B_2$，如果 A1 和 B2 爆炸范围相交则连接 $A_1 \to B_1$ 以此类推判断四次加边与否 就可以用 染色大法 尽情的 2-SAT 了
这道题起初较的时候 TLE 了，看到同学们都是 990ms+ 卡着时限过的，以为又是一道费优化的题目，然后做了一个小优化，把两点之间的距离存进二维数组就不用每次都去算一遍
抱着能过就行的心态点了 Submit，结果跑了 272ms ??? 数组这么快的吗？？
Codes
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
| #include <cstdio>
#include <cstring>
#include <queue>
#include <iostream>
#include <vector>
#include <cmath>
#include <algorithm>
#define maxn 1001*4
#define maxm 1001*1001*4
#define INF 1e-7
int to[maxm],nxt[maxm],head[maxn];
int tot,n,m,other[maxn],stk[maxn];
bool color[maxn];
double dists[2002][2002];
using namespace std;
template<typename t>inline void fcin(t &x){
int sign=1; x=0; char op=getchar();
while(op<'0'||op>'9'){if(op=='-') sign=-1;op=getchar();}
while(op>='0'&&op<='9'){x=x*10+(op-48);op=getchar();}
x*=sign;
}
struct node{
int x,y;
inline void init(){fcin(x);fcin(y);}
double operator -(const node &obj)const
{return sqrt(pow(fabs((double)x-obj.x),2)+pow(fabs((double)y-obj.y),2));}
}b1[maxn],b2[maxn];
inline void Eadd(int u,int v){
to[++tot]=v; nxt[tot]=head[u];
head[u]=tot;
}
bool DFS(int u){
if(color[u]) return true;
if(color[other[u]]) return false;
color[u]=1; stk[++stk[0]]=u;
for(int i=head[u];i;i=nxt[i])
if(!DFS(to[i])) return false;
return true;
}
bool twoSAT(){
for(int i=1;i<=n;i++){
if(color[2*i-1] && color[2*i]) continue;
stk[0]=0;
if(!DFS(2*i-1)){
while(stk[0]) color[stk[stk[0]]]=0,stk[0]--;
if(!DFS(2*i)) return false;
}
}
return true;
}
inline void init(){
fcin(n);
for(int i=1;i<=2*n;i++){
if(i&1) other[i]=i+1;
else other[i]=i-1;
}
for(int i=1;i<=n;i++)
b1[i].init(),b2[i].init();
for(int i=1;i<=n;i++)
for(int j=i+1;j<=n;j++)
dists[i][j]=dists[j][i]=b1[i]-b1[j],
dists[i][j+n]=dists[j+n][i]=b1[i]-b2[j],
dists[i+n][j]=dists[j][i+n]=b2[i]-b1[j],
dists[i+n][j+n]=dists[j+n][i+n]=b2[i]-b2[j];
}
inline void cls(){
memset(head,0,sizeof(head));tot=0;
memset(color,false,sizeof(color));stk[0]=0;
}
double solve(){
double L=0.0,R=1000000.0,ans=0.0,mid;
while(R-L>INF){
cls(); mid=(L+R)/2.0;
for(int i=1;i<=n;i++)
for(int j=i+1;j<=n;j++){
if(dists[i][j]<2*mid) Eadd(2*i-1,2*j),Eadd(2*j-1,2*i);
if(dists[i][j+n]<2*mid) Eadd(2*i-1,2*j-1),Eadd(2*j,2*i);
if(dists[i+n][j]<2*mid) Eadd(2*i,2*j),Eadd(2*j-1,2*i-1);
if(dists[i+n][j+n]<2*mid) Eadd(2*i,2*j-1),Eadd(2*j,2*i-1);
}
if(twoSAT()) ans=max(ans,mid),L=mid;
else R=mid;
} return ans;
}
int main(){
#ifndef ONLINE_JUDGE
freopen("testin.txt","r",stdin);
freopen("testout.txt","w",stdout);
#endif
init();
printf("%.2lf",solve());
return 0;
}
|
