2019 Fiscal Year Research-status Report

大規模制約充足問題の全解探索のための実用的な計算基盤の確立とその応用

Research Project

Project/Area Number	17K17725
Research Institution	The University of Electro-Communications
Principal Investigator	戸田貴久電気通信大学, 大学院情報理工学研究科, 准教授 (50451159)
Project Period (FY)	2017-04-01 – 2021-03-31
Keywords	モデル検査 / アルゴリズム / SAT / 制約
Outline of Annual Research Achievements	数独のヒント生成を制約充足問題としてモデル化し、高速ソルバーを適用することで解を求める手法を提案した。数独はパズルの計算論的な観点から研究対象とされることも多く、また、大規模な問題の求解に取り組むことで特定の問題に依存しない制約充足解法の開発や発展につながることも期待される。数独のヒント生成では、（有界モデル検査と同様に）状態遷移の観点から計算を抽象化できることが分かり、本研究では、これを数独の状態遷移モデルとして形式化した。このモデルにより、いくつかの戦略（数独の解を求めるための手続き）が指定されるとき、数独ヒントがそれらの戦略だけを使って解を求められるか否か（戦略可解と呼ぶ）について、厳密に特徴づけることが可能になる。既知の戦略だけでなく、一定の仮定の下で未知の戦略をもこの枠組みの中で扱うことができるようになる。この枠組みに基づき、本研究では戦略可解なヒントを生成するための厳密手法を開発した。９ｘ９の盤面でさえ、戦略可解なヒントを生成する問題（特に少数ヒントの場合）は制約充足問題として非常の大きな規模となり、その解を求めることはかなり難しいことが実験により判明した。ただ、いくつかの場合では、制約充足の最新技法を駆使することで、例えば、戦略可解なヒントが存在しないことの証明を与えることなどが現実に可能になることが判明した。数独の最小ヒント数が１７であるという非常に有名な既存研究があるが、これに対して戦略可解な数独の最小ヒントが17であるかという興味深い（おそらく）未解決の問題を考えることができることを提示した。この問題の解決のためには、さらなる効率化が必要になる。
Current Status of Research Progress	Current Status of Research Progress 2: Research has progressed on the whole more than it was originally planned. Reason 新たな展開として、数独のヒント生成に関わる厳密解法を開発することができた。これまでの制約充足問題に関する知見や最新の技法を駆使することで、いくつかの設定では、他の方法では不可能であったような計算も現実に可能になることが判明し、大きな進展が得られた。これらの結果はすでに論文にまとめ、学術雑誌に投稿した。また、本研究に関わるプログラムや各種のデータはホームページで誰でも利用できる形で公開した。
Strategy for Future Research Activity	これまでにひきつづき、有界モデル検査に関わるこれまでの研究結果を整理をする。プログラムはまだ一般に公開できるレベルにはなっていないので、プログラムや関連する各種の資料の整理をすることが残されている。今回あらたに得られた数独の結果に関しては、重要な未解決問題が残されている。事前実験で現状の技術でこの問題を解決することは相当困難になりそうなことが分かっているので、最新の制約充足技法を適用することやさらなる工夫を考案することなどにより、問題の解決に向けて取り組みたい。また、この結果の本質的な部分は数独に限定されないので、数独以外の問題にも応用することを検討していきたい。
Causes of Carryover	昨年度に予定していた出張やそれにかかわる招待講演者の依頼出張などがコロナ感染拡大のため取りやめになったため。