2 – SAT
2 – SAT 就是2判定性问题,是一种特殊的逻辑判定问题。
例,n对东西,每对只能选一个(i0或i1),不能不选。即:A or _A = 1 , A xor _A = 1
还存在一些约束关系(i0,j0),表示i0不能跟j0一起选。那需连边
i0-> j1 如果选i0的话必须选j1
j0-> i1如果选j0的话必须选i1
表示了一种递推的关系:选哪个必选哪一个
一般题目给的都是一对一对的东西,二选一,不能不选。本身那几对东西是没有关系的,然后题目会定义一些规则,或者我们自己加入条件(如二分的参数),使对与对之间有了一些约束关系: 1)选a必选b a->b
2)a必选 _a->a
对这个新图求SCC,同一SCC的要么全选,要么都不选。
如果发现a,_a在同一SCC,表明矛盾了。
不矛盾的话,对缩点后的图按照自底向上选择一个还未被标记的点,标记选上,然后把它的对立点及其前代都删除。
(选择一个点要把它及其所有后代都选上。不选一个点,要把它及其前代都不选。)
算法流程:
1、建图,求SCC。若某一个点,a与_a在同一个SCC,则无解,退出;
2、对求得的缩点,用原来的反图建一个DAG;
3、TopoSort得到一个原图的自底向上的序列,点是缩点后的SCC,没必要原来的每个点;
4、从左往右,对整个序列的点,如果未标记删除,就标记选它,同时把这个SCC里的所有原来的点的对立点及其各自的后代(因为是反图)都标记删除;
5、重复上面过程,最后被标记选上的SCC内的点都是选择的点。其个数=n
虽然被删除的点也是n个,但是他们可能会存在冲突关系。而标记选上的点间是相容的。
挺多用二分的。对于二分设定的参数,可能建图时要考虑这个条件,如POJ 2749
 /**//*
POJ 2749 Building roads
题意:给出n个牛棚、两个特殊点S1,S2的坐标。S1、S2直连。牛棚只能连S1或S2
还有,某些牛棚只能连在同一个S,某些牛棚不能连在同一个S
求使最长的牛棚间距离最小 距离是曼哈顿距离
使最大值最小,二分的经典应用
二分枚举最大值limit,然后重新构图,用2-SAT判定可行性
用布尔变量Xi表示第i个牛棚连到S1,~Xi表示连到S2
检查每一个约束条件,构图:
1.hate关系的i,j Xi->~Xj ~Xi->Xj Xj->~Xi ~Xj->Xi
2.friend关系的i,j Xi->Xj ~Xi->~Xj Xj->Xi ~Xj->~Xi
接下来的也要检查,因为引入参数,就是多了约束条件了
这四种情况就是i,j到达对方的所有情况了
3.dist(i,S1)+dist(S1,j)>limit Xi->~Xj Xj->Xi
4.dist(i,S2)+dist(S2,j)>limit ~Xi->Xj ~Xj->Xi
5.dist(i,S1)+dist(S1,S2)+dist(S2,j)>limit Xi->Xj ~Xj->~Xi
5.dist(i,S2)+dist(S2,S1)+dist(S1,j)>limit ~Xi->~Xj Xj->Xi
然后求SCC 判断Xi与~Xi是否在同一个SCC中,是的话就有矛盾
*/
#include<cstdio>
#include<cstring>
#include<algorithm>
#include<vector>
using namespace std;
const int MAXN = 500;
const int INF = 1000000000;
int N,A,B;
struct Two
  {
int x,y;
};
Two pt[MAXN+10],s1,s2;
Two fre[MAXN*2+10],hate[MAXN*2+10];
struct Graph
  {
vector<int>G[2*MAXN+10],_G[2*MAXN+10];
int ID[MAXN*2+10],ord[MAXN*2+10];
int SCC;
void init(int n)
 {
for(int i=1;i<=n;i++)
 {
G[i].clear();
_G[i].clear();
}
}
void add(int a,int b)
 {
G[a].push_back(b);
_G[b].push_back(a);
}
void dfs1(int u)
 {
ID[u]=1;
for(int i=0,size=_G[u].size();i<size;i++)
 {
int v=_G[u][i];
if(!ID[v])dfs1(v);
}
ord[++SCC]=u;
}
void dfs2(int u)
 {
ID[u]=SCC;
for(int i=0,size=G[u].size();i<size;i++)
 {
int v=G[u][i];
if(!ID[v])dfs2(v);
}
}
void kosaraju()
 {
memset(ID,0,sizeof(ID));
SCC=0;
for(int i=1;i<=2*N;i++)
 {
if(!ID[i])dfs1(i);
}
memset(ID,0,sizeof(ID));
SCC=0;
for(int i=2*N;i;i--)
 {
if(!ID[ord[i]])
 {
SCC++;
dfs2(ord[i]);//
}
}
}

}graph;
inline int dist(Two &a,Two &b)
  {
return abs(a.x-b.x)+abs(a.y-b.y);
}
bool chk(int limit)
  {
graph.init(2*N);
//build
for(int i=1;i<N;i++)
for(int j=i+1;j<=N;j++)
 {
//dist(i,s1)+dist(j,s1)>L i0->j1 j0->i1
if(dist(pt[i],s1)+dist(pt[j],s1)>limit)
 {
graph.add(i,j+N);
graph.add(j,i+N);
}
//dist(i,s2)+dist(j,s2)>L i1->j0 j1->i0
if(dist(pt[i],s2)+dist(pt[j],s2)>limit)
 {
graph.add(i+N,j);
graph.add(j+N,i);
}
//dist(i,s1)+dist(s1,s2)+dist(s2,j)>L i0->j0 j1->i1
if(dist(pt[i],s1)+dist(s1,s2)+dist(s2,pt[j])>limit)
 {
graph.add(i,j);
graph.add(j+N,i+N);
}
//dist(i,s2)+dist(s2,s1)+dist(s1,j)>L i1->j1 j0->i0
if(dist(pt[i],s2)+dist(s2,s1)+dist(s1,pt[j])>limit)
 {
graph.add(i+N,j+N);
graph.add(j,i);
}
}
for(int i=1;i<=A;i++)
 {
//i0->j1,i1->j0,j0->i1,j1->i0
graph.add(hate[i].x,hate[i].y+N);
graph.add(hate[i].x+N,hate[i].y);
graph.add(hate[i].y,hate[i].x+N);
graph.add(hate[i].y+N,hate[i].x);
}
for(int i=1;i<=B;i++)
 {
//i0->j0,i1->j1,j0->i0,j1->i1
graph.add(fre[i].x,fre[i].y);
graph.add(fre[i].x+N,fre[i].y+N);
graph.add(fre[i].y,fre[i].x);
graph.add(fre[i].y+N,fre[i].x+N);
}
graph.kosaraju();
for(int i=1;i<=N;i++)
 {
if(graph.ID[i]==graph.ID[i+N])return false;
}
return true;
}
int main()
  {
int Max;
while(~scanf("%d%d%d",&N,&A,&B))
 {
scanf("%d%d%d%d",&s1.x,&s1.y,&s2.x,&s2.y);
//Max = 0;
for(int i=1;i<=N;i++)
 {
scanf("%d%d",&pt[i].x,&pt[i].y);
//Max = max(Max,dist(pt[i],s1));
//Max = max(Max,dist(pt[i],s2));
}
//Max = 2*Max+dist(s1,s2)+1;
for(int i=1;i<=A;i++)
scanf("%d%d",&hate[i].x,&hate[i].y);
for(int i=1;i<=B;i++)
scanf("%d%d",&fre[i].x,&fre[i].y);

int left = 0,right = INF;
while(right-left>1)
 {
int mid = (right+left)>>1;
if(chk(mid))right=mid;
else left=mid;
}
if(right==INF)puts("-1");
else printf("%d\n",right);
}
return 0;
}

 /**//*
POJ 2723 Get Luffy Out
题意:给出N对钥匙,一对钥匙只能用一个 M个门,每个门上2个值,只要有其中一个值的钥匙即可开门了,问最大能开的门,门得按顺序开。
既然是按顺序开,就可以二分枚举能开的门的个数
然后用2-SAT判可行性
建图方法为,对于门上的两个值a,b 显然有_a->b,_b->a
*/

 /**//*
POJ 3678 Katu Puzzle
6个逻辑表达式,建图用
a AND b = 1 <==> _a->a _b->b
a AND b = 0 <==> a->_b b->_a
a OR b = 1 <==> _a->b _b->a
a OR b = 0 <==> a->_a b->_b
a XOR b = 1 <==> _a->b a->_b _b->a b->_a
a XOR b = 0 <==> a->b _a->_b b->a _b->_a
其实记住三个就够了,另外三个就两边取反就可以了
*/

 /**//*
POJ 3648 Wedding
题意:n对夫妻,夫妻不能坐在同一排。m种通奸关系,有通奸关系的a,b不能同时坐在新娘的对面一排,求方案
以新娘为参考系,x表示坐在新娘一侧,_x表示坐在对面一侧
有通奸关系的a,b 有_a->b _b->a
最后!新娘一定要选上,所以连0h->0w 这样子连,拓扑排序后自底向上肯定会选上新娘
缩点建图后再拓扑排序
select的过程,遇到没有标记的块就选上它,并把它内所有点的对立点及其前代都标记删除
最后删除掉的肯定是n个
这里对反图建图,所以直接拓扑排序就可以自底向上了
*/
#include<cstdio>
#include<cstring>
#include<vector>
#include<queue>
using namespace std;
const int MAXN = 1000;
struct Graph
  {
vector<int>G[MAXN*2+10],_G[MAXN*2+10];
vector<int>Dag[MAXN*2+10],inDag[MAXN*2+10];
int n,SCC;
int ID[MAXN*2+10],ord[MAXN*2+10];
int in[MAXN*2+10],pos[MAXN*2+10];
int color[MAXN*2+10];
void init(int nn)
 {
n=nn;
for(int i=0;i<2*n;i++)
 {
G[i].clear();
_G[i].clear();
}
}
void add(int u,int v)
 {
G[u].push_back(v);
_G[v].push_back(u);
}
void dfs1(int u)
 {
ID[u]=1;
for(int i=0,size=_G[u].size();i<size;i++)
 {
int v=_G[u][i];
if(ID[v]==-1)dfs1(v);
}
ord[SCC++]=u;
}
void dfs2(int u)
 {
ID[u]=SCC;
for(int i=0,size=G[u].size();i<size;i++)
 {
int v=G[u][i];
if(ID[v]==-1)dfs2(v);
}
}
void kosaraju()
 {
SCC = 0;
memset(ID,-1,sizeof(ID));
for(int i=0;i<2*n;i++)
if(ID[i]==-1)dfs1(i);
SCC = 0;
memset(ID,-1,sizeof(ID));
for(int i=2*n-1;i>=0;i--)
if(ID[ord[i]]==-1)
 {
dfs2(ord[i]);
SCC++;
}
}
bool chk()
 {
for(int i=0;i<2*n;i+=2)
if(ID[i]==ID[i+1])return false;
return true;
}
void build_Dag()//对反图建DAG 这样topoSort就是自底向上的了
 {
for(int i=0;i<SCC;i++)
 {
Dag[i].clear();
inDag[i].clear();
}
memset(in,0,sizeof(in));
for(int u=0,v;u<2*n;u++)
 {
inDag[ID[u]].push_back(u);
for(int i=0,size=_G[u].size();i<size;i++)
 {
v=_G[u][i];
if(ID[u]!=ID[v])
 {
Dag[ID[u]].push_back(ID[v]);
++in[ID[v]];
}
}
}
}
void topo_Sort()
 {
queue<int>Q;
for(int i=0;i<SCC;i++)
if(in[i]==0)Q.push(i);
int cnt = 0;
while(!Q.empty())
 {
int u=Q.front();Q.pop();
pos[cnt++]=u;
for(int i=0,size=Dag[u].size();i<size;i++)
 {
int v=Dag[u][i];
if(--in[v]==0)Q.push(v);
}
}
}
void setColor(int u)
 {
color[u]=2;
for(int i=0,size=Dag[u].size();i<size;i++)
 {
int v=Dag[u][i];
if(color[v]!=2)setColor(v);
}
}
void select()
 {
memset(color,0,sizeof(color));
for(int i=0;i<SCC;i++)
 {
int u=pos[i];
if(color[u]==0)
 {
color[u]=1;//select
for(int j=0,size=inDag[u].size();j<size;j++)//set every _v
 {
int v=inDag[u][j]^1;
if(color[ID[v]]==2)continue;
setColor(ID[v]);
}
}
}
}
void solve()
 {
build_Dag();
topo_Sort();
select();
for(int i=2;i<2*n;i++)
if(color[ID[i]]==1)printf("%d%c ",i/2,(i&1)?'h':'w');
puts("");
}

}graph;

int main()
  {
//freopen("in","r",stdin);
int n,m,a,b;
char ca,cb;
while(scanf("%d%d",&n,&m),n)
 {
graph.init(n);
for(int i=0;i<m;i++)
 {
scanf("%d%c%d%c",&a,&ca,&b,&cb);
a=a*2+(ca=='h');
b=b*2+(cb=='h');
//_a->b _b->a
graph.add(a^1,b);
graph.add(b^1,a);
}
//0h->0w 0wife一定要选
graph.add(1,0);
graph.kosaraju();
if(!graph.chk())puts("bad luck");
else graph.solve();
}
return 0;
}

还有2道
POJ 3207 把线当成SAT的点
POJ 3683 跟wedding类似
|
|
常用链接
随笔分类
Links
搜索
最新评论

|
|