2-SAT 入门

Posted 2021-01-11 yuyanjiab

一、前置技能

 >  Tarjan求割点

 >  高中数学选修2-1 命题与逻辑关系（好像是这个名字）

 >  莓了

（本文用&&表示与 || 表示或  !x表示x的否命题 与正常的数学符号不同食用请注意）

 

二、k-SAT

 >  Q: 为什么讲2-SAT之前要先讲k-SAT？

因为k-SAT被证明是NP-完全问题

所以暴搜就不去管它……

 >  Q: 所以什么是“SAT”？

由美国大学委员会主办的一场考试 

SAT被称为布尔方程的可满足性问题

就是判断一组逻辑关系同时满足的正确性……

比如a&&(!a) 就不满足

再比如a&&b||c&&!d&&(.....)

我们给一种特殊的布尔方程起一个名字叫 合取范式 

就是形如（a || !b || c) && (d || e) && (...)

其中每个bool变量叫 文字 打了括号的部分就叫 子句 

如果每个子句大小不超过k那么就叫 k-SAT

同理 如果合取范式的每个子句中的文字个数都不超过两个，那么对应的 SAT 问题又称为 2-SAT 问题。

 

三、解法

考虑一个二分图 左边表示bool变量值为0（伪） 右边表示值为1（真）

如果满足一个命题必然能推出另一个命题 那么就在这两个命题之间连一条边

考虑两个bool变量之间的关系无非是 && 和 || 

由于我们是2-SAT 所以最多出现a || b两个变量

那么转化为蕴含（推出）关系

由 || 运算的定义

!a => b 且 !b => a

然后是 &&

!a => a 且 !b => b  

 

 >  Q: 这……bool变量还能同时满足真和伪？

当然不是 这里的推出 可以理解为如果选择了a为伪，那么最后会推出a为真

所以我们最后选择的时候不能选择a为伪 只能选择a为真 达到了我们的目的

 

 >  Q: 好吧……可是，为什么要这么建图？

我们考虑bool运算的性质

命题成立则它的逆否命题成立 这个性质又叫 对称性

同时考虑推出的 传递性  ，如果b是由某一个变量推知为真 和它为真的效果是一样的 都能推知下一步的变量

所以拆完真伪最终在一个强连通分量里的点的bool值相同（注意并不是变量的bool值相同）

同时上一个Q表示建图可以处理单个变量定值的问题

 

 >  Q:嗯……如何求出最终答案呢？

我们对于最后建好的图跑一个Tarjan缩点 如果变量的真值和伪值在同一个强连通分量里（即既不能为真也不能为伪）那么就无解

否则 每个点的答案应该是真值和伪值中拓扑序靠后的那个（同第一个Q）

（所以要缩点）

然后由于我们跑tarjan的时候 就是拓扑序靠后的强连通分量编号小

所以就不用建新图辣

 

四、代码

Code:(luogu P4782)

 1 #include<cstdio>
 2 #include<cstring>
 3 #include<algorithm>
 4 #include<cmath>
 5 #define itn int
 6 #define ms(a,b) memset(a,b,sizeof a)
 7 #define rep(i,a,n) for(int i = a;i <= n;i++)
 8 #define per(i,n,a) for(int i = n;i >= a;i--)
 9 using namespace std;
10 typedef long long ll;
11 ll read() {
12     ll as = 0,fu = 1;
13     char c = getchar();
14     while(c < ‘0‘ || c > ‘9‘) {
15         if(c == ‘-‘) fu = -1;
16         c = getchar();
17     }
18     while(c >= ‘0‘ && c <= ‘9‘) {
19         as = as * 10 + c - ‘0‘;
20         c = getchar();
21     }
22     return as * fu;
23 }
24 const int N = 2000005;
25 //head
26 int n,m;
27 int head[N],nxt[N<<1],mo[N<<1],cnt = -1;
28 bool flag[N];
29 void add(itn x,int y) {
30     mo[++cnt] = y;
31     nxt[cnt] = head[x];
32     head[x] = cnt;
33 }
34 int rev(int x) {return x>n?x-n:x+n;}
35 
36 int dfn[N],low[N],col[N],stk[N];
37 int scc,idx,top;
38 bool ins[N];
39 void tarjan(int x) {
40     dfn[x] = low[x] = ++idx;
41     stk[++top] = x,ins[x] = 1;
42     for(int i = head[x];i;i = nxt[i]) {
43     int sn = mo[i];
44     if(!dfn[sn]) {
45         tarjan(sn);
46         low[x] = min(low[x],low[sn]);
47     } else if(ins[sn]) low[x] = min(low[x],dfn[sn]);
48     }
49     if(dfn[x] == low[x]) {
50     int t = -1;
51     scc++;
52     while(t!=x) {
53         t = stk[top--];
54         col[t] = scc;
55         ins[t] = 0;
56     }
57     }
58 }
59 
60 int main() {
61     n = read();
62     m = read();
63     rep(i,1,m) {
64     int x = read();x += read()*n;
65     int y = read();y += read()*n;
66     add(rev(x),y),add(rev(y),x);
67     }
68     rep(i,1,n<<1) if(!dfn[i]) tarjan(i);
69     bool flag = 1;
70     rep(i,1,n) if(col[i] == col[n+i]) flag = 0;
71     if(!flag) puts("IMPOSSIBLE");
72     else {
73     puts("POSSIBLE");
74     rep(i,1,n) printf("%d ",col[i] > col[i+n]);
75     puts("");
76     }
77     return 0;
78 }

View Code

注意:

1.跑的时候依然像Tarjan一样考虑多个联通块

2.本题全部是或的关系 注意反向建图

3.最后比较的时候每个人写法不一样要考虑大于还是小于

 

例题详见Practice 1

By prophetB