今回は、２８０合体ナンプレの問題としての正当性について書く。
ギネス世界記録™として認めてもらうには、当然問題の正当性が保証されないといけない。
その中でも面倒なのが、解の一意性（ユニーク性）である。
「ルールを満たす解が存在し、その数は１つだけである」
これは、ギネス世界記録™だけでなく、普通にナンプレ本、ナンプレ雑誌などに載る問題でも当然保証しなければいけない事で、問題を作ったプログラムの中に、そういう検証も含まれている。
しかし、パズルを作ったプログラムで、ユニーク性を確認しても、それは保証にはならないだろう。
公式記録となるためには、第三者がユニーク性を確認しなければいけない。
方法としては、まあ色々あり、検討された。
ナンプレの権威者の保証
そもそも、ナンプレの権威者って存在するのか？
権威者なら間違わないのか？ 所詮人間であり、２８０合体ナンプレをノーミスで解くのは神でも無い限り無理だろう。
ということで却下。
第三者のプログラムで検証
人間が無理なら、プログラムで解くことになる。
第三者のプログラムで２８０合体を解けるプログラムが存在するかどうかよく分からない。
誰かに頼んでプログラムを作ってもらうのは可能かもしれないが、こういうのをホイホイ作るようなプログラマとは何らかの関係があったりして第三者として認められない。
他にも問題がある。
標準の９ｘ９のナンプレ問題を解くプログラムでよく使われる、ルールと手筋を実装して調べるのでは、問題を自動生成するプログラムに使われている方法と本質的な差がなく、正当性の検証には無理がある。
全く違う原理のプログラムで確認
全く違う原理で解くにはどうすれば良いだろうか？
ルールの実装はどうしても必要だろう。それが無ければ、そもそもパズルが成立しない。
しかし、手筋の実装はバグが入っている可能性が否定できない。人間が手筋を考えた時点で既にバグがあるかも知れないし、ましてプログラムにするとさらにバグが入る可能性がある。
なので、手筋の実装をしないで確認する方法を選ぶべきである。
となると、全件探索、虱潰しが考えられる。標準の９ｘ９のナンプレ問題なら、延々と再帰を使って虱潰しをしても、１秒のかかることはないだろう。簡単な練習問題なので、再帰を勉強した初心者が挑戦するに手頃な課題だ。
でも、２８０合体ナンプレを虱潰しをするのは、どう考えて無謀である。単純に虱潰しをしたら、たぶん地球の寿命の方が先に尽きるだろう。
量子コンピュータを使うとどうなるだろう。しかし、量子コンピュータでこの手の問題がサクッと解けるかどうか、自分は知らない。とりあえず、将来の課題にしておく。
世の中には、手筋を書けないようなプログラミング言語が存在する。プログラミング的に言えば、制御文が無く、条件だけ与えて問題を解く。
その代表の１つが充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）である。以下、SATと書く。
SATで解く場合、各マスには１から９のいずれかが入ると宣言し、それらのマスの間で成立しなければいけない条件はルールから与えられる。手筋はプログラムしないので、今回の条件をとても良く満たしている。
さて、SATなのだが、これを自分、あるいは自分たちでプログラムを作って解いたのではいけない。第三者がSATのプログラムを作らないといけない。
それで、日本のSATの権威者を探しだした。というか、探すまでもなく、神戸大学情報基盤センターの田村教授以外に考えられない。この分野で有名な国際制約ソルバー競技会で何度も優勝しているチームの代表である。とくに、パズルをSugar制約ソルバーで解くというページには、多数のパズルを解いた例があり、 Sugarのプログラムも掲載されていて、至れり尽くせりである。
ということで、田村教授にお願いして検証していただき、検証を終えることができた。
SATについての説明は長くなるので省略する。詳しくは、田村教授のページなどで調べて欲しい。
ということで、正当性が裏付けられた。
ちなみに、SATでの検証時間は、ユニーク性まで調べて、全てで１分かからなかったそうだ。
SATは、条件だけ、つまり条件全部を１つの命題論理式にまとめて、その論理式の真偽を問うもので、真になったときに命題論理式に含まれる全ての変数の値を出力するのが一般的。
SATの場合、通常のプログラミング言語と違い、処理を考える必要はない。とくに、処理を考えるのが困難な場合、非常に有効になる。
SATでは、結局は虱潰しをしている訳だが、実装によって虱潰しの効率に著しい違いが存在する。
普通の制御文だらけのプログラム以外の世界を覗いてみたい場合、SATはその候補の１つだろう。
プログラムは上から順番に実行されるなどという思考に囚われた石頭を壊すために、ぜひ試用してみよう。
ということで、MATH POWER 2018でギネス世界記録™のシリーズを終える。
完
＃人気の記事
＃タグ
