大規模並列論理ソルバと記述計算量への応用

2021 年度 研究成果報告書

• 研究課題/領域番号: 18K18027
• 研究種目: 若手研究
• 配分区分: 基金
• 審査区分: 小区分60050:ソフトウェア関連
• 研究機関: 小樽商科大学 (2021); 北海道大学 (2018-2020)
• 研究代表者: ジョーダン チャールズハロルド 小樽商科大学, 商学部, 准教授 (60647577)
• 研究期間 (年度): 2018-04-01 – 2022-03-31
• キーワード: QBF / 並列論理ソルバ / QBFソルバ

研究成果の概要

並列計算機の普及と高速アルゴリズムが極めて有向な組合せで様々な分野で応用されてきた。問題を数理論理で表し、その式化された問題を解く論理ソルバも近年広く応用される。本研究の目的は、(1)近年話題になった「量化されたブール式問題」(QBF)論理ソルバをより大規模な並列計算機で利用できるようにすること及び(2)このような論理ソルバを数学未解決問題に適応できることになった。
成果は主に(1)本研究で開発してきた並列ソルバをフリーソフトとして公開、(2)現在公開準備中の環境においてこれをグラフ理論の未解決問題に適応するフレームワークの開発、(3)当初想像しなかった幾何計算での論理ソルバの応用になる。

自由記述の分野

アルゴリズム、形式論理

研究成果の学術的意義や社会的意義

近年並列計算機および高速アルゴリズムを様々な分野や問題に適応されている。本研究の成果では、より大規模な並列計算機で高速論理ソルバが利用できるようになったことと、記述計算量に基づくフレームワークを利用することによって、最新QBFソルバを利用する時のより記述しやすい高水準言語が使えるようになった。また、当初想像しなかった幾何計算での応用も量子物理学に応用があり、他の研究者に利用されると期待できる。これらは実装し、フリーソフトとして公開するため、無料で自由に使える研究道具になっている。