knight tour problem を解いてみた
皆さん、こんにちは！ Ken.Sです！
毎週トビタテ生とオンライン飲み会をしているのですが、そこでオセロや将棋などボードゲームの話になりました。インドに留学していた友達が、将棋をインド人に教えた話を聞かせてくれました。そのインド人はチェスは分かるようなのでそれを基に教えたそうなのですが、桂馬をknightのように動かしたそうなのです。友達は桂馬はknightの1/4しか動かせない、前2マスと横1マスしか行けないとちゃんと伝えたそうなのですがそのインド人に噓つき呼ばわりされてしまったそうです(笑) たしかにknightって特殊な駒で、子供のころに教えられて桂馬より動く幅が4倍になる！とかなり印象的だったことを今でも覚えています。
そんなknightに関する大学の課題で記憶に残っているのが「knight tour problem」ナイト・ツアー - Wikipedia です。
8×8のチェス盤においてknightが全てのマスを一回だけ訪れることは可能か、という問題です。解けることは知られており、それを示せというのが2年前にあった課題でした。この問題の事をそのトビタテ生に話したときに、「どのマスから始めても可能なのか」と質問してもらったのですが、その課題のレポートには角から始めた結果しかありませんでした。気になって調べた結果を書いていきますので、興味のある方是非読んでください！ 反論はいくらでも受け付けます(笑)
まず初めに、c++で書いてみました。競プロでやはりc++の速さが強いので、pythonやgoに比べると書きにくさは感じるのですが勉強ということでc++を利用しました。深さ優先探索で実行しどこにも行けなかったらfalseを返し、1通りでも見つけたらtrueを返して終了するというプログラムを書いたのですが、c++の速さをもってしてもなかなか終わらない…。明らかに1周できないと判断できる場合(あるマスから行けるマスが全て既に訪れていてそのマスに行けない等)にfalseを返していなく、訪れたマスからどこにも行けなくなるまで計算を続けているので範囲の絞りが甘いのもあるのですが、丸2日かかっても終わりません…。総計算量を考えると、あるマスからチェス盤からはみ出さず行くことができるマス数の平均は5.25マス。その内の1マスはそのマスへ訪れる前に訪れているのでその分を引く。これを64回繰り返すので概算で(5.25-1)^64≒10^40となります。c++が1秒で100万通り計算できたとしても、約10^29日かかってしまう…。実際はもっと小さいですが、終わらないわけです。プログラム内にバグがありそれで遅くなっている可能性もありますが、直しても時間がかかりそうなので別の方法を考えます。
そもそも2年前はどう解いていたのか、もう一度提出したレポートを確認しました。充足可能性問題 充足可能性問題 - Wikipedia を解くSAT solverの一つ minisatを利用して解いており、なんと1分程度で解の一つを出していました！
いくつかのリテラル(真か偽となる変数のようなもの)の論理和(クローズ)の論理積がTrueとなるようなリテラルの真と偽の選び方はあるのか、といった問題です。例題は上記のwikiなど見てください。
このsolverであるminisatは以下のコマンドで簡単にインストールできます。
Linux : sudo apt-get install minisat
minisatはDLLアルゴリズムを採用しています。二分探索でリテラルを真or偽と決め、その場合全てのクローズが真となるかを計算していきます。全て真であるならばクローズの論理積も真となり、その充足可能性問題が解けたということになります。
ではこの問題の核となる、knight tour problemを解くためにどのような充足可能性問題を作るかを考えていきます。
- 時間i(1~64)において、リテラル( (i-1)*64+1 ~ i*64)を用意する(時間1(初手)は1~64, 時間2は65~128, ...)。※この64個はチェス盤の64マスに該当し、時間iは何手目に対応します。knightがいるマスに対応するリテラルを真、そうでないリテラルを偽とする。
前提を決めたところで、クローズを作る条件を作っていきます。
- knightは1つしか存在しない = 時間iに対応するリテラル( (i-1)*64+1 ~ i*64)のうち真は1つだけ。
- knightは移動距離3かつ縦横の距離は1以上で動く = 例えばリテラル1が真の(knightがそのマスにいる)場合、75(=64+11), 82(=64+18)のどちらかが真となる。
- 同じマスには1回しか行けない = 64で割った余りでグループ分けした時に(リテラル番号 mod 64)、真は1つだけ。
この条件1~3を満たすよう命題論理式を組んでいきます。
knightは1つしか存在しない = 時間iに対応するリテラル( (i-1)*64+1 ~ i*64)のうち真は1つだけ。
1-i) ある時間iにおいてknightは1個以上存在する、1-ii) ある時間iにおいてknightは1個以下存在する、と条件1を二つに分けて考えます。
1-i)
リテラル1つでも真であれば、論理和は真となります。偽となる場合は時間iのリテラル全てが偽となり、knightが時間iにおいて存在しないこととなります。故にこの論理式が真の場合、時間iにおいてknightが1個以上存在することとなります。
1-ii)
時間iにおいてリテラル64個の内2つ選び、その2つの否定の論理和は真となる。
例えば、マス1にknightがいるとします。1の否定=偽, 2の否定=真となりその論理和は真となります。マス3にいる場合も1,2の否定の論理和は真です。偽となる場合は、1,2が共に真の場合です。となると、knightが時間iにおいて2個以上存在することとなります。故にこの論理式が真の場合、時間iにおいてknightが1個以下存在することとなります。
1-i),1-ii)の式で、ある時間iにおいてknightが一つ存在している命題論理式が立てられました。これは条件3の時にも利用します。
knightは移動距離3かつ縦横の距離は1以上で動く = 例えばリテラル1が真の(knightがそのマスにいる)場合、75(=64+11), 82(=64+18)のどちらかが真となる。
この例を使うと、リテラル1が真ならばリテラル75と82のどちらかが真とならなければなりません。リテラル1,75,82の論理和だと、マス1にknightがいたら真となりマス75,82にknightがいなくても真となってしまいます。なので、リテラル1の否定と75,82の論理和を取ることとします(￢1⋁75⋁82)。リテラル1が真ならば￢1は偽となるので75,82のどちらかが真となる必要があります。これは条件2そのままですね。つまり、時間iのリテラルの一つの否定と、そのリテラル(マス)から行くことができる時間(i+1)の全てのリテラルの論理和全ての論理積が条件2となります。つまり、この論理式が真となる場合、knightが正しく動いていることとなります。
同じマスには1回しか行けない = 64で割った余りでグループ分けした時に(リテラル番号 mod 64)、真は1つだけ。
3) 64で割った余りでグループ分けし、そのグループのリテラル64個の内2つ選び、その2つの否定の論理和は真となる。
条件3では条件1でknightは1個以下を示す命題論理式を真似ます。つまり、1 mod 64のグループの場合、リテラル1,65の否定の論理和を取ります。偽となる場合はマス1,65にknightが訪れ同じマスを2回訪れていることになります。このやり方ではあるマスに1回以下訪れていることになる、ということを示しています。しかし条件1より時間iにおいてknightが1つだけ存在する命題論理式を立てたので、あるマスを訪れていないとしても他のマスに2回訪れたことにもなるので、1回以下の訪問という論理式で本問題は解けます。
故にこの論理式が真となる場合は、knightが全てのマスを1回ずつ訪れていることになります。
これらの条件1~3が真となればこのknight tour problemは解けたことになります！
充足可能性問題の命題論理式を立てられたので、今度はminisatで検証できるようcnfファイルをpythonで作成します。以下の命題論理式はこのようにcnfファイルに記述します。
命題論理式
(￢1⋁￢2⋁￢3) ⋀ (￢1⋁2⋁￢4) ⋀ (1⋁￢3⋁4) ⋀ (2⋁3⋁4)
論理和のクローズを0と改行で区切り、否定はマイナスで表現します。これを以下のコマンドで実行します。
minisat test.cnf ans.cnf
実行すると色んな文字が出力され、最後に「SATISFIABLE」or「UNSATISFIABLE」と出ます。「SATISFIABLE」と出れば充足可能となり、その解の一つをans.cnfに出力します。
これは、リテラル4が真、1~3が偽となる場合が解の1つとなります。
別解として{(1,2,-3,4),(1,2,-3,-4),(1,-2,3,-4),(-1,2,3,4),(-1,2,-3,4),(-1,2,-3,-4),(-1,-2,3,4)}があります。
では、先程の条件1~3を表す命題論理式をcnfファイルに記述するpythonプログラムを作ります。
このまま実行すると、1分程で結果が出ます。しかし、これだと開始地点を自力で決められません。先のチェス盤を1~64で表したように、開始地点のマスのリテラルをcnfファイルに追加します(マス1から始めたい場合にはcnfファイルに「1 0」を追加します)。
線対称、点対称を考えると以下の10マスを開始地点とし全てSATISFIABLEであれば、目的であったどの地点からでもknightがtourできるということになります。
結果は開始地点によらず巡回できることが分かりました！！
裏でc++のプログラムも回していたので遅くなったのかもしれませんが、一番計算に時間がかかったのが10番マスからのスタートで約22時間かかりました…。朝起きたら終わっているだろうと思ったら計算途中だった時は不安になりました(笑)
開始地点のそれぞれの結果はGithubに載せておきます。
(githubに掲載するの初めてで不安…。これで合ってるかな、閲覧だけで編集できないようになっているかな…。)
cnfファイルを作るpythonプログラムもこのgithubに載せてあります。コメントでどの条件の命題論理式を記述しているか書いてあります。
ということで、knight tour problemは充足可能性問題として解いてみました。2年前の自分のレポートを読み返して、こう書いた方が分かりやすいのに等2年間で自分の国語力が変わっているなぁと実感させられることが多く良い経験になりました。こんなの解いて何になるんだ、と思われた方。御尤もです。ですが、情報系学生としてはこういう課題の方が面白く、身近なものが扱われる課題は稀なので新鮮でした。いずれはこの経験が何かに繋がるかも…？こういった問題を楽しめる方は情報系に向いているのかもしれません。つまらないと感じた方はここまで読んでいないと思うので、ここまで読んでいる方は情報系向きかもしれません(笑)
こんな感じで解いてて面白いと感じた問題はまたブログに載せようと思います！他にもこんな方法があるよ、こっちの方が速いよ！などの意見も待ってます。
それでは！
See you next time!
