はじめに

きっかけは、こんなパズル。

○どうし、●どうしをそれぞれ1本の線でつなぎなさい。
ただし、線は点線にそって引き、途中で交わったり分かれたりしないようにしなさい。

この例題は盤面のサイズも小さいので、直感でも以下の解が比較的かんたんに見つかります。

この記事では、このようなパズルを制約充足問題として定式化して、制約ソルバーのSugar¹を使って自動で解くことを目指します。

方針

「ナンバーズリンク(仮)」

さて、まず本パズルですが、自動で解くやり方を色々調べているうちに、いわゆる「ナンバーリンク²」と呼ばれるパズルに似ていることに気づきました。試しに、上記例題の○と●を数字の(1)と(2)に置き換えたものと、注釈²にリンクを貼ったニコリ社のホームページにある例題を並べました。

まぁ、似てます。同じ数字どうしを1本の線でつなぐ、という基本的なルールは同じ。一方で、複数の点を1本でつなぎ、その始点と終点が決まっていない、というポイントがナンバーリンクとは少し異なります。そこでこのパズルを、「複数の」同じ数字どうしをつなぐ、という意を込めて**「ナンバーズリンク(仮)」**と名付けます。

このナンバーズリンクの自動解法について、当初は、経路探索アルゴリズム(A*アルゴリズム³など)を用いたアプローチ⁴をベースに試行錯誤していました。が、、、ナンバーズリンクでは、複数の地点を通過する順番が不定で経路の探索空間が大きく、私の力では盤面が7x7や8x8のサイズでも解にたどり着くことができませんでした。残念。。。

そこで今回は、ナンバーリンクの解き方としてメジャーと思われる、制約ソルバーで解くアプリーチで進めてみます。

制約ソルバー

まず、制約ソルバーとは、制約充足問題の解を探索するプログラムのことを指します。ここで、制約充足問題とは、以下のようなものです⁵。

制約充足問題は、以下を満たす組$(X,D,C)$で与えられる。

$X$: 変数の有限集合

$D$: 各変数のドメイン(有限な値領域、整数)を与える関数

$C$: $X$上の制約の有限集合

要は、変数と、変数の取り得る値と、その制約、ということですね。これらを決めることができれば、あとは、制約ソルバーが高速に解いて変数の値を決めてくれます⁶。

ちなみに、この制約充足問題や制約ソルバー(CSPソルバー)ですが、情報処理学会のSLDM研究会⁷というところが2012年から毎年開催しているアルゴリズムコンテスト⁸のWEBサイトを見て、今回初めて知りました。このコンテストで取り組んでいるのは、ナンバーリンクやそれをアレンジしたパズルの自動解法。研究会の特性からも、電子回路の自動配線アルゴリズムの研究が背景にあるようですが、制約ソルバー自体は、割当問題やスケジューリング問題など、幅広い応用が可能なようです。

「ナンバーズリンク(仮)」の制約モデル

というわけで、過去のナンバーリンク解法なども参考に、ナンバーズリンクの制約モデルを作ってみました⁹。
まず、盤面は、各節点を頂点とし、隣接する節点の間に辺がある有向グラフとして考えます¹⁰。
制約モデルの骨子は以下の3つの制約です。

節点と辺を通る線は多くても1本(交差や枝分かれもなし)
同じ数字同士を線でつなぐ
同じ数字は全て1本の線でつながる

この中で、特に制約3がナンバーズリンクに特有の制約となります。
制約モデルの詳細は、次で具体的に示します。

実装

今回は、制約ソルバーとしてSugar¹を、SATソルバーとしてcryptominisat¹¹を用いました¹²。
まず、ナンバーズリンクの問題は以下のようなテキストで表現します。

入力データ例(冒頭のナンバーズリンク問題を表したテキストデータ)

このような入力データに基づいて制約モデル(CSPファイル)を作りSugarを実行するコードをPythonで書きました。参考までに、コード(NumbersLink_CSP.py)と、本コードで生成されるCSPファイル例(上記の入力データ例から生成されるもの)を以下に置いておきます。

あり得る解は全て求められるよう、得られた解を除外するような条件をCSPファイルに追記して制約ソルバーを再実行する、ということをしています。また、自動で解を求めるだけではなく、自動で問題を作ることもできるようにしてみました。問題をランダムに作って解く、を繰り返すことで、筋の良い問題を作ろうとするものです。

制約モデルの詳細

実装した制約モデルについて、CSPでの表現も一部交えて説明します。

制約1：節点と辺を通る線は多くても1本(交差や枝分かれもなし)

節点$u$と節点$v$の間の辺$(u,v)$について
- $辺(u,v) \in \{0,1\}$　　※線がある場合は1、ない場合は0
- $辺(u,v) + 辺(v,u) \leq 1$　　※線は多くてもどちらかの向き1本

(int hr_2_1 0 1)  ;右向きの辺
(int hl_2_1 0 1)  ;左向きの辺
(int vu_2_1 0 1)  ;上向きの辺
(int vd_2_1 0 1)  ;下向きの辺

(<= (+ hr_2_1 hl_2_1) 1)  ;右向きと左向きの辺を足して1以下
(<= (+ vu_2_1 vd_2_1) 1)  ;上向きと下向きの辺を足して1以下

節点$u$について
- $入次数(u) \in \{0,1\}$　　※節点に入る線の本数
- $出次数(u) \in \{0,1\}$　　※節点から出る線の本数
- $入次数(u) = 辺(u_{上},u) + \cdots + 辺(u_{右},u)$　　※入次数＝周囲の節点から入る線の本数
- $出次数(u) = 辺(u,u_{上}) + \cdots + 辺(u,u_{右})$　　※出次数＝周囲の節点に出る線の本数

(int di_2_1 0 1)  ;入次数
(int do_2_1 0 1)  ;出次数

(= di_2_1 (+ hr_1_1 hl_2_1 vd_2_0 vu_2_1))  ;入次数は周囲の節点から入る辺の和
(= do_2_1 (+ hl_1_1 hr_2_1 vu_2_0 vd_2_1))  ;出次数は周囲の節点に出る辺の和

制約2：同じ数字同士を線でつなぐ

はじめに数字が配置されなかった節点$u$について
- $数(u) = \{0,1,2, \cdots ,最大数\}$　　※配置する数は1以上、0は線が通過しないことを表す
- $入次数(u) = 出次数(v)$　　※線は通過するか通らない

(domain number (0 1 2))  ;数は0~2(0は線が通過しないことを表す)
(int x_2_1 number)       ;接点を通過する線がつなぐ数
(int i_2_1 0)            ;はじめに数字が配置されなかった場合0
(= di_2_1 do_2_1)        ;入次数=出次数

はじめに数字$n$が配置された節点$u$ (全$m$個) について
- $数(u) = n$
- いずれか１つ：　$入次数(u) = 0　\land　出次数(u) = 1$　　※始点
- いずれか１つ：　$入次数(u) = 1　\land　出次数(u) = 0$　　※終点
- 他の$m-2$個：　$入次数(u) = 1　\land　出次数(u) = 1$　　※通過点

(int x_1_2 1)  ;はじめに数字が配置された場合、配置された数字
(int i_1_2 1)  ;はじめに数字が配置された場合、配置された数字
(count 0 (di_1_2 di_0_3 di_5_3 di_3_4 di_5_5) eq 1)  ;いずれか1つの入次数が0
(count 0 (do_1_2 do_0_3 do_5_3 do_3_4 do_5_5) eq 1)  ;いずれか1つの出次数が0
(count 1 ((+ di_1_2 do_1_2) (+ di_0_3 do_0_3) (+ di_5_3 do_5_3) (+ di_3_4 do_3_4) (+ di_5_5 do_5_5)) eq 2)  ;いずれか2つの入次数と出自数の和が1
;上記の3式の組み合わせにより、いずれか1つが始点、いずれか1つが終点、残りが通過点、となる

全ての節点$u$と節点$v$について
- $辺(u,v) > 0　\Rightarrow　数(u) = 数(v)$　　※同じ数字同士を線でつなぐ

(=> (> hr_2_1 0) (= x_2_1 x_3_1))  ;つながった節点は同じ数
(=> (> hl_2_1 0) (= x_2_1 x_3_1))  ;つながった節点は同じ数

制約3：同じ数字は全て1本の線でつながる

節点$u$（$数(u)=n$）について
- $入次数(u) = 0 \land 出次数(u) = 1　\Rightarrow　順序(u) = 0$　　※始点の順序は0
- $入次数(u) = 1 \land 出次数(u) = 0　\Rightarrow　順序(u) = m-1$　　※終点の順序はm-1

(=> (and (= di_1_2 0) (= do_1_2 1)) (= o_1_2 0))  ;始点の順序は0
(=> (and (= di_1_2 1) (= do_1_2 0)) (= o_1_2 4))  ;終点の順序はm-1

はじめに数字が配置されなかった節点$u$と節点$v$について
- $辺(u,v) > 0　\Rightarrow　順序(v) = 順序(u)$

(=> (and (> hr_2_1 0) (= i_3_1 0)) (= o_2_1 o_3_1))
(=> (and (> hl_2_1 0) (= i_2_1 0)) (= o_2_1 o_3_1))

はじめに数字$n$が配置された節点$v$について
- $辺(u,v) > 0　\Rightarrow　順序(v) = 順序(u) + 1$　　※通過するときに順序を+1

(=> (and (> hr_2_1 0) (> i_3_1 0)) (= o_3_1 (+ o_2_1 1)))
(=> (and (> hl_2_1 0) (> i_2_1 0)) (= o_2_1 (+ o_3_1 1)))

実行例

作ったPythonコードで上記入力データ例を解いた結果は、こうなります。

mbp:puzzle nikotan$ python NumbersLink_CSP.py --solver --map map_6x6_1-2_5.txt --tmp tmp
width : 6
height: 6
=====================
[result: 1]
+ - + - + - + - + - +
|                   |
+   2 - + - + - +   +
|               |   |
+   1 - + - +   +   +
|   |       |   |   |
1 - +   2   +   +   1
        |   |   |   |
+ - + - 2   1   2   +
|               |   |
2 - + - + - + - +   1
=====================
num satisfiable results = 1
elapsed_time = 1.132[sec]

サイズも小さく簡単な問題ですが、解が正しく求まっています。
また、この解が唯一の解であると判定されています。真偽は、、、たぶん合ってますよね？

おわりに

パズルの制約(ルール)を定式化するだけでパズルが解けてしまう¹³、というのは、当たり前のようで実は難しいこと、だと思います。CSPソルバーやSATソルバーの強力さを実感できました。また、問題を自動で解くことができると、問題を自動で作ることもできる、というのも大変面白い気付きでした。
というわけで、これも小規模ですが、ランダムに問題を作って解く、という自作自演行為をプログラムにひたすら繰り返させて見つけた問題の一例を以下に紹介し、本記事を締めさせていただきます。

Sugar: a SAT-based Constraint Solver ↩ ↩²
盤面上の同じ数字のペアを線でつなぐパズル。参考：[ナンバーリンク - Wikipedia] [ナンバーリンクの遊び方、ルール、解き方 | WEBニコリ] ↩ ↩²
グラフ探索アルゴリズムの一種。参考：[よくわかるA*(A-star)アルゴリズム (Unity2Dのサンプルコードつき) - Qiita] [2009-07-13 | Pashango’s Blog] ↩
電子回路設計の分野などでは、A*アルゴリズムなどの経路探索アルゴリズムとRip-up and Rerouteと呼ばれる手法などを組み合わせたアプローチが古くから研究されているようです。参考：[ナンバーリンクの解探索について考えてみた – PSYENCE:MEDIA] ↩
SAT型制約ソルバーを用いたナンバーリンクの解法 ↩
実際には、制約ソルバーは制約充足問題をさらにSAT(Boolean satisfiability testing)と呼ばれる論理式集合に変換し、SATソルバーが充足可能かを判定します。近年、このSATソルバーに様々な技術が導入されて大幅な性能向上(高速化)が進んでおり、SATソルバーを利用する制約ソルバーを実用的なものにしているそうです。 ↩
IPSJ SIGSLDM Home Page ↩
2012年から毎年、ナンバーリンクをアレンジした題材でアルゴリズムコンテストを行っているようです。参考：[DAシンポジウムアルゴリズムデザインコンテスト] [DA Symposium, Algorithm Design Contest] ↩
高速化などの改良の余地がまだまだ残ってそうです。 ↩
有向グラフとしたのは、後述する制約3を表現するためです。当初は無向グラフとしていましたが、無向グラフでは制約3をうまく表現できませんでした。 ↩
msoos/cryptominisat: An advanced SAT solver ↩
macbook proで環境を構築しましたが、特に手こずることはありませんでした。参考：Sugarと制約ソルバーcryptominisatの開発環境の構築 | コマログ ↩
ナンバーリンクだけでなく、様々なパズルが制約ソルバーで解かれているようです。参考：パズルをSugar制約ソルバーで解く ↩