2-SAT学习笔记

标签：cup int 笔记 stk 学习 low Leftrightarrow SAT rightarrow

\(SAT:satisfaction\)

\(SAT\)问题：若干问题\(x_1, x_2, ..., x_n\)，另有\(m\)个需要满足条件,其中每个命题为真或假，求\(x_1, x_2, ..., x_n\)的一种取值。

一般\(k-SAT\)问题为\(NP\)完全问题，故只考虑\(O(n+m)\)的\(2-SAT\)问题

算法复习

拓扑排序

统计入度和出度，不再赘述。

code

bool topsort()
{
    int hh = 0, tt = -1;

    for (int i = 1; i <= n; i ++ )
        if (!d[i])
            q[ ++ tt] = i;

    while (hh <= tt)
    {
        int t = q[hh ++ ];

        for (int i = h[t]; i != -1; i = ne[i])
        {
            int j = e[i];
            if (-- d[j] == 0)
                q[ ++ tt] = j;
        }
    }

    return tt == n - 1;
}

\(Tarjan\)算法

求强连通分量，缩点，不再赘述.

code

int h[N], e[M], ne[M], idx;
int dfn[N], low[N], timestamp;
int stk[N], top;
bool in_stk[N];
int id[N], scc_cnt, Size[N];
int dout[N];

void add(int a, int b)
{
    e[idx] = b, ne[idx] = h[a], h[a] = idx ++ ;
}

void tarjan(int u)
{
    dfn[u] = low[u] = ++ timestamp;
    stk[ ++ top] = u, in_stk[u] = true;
    for (int i = h[u]; i != -1; i = ne[i])
    {
        int j = e[i];
        if (!dfn[j])
        {
            tarjan(j);
            low[u] = min(low[u], low[j]);
        }
        else if (in_stk[j]) low[u] = min(low[u], dfn[j]);
    }

    if (dfn[u] == low[u])
    {
        ++ scc_cnt;
        int y;
        do {
            y = stk[top -- ];
            in_stk[y] = false;
            id[y] = scc_cnt;
            Size[scc_cnt] ++ ;
        } while (y != u);
    }
}

\(a \rightarrow b \Leftrightarrow -a \cup b\)

\(a \cup b \Leftrightarrow -a \rightarrow b \Leftrightarrow -b \rightarrow a\)

\(\rightarrow\)可以视作\(a,b\)连一条有向边

原问题因此可以转化成图论问题。

• 无解情况：\(x_1 \rightarrow ... \rightarrow -x_1 \quad or\quad x_1 \rightarrow ... \rightarrow -x_1\)
  (\(x_i\)与\(-x_i\)在同一个强连通分量中，即\(x_i\)既等于\(1\)，又等于\(0\))

若上述条件不成立是否一定有解？

构造：按照任意顺序枚举所有\(x_i\)
用\(tarjan\)算法缩点成一个\(DAG\), 然后拓扑排序，在合法与非法中选择拓扑序编号更靠后的一个。

为什么此构造成立？

• 对于每一个\(x_i\)，只有一种值。
• 对于每一个强联通分量，如果选了其中的一个点，则其中所有点都被选了，即要选都选，要不选都不选。还存在一个强连通分量与之所有成分都相反，成对出现。（原命题和逆否命题等价）
• 对于条件\(a \cup b\)，假设\(a = 0\)，则\(a\)的拓扑序更靠前，则\(-a \rightarrow b\)，故\(b\)所在强连通分量更靠后\(，b\)一定取\(1\)，由对称性，反之亦成立。

故成立。

细节问题

满足需求不同形式的实现：

• \(a \cup b \Leftrightarrow -a \rightarrow b \Leftrightarrow -b \rightarrow a\)

• \(a \rightarrow b \Leftrightarrow -a \cup b\)

• \(a = 1 \Leftrightarrow a \cup a\)

code 略

标签：cup,int,笔记,stk,学习,low,Leftrightarrow,SAT,rightarrow
From： https://www.cnblogs.com/sunruize/p/17018525.html