| 研究課題/領域番号 |
18K18027
|
|---|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2022-03-31
|
| キーワード | QBF / 並列論理ソルバ / QBFソルバ |
|---|
| 研究実績の概要 |
近年は計算機の進化、並列システムの普及と充足可能性問題(SAT)ソルバの高速化が非常に有効な組み合わせになり、様々な分野で応用されている。このような 問題の一部は、SATに効率的に書き換えられないと思われるがSATの一般化である「量化されたブール式問題」(QBF)に書き換えQBFソルバを応用するのが望まし い。QBFはまだSATほど普及していないが、今後普及されると思われるので、現時点は大きな機会だと思われる。特に数学の未解決問題等に論理ソルバを応用する 場合は大規模並列計算機の利用が重要になる。したがって、本研究の目的は大規模な複雑な問題に対するQBF技術とその応用になっている。
本年度の主な成果は、本研究の中心部になる分散QBFソルバ(cmdqbf)の開発と公開である。オープンソースとして実装しているため、https://www-alg.ist.hokudai.ac.jp/~skip/cmdqbf/からダウンロード可能であり、上記述べたように様々な計算問題で応用できる。本研究の目的になる並列QBFソルバは一年間で完成するものではないと当初の計画でも述べたが、従来研究の2014年に共同で開発したソルバを超えている。特に探索空間の分け方、探索空間の部分的な結果を一般化できる場合探索空間の簡単化等が挙げられる。つまり、探索空間の一部を探索する場合は論理変数の一部を設定するが、部分的な結果を得るため不要の設定がある場合があり、それを利用することにより従来のソルバより高速化できている。また、本研究に関する打ち合わせや議論の影響で、当初計画していなかった関連する研究成果もあり、本研究と関係する技術を他分野で応用ができている。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初予定や去年度の推進方策では、今年度は本研究の中心部である分散QBFソルバをオープンソースとして公開することを計画していたが、それはできている。もちろん、2年間で完成や最終版にはなっていないが、従来研究のソルバを超えている。予定通り基礎研究と開発を進めているので計画通り概ね順調に進展している。本研究のための打ち合わせと議論をした影響で当初計画していなかった他分野の共同研究の成果もできた。本研究の目的は上記述べた分散QBFソルバと有限モデル理論等での応用になっているが、有限モデル理論での面白い新しい応用も今年度分かったため、2020年度はその応用についても研究する。一部の国際会議等は新型コロナウイルスの影響があるため、発表する場所を検討する。
|
| 今後の研究の推進方策 |
今後は基本的に当初の計画通り進める。大規模な並列ソルバの開発は一年で終わるテーマではないため、まずは2020年度もソルバの基礎研究と開発を続ける。また、上記述べたように有限モデル理論経由で数学のオープン問題に応用する研究に集中する。特に、従来研究ではグラフ理論の問題等を二階述語論理で表しQBFソルバを利用する研究がある。つまり、QBFの高水準言語として二階述語論理を用いることは有効だが、推移閉包の演算子で拡張してもQBFの高水準言語として理論的に適切な言語でありより効果的になる。したがって、2020年度からはこのような理論と応用をしながら、数学のオープン問題に本研究の並列ソルバを応用する。
2020年度は新型コロナウイルスの影響で国際会議等例年と異なる開催になると想像できるので、研究を発表する場所についても検討する。
|
