2-SATと強連結成分分解

ふと2-SATの事が気になって、復習がてらPractice RoomでSRM464のDiv1 Medium問題を開いてみた。（ちなみにSRM464には出場している）

SAT (充足可能性問題, SATisfiability problem) についてはここの読者の皆さんはご存知とは思います。NP完全問題でおなじみのあれです

(x_0 ∨ ¬x_1) ∧ (¬x_0 ∨ ¬x_3) ∧ ...
みたいな論理式（乗法標準形）を満たす真偽値 x_0, x_1, ... の組み合わせが存在するか否か。（存在する場合、その組み合わせを知りたかったりする）

上の例ではすべての節が(高々)2変数なので2-SATと呼ばれる。
（2-SATは線形時間で解けるらしい）。

• 論理和 x ∨ y が論理包含 ¬x⇒y （または ¬y⇒x）に書き換え可能なことを利用して、論理式を有向グラフに変換してみたり
• 出来上がったdagを強連結成分分解してみる
• 同じ強連結成分に含まれるノード（が表すリテラル、すなわちxなり¬yなり）は同じ真偽値をもつ。ということは、xと¬xが同じ強連結成分に含まれたらアウト。

2-SATも強連結成分分解も、蟻本§4-3「グラフマスターへの道」(p.285〜) で解説されている（のを以前読んだがすっかり忘れている。p.286のグラフをノートに書いてscc()を手動トレースして一度は納得したはずなのだが）。

プログラミングコンテストチャレンジブック [第2版]　～問題解決のアルゴリズム活用力とコーディングテクニックを鍛える～

posted with amazlet at 13.07.13

秋葉拓哉 岩田陽一 北川宜稔
マイナビ
売り上げランキング: 40,311

Amazon.co.jpで詳細を見る

参考

• 2-SATを解いた時のメモ - TopCoderとJ言語と時々F# (JAPLJさん)
• TopCoder SRM 464 Div1 Medium ColorfulDecoration - simezi_tanの日記
• SRM 464 500pt： ColorfulDecoration - komiyamの日記
• http://d.hatena.ne.jp/tomiflu/20121219/1355917871%E2%80%8E:2-SAT - Win The Game
• 2SAT - yasu0207の日記

Medium ("ColorfulDecoration", 550)

この問題で何が x ∨ y にあたるのか思いつかない…orz

http://d.hatena.ne.jp/komiyam/20110925/1316920692 を見たら、
「x と y が共存できない」¬(x ∧ y) が ¬x ∨ ¬y に等しいことを利用すればいいらしい。

するとこれは 「x⇒¬y かつ y⇒¬x」に書き直すことができる。

書いてみたコード

• 強連結成分分解ではなく、x から ¬x に行く経路（とその逆）が存在するかをWFで求めている。O(n^3)ですけど。
• passed system test

#include <vector>
using namespace std;

#define rep(var,n)  for(int var=0;var<(n);++var)
#define all(c)  (c).begin(),(c).end()
#define tr(i,c)  for(typeof((c).begin()) i=(c).begin(); i!=(c).end(); ++i)
#define mid(x,y) ((x)+((y)-(x))/2)
#define ev(v1,v2,n) for(int v1=0;v1<(n)-1;++v1)for(int v2=v1+1;v2<(n);++v2)

vector<int> xa_, ya_, xb_, yb_;
vector<vector<int> > arc;
int n;

inline bool intersects(int xi, int yi, int xj, int yj, int d){
  int dx = abs(xi - xj), dy = abs(yi - yj);
  return (dx < d && dy < d);
}

inline void add_edge(int i, int j) {
  // ¬(i ∧ j)
  // ¬i ∨ ¬j
  // (i ⇒ ¬j) かつ (j ⇒ ¬i)
  arc[i][j<n ? j+n : j-n] = 1;
  arc[j][i<n ? i+n : i-n] = 1;
}

bool po(int d){
  if (d == 0) return true;

  arc.assign(n*2, vector<int>(n*2, 10000));
  rep(i,n*2) arc[i][i] = 0;

  ev(i,j,n) {
    if (intersects(xa_[i],ya_[i], xa_[j],ya_[j], d)) { // i && j が駄目
      add_edge(i, j);
    }
    if (intersects(xa_[i],ya_[i], xb_[j],yb_[j], d)) { // i && ¬j が駄目
      add_edge(i, n+j);
    }
    if (intersects(xb_[i],yb_[i], xa_[j],ya_[j], d)) { // ¬i && j が駄目
      add_edge(n+i, j);
    }
    if (intersects(xb_[i],yb_[i], xb_[j],yb_[j], d)) { // ¬i && ¬j が駄目
      add_edge(n+i, n+j);
    }
  }

  rep(k,n*2) rep(i,n*2) rep(j,n*2){
    arc[i][j] = min(arc[i][j], arc[i][k] + arc[k][j]);
  }

  rep(i, n) {
    if (arc[i][n+i] < 10000 && arc[n+i][i] < 10000) return false;
  }

  return true;
}

class ColorfulDecoration {
 public:
  int getMaximum(vector<int> xa, vector<int> ya, vector<int> xb, vector<int> yb) {
    n = xa.size();
    xa_ = xa; ya_ = ya; xb_ = xb; yb_ = yb;

    int lo = 0, hi = INT_MAX;
    while (true) {
      int mi = mid(lo, hi);
      if (mi == lo) break;
      if (po(mi))
        lo = mi;
      else
        hi = mi;
    }
    return lo;
  }
};

さて。
強連結成分分解をちゃんとやってみよう。

dagの強連結な部分集合：「有向グラフの部分集合のうち、それに含まれる任意の2頂点u, vを取った時 uからvへ辿り着く有向路が存在する」
強連結成分：強連結な部分集合のうち、これ以上頂点を付け足したら強連結でなくなってしまうもの

最大クリーク（無向グラフで、あらゆる2つの頂点を繋ぐ辺が存在する集合（＝クリーク）のうち、これ以上頂点を付け足したらクリークでなくなってしまうもの）に似ている。

vector<vector<int> > arc;
vector<vector<int> > arc_r;
vector<int> cmp; // 属する強連結成分の、グラフ全体におけるトポロジカル順序

vector<bool> visited;
vector<int> vs; // post-order

void dfs(int v) {
  visited[v] = true;
  tr(it, arc[v]) {
    if (!visited[*it]) dfs(*it);
  }
  vs.push_back(v); // 帰りがけにvを記録。グラフの末端に近いものから並ぶ
}
void rdfs(int v, int k) {
  visited[v] = true;
  cmp[v] = k;
  tr(it, arc_r[v]) {
    if (!visited[*it]) rdfs(*it, k);
  }
}

int scc() { // 強連結成分分解
  vs.clear();

  visited.assign(n*2, false);
  rep(i,n*2) {
    if (!visited[i]) dfs(i);
  }

  visited.assign(n*2, false);
  int k=0;
  reverse(all(vs)); // グラフの末端から遠いものから始めたい
  tr(it, vs) {
    if (!visited[*it]) rdfs(*it, k++);
  }
  return k;
}

bool po(int d){
  if (d == 0) return true;

  arc.assign(n*2, vector<int>());
  arc_r.assign(n*2, vector<int>()); // 追加
  cmp.assign(n*2, -1); // 追加

  ev(i,j,n) {
    if (intersects(xa_[i],ya_[i], xa_[j],ya_[j], d)) {
    ...
  }

  scc(); // 強連結成分分解

  rep(i, n) {
    // x と¬x が同じ強連結成分に属してしまったらアウト
    if (cmp[i] == cmp[n+i]) return false;
  }

  /* 
  // 式を満たす具体的な真偽値を求める方法。
  //「 x を含む強連結成分のトポロジカル順序 cmp[x] が、¬x を含む強連結成分のトポロジカル順序 cmp[¬x] よりも後ろ」⇔「xは真」
  vector<bool> ans(n);
  rep(i, n) {
    ans[i] = (cmp[i] > cmp[n+i]);
  }
  cout << ans << endl;
  */

  return true;
}