| 研究課題/領域番号 |
18K18027
|
|---|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2022-03-31
|
| キーワード | QBF / 並列論理ソルバ / QBFソルバ |
|---|
| 研究実績の概要 |
近年は計算機の進化、並列システムの普及と充足可能性問題(SAT)ソルバの高速化が非常に有効な組み合わせになり、様々な分野で応用されている。このような 問題の一部は、SATに効率的に書き換えられないと思われるがSATの一般化である「量化されたブール式問題」(QBF)に書き換えQBFソルバを応用するのが望まし い。QBFはまだSATほど普及していないが、今後普及されると思われるので、現時点は大きな機会だと思われる。特に数学の未解決問題等に論理ソルバを応用する 場合は大規模並列計算機の利用が重要になる。したがって、本研究の目的は大規模な複雑な問題に対するQBF技術とその応用になっている。
本年度は新型コロナウィルスの影響で国際会議への出張や海外の研究者との交流に様々な影響があり、国内・海外出張をせずに直接経費は利用しなかった。当初の計画では新型コロナウィルスは想像していなかったので影響はあったが、本年度の主な成果は以下のようになる。
まずは、去年度の報告で本年度計画していた課題になる。有限モデル理論経由で数学のオープン問題に本研究で開発しているQBFソルバを応用することが目的の一つになる。従来研究ではグラフ理論の問題等を二階述語論理で表しQBFソルバを利用する研究がある。つまり、QBFの高水準言語として二階述語論理を用いることは有効だが、推移閉包の演算子で拡張してもQBFの高水準言語として理論的に適切な言語でありより効果的になる。特にグラフマイナー関連の推測の有限版を表す場合推移閉包の演算子が有効になり、この推測の様々な有限版をQBFソルバで確認することができる。本年度は主にこの応用に集中しているが、大規模な並列ソルバに関する基礎研究と開発を続けている。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
当初予定では新型コロナウィルスの影響を想像していなかったが、出張や交流が突然計画通りできなくなって、本年度は出張や関連研究者の訪問がなかった。それにより本年度は本研究の直接経費の利用がなかったので、来年度等フレキシブルに対応できるようになった。やや遅れているのは主に成果発表だといえる。
上記述べたように、有限モデル理論の概念に基づいて数学のオープン問題に関する応用に関する研究は概ね順調に進んでいるといえる。また、大規模な並列QBFソルバの開発と基礎研究が去年度も順調に進んでいたので、最終年度は新型コロナウィルスの現状によって、様々な交流や成果発表を計画している。その成果はまだ発表していないが、最終年度中発表できるようにする。
|
| 今後の研究の推進方策 |
新型コロナウィルスの影響で本年度は本研究の直接経費の利用がなかったため、今後フレキシブルに対応できる。最終年度は主に成果発表がしたいが、他大学に移動することにあたり並列計算機がなくなり最終年度は並列計算機を購入する予定になる。
最終年度に向かってまずは有限モデル理論に基づく数学のオープン問題に並列QBFソルバの応用に関する成果を発表する予定である。
|
| 次年度使用額が生じた理由 |
本年度は新型コロナウィルスのため、出張や共同研究者の訪問ができなかった。例年なら本研究の経費は国際会議SATとその連携ワークショップQBFに参加するための経費として不可欠だが、今年度は遠隔参加が無料等当初計画と異なる。当初新型コロナウィルスは想像していなかったので、今年度の経費は次年度使用を予定している。同時に他大学に移動することになるので、上記述べたように最終年度は並列計算機の購入が必要になることと新型コロナウィルスの現状によって成果発表・交流で使う予定。
|
