UVALive 3713 Astronauts：2-SAT 模型解決任務分配

問題建模為 2-SAT

n 個宇航員，每人必須分配到 A、B、C 三種任務之一。約束條件：
- 年齡 ≥ 平均年齡 → 可做 A 或 C
- 年齡 < 平均年齡 → 可做 B 或 C
- 討厭關系：某些人不能分配到同一任務

變量設計

每人一個布爾變量 x_i：
- 年齡 ≥ 平均：x_i = true → 任務 A，false → 任務 C
- 年齡 < 平均：x_i = true → 任務 B，false → 任務 C
每人必須且只能選一個任務 → 天然符合 2-SAT「二選一」模型。

約束轉化為蕴含圖邊

• 討厭關系 (u, v) 不能同任務：
  若 u、v 年齡類別相同（都≥或都<）：
  u 選 A → v 不能選 A → v 選 C，即 u_true → v_false
  同理 v_true → u_false
  兩人類別不同：任務集合不重疊，無衝突
• 必須選一個：
  u_false → u_true 和 u_true → u_false（互斥）
  實際上通過「至少選一」+「最多選一」建模，但在 2-SAT 中通常只加互斥邊，賦值階段保證至少一個

Tarjan SCC 求解可行性

struct Edge { int u, v, next; } ed[MAXE];
int head[MAXV], dfn[MAXV], low[MAXV], stk[MAXV], belong[MAXV];
int idx, top, cnt, tot;
bool instack[MAXV];

void add_edge(int u, int v) {
    ed[tot] = {u, v, head[u]};
    head[u] = tot++;
}

void tarjan(int u) {
    dfn[u] = low[u] = ++idx;
    instack[u] = true; stk[++top] = u;
    for (int i = head[u]; ~i; i = ed[i].next) {
        int v = ed[i].v;
        if (dfn[v] == -1) {
            tarjan(v);
            low[u] = min(low[u], low[v]);
        } else if (instack[v]) {
            low[u] = min(low[u], dfn[v]);
        }
    }
    if (dfn[u] == low[u]) {
        cnt++;
        do {
            int v = stk[top--];
            instack[v] = false;
            belong[v] = cnt;
        } while (v != u);
    }
}

bool check_sat() {
    // 建圖...
    for (int i = 0; i < 2*n; i++) if (dfn[i] == -1) tarjan(i);
    for (int i = 0; i < 2*n; i += 2)
        if (belong[i] == belong[i^1]) return false; // 矛盾
    return true;
}

拓撲序賦值構造任意可行解

void solve() {
    // 建立縮點 DAG 的入度
    for (int i = 0; i < tot; i++) {
        int u = belong[ed[i].u], v = belong[ed[i].v];
        if (u != v) { add_dag_edge(v, u); in_deg[u]++; }
    }
    
    // 互斥對應關系
    for (int i = 0; i < 2*n; i++) opp[belong[i]] = belong[i^1];
    
    // 拓撲序 BFS
    queue q;
    for (int i = 1; i <= cnt; i++) if (!in_deg[i]) q.push(i);
    
    while (!q.empty()) {
        int u = q.front(); q.pop();
        if (!color[u]) {
            color[u] = 1;      // 當前分量為 true
            color[opp[u]] = 2; // 互斥分量為 false
        }
        for (int i = dag_head[u]; ~i; i = dag_ed[i].next) {
            int v = dag_ed[i].v;
            if (--in_deg[v] == 0) q.push(v);
        }
    }
    
    // 輸出任務
    for (int i = 0; i < 2*n; i += 2) {
        if (color[belong[i]] == 1) {
            if (type[i] == 1) puts("A"); else puts("B");
        } else puts("C");
    }
}

關鍵點總結

• 變量編碼：每人兩個字面量（i, i^1），按年齡類別映射到 A/B/C
• 衝突邊：同年齡類別的討厭關系產生互斥蕴含
• 可行性判斷：SCC 中檢查變量與其否定是否在同一強連通分量
• 構造解：縮點 DAG 拓撲序賦值，先處理的分量設為 true，其互斥設為 false

2-SAT 是解決「二選一約束」問題的利器，Tarjan SCC + 拓撲賦值是標準解法框架。