2-SAT学习笔记
问题
由数理逻辑的知识我们知道,任何一个合式公式对应于一个合取范式。判断一般合式公式的可满足性是一个NPC问题,甚至当存在一些项由三个或以上原子命题时,判断其可满足性仍然是NPC。
考虑一个每一项都只有至多两个原子命题的合取范式(2-SAT),其中要支持
2-SAT形如:
(p∨q)∧(a→b)∧(¬c)
一些简化
由于
a∨b=¬(¬a)∨b=¬a→b a∧b=¬(¬(a∧b))=¬(¬a∨¬b) a↔b=(a→b)∧(b→a)
因而我们只需要考虑含有
建图
我们考虑图论手段。将每个原子命题拆成为真和为假两个点,记作
定理: 一个2-SAT是不可满足的当且仅当
为了证明这个定理,我们需要先证明一个引理:当且仅当
定理的证明:命题的必要性(
充分性(
- 如果是二分图,将图黑白染色,即可以说明存在一种真值指派满足2-SAT(这是显然的)。
如果不是二分图,我们假设图中有一个奇环。任取一个元素
i ,则Aφ(i),Aφ(¬i) 之间必有一个经过奇数个点(偶数条边)的路径。设建立这些路径的原子命题为a1,a2,…,a2k ,则有:i⟺a1 ¬a1⟺a2 ¬a2⟺a3 … ¬a2k−1⟺a2k ¬a2k⟺¬i
我们将上面的式子整理为:
i⟺a1 a1⟺¬a2 ¬a2⟺a3 … ¬a2k⟺¬i
也就是
i⟺¬i ,根据引理,i,¬i 在同一个强连通分量内,矛盾。
计算
对于给定的2-SAT,我们可以建出这样的一张图,通过Tarjan判断强联通分量即可。
struct TwoSat {
struct node {
int to, next;
} edge[MAXN*30];
int n, head[MAXN], top = 0;
int Not(int i)
{ return n+i; }
void push(int i, int j)
{ ++top, edge[top] = (node){j, head[i]}, head[i] = top; }
int dfn[MAXN], low[MAXN], stk[MAXN], stk_top, instk[MAXN];
int gp[MAXN], gp_top, dfn_top;
void init(int _n)
{
n = _n;
memset(dfn, 0, sizeof dfn); memset(head, 0, sizeof head);
memset(instk, 0, sizeof instk); memset(gp, 0, sizeof gp);
gp_top = dfn_top = stk_top = top = 0;
}
void tarjan(int nd)
{
dfn[nd] = low[nd] = ++dfn_top, stk[++stk_top] = nd, instk[nd] = 1;
for (int i = head[nd]; i; i = edge[i].next) {
int to = edge[i].to;
if (!dfn[to]) tarjan(to), low[nd] = min(low[nd], low[to]);
else if (instk[to]) low[nd] = min(low[nd], dfn[to]);
}
if (dfn[nd] == low[nd]) {
int now; ++gp_top;
do {
now = stk[stk_top--], gp[now] = gp_top, instk[now] = 0;
} while (now != nd);
}
}
bool work()
{
for (int i = 1; i <= n*2; i++)
if (!dfn[i])
tarjan(i);
for (int i = 1; i <= n; i++)
if (gp[i] == gp[i+n])
return false;
return true;
}
} ;