交差回避制約によるSAT型ナンバーリンクソルバーの高速化

交差回避制約による

SAT

型ナンバーリンクソルバーの高速化

Speeding up SAT-based NumerLink Solvers with Crossing-Path

Avoidance Constraints

渡辺光洋

1

戸田貴久

1∗

Mitsuhiro Watanabe

1

Takahisa Toda

1 1

_{電気通信大学}

1

_{The University of Electro-Communications}

Abstract: 本稿では，ナンバーリンクに対する解法の１つである SAT 型解法を高速化する手法を提 案する．SAT 型解法とは，一般に，制約充足問題 (CSP) を命題論理式に符号化して，その解を SAT ソルバーを用いて求める手法である．本研究では，事前実験として，先行研究で与えられたナンバー リンクに対する CSP 定式化 (基本モデル) に従い，SAT 型解法をナンバーリンク問題に適用したと き，線交差を解消するために多数のバックトラックが発生し，大幅な時間的ロスにつながる場合が あった．そこで，本研究では，探索の各時点でその後どのように線を引いても必ず線が交差してしま う状態に着目し，そのような状態に陥ったと判明した時点でただちにバックトラックさせる制約 (交 差回避制約) を導入する．ナンバーリンクソルバーの競技会の問題例を用いた計算機実験を行い，基 本モデルで時間のかかった問題に対して，交差回避制約が大きな効果を発揮することを観察し，問題 別では最大で 20 倍近くの高速化を達成することを確認する．

1

はじめに

与えられた全ての制約を満たす解を求める問題を制 約充足問題 (CSP) という．これは身近な例では数独や ナンバーリンク1，魔方陣などのパズル問題が挙げら れる．これらのパズル問題は，パズルの解を満たすた めのルールが制約として与えられるので，自然に制約 充足問題となる．例えば，ナンバーリンクでは，図 1 のように盤面にある同じ数字同士を以下のルールを満 たすように線でつなげることが求められる [1]． 1. 白マスに線を引いて，同じ数字同士をつなげる． 2. 線はマスの中央を通るようにタテヨコに引く．線 を交差させたり枝分かれさせたりしてはいけない． 3. 数字の入っているマスを通過するように線を引い てはいけない． 4. 1マスに 2 本以上の線を引いてはいけない． ナンバーリンクは LSI の配線問題 [2] と深い関係が あり，ナンバーリンクに関連する問題を解くソフトウェ アの競技会 [3] が毎年開催されている．この競技会で は，現実の LSI 配線問題に近づけるために配線長など ∗_{連絡先：電気通信大学 大学院情報理工学研究科}       〒 182-8585 東京都調布市調布ケ丘 1 丁目 5-1        E-mail: [email protected] 1_{「ナンバーリンク」は株式会社ニコリの登録商標．} 図 1: ナンバーリンクの問題 (左) と解答 (右) に関する最適化や盤面の三次元化などの拡張がされた 問題が出題されるが，問題解法の基本となるのは通常 のナンバーリンクの解を高速に求める手法であり，そ のような手法として，機械学習，最適化，ZDD，SAT 型解法などが知られている． SAT型解法 [4] は (ナンバーリンクに限らず) 制約 充足問題を命題論理式に変換し，その解を SATソル バーを用いて求める一般的な手法である (図 2)．その ソフトウェア実装である SAT型制約ソルバーは通常の CSPソルバーよりも優れた性能を示す場合があること が報告されている (例えば Sugar [5] は 2008 年 2009 年， sCOP [6]は 2018 年の CSP ソルバーの国際競技会の複 数部門で優勝)．田村ら [7] は，ナンバーリンクを制約 充足問題として定式化し，SAT 型解法を適用して解く 手法を提案している．ナンバーリンクに対する SAT 型 解法は，過去のナンバーリンクソルバーの競技会で優 人工知能学会研究会資料 SIG-FPAI-B803-07

図 2: SAT 型解法 勝するなど優れた解法であることが知られている． 先行研究で与えられた基本的な CSP の制約 (基本モ デル) では，盤面上の線が実際に交差した際に初めて 制約が満たされないと判定され，SAT ソルバーによる バックトラックが発生する．このバックトラックが多 くの線が引かれた後に発生した場合，線交差を解消す るために，その後，多数のバックトラックが繰り返さ れ，大幅な時間的ロスにつながることが，本研究の事 前実験で確認されている．もし，早い段階でその後ど のように線を引いても線交差が避けられない状況に陥 ると分かるならば，その時点でバックトラックを行う ことにより，多くの無駄なバックトラックを削減する ことができる． そこで本研究では，探索の各時点で将来の線交差が 避けられないかどうかを判定する制約 (交差回避制約) を考える．この制約を定式化し，基本モデルに追加す ることにより，SAT ソルバーの探索は将来の線交差を 回避するように誘導されるので，無駄なバックトラッ クが大幅に削減されると考えられる．ただ，将来の線 交差の判定を厳密に行うことはとても高い計算コスト を伴い，現実的ではないので，本研究では計算コスト とのトレードオフを考慮し，いくつかの簡易的な交差 回避制約を導入する． 計算機実験により，どのような交差回避制約が，ど のような問題に対して有効であるかを観察し，それぞ れの交差回避制約の有効性について考察する．さらに， ナンバーリンクソルバーの競技会の問題例を用いて，基 本モデルに基づく SAT 型解法と比較実験を実施して， 問題別に見ると最大で 20 倍近い高速化を達成すること を確認する．

2

SAT

型ナンバーリンク解法の基本

モデル

田村ら [7] は，ナンバーリンクの盤面を有向グラフ として表現し，盤面がナンバーリンク問題のルールを 満たすことを表す制約 (基本モデル) を CSP の変数を 用いて定式化している．他にも改良モデルや追加制約 が提案されているが，本稿では扱わないので省略する． まず，有向グラフとしての表現方法と制約において 用いられる記法を説明する．行数を m，列数 n とし， 行番号と列番号は 0 から始まるものとする．i 行 j 列の マスを (i, j) と表す．このとき，すべてのマスの集合を 頂点集合 V とし，隣り合うマスの間に張られた弧から なる集合を A とすることで，有向グラフ (V, A) を定義 する． V = {(i, j) | 0 ≤ i < m, 0 ≤ j < n} A = {(u, v) | u ∈ V, v ∈ adj(u)} ここで，マス u = (i, j) に隣接するマスの集合を adj(u) あるいは adj((i, j)) と表す．例えば，5× 5 の盤面にお いて adj((1, 3)) ={(0, 3), (1, 2), (1, 4), (2, 3)} である． 盤面に存在する数字の集合を N とする．盤面のマス で，数字の割り当てられたマスを数字マス，それ以外 を白マスと呼ぶ．同じ数字の割り当てられた数字マス は 2 つ存在するので，(任意に選んだ) 一方を始点とし 他方を終点とする．そして，そのような始点の集合を S (⊆ V )，終点の集合を T (⊆ V ) とする．白マスの集 合を B とする．定義から明らかに S, T , B は V の分 割になっている． それでは基本モデルの制約を以降で与える．各弧 (u, v)∈ Aに対して論理変数 au,vを導入する．これは盤面にお いて u から v に線が引かれていることを表す．ルール 上，線の重複は許されないので au,v= 1と av,u= 1は 同時には成立しない． au,v∈ {0, 1}, ∀(u, v) ∈ A (1) au,v+ av,u≤ 1, ∀(u, v) ∈ A (2)

次に各頂点 u∈ V に対して入出次数を考える．頂点 u∈ S の出次数は 1，入次数は 0 となり，頂点 u ∈ T はその逆である． ∑ v∈adj(u) auv= 1, ∀u ∈ S (3) ∑ v∈adj(u) avu= 0, ∀u ∈ S (4) ∑ v_∈adj(u) auv= 0, ∀u ∈ T (5) ∑ v∈adj(u) avu= 1, ∀u ∈ T (6) 白マスに対応する各頂点 u∈ B に対して，線が引か れているか否かを表す論理変数 duを導入する．線が交 差してはならないので，白マスの入次数と出次数は等 しく，ともに 0 あるいはともに 1 でなければならない．

0のとき線がひかれないことを表し，1 のとき線が通過 することを表す． du∈ {0, 1}, ∀u ∈ B (7) ∑ v∈adj(u) auv= du, ∀u ∈ B (8) ∑ v_∈adj(u) avu= du, ∀u ∈ B (9) 各頂点 u∈ V に対して，u がどの数字につながるかを 表すために，u につながる数字を表す整数変数 fu∈ N を導入する．u が数字マスならば fuは u に割り当てら れた数字 num(u) と等しく，白マスならば弧で結ばれ る頂点間の変数 fuの値は等しくなければならない． fu∈ N, ∀u ∈ V (10) fu= num(u), ∀u ∈ S ∪ T (11) auv= 1⇒ fu= fv, ∀(u, v) ∈ A (12)

3

提案手法

3.1

基本的な考え方

従来のナンバーリンク問題のモデル化では，線の交 差を禁止する制約が含まれてはいるものの，その制約 は実際に線が交差した瞬間に作用するものであり，線 交差を解消するために多数のバックトラックが引き起 こされる場合がある．ナンバーリンクの盤面がその後 どのように線を引いても交差してしまう状態になった とき，この盤面の下でそれ以降の探索を進めるのは無 駄であるから，そのような状態に至ったと判断できる 場合はただちにバックトラックさせる．この仕組みを 実現するために，ナンバーリンクの盤面がその後どの ように線を引いても交差してしまう状態を交差不可避 状態と定義する．そして，交差不可避状態に至った時 点でただちにバックトラックを発生させる制約 (交差回 避制約) を定式化し，基本モデルに追加する． 例 3.1. 図 3 の左の盤面のように，最上段に 2 種類の 数字マスが交互に並んでいる問題が与えられるとする． このとき，2 つの数字を線でつなげようとすると，ど のように線を引いても右の盤面のように必ず交差して しまう．それゆえ，左の盤面が与えられた時点で交差 不可避状態になっていることがわかる． しかし，図 3 のように最初から数字マスが盤面の端 に交互に並んで与えられる場合はほぼないので，より 一般的な場合を考えたい．例えば図 4 の左の盤面を解 いていくとき，中央の盤面のように 2 種類の数字マス とそれにつながる線が盤面の外周に交互に並んだ状態 図 3: 交差不可避状態 (左) と交差が生じた状態 (右) を考える．この状態もそれ以降どのように線を引いて も右の盤面のように必ず交差してしまう．したがって， 図 4 の中央の盤面になった時点で交差不可避状態となっ ていることが分かる．なお，左の盤面からは交差が生 じないように数字をつなげることができるため，左の 盤面の時点では交差不可避状態ではないことに注意さ れたい． 図 4: より一般的な例：最初の状態 (左)，交差不可避状 態 (中央)，交差が生じた状態 (右) 以上のように，盤面の外周に数字マスやそれにつな がる線が交互に存在する場合，数字マスのみでなくと も交差不可避状態となりうることが分かる．もちろん 外周に着目するだけでは判断できない交差不可避状態 もある．例えば，閉路の内側と外側に同じ数字が現れ る場合などである．しかし，あらゆる交差不可避状態 を回避する制約を導入することは，とても高い計算コ ストがかかるだけであるので，本研究では上の例で与 えたような外周の 4 マスで判断できるものだけを扱う．

3.2

交差回避制約の定式化

本研究で扱う交差不可避状態は盤面の外周マスだけ で判断できるものを扱うので，図 5 で示されるように， 一般の盤面において外周マスだけを抜き出して，隣り 合うマスを一列に並べた場合を考える．簡単のため，左 上隅のマス (0, 0) から始まり，時計回りにマスを並べ ていくものとする． 図 5: 外周マスの抽出

このマスの列において 4 つの異なるマス u1, u2, u3, u4 を左から順に選ぶ．u1と u3に同じ数字の線が引かれ, u2と u4に同じ数字の線が引かれ，またこれら 2 つの 線は異なる数の線となる場合を考える．盤面がこのよ うな状態になった場合，交差不可避状態になることは 既に明らかであろう．これを数式で表すとき fu1 = fu3 かつ fu2 = fu4 かつ fu1 ̸= fu2 (13) となる．ここで，整数変数 fui は基本モデルで導入さ れたものであり，マス uiにどの数字の線が引かれてい るかを表している． 交差不可避状態に陥る場合に SAT ソルバーにバック トラックさせるためには，基本モデルに交差不可避状 態に陥らないことを表す制約 (交差回避制約) を追加す ればよい．これは式 13 を否定すれば得られる． fu1 ̸= fu3 または fu2 ̸= fu4 または fu1 = fu2 (14)

3.3

交差回避制約の簡易化

式 14 は外周から選ばれた 4 マスにつき１つ定まる ので，交差回避制約の個数は ( 2m + 2n− 4 4 ) である． ここで行数を m，列数を n とする．これでは比較的小 さな盤面でも多くの制約が生成され，SAT ソルバーの 速度が著しく低下することが予想される．そこで本研 究では，以下の 3 通りの方法で制約の個数を限定する (m≥ 2, n ≥ 2)． 1. マスの間隔をちょうど k にする． 2. マスの間隔を k 以上にする． 3. マスの間隔を l 以下にする (l:小さな定数値)． ここで，k =⌈(2m + 2n − 4)/4⌉ とする．2 マス u, v の 間隔とは，図 5 のマスの列を，マスを頂点，隣り合う マスを辺で結んだグラフとみなすとき，頂点 u と v を 結ぶパスの長さを意味する． 上の 3 通りの方法は，外周マスの列から u1, u2, u3, u4 をこの順番で選んだとき，それぞれ u1と u2の間隔，u2 と u3の間隔, u3と u4の間隔のとり方を指定している． u4と u1の間隔は何も指定していないことに注意され たい．指定の間隔で 4 マスを選べない場合の制約は生 成しないこととする． 方法 1 では，ほぼ対角の位置にある 4 マスだけに対 して交差回避制約を考えている．方法 2 では，対角よ りも遠い位置にあるようなマスも扱えるように緩和し ている．方法 3 では，近くのマスの間だけ交差回避制 約を考えている． 命題 1. 方法 1, 2, 3 の交差回避制約の個数はそれぞれ 高々k,(k+3₄ ), 4kl3_である． 証明. 以下，外周マスの列の先頭から順に選ばれた 4 マ スを u1, u2, u3, u4と表す． 方法 1 に関しては，u1のとり方が高々k 通り存在し， そのそれぞれに対して他のマスのとり方は一意に定ま るので，制約の個数は高々k である． 方法 2 に関しては，簡単のため外周マスの列の先頭 のマスを u0として，末尾のマスを u5とする．そして， u0と u1の間隔は d0,1とし，u4と u5の間隔は d4,5と する．さらに，各 i∈ {1, . . . , 3} に対して，uiと ui+1 の間隔は k + di,i+1とする．このとき d0,1+ (k + d1,2) + (k + d2,3) + (k + d3,4) + d4,5 = (2n + 2m− 4) − 1 が成り立つ．これを整理して d0,1+ d1,2+ d2,3+ d3,4+ d4,5= (2n + 2m−4)−(3k+1) を得る．これを満たす d0,1, . . . , d4,5 ≥ 0 の選び方は， 異なる 5 個の要素から重複を許して (2n + 2m− 4) − (3k + 1)個をとる組合せの総数 ( 5 + (2n + 2m− 4) − (3k + 1) − 1 4 ) に等しい．2n + 2m− 4 ≤ 4k より，この数は(k+3₄ )で 抑えられる． 方法 3 に関しては，u1のとり方が 2n+2m−4 (≤ 4k) 通り存在し，そのそれぞれに対して他のマスのとり方 は高々l3_{通り存在するので，制約の個数は 4kl}3_で抑え られる． 漸近的には方法 2 の制約の個数は O(k4_{)となり，制} 限なしで任意の 4 マスを選ぶ場合と同じオーダーであ るが，それ程大きくない k に関してはソルバーを動作 させられる程度には制約サイズを抑えられていること が期待される．

4

性能評価

4.1

実験の設定

本実験で比較する手法は以下の通りである． • 基本: 田村ら [7] によって示された基本モデル． • 提案 1: 基本モデルに対し，マスの間隔をちょう ど k とした交差回避制約を追加する． • 提案 2: 基本モデルに対し，マスの間隔を k 以上 とした交差回避制約を追加する． • 提案 3: 基本モデルに対し，マスの間隔を l 以下 とした交差回避制約を追加する．

ここで，提案 1, 2 でマスの間隔を指定する k は前節で 定めたとおり k =⌈(2m + 2n − 4)/4)⌉ である．提案 3 でマスの間隔を指定する l は 2, 3, 4 のそれぞれの値に ついて実験した． ちなみに，盤面の外周マスから制限なしで任意の 4 マスを選び交差回避制約を生成する場合，制約の個数 が非常に大きくなり，メモリーエラーにより Sugar を 動作させられなかった． 次に，使用するデータセットについて説明する．DA シ ンポジウムのアルゴリズムデザインコンテスト 2014 [8] で使用された問題のうち配布されている 11 問と，文 献 [9] の 170 ページにある練習問題 (a),(b) の合わせて 13問を利用する．各問題のサイズを表 1 に示す．各問 題は表 1 の第一行に示しているように 01 から 13 まで 番号を振っており，[8] の番号付けの中で欠番であった 05,10は [9] の (a),(b) 問が該当し，以降の欠番は飛ば して番号を振っている．各列が問題のサイズを示して おり，列，行の値と，初期盤面に配置されている相異 なる数字の個数を表す． 解を求める最大時間は 168 時間とした．13 問のうち 07以外は制限時間内で解を求めることができた．

実験の環境は以下の通りである．OS: Red Hat En-terprise Linux 6.3, 主メモリ: 512GB, CPU: インテ ル Xeon プロセッサ E7-2830 2.13GHz. 本実験では， SAT型制約ソルバーとして Sugar version 2.3.3 [5] を， 内部の SAT ソルバーとして Minisat version 2.2.0 [10] を利用する．提示された問題を読み込み，従来手法や 提案手法の制約を生成するプログラムや，その制約を Sugarに与え解を求めさせるプログラムには C 言語を 利用する．

4.2

結果と考察

実験結果を図 6 に示す．ここで縦軸は計算時間 (秒) であり，対数尺度で与えている．横軸は表 1 の 13 個の 問題番号を表す． 図 6 によると，使用した問題は手法によらずすぐに 解が求まるものと，手法によって求解に時間を要する ものの二種類がある．実際，問題 01,02,03,04,05,08,10 は手法によらず 10 秒以下で解けているが，その他の問 題は手法によって数倍∼十数倍の差が生じていること が観察される． 次に図 7 に示す問題 09 を取り上げる．問題 09 は基 本手法が最も早く解けており，提案手法全てで遅くなっ てしまった．これは元々問題 09 が高速に解ける問題で あるのに対し，提案手法によって制約を追加してもそ の制約の処理に時間がかかってしまったからであると 考えられる． 図 8 に示されるように，基本手法で時間のかかる問 題の解答は遠くの数字を盤面を回り込むようにつなげ 図 6: 計算時間 (秒) の比較 (縦軸は対数尺度) 図 7: 問題 09 とその解答 るものが多く，バックトラックの処理が多数発生して いると考えられる．それゆえに提案手法の交差回避制 約によるバックトラックの削減が効き，基本モデルを 凌駕する結果が得られたと考察される． また，提案手法の中でも提案 2 が特に高速に解を求 めている傾向が見られる．提案 1 がちょうど k マスの 間隔のみを選んでいたのに対し，提案 2 は k マス以上 の間隔をとっており，制約の個数としては提案 2 の方 が多い．それにも関わらず提案 2 が良い結果であるの は，対角の位置よりも遠いマスの交差が生じ，提案 1 と 2 の速度差として現れたと考えられる． 提案 3 が提案 1, 2 に対して良い結果を得られなかっ たのは，近い所で交差はするものの，浅いレベルのバッ クトラックで線交差を解消できるのでそれほど大きな 時間のロスにつながらないからだと考えられる．

表 1: 問題のサイズと含まれる数字の個数 問題番号 01 02 03 04 05 06 07 08 09 10 11 12 13 列数 10 10 18 18 5 18 17 19 18 8 21 21 19 行数 10 10 10 10 5 14 15 16 18 8 18 18 35 数字の個数 7 10 9 20 3 9 13 28 18 5 17 17 35 図 8: 問題 11 とその解答

5

まとめ

本研究では，ナンバーリンク問題に対して SAT ソル バーを用いる解法の高速化方法を提案した．ナンバー リンク問題には機械学習や最適化，ZDD など様々な手 法が提案されているが，SAT ソルバーを用いる SAT 型 解法はプログラミングコンテストで優勝するなど効率 的な解法として知られているので，本研究ではこの解 法をさらに高速化することを試みた． 従来の SAT 型解法 (基本モデル) はナンバーリンク 問題の数字のペアが盤面上遠い位置にある場合に，多 くのバックトラックが生じていた．そこで探索の各時 点でその後どのように線を引いても必ず線が交差して しまう状態を特徴づけ，探索の早い段階でそのような 状態を避けるための交差回避制約をモデル化して基本 モデルに組み込んだ．基本モデルとの比較実験により， 基本モデルで解を求めるのに時間のかかっていた問題 に対して，問題別では最大で 20 倍の高速化を達成した． 今後の課題は，より複雑な交差回避制約 (例えば, 閉 路に着目した制約) の導入である．基本モデルの制約で は閉路が生じることを阻止できない。最終的な解に閉 路が存在しても、それを取り除くことで望ましい解が 得られるので計算の正当性に問題はないが，探索途中 に形成される閉路により盤面が交差不可避状態となり， 速度低下につながる可能性がある．そこで，閉路を阻 止する制約の定式化と性能評価が今後の課題となる． 本研究では単にナンバーリンクの解を求めるだけで あったが，近年のナンバーリンクソルバーの競技会で 出題される問題は，現実の LSI 配線問題に近づけるた めに，配線長を最小化するような最適化や，三次元盤 面への対応が要請される．従って，今後の研究課題と しては，制約最適化問題と 3 次元盤面の問題への対応 を目指す．制約最適化問題への対応は，従来手法で制 約最適化問題への対応が行われていたため，同様の方 法で対応できるのではないかと考えている．3 次元盤 面に関しては，交差回避制約のアイディアを 3 次元盤 面に応用できるか検討していきたい．

参考文献

[1] 株式会社ニコリ. ナンバーリンクの遊び方、ルール、 解き方. https://www.nikoli.co.jp/ja/puzzles/ numberlink/. [2] 高島康裕,島村光太郎. Lsiの配線問題-daシンポジウム の配線問題解法コンテスト-：1．lsiの配線問題と解法コ

ンテスト. 情報処理, Vol. 59, No. 3, pp. 224–227, feb 2018. [3] DAシンポジウム実行委員会. DAシンポジウム2018 アルゴリズムデザインコンテスト. https://dasadc. github.io/adc2018/. [4] 田村直之,丹生智也,番原睦則.制約最適化問題とsat符 号化( (特集)最近のsat技術の発展). 人工知能学会誌,

Vol. 25, No. 1, pp. 77–85, jan 2010.

[5] 田村直之. Sugar: a SAT-based Constraint Solver. http://bach.istc.kobe-u.ac.jp/sugar/.

[6] 宋剛秀. sCOP: a SAT-based CP System. https:

//tsoh.org/sCOP/. [7] 田村直之,宋剛秀,番原睦則,鍋島英知ほか. Sat型制約 ソルバーを用いたナンバーリンクの解法. DAシンポジ ウム2014論文集, Vol. 2014, pp. 215–220, 2014. [8] 情報処理学会システムとLSIの設計技術研究会(SLDM). DAシンポジウム2015，アルゴリズムデザインコンテ スト，問題サンプル1. http://www.sig-sldm.org/ DC2014/ADC2014\_QA.zip.

[9] Donald E. Knuth. The Art of Computer

Program-ming, Volume 4, Fascicle 6: Satisfiability.

Addison-Wesley Professional, 1st edition, 2015.

[10] Niklas E´en and Niklas S¨orensson. The MiniSat Page. http://minisat.se/.