ICFPC 2025 では、チーム Unagi は全問題を SAT Solver で解いた。他チームも SAT Solver を使っていたが、Encoding 方法の違いで大きな差が出たように思う。本記事では、その Encoding の違いによる実行速度の差を検証する。
問題概要
Lightning
N 部屋が通路でつながった無向グラフがある。各部屋には 0−5 の連番が振られた 6 個のドアがあり、ドア間が通路でつながっている。また、各部屋は 0-3 の色が塗られている。
グラフの構造は未知であり、以下のクエリによって構造を高確率で特定したい。(どのようなクエリを行っても同じ結果が返ってくるようなグラフを答えると AC となる)
クエリとして、長さ 18N の [0,5] 列を与える。始点から開始し、対応する番号のドアを順に開ける。訪れた部屋の色を順に並べた長さ 18N+1 の [0,3] 列が得られる。
Full
D=2 or 3 に対し、グラフは以下のようにして N/D 部屋の未知の無向グラフ (base graph) を D 倍にコピーしたもの(それぞれレイヤー1, ..., レイヤーDと呼ぶことにする)であることがわかっている。base graph の部屋 u から u1, ..., uD の D 部屋が作られ、base graph において u のドア e と v のドア f がつながっているならば、各 ui のドア e はどれかの vj のドア f とつながっている。
コピーされた部屋は理論的に区別不能であるため、区別を可能にする仕組みとして、移動しながら部屋の色を変更できるようになっている。
長さ 6N のクエリを出来るだけ少ない数一気に投げてグラフを完全に特定せよ。
SAT Encoding
Fullの解法は主に以下の2通りがある。
二段階方針
色を塗らないクエリを用い、base graph の特定を lightning と同じ方法で行う。次に、特定した base graph が正しいと仮定して、色を塗りながらの移動によりコピーの区別を行う。Unagi は (D=2,N=60) と (D=3, N>=36) に対してこの解法を使用した。Unagi は前半パート・後半パートともに SAT Solver を用いたが、他のチームによると前半パートは SAT Solver ではなく焼き鈍しを用いた方がかなり高速だったらしい。
一発方針
全体を一つのCNFとして表現し、SAT solver 一回で解く。二段階方針では base graph の推定が間違うと後半パートがUNSATとなるが、一発方針では後半が充足可能となるような base graph を推定できるようになり、正解率が向上する。一方で、二段階方針と比較してSAT Solver で解く CNFが巨大になってしまう。Unagi は (D=2, N<=48) と (D=3,N=18) に対してこの解法を使用した。特に D=2, N=48 は順位表凍結前段階で唯一2クエリを達成出来た。これは SAT-Encoding の違いによる差が要因と思われるので、本記事では特にD=2の場合について、他のEncodingとの差を検証をしてみた。
1. ナイーブな Encoding
V[t][ui] := 時刻 t に居る部屋は ui である
E[ui][e][vj][f] := 部屋 ui のドア e は部屋 vj のドア f とつながっている
C[t][ui][c] := 時刻 t における部屋 ui の色は c である
2. base graph とコピーの分離
部屋を直接 [1,2N] により表現するのではなく、base graph の部屋 [1,N] と、レイヤー [1,2] の積で表現する。
V[t][u] := 時刻 t に居る部屋は u のコピーのどれかである
E[u][e][v][f] := base graph において、u のドア e は v のドア f とつながっている
F[u][e] := u のドア e はレイヤーを入れ替える (E[u][e][v][f] のとき、F[u][e] ならば u1のドア e は v2のドア f とつながり、!F[u][e] ならば u1 のドア e は v1 のドア f とつながる)
S[t] := 時刻 t に居るレイヤーは2である
C[t][ui][c] := 時刻 t における部屋 ui の色は c である
例えば、V[t][u] かつ S[t] であれば、時刻 t にいる部屋は u2 である。
3. 行き先のドアを無視した変数の導入
2に加え、以下の変数を導入
A[u][e][v] := base graph において、u のドア e は v とつながっている (どのドアかは指定しない)
実験結果
D=2, N=24 に対し、10回実行して実行時間を計測してみた。
| Encoding | 平均時間(s)±標準偏差 |
|---|---|
| 1 | 531.5 ± 464.1 |
| 2 | 3.5 ± 1.1 |
| 3 | 1.5 ± 0.5 |
1. ナイーブな Encoding → 2. base graph とコピーの分離 で実行時間が圧倒的に短縮されている。N=24で実験したが、N が大きくなるほど差はさらに広がると予想される。
Encoding のお気持ち
SAT solver は局所探索ではなく木探索(CDCL+restartにより厳密には違うが)なので、x1=true と仮定する→…→ xk=true と仮定する→矛盾、となったときに、x2〜xk をそのままにして x1=false を試そう、ということにはならない。
今回の問題の場合、一発方針であっても、SAT solverの内部では、クエリ前半の色塗りなしパートの情報から base graph を特定し、クエリ後半の色塗りパートの情報からコピーの情報を特定する、という流れになると想定される。1. ナイーブなEncoding の場合、色塗りなしパートで u のドア e は v のドア f とつながっていそうだなと分かっても、コピーの繋がり方まで仮定しないと探索は先に進めない。そのため、その仮定が間違っていたときに、base graph の繋がり方はそのままキープしてコピーの繋がり方だけ逆を試す、ということが出来ない。
2. base graph とコピーの分離 では、まず base graph に関する変数 (V, E) のみを探索して矛盾しない base graph を探し、その base graph を仮定した上で後半部分 (F, S, C) の充足解を探す(充足不能だったら他の base graph を探す)、という探索が可能になる。これにより大幅な効率化が実現できている。
3. 行き先のドアを無視した変数の導入 も同様で、クエリ結果からドアの行き先の色が分かり、対応する何通りかの部屋に絞り込まれるが、E[u][e][v][f] のみを用いた場合、この時点で明らかに情報の足りていない v 側のドアとの対応まで仮定しなければならない。一方で、A[u][e][v] を導入すると、ドアの対応の決定を後回しにすることが出来、最後に入次数=出次数となるように対応を取るという探索が可能となる。
