专栏文章

2-SAT(记录)

个人记录参与者 1已保存评论 0

文章操作

快速查看文章及其快照的属性,并进行相关操作。

当前评论
0 条
当前快照
1 份
快照标识符
@mipsr9tm
此快照首次捕获于
2025/12/03 17:20
3 个月前
此快照最后确认于
2025/12/03 17:20
3 个月前
查看原文

2-SAT

① 是指一类题型

——在nn对数中在每两对的两个数中选一个是否可以满足选够nn个数

(1)例如以下问题

HDU 3062HDU~3062
——>party
也可以从这里也可以从这里
——>A-party

解析如下解析如下

(一)建图分析

声明A的伴侣为A,B的伴侣为B声明 A的伴侣为A',则B的伴侣为B'

图1
在这个题中在这个题中
我们知道如果AB有矛盾的话我们知道如果A和B有矛盾的话 那么为了尽量满足前去n人去参加那么为了尽量满足前去n人去参加

我们就有了两种选择我们就有了两种选择

①让AB①让 A和B' 去

②让BA②让 B和A'去

这样我们就不难想到这样我们就不难想到

假设存在这样一组矛盾关系

我们就可以建两条有向边

第一条边是由A指向B第一条边是由A指向B'的

第二条边是由B指向A第二条边是由B'指向A的

图2

(1)每条有向边(u,v)表示从u指向v每条有向边(u,v)表示从u指向v

uv必选①u选v必选

②但vu无限制②但v选u无限制

(2)

那么由此可得那么由此可得

①这每个点表示选这个点时①这每个点表示选这个点时

②其所连的的有向边所能遍历到的所有点都得选②其所连的的有向边所能遍历到的所有点都得选

(二)判断解是否存在

然后我们去判断是否无解,如果有就进行有的操作然后我们去判断是否无解,如果有就进行有的操作

我们先判断是否无解我们先判断是否无解

在这个题里无解即为两种在这个题里无解即为两种

①矛盾同出现①矛盾同出现

②夫妻同出现②夫妻同出现

由于我们先前的存储方式,①即为解决了由于我们先前的存储方式,①即为解决了

再看(夫妻同出现的问题)再看(夫妻同出现的问题)

在这个题里,在我们的建图方法下在这个题里,在我们的建图方法下

如果在一对夫妻里我们选谁,其伴侣都必须选的话如果在一对夫妻里我们选谁,其伴侣都必须选的话

那即为无解,因为题目里要求了,夫妻不同现嘛那即为无解,因为题目里要求了,夫妻不同现嘛


(三)转化题目

我们现在在看这个无解的情况我们现在在看这个无解的情况

"互选"不就是强连通分量吗"互选"不就是强连通分量吗

似乎与可互相到达有异曲同工之妙似乎与可互相到达有异曲同工之妙

夫妻不同现,也即为夫妻这两所代表的点不在同一个强连通分量里夫妻不同现,也即为夫妻这两所代表的点不在同一个强连通分量里\

这个题也就转化成为了求图中强连通分量这个题也就转化成为了求图中强连通分量

这个可以用tarjan+栈解决这个可以用tarjan+栈解决

(四)奉上Code

CPP
#include<bits/stdc++.h>
#define N 2500
#define M 1000000
using namespace std;
int n,m,cnt=0,b=0,top=0,ans=0;
int s[N],ins[N],dfn[N],low[N],scc[N];
vector<int>v[N<<1];
int read();
int wf(int u){return u<<1;}
int hs(int u){return u<<1|1;}
void tarjan(int u);
void add(int from,int to){v[from].push_back(to);}

int main()
{
   ios::sync_with_stdio(false);
   cin.tie(0);
   while(cin>>n>>m){	
   	for(int i=1;i<=m;i++){
   		//int a1=read(),a2=read(),c1=read(),c2=read();
   		int a1,a2,c1,c2;
   		cin>>a1>>a2>>c1>>c2;
   		int f=(c1?hs(a1):wf(a1)),s=(c2?hs(a2):wf(a2));
   		add(f,(s^1));
   		add(s,(f^1));
   	}
   	for(int i=0;i<(n<<1);i++){
   		if(dfn[i])continue;
   		tarjan(i);
   	}
   	for(int i=0;i<(n<<1);i+=2){
   		if(scc[i]==scc[i^1]){
   			b=1;
   			break;
   		}
   	}
   	if(!b)cout<<"YES\n";
   	else cout<<"NO\n";
   	cnt=0,ans=0,b=0;
   	for(int i=0;i<(n<<1);i++)dfn[i]=0;
   	for(int i=0;i<(n<<1);i++)ins[i]=0;
   	for(int i=0;i<(n<<1);i++)v[i].clear();
   }
   return 0;
}
int read(){
   int x=0,f=1;char c=getchar();
   while(c<'0'||c>'9'){if(c=='-')f=-1;c=getchar();}
   while(c>='0'&&c<='9'){x=(x<<3)+(x<<1)+c-'0';c=getchar();}
   return x*f;
}
void tarjan(int u){
   low[u]=dfn[u]=++cnt;
   ins[u]=1;
   s[++top]=u;
   for(int i=0;i<v[u].size();i++){
   	int g=v[u][i];
   	if(!dfn[g]){//Q1,u->g 
   		tarjan(g);
   		low[u]=min(low[u],low[g]);
   	}
   	else if(ins[g]){//Q2,u->g
   		low[u]=min(low[u],dfn[g]);//Q3,u->g
   	}
   }
   if(dfn[u]==low[u]){
   	++ans;
   	while(1){
   		scc[s[top]]=ans;
   		ins[s[top]]=0;
   		if(s[top--]==u)break;//Q4,->top位置不对 
   	}
   }
   return ;
}

评论

0 条评论,欢迎与作者交流。

正在加载评论...