首页 > 其他分享 >2-SAT

2-SAT

时间:2024-02-02 13:22:55浏览次数:21  
标签:false int back tail now true SAT

2-SAT 总结:

  • 要有 \(2\) 个变量,形如 x1 AND x2 = truex1 OR x2 = true 之类的,给定 \(m\) 组限制,问在这样的限制条件下有没有一组 \(x_1,x_2,\cdots,x_n\) 满足这些限制。

  • 基本思路就是对于每个 \(x_i\) 建 \(2\) 个点,分别是 \(x_i\) 的 true 和 \(x_i\) 的 false。然后连边。

  • 想仔细怎么建边。这里举 \(3\) 个例子:

    1. x1 AND x2 = true。如果 x1 = true,那么 x2 = true。反之亦然。所以从 \(x_1\) 的 true 向 \(x_2\) 的 true 连一条有向边,从 \(x_2\) 的 true 向 \(x_1\) 的 true 连一条有向边,

    2. x1 OR x2 = true。如果 x1 = false,那么 x2 = true;同理,如果 x2 = false,那么 x1 = true。所以从 \(x_1\) 的 false 向 \(x_2\) 的 true 连一条有向边,从 \(x_2\) 的 false 向 \(x_1\) 的 true 连一条有向边。

    3. x1 = true。考虑从 \(x_1\) 的 false 向 \(x_1\) 的 true 连一条有向边。如果 \(x_1\) 为 false,那么 \(x_1\) 为 true。这种逻辑显然是矛盾的。至于为什么,马上就说。

  • 我们把边建好之后跑一遍 Tarjan,如果 \(x_i\) 的 truefalse 在同一个连通块里,就说明从 \(x_i\) 为 false 可以推导出 \(x_i\) 为 true。这种逻辑显然是矛盾的,所以没有解;反之则有解。

  • 可以用 \(x\) 表示 true,用 \(x+n\) 表示 false

代码(以 P4782 为例):

#include <bits/stdc++.h>

using namespace std;

const int MAXN = 4e6 + 5;

int n, m;
vector<int> z[MAXN];//z[x]为真,z[x + n]为假
int dfn[MAXN], low[MAXN];
int st[MAXN], tail;
bool inst[MAXN];
int belong[MAXN], cnt;
int t;

void add_edge(int i, int a, int j, int b) {
	if(a == 0 && b == 0) {
		z[i].push_back(j + n);
		z[j].push_back(i + n);
	}
	else if(a == 0 && b == 1) {
		z[i].push_back(j);
		z[j + n].push_back(i + n);
	}
	else if(a == 1 && b == 0) {
		z[i + n].push_back(j + n);
		z[j].push_back(i);
	}
	else {
		z[i + n].push_back(j);
		z[j + n].push_back(i);
	}
}

void dfs(int now) {
	t++;
	dfn[now] = low[now] = t;
	inst[now] = true;
	st[++tail] = now;
	for (int i = 0; i < int(z[now].size()); i++) {
		int j = z[now][i];
		if (!dfn[j]) {
			dfs(j);
			low[now] = min(low[now], low[j]);
		}
		else {
			if(inst[j]) low[now] = min(low[now], dfn[j]);
		}
	}
	if(low[now] == dfn[now]) {
		cnt++;
		belong[now] = cnt;
		while(st[tail] != now) {
			belong[st[tail]] = cnt;
			inst[st[tail]] = false;
			tail--;
		}
		inst[st[tail]] = false;
		tail--;
	}
}

int main() {
	scanf("%d%d", &n, &m);
	for (int k = 1; k <= m; k++) {
		int i, a, j, b;
		scanf("%d%d%d%d", &i, &a, &j, &b);
		add_edge(i, a, j, b);
	}
	for (int i = 1; i <= n + n; i++) {
		if(!dfn[i]) dfs(i);
	}
	for (int i = 1; i <= n; i++) {
		if(belong[i] == belong[i + n]) {
			printf("IMPOSSIBLE");
			return 0;
		}
	}
	printf("POSSIBLE\n");
	for (int i = 1; i <= n; i++) {
		printf("%d ", (belong[i] < belong[i + n]));
	}
	return 0;
}

标签:false,int,back,tail,now,true,SAT
From: https://www.cnblogs.com/ljlbj-fengyuwuzu/p/18003011/2-SAT

相关文章

  • 【GEE】基于GEE可视化和下载Landsat8 L2A数据(镶嵌、裁剪)
    ​        之前发过一篇使用GEE下载Landsat8的文章,然后有很多小伙伴私信我各种问题,如L1C、L2数据代码怎么修改,如何镶嵌,如何去云、如何裁剪等一系列问题。正好快过年了,手头的事也没有多少了,所以这两天整理了一下GEE的相关代码,后续会陆续发出来。代码比较简单就是查询函......
  • 【GEE】基于GEE可视化和下载Landsat8 L1C数据(镶嵌、裁剪)
    ​        之前发过一篇使用GEE下载Landsat8的文章,然后有很多小伙伴私信我各种问题,如L1C、L2数据代码怎么修改,如何镶嵌,如何去云、如何裁剪等一系列问题。正好快过年了,手头的事也没有多少了,所以这两天整理了一下GEE的相关代码,后续会陆续发出来。代码比较简单就是查询函......
  • 【GEE】基于GEE批量下载Landsat8 L1C数据(整幅)
    ​     之前发过一篇使用GEE下载Landsat8的文章,然后有很多小伙伴私信我各种问题,如L1C、L2数据代码怎么修改,如何镶嵌,如何去云、如何裁剪等一系列问题。正好快过年了,手头的事也没有多少了,所以这两天整理了一下GEE的相关代码,后续会陆续发出来。    今天给大家......
  • 【GEE】基于GEE批量下载Landsat8 L2A数据(整幅)
    ​    之前发过一篇使用GEE下载Landsat8的文章,然后有很多小伙伴私信我各种问题,如L1C、L2数据代码怎么修改,如何镶嵌,如何去云、如何裁剪等一系列问题。正好快过年了,手头的事也没有多少了,所以这两天整理了一下GEE的相关代码,后续会陆续发出来。代码比较简单就是查询函数和......
  • kettle Redhat7连接资源库报错No more handles [MOZILLA_FIVE_HOME=''] (java.lang.Un
    今天把kettle7.1放到redhat7上运行,发现在连接资源库的时候会报一个错误,就是标题的错误。本来是想在windows上用kettle工具创建了一些job和trans打算迁移到linux上去执行,或者到任意机器上执行,突然想到这些kettle文件的还会存在迁移的问题,因为在job和trans文件里的数据库连接信息都......
  • 金邦2.5寸SATA固态硬盘R3 2TB开箱
          上次帖子里根据坛友的反馈,然后结合狗东的搜索,找了个金邦的2.5寸的SATA的固态硬盘,图的是它的价格和容量。但是我拿到它这个实物的时候还是略有点失望,因为包装太简单,坛友里说估计是贴牌。反正已经入手了,就贴出来大家共赏吧。1、       包装照;  2、     ......
  • SpringBoot启动项目报错:java.lang.UnsatisfiedLinkError: D:\files\software\jdk-1
    目录问题描述解决方法:问题描述在运行向的时候出现报错:java.lang.UnsatisfiedLinkError:D:\files\software\jdk-15.0.1\jdk-17.0.3.1\bin\tcnative-1.dll:Can'tloadIA32-bit.dllonaAMD64-bitplatform atjava.base/jdk.internal.loader.NativeLibraries.load(Native......
  • CodeForces 995F Cowmpany Cowmpensation
    洛谷传送门CF传送门考虑一个显然的树形dp,设\(f_{u,i}\)为\(u\)结点染颜色\(i\)的方案数,有\(f_{u,i}=\prod\limits_{v\inson_u}\sum\limits_{j=1}^if_{v,j}\)。前缀和后可得\(f_{u,i}=f_{u,i-1}+\prod\limits_{v\inson_u}f_{v,i}\)。发现\(f_......
  • 【GEE】GEE反演地表温度相关问题说明(空洞、Landsat9数据集等)
    ​     之前分享了基于GEE-Landsat8数据集地表温度反演(LST热度计算),最近有很多小伙伴私信我很多问题,一一回复太慢了,所以今天写篇文章统一回答一下大家的问题。问题1:数据有很多空洞、某些条带没有数据等问题2:如何使用Landsat9数据进行温度反演问题3:该反演算法的来源......
  • CodeForces 1466H Finding satisfactory solutions
    洛谷传送门CF传送门考虑给定\(b\)如何构造\(a\)。拎出基环树的环部分,把这些点连同它们的边删掉(这个环一定在答案中)。递归做即可。考虑我们在\(a\)的环上连一些在\(\{b_{i,n}\}\)中排得比\(a_i\)前的\(i\toj\)。可以将问题转化为,若干个环,缩点后连一些边使得它成......