2-SAT

SAT 是適定性（Satisfiability）問題的簡稱。一般形式為 k - 適定性問題，簡稱 k-SAT。而當 \(k>2\) 時該問題為 NP 完全的。所以我們只研究 \(k=2\) 的情況。

定義

2-SAT，簡單的説就是給出 \(n\) 個集合，每個集合有兩個元素，已知若干個 \(\langle a,b \rangle\)，表示 \(a\) 與 \(b\) 矛盾（其中 \(a\) 與 \(b\) 屬於不同的集合）。然後從每個集合選擇一個元素，判斷能否一共選 \(n\) 個兩兩不矛盾的元素。顯然可能有多種選擇方案，一般題中只需要求出一種即可。

現實意義

比如邀請人來吃喜酒，夫妻二人必須去一個，然而某些人之間有矛盾（比如 A 先生與 B 女士有矛盾，C 女士不想和 D 先生在一起），那麼我們要確定能否避免來人之間有矛盾，有時需要方案。這是一類生活中常見的問題。

使用布爾方程表示上述問題。設 \(a\) 表示 A 先生去參加，那麼 B 女士就不能參加（\(\neg a\)）；\(b\) 表示 C 女士參加，那麼 \(\neg b\) 也一定成立（D 先生不參加）。總結一下，即 \((a \vee b)\)（變量 \(a, b\) 至少滿足一個）。對這些變量關係建有向圖，則有：\(\neg a\to b\wedge\neg b\to a\)（\(a\) 不成立則 \(b\) 一定成立；同理，\(b\) 不成立則 \(a\) 一定成立）。建圖之後，我們就可以使用縮點算法來求解 2-SAT 問題了。

常用解決方法

Tarjan SCC 縮點

算法考究在建圖這點，我們舉個例子來講：

假設有 \({a1,a2}\) 和 \({b1,b2}\) 兩對，已知 \(a1\) 和 \(b2\) 間有矛盾，於是為了方案自洽，由於兩者中必須選一個，所以我們就要拉兩條有向邊 \((a1,b1)\) 和 \((b2,a2)\) 表示選了 \(a1\) 則必須選 \(b1\)，選了 \(b2\) 則必須選 \(a2\) 才能夠自洽。

然後通過這樣子建邊我們跑一遍 Tarjan SCC 判斷是否有一個集合中的兩個元素在同一個 SCC 中，若有則輸出不可能，否則輸出方案。構造方案只需要把幾個不矛盾的 SCC 拼起來就好了。

輸出方案時可以通過變量在圖中的拓撲序確定該變量的取值。如果變量 \(x\) 的拓撲序在 \(\neg x\) 之後，那麼取 \(x\) 值為真。應用到 Tarjan 算法的縮點，即 \(x\) 所在 SCC 編號在 \(\neg x\) 之前時，取 \(x\) 為真。因為 Tarjan 算法求強連通分量時使用了棧，所以 Tarjan 求得的 SCC 編號相當於反拓撲序。

顯然地，時間複雜度為 \(O(n+m)\)。

暴搜

就是沿着圖上一條路徑，如果一個點被選擇了，那麼這條路徑以後的點都將被選擇，那麼，出現不可行的情況就是，存在一個集合中兩者都被選擇了。

那麼，我們只需要枚舉一下就可以了，數據不大，答案總是可以出來的。

暴搜模板

// 來源：劉汝佳白書第 323 頁
struct Twosat {
  int n;
  vector<int> g[maxn * 2];
  bool mark[maxn * 2];
  int s[maxn * 2], c;

  bool dfs(int x) {
    if (mark[x ^ 1]) return false;
    if (mark[x]) return true;
    mark[x] = true;
    s[c++] = x;
    for (int i = 0; i < (int)g[x].size(); i++)
      if (!dfs(g[x][i])) return false;
    return true;
  }

  void init(int n) {
    this->n = n;
    for (int i = 0; i < n * 2; i++) g[i].clear();
    memset(mark, 0, sizeof(mark));
  }

  void add_clause(int x, int y) {  // 這個函數隨題意變化
    g[x].push_back(y ^ 1);         // 選了 x 就必須選 y^1
    g[y].push_back(x ^ 1);
  }

  bool solve() {
    for (int i = 0; i < n * 2; i += 2)
      if (!mark[i] && !mark[i + 1]) {
        c = 0;
        if (!dfs(i)) {
          while (c > 0) mark[s[--c]] = false;
          if (!dfs(i + 1)) return false;
        }
      }
    return true;
  }
};

例題

HDU3062 Party

題面：有 n 對夫妻被邀請參加一個聚會，因為場地的問題，每對夫妻中只有 \(1\) 人可以列席。在 \(2n\) 個人中，某些人之間有着很大的矛盾（當然夫妻之間是沒有矛盾的），有矛盾的 \(2\) 個人是不會同時出現在聚會上的。有沒有可能會有 \(n\) 個人同時列席？

這是一道多校題，裸的 2-SAT 判斷是否有方案，按照我們上面的分析，如果 \(a1\) 中的丈夫和 \(a2\) 中的妻子不合，我們就把 \(a1\) 中的丈夫和 \(a2\) 中的丈夫連邊，把 \(a2\) 中的妻子和 \(a1\) 中的妻子連邊，然後縮點染色判斷即可。

參考代碼

#include <algorithm>
#include <cstdio>
#include <cstring>
#include <iostream>
#define maxn 2018
#define maxm 4000400
using namespace std;
int Index, instack[maxn], DFN[maxn], LOW[maxn];
int tot, color[maxn];
int numedge, head[maxn];

struct Edge {
  int nxt, to;
} edge[maxm];

int sta[maxn], top;
int n, m;

void add(int x, int y) {
  edge[++numedge].to = y;
  edge[numedge].nxt = head[x];
  head[x] = numedge;
}

void tarjan(int x) {  // 缩点看不懂请移步强连通分量上面有一个链接可以点。
  sta[++top] = x;
  instack[x] = 1;
  DFN[x] = LOW[x] = ++Index;
  for (int i = head[x]; i; i = edge[i].nxt) {
    int v = edge[i].to;
    if (!DFN[v]) {
      tarjan(v);
      LOW[x] = min(LOW[x], LOW[v]);
    } else if (instack[v])
      LOW[x] = min(LOW[x], DFN[v]);
  }
  if (DFN[x] == LOW[x]) {
    tot++;
    do {
      color[sta[top]] = tot;  // 染色
      instack[sta[top]] = 0;
    } while (sta[top--] != x);
  }
}

bool solve() {
  for (int i = 0; i < 2 * n; i++)
    if (!DFN[i]) tarjan(i);
  for (int i = 0; i < 2 * n; i += 2)
    if (color[i] == color[i + 1]) return 0;
  return 1;
}

void init() {
  top = 0;
  tot = 0;
  Index = 0;
  numedge = 0;
  memset(sta, 0, sizeof(sta));
  memset(DFN, 0, sizeof(DFN));
  memset(instack, 0, sizeof(instack));
  memset(LOW, 0, sizeof(LOW));
  memset(color, 0, sizeof(color));
  memset(head, 0, sizeof(head));
}

int main() {
  while (~scanf("%d%d", &n, &m)) {
    init();
    for (int i = 1; i <= m; i++) {
      int a1, a2, c1, c2;
      scanf("%d%d%d%d", &a1, &a2, &c1, &c2);  // 自己做的时候别用 cin 会被卡
      add(2 * a1 + c1, 2 * a2 + 1 - c2);
      // 对于第 i 对夫妇，我们用 2i+1 表示丈夫，2i 表示妻子。
      add(2 * a2 + c2, 2 * a1 + 1 - c1);
    }
    if (solve())
      printf("YES\n");
    else
      printf("NO\n");
  }
  return 0;
}

2018-2019 ACM-ICPC Asia Seoul Regional K TV Show Game

題面：有 \(k(k>3)\) 盞燈，每盞燈是紅色或者藍色，但是初始的時候不知道燈的顏色。有 \(n\) 個人，每個人選擇 3 盞燈並猜燈的顏色。一個人猜對兩盞燈或以上的顏色就可以獲得獎品。判斷是否存在一個燈的着色方案使得每個人都能領獎，若有則輸出一種燈的着色方案。

這道題在判斷是否有方案的基礎上，在有方案時還要輸出一個可行解。

根據 伍昱 -《由對稱性解 2-sat 問題》，我們可以得出：如果要輸出 2-SAT 問題的一個可行解，只需要在 tarjan 縮點後所得的 DAG 上自底向上地進行選擇和刪除。

具體實現的時候，可以通過構造 DAG 的反圖後在反圖上進行拓撲排序實現；也可以根據 tarjan 縮點後，所屬連通塊編號越小，節點越靠近葉子節點這一性質，優先對所屬連通塊編號小的節點進行選擇。

下面給出第二種實現方法的代碼。

參考代碼

#include <bits/stdc++.h>
using namespace std;
const int maxn = 1e4 + 5;
const int maxk = 5005;

int n, k;
int id[maxn][5];
char s[maxn][5][5], ans[maxk];
bool vis[maxn];

struct Edge {
  int v, nxt;
} e[maxn * 100];

int head[maxn], tot = 1;

void addedge(int u, int v) {
  e[tot].v = v;
  e[tot].nxt = head[u];
  head[u] = tot++;
}

int dfn[maxn], low[maxn], color[maxn], stk[maxn], ins[maxn], top, dfs_clock, c;

void tarjan(int x) {  // tarjan算法求强联通
  stk[++top] = x;
  ins[x] = 1;
  dfn[x] = low[x] = ++dfs_clock;
  for (int i = head[x]; i; i = e[i].nxt) {
    int v = e[i].v;
    if (!dfn[v]) {
      tarjan(v);
      low[x] = min(low[x], low[v]);
    } else if (ins[v])
      low[x] = min(low[x], dfn[v]);
  }
  if (dfn[x] == low[x]) {
    c++;
    do {
      color[stk[top]] = c;
      ins[stk[top]] = 0;
    } while (stk[top--] != x);
  }
}

int main() {
  scanf("%d %d", &k, &n);
  for (int i = 1; i <= n; i++) {
    for (int j = 1; j <= 3; j++) scanf("%d%s", &id[i][j], s[i][j]);

    for (int j = 1; j <= 3; j++) {
      for (int k = 1; k <= 3; k++) {
        if (j == k) continue;
        int u = 2 * id[i][j] - (s[i][j][0] == 'B');
        int v = 2 * id[i][k] - (s[i][k][0] == 'R');
        addedge(u, v);
      }
    }
  }

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

  for (int i = 1; i <= 2 * k; i += 2)
    if (color[i] == color[i + 1]) {
      puts("-1");
      return 0;
    }

  for (int i = 1; i <= 2 * k; i += 2) {
    int f1 = color[i], f2 = color[i + 1];
    if (vis[f1]) {
      ans[(i + 1) >> 1] = 'R';
      continue;
    }
    if (vis[f2]) {
      ans[(i + 1) >> 1] = 'B';
      continue;
    }
    if (f1 < f2) {
      vis[f1] = 1;
      ans[(i + 1) >> 1] = 'R';
    } else {
      vis[f2] = 1;
      ans[(i + 1) >> 1] = 'B';
    }
  }
  ans[k + 1] = 0;
  printf("%s\n", ans + 1);
  return 0;
}

練習題

洛谷 P5782 和平委員會

POJ3683 牧師忙碌日

---

本页面最近更新：，更新历史
发现错误？想一起完善？ 在 GitHub 上编辑此页！
本页面贡献者：OI-wiki
本页面的全部内容在 CC BY-SA 4.0 和 SATA 协议之条款下提供，附加条款亦可能应用