|
本研究は、組み合わせ問題を関係データベース上の制約問題として捉えることで問題を容易に記述可能な拡張SQL言語を設計すると共に、その問題記述に隠れている構造情報を基とする巧みな変換を与えることで、効率的な処理システムを実現する。これにより、制約ソルバの知識なしに効率良く問題解決するための手法の構築を目的としている。
平成３０年度までに想定よりも早く最低限の実装が済んたため、令和１年度より評価と性能改善に取り組み、研究成果の発表を行った。その具体的な内容は以下のとおりである。
当初の実装においては、外部SMTソルバに送付する問題を線形整数問題（QFLIA）のクラスとして表現していた。そのなかで、ブール変数を含む線形整数制約を構成するための手段として、if-then-else節を用いた型の形式変換を採用していたが、この形式の制約が外部SMTソルバの性能を引き出せず、効率を落とす一因であることが判明した。その対策として、線形整数制約に加えて、擬ブール節（Pseudo-Boolean constraint）の利用が効果的であると予想し、可能な場合にはそれを生成する方針を立て、システム改善を行った。これまでは入力仕様のSQL構文の各要素ごとにSMTソルバに送る制約を生成し要素間の橋渡しには制約変数を用いていたが、擬ブール節生成のためには複数の要素の情報を合わせて一括処理を行う必要があるため、必要に応じて制約生成を遅延させる機構を導入することで実装を可能にした。実験の結果、オーバーヘッドはほとんどなく、問題によっては一桁の速度向上が確認された。
|
