|
近年は並列計算機の普及と高速アルゴリズムの進達が極めて有効な組み合わせになり、様々な分野に適応されてきた。計算問題を数理論理で表し、その式化された問題を解く高速論理ソルバも近年アルゴリズムと実装の高速化により広く応用される。この背景において、本研究は「量化されたブール式問題」(QBF)と呼ばれる数理論理の計算問題とその応用になる。特に、QBFはまだ他のソルバ程普及していないため、本研究の目的は(1)QBFソルバの大規模な並列化、(2)論理ソルバの使いやすさと(3)QBFソルバ等を数学の未解決問題に適応できることとなっている。
研究期間中新型コロナウィルスの影響で突然国際会議への出席や海外の研究者との交流に様々な影響を受けて、また2021年度は北海道大学から小樽商科大学に移った時並列計算機の計算機室がなくなったことがあったが、研究実績は以下のようだった。
まずは、QBFソルバを未解決問題に適応するためより表現力のある高水準言語が必要だった。本研究では、有限モデル理論の分野に基づいて、従来利用される二階述語論理に推移閉包の演算子を追加することを行い、記述プログラミング環境にその実装を追加した。これにより、グラフ理論の有名なオープン問題にQBFソルバを応用できるようになった。
小樽商科大学に移ったため実験用の計算機室が大幅に変わったが、本年度の主な成果は以下のようになる。
次は本研究の基礎の一つの並列QBFソルバ開発についても研究と開発続けてきた。フリーソフトのcmdqbfとして公開している。今年度計算機室がなくなり、新しい並列計算機で実験できるようになったため、現在性能評価を行なっている。
また、当初計画していなかった成果もあった。幾何計算において有名なプリトープに論理ソルバを適応することが有効だと分かり、開発したフリーソフトをこの分野において有名なlrslibの中で公開した。
|
