[学习笔记] 2-SAT

1. 拆点 : 将每个 bool 变量拆成 0, 1 两个点.

2. 连边 : 将限制条件转化为连边.

3. 图是 DAG 时, 对于每个 bool 变量, 合法点的拓扑序大于非法点.

   证明 : 若某个 bool 变量拆分成的两个点为 u,v , 若 u 为非法点, 则存在一条从 u 到 v 的路径, 所以 v 的拓扑序一定大于 u 的拓扑序.

4. 当图不是 DAG 时, 用 Tarjan 算法将强联通分量缩成一个点, 把原图变为 DAG.

5. Tarjan 求完强联通分量后不用缩点, 判断两个点所属的强联通分量序号即可, 序号小的为合法点.

   证明 : 根据 Tarjan 求强联通分量的过程可知, 若存在一条从点 u 到点 v 的路径, 则 v 所属的强联通分量一定会在 u 所属的强联通分量之前被统计到, 所以点 v 所属的强联通分量序号更小.

6. 当一个 bool 变量拆分成的两个点在同一个强联通分量里, 则无解.

7. 输出方案时，选择 scc 编号较小的那个点，且不需要从它开始 Dfs 把它所连的点选中，这样不会产生矛盾。

   证明：

   假设变量 (n) 的两个点 (x,y) 的 (scc) 编号分别为 (a,b (a < b))，若 (x) 连向点 (x')，则必定会有一条边从 (y') 连向 (y)，

   设 (x',y') 的 (scc) 编号分别为 (c,d)，则有 (c < a, b < d)（由第5点可以得到），

   又因为 (a<b)，所以 (c<d)，所以 (x') 点一定会被选到。

【模板】2-SAT 问题

#include <cstdio>
#include <iostream>

using namespace std;

const int _ = 2e6 + 7;

int n, m, dfn[_], low[_], cnt, stk[_], top, scc[_], num;
bool vis[_], b[_];
int lst[_], nxt[_], to[_], tot;

int gi() {
  int x = 0; char c = getchar();
  while (!isdigit(c)) c = getchar();
  while (isdigit(c)) x = (x << 3) + (x << 1) + c - '0', c = getchar();
  return x;
}

void Add(int x, int y) { nxt[++tot] = lst[x]; to[tot] = y; lst[x] = tot; }

void Tarjan(int u) {
  dfn[u] = low[u] = ++cnt, stk[++top] = u, b[u] = 1;
  for (int i = lst[u]; i; i = nxt[i]) {
    if (!dfn[to[i]]) Tarjan(to[i]);
    if (b[to[i]]) low[u] = min(low[u], low[to[i]]);
  }
  if (low[u] == dfn[u]) {
    scc[u] = ++num, b[u] = 0;
    while (stk[top] != u) scc[stk[top]] = num, b[stk[top]] = 0, --top;
    --top;
  }
}

void Dfs(int u) {
  vis[u] = 1;
  for (int i = lst[u]; i; i = nxt[i])
    if (!vis[to[i]]) Dfs(to[i]);
}

int main() {
  n = gi(), m = gi();
  for (int i = 1, x, y, a, b; i <= m; ++i) {
    x = gi(), a = gi(), y = gi(), b = gi();
    Add(x + (!a) * n, y + b * n);
    Add(y + (!b) * n, x + a * n);
  }
  for (int i = 1; i <= n + n; ++i)
    if (!dfn[i]) Tarjan(i);
  for (int i = 1; i <= n; ++i) {
    if (scc[i] == scc[i + n]) { puts("IMPOSSIBLE"); return 0; }
    if (vis[i] or vis[i + n]) continue;
    scc[i] < scc[i + n] ? vis[i] = 1 : vis[i + n] = 1;
    //Dfs(scc[i] < scc[i + n] ? i : i + n); 	// 不需要 DFS，直接选择 scc 较小的点即可。
  }
  puts("POSSIBLE");
  for (int i = 1; i <= n; ++i) printf("%d ", vis[i] ? 0 : 1);
  putchar('
');
  return 0;
}