zoukankan      html  css  js  c++  java
  • 2-SAT学习笔记

    2-SAT学习笔记

    问题

    由数理逻辑的知识我们知道,任何一个合式公式对应于一个合取范式。判断一般合式公式的可满足性是一个NPC问题,甚至当存在一些项由三个或以上原子命题时,判断其可满足性仍然是NPC。

    考虑一个每一项都只有至多两个原子命题的合取范式(2-SAT),其中要支持¬,,,,,问是否存在一种真值指派,使得合取范式为真。

    2-SAT形如:

    (pq)(ab)(¬c)


    一些简化

    由于¬是“直观的”,我们考虑用这两种联结词表示其他联结词。不难证明,{¬,}构成一个联结词完备集。其中:

    1. ab=¬(¬a)b=¬ab
    2. ab=¬(¬(ab))=¬(¬a¬b)
    3. ab=(ab)(ba)

    因而我们只需要考虑含有¬的2-SAT即可。


    建图

    我们考虑图论手段。将每个原子命题拆成为真和为假两个点,记作i,¬i。如果存在一个ab,则从a到b连一条有向边。特别的,当存在一个约束¬a¬b时,应该加上ba(容易证明)。一个重要的论断告诉我们:

    定理: 一个2-SAT是不可满足的当且仅当i,使得i,¬i在同一个强连通分量内。

    为了证明这个定理,我们需要先证明一个引理:当且仅当ab,a和b在同一个强联通分量内。证明需要对其间的链长做归纳,这里不再赘述。

    定理的证明:命题的必要性()是显然的。

    充分性()(反证法)。假设i,¬(i)不在一个强联通分量内。考虑所有的强联通分量A1,A2,,Ak,对于i,¬i分别位于Aφ(i),Aφ(¬i),我们用一条无向边连接Aφ(i),Aφ(¬i)。这样则利用强联通分量建出一张图,这个图要么是二分图,要么不是二分图。

    1. 如果是二分图,将图黑白染色,即可以说明存在一种真值指派满足2-SAT(这是显然的)。
    2. 如果不是二分图,我们假设图中有一个奇环。任取一个元素i,则Aφ(i),Aφ(¬i)之间必有一个经过奇数个点(偶数条边)的路径。设建立这些路径的原子命题为a1,a2,,a2k,则有:

      • ia1
      • ¬a1a2
      • ¬a2a3
      • ¬a2k1a2k
      • ¬a2k¬i

      我们将上面的式子整理为:

      • ia1
      • a1¬a2
      • ¬a2a3
      • ¬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;
        }
    } ;

    构造一组解

  • 相关阅读:
    搭建 springboot selenium 网页文件转图片环境
    洛谷P1352没有上司的舞会-题解
    错误集合
    洛谷P1434滑雪-题解
    洛谷P1278单词游戏-题解
    洛谷P1219八皇后-题解
    洛谷P1443马的遍历-题解
    洛谷P1135奇怪的电梯-题解
    经验集合
    洛谷P1019单词接龙-题解
  • 原文地址:https://www.cnblogs.com/ljt12138/p/6684335.html
Copyright © 2011-2022 走看看