研究課題
本研究は、組み合わせ問題を関係データベース上の制約問題として捉えることで問題を容易に記述可能な拡張SQL言語を設計すると共に、その問題記述に隠れている構造情報を基とする巧みな変換を与えることで、効率的な処理システムを実現する。これにより、制約ソルバの知識なしに効率良く問題解決するための手法の構築を目的としている。初年度のアイデアが効果的であったことで、システムの実装のための理論の整備、ならびに、実装が予想よりもうまく進んだ。その内容を以下で具体的に述べる。（１）データだけでなく変数を格納できるように拡張した表と変数上の制約の対（制約付き表）による表の集合の表現に対して、各要素からSQL演算により得られる制約付き表を形式的に定義し、その正しさの証明を与えた。（２）前項の処理は限られたSQL演算のみに制限しても非常に複雑であり、システム実装には今後の拡張や保守に不利であると判断し、新たな変換に基づく手法を考案した。このSQL間の変換は、出力のSQL式を制約付き表に対してSQLエンジンにより実行するだけで、入力の集合上のSQL演算で定義される制約付き表を生成できるという特長を持つ。これにより、複雑なSQLエンジンに手を入れることなくシステムが実現できるだけでなく、既存SQLエンジンの最適化によるメリットが享受できた。（３）提案手法に基づき、拡張SQL言語による組合せ最適化問題記述と個々のデータベースの表から、既存の最新のSMTソルバを利用して求解するシステムを作成し、ほぼ全てのSQL演算を扱うことに成功した。（４）頂点色付け問題においては手作業でSMTソルバの入力を作成・実行した場合と比較しても遜色のない効率であることが確認できた。一方でより複雑な問題の場合には、期待ほどの効率的な実行が出来ずSMTソルバの入力を生成する部分の改良が必須であるとの主観的な評価を得た。
1: 当初の計画以上に進展している
当初の計画においては、設計した拡張SQL言語で利用できるSQL演算を限定したシステムの実装を行う予定であったが、変換に基づく画期的な実装理論を思いつき理論的詳細化に成功したことにより、ベースシステムであるSQLiteで利用可能なほぼすべてのSQL演算を利用した組合せ最適化問題記述を扱うシステムが実装できた。これにより、初年度の遅れ分を取り戻すばかりか、予定以上に研究が進捗したと言える。一方で、処理対象が複雑な問題の場合に、期待ほどの効率的な実行が出来ていない。そのためSMTソルバの入力を生成する部分の改良が必須である。
これまでにシステムの実装が完了したので、これまで以上に様々な組合せ問題を実際に記述し実験・評価を行い、効率化を謀る。すでに判明したいくつかのSMTソルバに与える制約の生成における効率化のためのアイデアを実装し、さらなる問題点や効率化のアイデアを探る。具体的には、SMTソルバに与える制約の生成法の改良だけでなく既存のSMTソルバの改良も視野に入れる。
すべて 2019 2018
すべて 雑誌論文 (1件) (うち査読あり 1件、 オープンアクセス 1件) 学会発表 (3件) (うち国際学会 1件)
Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018), ACM, isbn:978-1-4503-6441-6
巻: PPDP2018 ページ: 19:1-19:13
10.1145/3236950.3236963
