| 研究課題/領域番号 |
18K18027
|
|---|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2022-03-31
|
| キーワード | QBF / 論理ソルバ / 並列計算 |
|---|
| 研究実績の概要 |
近年は計算機の進化、並列システムの普及と充足可能性問題(SAT)ソルバの高速化が非常に有効な組み合わせになり、様々な分野で応用されている。このような問題の一部は、SATに効率的に書き換えられないと思われるがSATの一般化である「量化されたブール式問題」(QBF)に書き換えQBFソルバを応用するのが望ましい。QBFはまだSATほど普及していないが、今後普及されると思われるので、現時点は大きな機会だと思われる。特に数学の未解決問題等に論理ソルバを応用する場合は大規模並列計算機の利用が重要になる。したがって、本研究の目的は大規模な複雑な問題に対するQBF技術とその応用になっている。
このような並列QBFソルバを応用する前は並列ソルバに関する基礎研究と開発が必要になるため、初年度の計画と予定は大規模な並列QBFソルバに関する基礎的な研究とその並列ソルバの開発になった。2018年度は概ね予定通りにその基礎研究と開発を進めてきて、予定通り2014年に共同で開発したソルバを超えている。本研究の目的になる並列QBFソルバは一年間で完成するものではないと当初の計画でも述べたが、基礎のところから始まり順調に進んでいる。開発中のソルバは現時点公開していないため、今後開発を進めて発表とオープンソーソとして公開に向かう計画である。また、本研究に関する打ち合わせや議論の影響で、当初計画していなかった関連する研究成果もあり、本研究と関係する技術を他分野で応用ができている。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初予定では、2018年度の計画は大規模な並列QBFソルバに関する基礎的な研究とその並列ソルバの開発になった。その並列ソルバは一年間で完成するものではないためまだ公開していないが、予定通り基礎研究と開発を進めているので計画通り概ね順調に進展している。本研究のための打ち合わせと議論をした影響で当初計画していなかった他分野の共同研究の成果もできた。
|
| 今後の研究の推進方策 |
今後は基本的に当初の計画通り進める。大規模な並列ソルバの開発は一年で終わるテーマではないため、まずは第二・三年度ではソルバの基礎研究と開発の続きと数学のオー プン問題に応用するための基礎研究を始める。具体的な例として、数学の問題を解くため証明も必要になるため、出力を証明す るcertificateの並列生成手法に関する基礎研究がある。また、並列ソルバにおいて学習節の共用に関する研究もする。
|
