2017 Fiscal Year Annual Research Report
An extension of SQL language for constraint programming on database and its processing system
| Project/Area Number |
17H01721
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
酒井 正彦 名古屋大学, 情報学研究科, 教授 (50215597)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 組合せ最適化問題 / SMTソルバ / SQL言語 |
|---|
| Outline of Annual Research Achievements |
本研究は、組み合わせ問題を関係データベース上の制約問題として捉えることで問題を容易に記述可能な拡張SQL言語を設計すると共に、その問題記述に隠れている構造情報を基とする巧みな変換を与えることで、効率的な処理システムを実現する。これにより、制約ソルバの知識なしに効率良く問題解決するための手法の構築を目的としている。
実際に言語設計ならびに処理系の基本設計に関わる言語が表現する意味の形式化を進めるうちに、研究計画当初のFind‐Subset‐Of‐Such‐That構文の拡張法よりも、意味の領域として表の集合を扱うのが自然でありユーザが組合せ問題を理解しやすいこと、処理系の設計にも問題がないことがわかった。具体的に定めた言語設計方針は以下のとおりである。（１）組合せ問題の探索空間に相当する表の集合を生成する構文を定める。（２）探索空間中で記述したい問題に由来する表のみが成立するような制約を通常のSQL構文のみで記述可能にする。（３）（２）と同様な手法を用いて最適化関数もSQL構文で記述可能にする。この言語は計画当初の構文での記述を含むだけでなく、より幅広い考え方での記述を可能に出来た。
記述に対して自然な方法で実装した場合には組合せ爆発が生じて全く実用的ではない。そのため、次の実装のための手法を考案した。（１）拡張表：データベースの表に通常のデータだけでなく変数を格納できるように拡張した表とする。（２）制約付き表：拡張表とそこで用いられている変数が満たすべき制約の対とする。制約付き表にある制約を満たす変すへの割当は一意ではないことから、制約付き表は通常の表の集合をあらわすことができる。（３）SQLのそれぞれの問い合わせ関数を制約付き表上の関数に拡張する。これにより得られた制約は記念注目を浴びているSMTソルバを利用して効率よく解くことが可能となる。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
当初の計画のFind‐Subset‐Of‐Such‐That構文を採用せず、より柔軟な記述を可能にするための概念と言語構造を模索したため、まだ該当年度終了時においては、実際に問題を解くために必要となる、言語記述からの制約生成のおおよその手法は確立できたものの、その正しさの証明やシステムの実現が完了していなかった。
この報告書執筆の時点では正しさの証明が完了している。その証明のプロセスにおいて、制約生成のための定義に誤りが見つかり、その修正を行うことが出来た。これにより、システム実装の障害を取り除くことが出来たため、２年度目では当初計画に追いつくことが可能であると予想している。
|
| Strategy for Future Research Activity |
２年度目当初で変換の正しさの証明が完了したので、今後はまずシステムの実装を完了させる。さらには、様々な組合せ問題を実際に記述し、実験・評価を行う。その結果により３年めである最終年度の研究の方向性を定める。具体的には、さらなる高速化のために既存のSMTソルバの改良、提案言語の改良も視野に入れる。
|
