2-SAT

2-SAT

给 $n$ 个命题,Each proposition has only two variables,Each variable is either $1$(真) 要么是 $0$(假).

Ask if there are valid constructs such that the AND of all propositions holds.

1. $a\to b*\neg a\vee b$ ($\to$ is implication,若 p 则 q的意思)
2. $a\to b*\neg b\to \neg a$ (原命题和逆否命题等价)
3. $x$ 和 $\neg x$ 在同一个 SCC 中 无解.（3is a necessary condition for a solution）
4. If the above conditions are met,There must be a solution？（证明充分性）
   1. 答案：一定有.
   2. 发现,如果有 $a\to x_1\to x_2\to ...\to b$ , $b\to y_1\to y_2\to ...\to a$ .Then according to the inverse negative proposition there must be：$\neg a\leftarrow x_1\leftarrow x_2\leftarrow ...\leftarrow \neg b$ , $\neg b\leftarrow y_1\leftarrow y_2\leftarrow ...\leftarrow \neg a$ .所以如果 $a,b$ 在同一个 SCC 中,$\neg a,\neg b$ Must be the same SCC 中.
   3. 每个 SCC The variables in either are selected,要么都不选.每个SCCThere must be a counterpart to himSCC.
   4. 构造方式：先 tarjan 缩点,进行拓扑排序,For both cases of a variable,Take the one that is further back.

Summary of propositional conditions：

1. $a\vee b*\neg a\to b*\neg b\to a$
2. $a\to b*\neg a\vee b*\neg b\vee a$
3. $a=1*a\vee a$
4. $a=0*\neg a\vee \neg a$

way of connecting：

1. i 对应 i+n , in the template title：

while (m -- )
{
    
    int i, a, j, b;
    scanf("%d%d%d%d", &i, &a, &j, &b);
    // i,i+n ; j,j+n
    add(i + n * (a & 1), j + n * (b ^ 1));
    add(j + n * (b & 1), i + n * (a ^ 1));
}

2. 2 * i 为真,2 * i + 1是假

add(2 * i + !a, 2 * j + b);
add(2 * j + !b, 2 * i + a);

因为tarjan得到的idis topological inversion,Finally, the forward order traversal will do.

#include <iostream>
#include <cstring>
#include <algorithm>
#include <cstdio>

using namespace std;

const int N = 2000010, M = 2000010;

int n, m;
int h[N], e[M], ne[M], idx;
int dfn[N], low[N], ts, stk[N], top;
int id[N], cnt;
bool ins[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] = ++ ts;
    stk[ ++ top] = u, ins[u] = true;
    for (int i = h[u]; ~i; i = ne[i])
    {
    
        int j = e[i];
        if (!dfn[j])
        {
    
            tarjan(j);
            low[u] = min(low[u], low[j]);
        } else if (ins[j]) low[u] = min(low[u], dfn[j]);
    }

    if (low[u] == dfn[u])
    {
    
        int y;
        cnt ++ ;
        do
        {
    
            y = stk[top -- ], ins[y] = false, id[y] = cnt;
        } while (y != u);
    }
}

int main()
{
    
    scanf("%d%d", &n, &m);
    memset(h, -1, sizeof h);

    while (m -- )
    {
    
        int i, a, j, b;
        scanf("%d%d%d%d", &i, &a, &j, &b);
        // i,i+n ; j,j+n
        add(i + n * (a & 1), j + n * (b ^ 1));
        add(j + n * (b & 1), i + n * (a ^ 1));
    }

    for (int i = 1; i <= n * 2; i ++ )
        if (!dfn[i])
            tarjan(i);

    for (int i = 1; i <= n; i ++ )
        if (id[i] == id[i + n])
        {
    
            puts("IMPOSSIBLE");
            return 0;
        }

    puts("POSSIBLE");
    for (int i = 1; i <= n; i ++ )
        if (id[i] < id[i + n]) printf("1 ");
        else printf("0 ");

    return 0;
}