首页 > 其他分享 >2-SAT 问题

2-SAT 问题

时间：2024-07-06 18:19:11浏览次数：13  
标签：int back 问题 vis dfn low push SAT

2-SAT 问题

模型

有 \(n\) 个布尔类型的变量 \(x_1, x_2, \ldots, x_n\)，有 \(m\) 条限制形如 \(x_i \space [\operatorname{or}/\operatorname{and}]\space x_j=[1/0]\).
求一组符合要求的解。

核心问题只需要考虑有没有解。

对于每个变量都只有两种取值：\(0/1\)，那么把每个变量拆成 \(0\) 和 \(1\) 两个点。

一般地，对 \(x, y\) 建边时，对 \(x\) 的 \(0, 1\) 两种取值分别考虑 \(y\) 的取值，若 \(y\) 的取值一定，则从 \(x\) 对应取值的点向 \(y\) 对应取值的点连边。

本质上是找到确定的变量间关系并判断是否有关系冲突。

连上边后，通过 Tarjan 找到所有强联通分量。同一强连通分量内的变量值一定是相等的，所以只需判断表示 \(x = 1\) 与 \(x = 0\) 的节点是否在同一个强联通分量里即可。如果是，则无解，反之有解。

在构造解时，对每个节点 \(x\)，我们会选择两种取值中拓扑序较大的点，这样就不会产生从一种取值推出另一种取值的情况（比如从 \(x=1\) 推出 \(x=0\)）。

注意到在 Tarjan 得到的搜索树上，拓扑序越大的点越远离树根，强联通分量编号也越小。所以直接选择表示两种取值的节点中强联通分量的编号较小的点即可。

例题

P4782 【模板】2-SAT

标准的 2-SAT 板子题，细节见代码。

#include <bits/stdc++.h>
using namespace std;

const int N = 2e6 + 5;

int n, m, a, b, x, y, dfn[N], low[N], h, ans, tot, idx, bel[N];
bool vis[N];
vector<int> g[N];
stack<int> stk;

void tarjan(int u, int fa)
{
	low[u] = dfn[u] = ++idx;
	stk.push(u), vis[u] = 1;
	for(auto v : g[u])
	{
		if(!dfn[v])
		{
			tarjan(v, u);
			low[u] = min(low[u], low[v]);
		}
		else if(vis[v]) low[u] = min(low[u], dfn[v]);
	}
	if(low[u] == dfn[u])
	{
		tot++;
		do
		{
			h = stk.top(); stk.pop();
			vis[h] = 0, bel[h] = tot;
		} while(h != u);
	}
	return;
}

int main()
{
	ios :: sync_with_stdio(false);
	cin.tie(0), cout.tie(0);
	cin >> n >> m;
	for(int i = 1; i <= m; i++)
	{
		/*
			限制：arr[a] = x 或 arr[b] = y
			建边：形如“若 arr[a] = ...，则 arr[b] = ...”，必须是确定的关系。
			用 x (x <= n) 代表值为 0，x + n 代表值为 1
		*/
		cin >> a >> x >> b >> y;
		if(x == 0 && y == 0)
		{
			g[a + n].push_back(b);      // a = 1 -> b = 0
			g[b + n].push_back(a);      // b = 1 -> a = 0
		}
		else if(x == 0 && y == 1)
		{
			g[a + n].push_back(b + n);  // a = 1 -> b = 1
			g[b].push_back(a);          // b = 0 -> a = 0
		}
		else if(x == 1 && y == 0)
		{
			g[a].push_back(b);          // a = 0 -> b = 0
			g[b + n].push_back(a + n);  // a = 1 -> b = 1
		}
		else
		{
			g[a].push_back(b + n);      // a = 0 -> b = 1
			g[b].push_back(a + n);      // b = 0 -> a = 1
		}
	}
	for(int i = 1; i <= 2 * n; i++)
		if(!dfn[i]) tarjan(i, 0);
	for(int i = 1; i <= n; i++)
	{
		if(bel[i] == bel[i + n])
		{
			cout << "IMPOSSIBLE";
			return 0;
		}
	}
	cout << "POSSIBLE\n";
	for(int i = 1; i <= n; i++)
		cout << (bel[i] > bel[i + n]) << ' ';
	return 0;
}

P4171 [JSOI2010] 满汉全席

和模板题一样，不过要用 \(0, 1\) 表示 \(\texttt{m}\) 和 \(\texttt{h}\).

初始化时要注意有 \(2n\) 个点，而不是 \(n\) 个。

#include <bits/stdc++.h>
using namespace std;

const int N = 2e6 + 5;

int n, m, a, b, x, y, dfn[N], low[N], h, ans, tot, idx, bel[N];
bool vis[N];
vector<int> g[N];
stack<int> stk;

void tarjan(int u, int fa)
{
	low[u] = dfn[u] = ++idx;
	stk.push(u), vis[u] = 1;
	for(auto v : g[u])
	{
		if(!dfn[v])
		{
			tarjan(v, u);
			low[u] = min(low[u], low[v]);
		}
		else if(vis[v]) low[u] = min(low[u], dfn[v]);
	}
	if(low[u] == dfn[u])
	{
		tot++;
		do
		{
			h = stk.top(); stk.pop();
			vis[h] = 0, bel[h] = tot;
		} while(h != u);
	}
	return;
}

void solve()
{
	cin >> n >> m;
	for(int i = 1; i <= 2 * n; i++)
		g[i].clear();
	memset(dfn, 0, sizeof dfn);
	memset(low, 0, sizeof low);
	memset(vis, 0, sizeof vis);
	memset(bel, 0, sizeof bel);
	for(int i = 1; i <= m; i++)
	{
		string s1, s2;
		cin >> s1 >> s2;
		a = b = 0;
		for(int i = 1; i < s1.size(); i++)
			a = a * 10 + s1[i] - '0';
		for(int i = 1; i < s2.size(); i++)
			b = b * 10 + s2[i] - '0';	
		x = (s1[0] == 'm');
		y = (s2[0] == 'm');
		if(x == 0 && y == 0)
		{
			g[a + n].push_back(b);
			g[b + n].push_back(a);
		}
		else if(x == 0 && y == 1)
		{
			g[a + n].push_back(b + n);
			g[b].push_back(a);
		}
		else if(x == 1 && y == 0)
		{
			g[a].push_back(b);
			g[b + n].push_back(a + n);
		}
		else
		{
			g[a].push_back(b + n);
			g[b].push_back(a + n);
		}
	}
	for(int i = 1; i <= 2 * n; i++)
		if(!dfn[i]) tarjan(i, 0);
	for(int i = 1; i <= n; i++)
		if(bel[i] == bel[i + n])
			return (void) (cout << "BAD\n");
	cout << "GOOD\n";
	return;
}

int main()
{
	ios :: sync_with_stdio(false);
	cin.tie(0), cout.tie(0);
	int T; cin >> T;
	while(T--) solve();
	return 0;
}

P6378 [PA2010] Riddle

  • 对于“每条边至少有一个端点是关键点”的限制，按照“\(a=1 \space \operatorname{or} \space b=1\)” 的限制来连边即可。
  • 对于“每个部分恰有几个关键点”的限制，直接连边会导致边数过多，达到 \(O\left(n^2\right)\) 级别，所以考虑对建图进行一些优化。

第一条限制的本质，是在每一个部分中，把每一个点的 “真状态” 连向其余所有点的 “假状态”。并且只要保证连通即可。考虑进行前后缀优化建图，将连向除了自身的另一个状态以外的所有点，转化为连向这个点之前的前缀以及这个点之后的后缀。

image

此时，这个新图的性质已经和原图完全等价了。

直接跑 2-SAT 模板即可。

#include <bits/stdc++.h>
using namespace std;

const int N = 4e6 + 5;

int n, m, a, b, k, w, dfn[N], low[N], h, ans, tot, idx, bel[N], c[N];
bool vis[N];
vector<int> g[N];
stack<int> stk;

void tarjan(int u, int fa)
{
	low[u] = dfn[u] = ++idx;
	stk.push(u), vis[u] = 1;
	for(auto v : g[u])
	{
		if(!dfn[v])
		{
			tarjan(v, u);
			low[u] = min(low[u], low[v]);
		}
		else if(vis[v]) low[u] = min(low[u], dfn[v]);
	}
	if(low[u] == dfn[u])
	{
		tot++;
		do
		{
			h = stk.top(); stk.pop();
			vis[h] = 0, bel[h] = tot;
		} while(h != u);
	}
	return;
}

int main()
{
	ios :: sync_with_stdio(false);
	cin.tie(0), cout.tie(0);
	cin >> n >> m >> k;
	for(int i = 1; i <= m; i++)
	{
		cin >> a >> b;
		g[a + n].push_back(b);
		g[b + n].push_back(a);
	}
	/*
		1 ~ n:       x = 1
		n + 1 ~ 2n:  x = 0
		2n + 1 ~ 3n: 前缀
		3n + 1 ~ 4n：后缀
	*/
	for(int i = 1; i <= k; i++) // 前缀优化建图
	{
		cin >> w;
		for(int j = 1; j <= w; j++)
		{
			cin >> c[j];
			g[c[j] + 2 * n].push_back(c[j] + n);
			g[c[j] + 3 * n].push_back(c[j] + n);
			if(j > 1)
			{
				g[c[j - 1]].push_back(c[j] + 2 * n);
				g[c[j - 1] + 2 * n].push_back(c[j] + 2 * n);
				
				g[c[j]].push_back(c[j - 1] + 3 * n);
				g[c[j] + 3 * n].push_back(c[j - 1] + 3 * n);
			}
		}
	}
	for(int i = 1; i <= 2 * n; i++)
		if(!dfn[i]) tarjan(i, 0);
	for(int i = 1; i <= n; i++)
	{
		if(bel[i] == bel[i + n])
		{
			cout << "NIE";
			return 0;
		}
	}
	cout << "TAK";
	return 0;
}

P3209 [HNOI2010] 平面图判定

首先，根据平面图的性质，若 \(m > 3n-6\)，则图肯定不为平面图，可以直接输出 NO。

将哈密顿回路画成一个圆，那么原图上不在哈密顿回路上的边可以看作是该圆的弦。

考虑圆中两条相交的弦 \((u_1, v_1), (u_2, v_2)\)，由于是平面图，我们可以将其中的一条翻到圆外去（但两条弦不能同时翻到圆外去，原因是如果他们在圆内相交，那么在圆外也会相交，可以画图模拟一下）。

设 \(x=1/0\) 表示一条边是否在圆外，由于两条在圆内相交的弦必有一个在圆外，一个在圆内，考虑将弦视为点，使用 2-SAT 建模。

具体连边有 \((x, y'), (x', y), (y, x'), (y', x)\) 四种。

#include <bits/stdc++.h>
using namespace std;

const int N = 2e3 + 5, M = 2e6 + 5;

int n, m, u[M], v[M], dfn[M], low[M], h, ans, tot, idx, bel[M], a[M], mp[N][N], cnt, rk[M];
bool vis[M];
vector<int> g[M];
stack<int> stk;

void tarjan(int u, int fa)
{
	low[u] = dfn[u] = ++idx;
	stk.push(u), vis[u] = 1;
	for(auto v : g[u])
	{
		if(!dfn[v])
		{
			tarjan(v, u);
			low[u] = min(low[u], low[v]);
		}
		else if(vis[v]) low[u] = min(low[u], dfn[v]);
	}
	if(low[u] == dfn[u])
	{
		tot++;
		do
		{
			h = stk.top(); stk.pop();
			vis[h] = 0, bel[h] = tot;
		} while(h != u);
	}
	return;
}

void solve()
{
	cnt = idx = tot = 0;
	memset(dfn, 0, sizeof dfn);
	memset(low, 0, sizeof low);
	memset(vis, 0, sizeof vis);
	memset(bel, 0, sizeof bel);
	memset(mp, 0, sizeof mp);
	memset(rk, 0, sizeof rk);
	cin >> n >> m;
	for(int i = 1; i <= m; i++)
	{
		cin >> u[i] >> v[i];
		if(u[i] > v[i]) swap(u[i], v[i]);
	}
		
	for(int i = 1; i <= n; i++)
	{
		cin >> a[i];
		rk[a[i]] = i;
		if(i > 1)
		{
			int x = a[i - 1], y = a[i];
			if(x > y) swap(x, y);
			mp[x][y] = 1;
		}
		if(i == n)
		{
			int x = a[i], y = a[1];
			if(x > y) swap(x, y);
			mp[x][y] = 1;
		}
	}
	if(m > 3 * n - 6) return (void) (cout << "NO\n");
	for(int i = 1; i <= m; i++)
		if(!mp[u[i]][v[i]]) u[++cnt] = u[i], v[cnt] = v[i];
	m = cnt;
	for(int i = 1; i < m; i++)
	{
		int x = rk[u[i]], y = rk[v[i]];
		if(x > y) swap(x, y);
		for(int j = i + 1; j <= m; j++)
		{
			int xx = rk[u[j]], yy = rk[v[j]];
			if(xx > yy) swap(xx, yy);
			if(xx < x && x < yy && yy < y || x < xx && xx < y && y < yy)
			{
				g[i].push_back(j + m);
				g[i + m].push_back(j);
				g[j].push_back(i + m);
				g[j + m].push_back(i);
			}
		}
	}
	for(int i = 1; i <= m * 2; i++)
		if(!dfn[i]) tarjan(i, 0);
	for(int i = 1; i <= 2 * m; i++) g[i].clear();
	for(int i = 1; i <= m; i++)
		if(bel[i] == bel[i + m])
			return (void) (cout << "NO\n");
	cout << "YES\n";
	return;
}

int main()
{
	ios :: sync_with_stdio(false);
	cin.tie(0), cout.tie(0);
	int T; cin >> T;
	while(T--) solve();
	return 0;
}

标签：int,back,问题,vis,dfn,low,push,SAT
From： https://www.cnblogs.com/Heartquakes/p/18287338

相关文章

  • 06-6.4.2 最短路径问题
    ......
  • pspice里面的VSTIM波形设置问题
    在网上看了关于vpwl的波形的定义,发现没有得到正确的结果,经过尝试,最终设置成功 ,可能选项有些歧义.这里的v1是sourcetm里面的vstim.有几个条件要正确:1,包含文件库,在profile里面,2.元件属性设置,这个实例名要注意,不是文件名,实例路径是带路径的文件名这样就可以......
  • SM5308调试问题以及解决办法
     第一版pcb打板后测试整体电路，只有sm5308充电管理芯片出问题，无法开机通电，输出也不稳定，时好时坏，只有在接上usb充电后才能正常工作。这个芯片在之前做的迷你充电宝方案中是没问题的，才将它移植到毕设上，所以电路图也是没问题的。测试时采用多种方案，先是对比可以使用板子和新焊接......
  • python-docx库 写入docx时中文不适配问题，中文异常问题解决办法。
    python-docx库写入docx时中文不适配问题，中文异常问题解决办法。通过以下方法可以成功将正文修改为宋体字体。这个是全文设置。fromdocx.oxml.nsimportqndoc=Document()doc.styles['Normal'].font.name=u'宋体'doc.styles['Normal']._element.rPr.rFonts.set(qn('w:......
  • 关于 Puerts 的性能问题
    Puerts在UE开发中提供了一定的便利性，可以用代码的方式写蓝图，但是官方是不推荐这么做的原话如下那么这个性能问题究竟有多大呢这里先用C++写一个测试代码#include"TestWidget.h"#include"Blueprint/WidgetBlueprintLibrary.h"#include"Blueprint/WidgetLayoutLibr......
  • 打卡信奥刷题（251）用Scratch图形化工具信奥P9771[普及组][HUSTFC 2023] 排列排序问题
    [HUSTFC2023]排列排序问题题目描述JokerShaco有一个长度为nnn的排列pp......
  • 两万字计算机毕设答辩相关问题汇总【文档问题均为自己指导毕设答辩学生反馈相关】附赠
    前言一年一度的毕业季既让人开心，也难免让人忧愁。以我的本科母校为例，毕业除了要提交毕业论文，还需要准备毕业设计作品。而对于毕业设计作品的答辩难免让一些同学感到头大，除了对项目本身了解不是很深入，又因为担心自己准备不充分难以通过答辩，还有些同学不太了解项目答辩会问......
  • 如何解决服务器开机报警问题
    解决服务器开机报警问题，需要按照一系列步骤进行故障排查和修复。一、初步检查与确认查看报警信息：观察服务器的指示灯，特别是电源指示灯、硬盘指示灯等，看是否有异常。如果服务器有显示屏或终端窗口，查看是否有相应的警告信息或错误代码。确认电源状态：检查电源线是否插好，电源插......
  • MSAMRNBSource.dll文件丢失导致程序无法运行问题
    其实很多用户玩单机游戏或者安装软件的时候就出现过这种问题，如果是新手第一时间会认为是软件或游戏出错了，其实并不是这样，其主要原因就是你电脑系统的该dll文件丢失了或没有安装一些系统软件平台所需要的动态链接库，这时你可以下载这个MSAMRNBSource.dll文件(挑选合适的版本文件)......
  • msaddsr.dll文件丢失导致程序无法运行问题
    其实很多用户玩单机游戏或者安装软件的时候就出现过这种问题，如果是新手第一时间会认为是软件或游戏出错了，其实并不是这样，其主要原因就是你电脑系统的该dll文件丢失了或没有安装一些系统软件平台所需要的动态链接库，这时你可以下载这个msaddsr.dll文件(挑选合适的版本文件)把它放......

赞助商

阅读排行

网站主页关于我们联系我们网站地图

本网站内容转载自其他媒体，侵权联系[admin##ips99.com]。

Copyright © 2020-2023 IPS99 版权所有 IPS99