けんちょんの競プロ精進記録

競プロの精進記録や小ネタを書いていきます

JOI 二次予選 2021 E - スパイ 2 (AOJ ????, 難易度 10)

面白かった。

問題概要

 N 人がいて、それぞれ「スパイ」か「非スパイ」かのどちらかである。 N 人のうち、何人かについてはスパイかどうかが予めわかっている ( T_{1}, \dots, T_{N} で与えられる)。

 M 個の証言がある。各証言は人  A_{i} が証言者によってなされ、「人  B_{i} はスパイである」かつ「人  C_{i} はスパイではない」というものである。

 A_{i} がスパイである場合は、「人  B_{i} はスパイである」かつ「人  C_{i} はスパイではない」のうちの少なくとも一方は虚偽の情報である。 A_{i} がスパイでない場合は、証言の真偽は不明である。

これらの情報が整合するように、 N 人それぞれが「スパイ」か「非スパイ」であるかどうかを特定せよ。解なしである場合は -1 を出力せよ。

制約

  •  1 \le N, M \le 3 \times 10^{5}

考えたこと

見た感じ SAT っぽいと思った。つまり

 \lnot A_{i} \lor \lnot B_{i} \lor C_{i}

を一つの closure とした 3-SAT になる。ただしいくつかのリテラルについてはすでに真偽が割り当てられているという状態だ。3-SAT になるので、一瞬解けない気持ちになった (3-SAT は一般には NP-Hard で解けない)。

まずは、真偽値が確定するところを確定させてしまうことを考えた。たとえば、closure の 3 個のリテラルのうち、2 個が確定していたら

  • その closure がすでに True になる
  • 残りの 1 個のリテラルの真偽が確定する

のどちらかになる (リテラルのうち 3 個が確定していて False の場合は解なし確定)。そしてリテラルの真偽が新たに確定すれば、他の closure によって新たに別のリテラルの真偽が確定したりする。

このような連鎖的な状況を扱うためには、queue を用いた後退解析と相性がいい。queue を用いた後退解析で解ける問題の代表例は「グラフの閉路検出」である。具体的には葉を queue に push して、queue から頂点を取り出して除去して、それによって新たに葉が生じたらまた queue に push して...というのを繰り返すアルゴリズムだ。問題例は以下。

drken1215.hatenablog.com

そして queue が空になったときには、「すでに矛盾が生じている」 or 「各節のリテラルの個数が 3 個以下の SAT が残る」という状態になる。この最後に残った SAT をどう解いたらよいか?

実は、この最後に残った SAT には、ある特異的な性質があることがわかってきた。それは、どの節にもからなず  \lnot X という形をしたリテラルがあるということだ。なぜなら、もとの 3-SAT は

どの closure も  \lnot のついていないリテラルはただ 1 個だけ

という性質を満たしている。よって、もし後退解析後に  \lnot X という形をしたリテラルを含まない closure があると仮定すると、そのような closure ではすでに「矛盾が生じる」or「True が確定する」or「 \lnot のついていないリテラルの真偽は確定する」という状態になっているはずなのだ。

以上から、queue を用いた後退解析後には、どの closure にも  \lnot のついたリテラルがあることがわかった。よって、この時点で真偽の確定していないリテラルはすべて False にすれば、すべての closure を True にすることができる!!!

コード

後退解析を素朴に実装すれば、計算量は  O(N + M) となる。

#include <bits/stdc++.h>
using namespace std;
using pint = pair<int,int>;

int main() {
    int N, M;
    cin >> N >> M;
    vector<int> T(N), A(M), B(M), C(M);
    for (int i = 0; i < N; ++i) cin >> T[i];
    for (int i = 0; i < M; ++i) cin >> A[i] >> B[i] >> C[i], --A[i], --B[i], --C[i];

    auto solve = [&]() -> bool {
        vector<vector<int>> where(N);
        vector<int> isok(M, false);
        queue<int> que;

        // リテラルを処理
        auto treat_closure = [&](int i) -> bool {
            int a = A[i], b = B[i], c = C[i];
            
            // すでに矛盾があったらダメ
            if (T[a] == 1 && T[b] == 1 && T[c] == 2) return false;

            // すでに確定 or 残りのリテラルが確定
            if (T[a] == 2 || T[b] == 2 || T[c] == 1) isok[i] = true;
            else {
                if (T[b] == 1 && T[c] == 2) T[a] = 2, que.push(a), isok[i] = true;
                if (T[c] == 2 && T[a] == 1) T[b] = 2, que.push(b), isok[i] = true;
                if (T[a] == 1 && T[b] == 1) T[c] = 1, que.push(c), isok[i] = true;
            }
            return true;
        };
        
        for (int i = 0; i < M; ++i) {
            // 節 i を処理
            if (!treat_closure(i)) return false;

            // 各リテラルをもつ節を格納
            if (!isok[i]) {
                where[A[i]].push_back(i);
                where[B[i]].push_back(i);
                where[C[i]].push_back(i);
            }
        }

        // 後退解析
        while (!que.empty()) {
            auto x = que.front();
            que.pop();
            for (auto id: where[x]) if (!treat_closure(id)) return false;
        }

        // 残りのリテラルはすべて false でよい (すべての節に not リテラルがあるため)
        for (int i = 0; i < N; ++i) if (T[i] == 3) T[i] = 2;
        return true;
    };
    
    if (!solve()) cout << -1 << endl;
    else for (int i = 0; i < N; ++i) cout << T[i] << endl;
}