高性能論理ソルバと幾何計算の結合による技術発展とその応用

Research Project

Project/Area Number	23K11043
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60050:Software-related
Research Institution	Otaru University of Commerce
Principal Investigator	ジョーダンチャールズハロルド小樽商科大学, 商学部, 准教授 (60647577)
Co-Investigator(Kenkyū-buntansha)	Avis David 京都大学, 情報学研究科, 非常勤講師 (90584110)
Project Period (FY)	2023-04-01 – 2028-03-31
Project Status	Granted (Fiscal Year 2023)
Budget Amount *help	¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000) Fiscal Year 2027: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000) Fiscal Year 2026: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000) Fiscal Year 2025: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000) Fiscal Year 2024: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000) Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Keywords	幾何計算 / ポリトープ / 論理ソルバ / SMTソルバ
Outline of Research at the Start	近年は計算機の進化と高速アルゴリズムの進達により、形式論理の計算問題を高速に解く論理ソルバが極めて有効な計算道具になり、数学の有名な未解決問題の回答から企業での成功まで、異分野の様々な重要な課題に適応されている。幾何計算の分野において、ポリトープと呼ばれる構造に関する計算が古典的な課題であり、生物学、材料工学、物理学等異分野で利用される重要な計算問題である。本研究は幾何計算の計算問題と高性能論理ソルバの組合せにより、異分野で行いたいが従来現実的ではない計算を可能にする。本研究で開発する新しいアプローチをフリーソフトとして実装し、無料で自由に使える研究道具になる。
Outline of Annual Research Achievements	幾何計算の分野ではポリトープと呼ばれる構造に関する計算が古典的な課題であり、生物学、材料工学、物理学等異分野で利用される重要な計算問題である。本研究は幾何計算のポリトープに関する計算と論理ソルバの組合せにより、異分野で行いたいが従来現実的ではない計算を可能にする。研究目的は(a)論理ソルバに基づいて、幾何計算の計算問題を解く新しいアプローチを提案・評価、(b)上記のアプローチを実装し、異分野研究者が自由に利用できるオープンソースとして公開、(c)異分野の実問題をベンチマーク問題として利用し、論理ソルバの進達と改善である。従って、本研究で期待できる貢献は(a)論理ソルバを利用する本研究の新しいアプローチにより、幾何計算の分野での貢献、(b) 開発するオープンソース実装が異分野の研究者に利用されることによるインパクト、(c) 幾何計算の計算問題をベンチマークとして利用し、論理ソルバ分野での改善と貢献になる。今年度の主な研究実績は(1)幾何計算のいくつかの計算問題を高速論理ソルバで解く手法とその実装、(2)この実装を利用して、幾何計算における応用をベンチマーク問題として論理ソルバの国際コンペティションに提供、(3)幾何計算における計算問題に対して当初考えていなかった新しい並列化とその実装になる。まずは(1)は本研究の基礎になるが、幾何計算のいくつかの計算問題に対して論理ソルバを利用する手法と実装をした。次のlrslibバージョンで公開する。次は(2)について、この新しい実装を利用して幾何計算の面白い計算問題からベンチマーク問題を作成し、SMTと呼ばれる論理ソルバを評価する国際コンペティションに提供した。新しいベンチマーク問題は論理ソルバの進達に貢献できる可能性がある。(3)についてはlrslib内の並列実装を新しい計算問題に拡張した。こちらも次のlrslibバージョンで公開する。
Current Status of Research Progress	Current Status of Research Progress 2: Research has progressed on the whole more than it was originally planned. Reason 研究目的は(a)論理ソルバに基づいて、幾何計算の計算問題を解く新しいアプローチを提案・評価、(b)上記のアプローチを実装し、異分野研究者が自由に利用できるオープンソースとして公開、(c)異分野の実問題をベンチマーク問題として利用し、論理ソルバの進達と改善である。研究実績の概要で述べたように、初年度では(1)幾何計算のいくつかの計算問題を高速論理ソルバで解く手法とその実装、(2)この実装を利用して、幾何計算における応用をベンチマーク問題として論理ソルバの国際コンペティションに提供、(3)幾何計算における計算問題に対して当初考えていなかった新しい並列化とその実装ができた。従って、おおむね順調に進展していると評価する。特に、(3)については当初予定していなかった課題だが、本研究と関連する目的を異なる手法になり当初計画以上進展している部分もある。(1)の実装をオープンソースとして公開することは第2年度予定しているため、総合的に評価するとおおむね順調に進展しているといえる。
Strategy for Future Research Activity	今後の研究の推進方策は様々あるが、ここでは次の３つについて述べる：(1)初年度での研究実績に関する報告や実装の公開、(2)当初予定していなかったlrslibでの並列実装をさらに拡張、(3)本研究の基礎になる幾何計算における論理ソルバに基づくアプローチをさらに拡張・解析する。まずは、(1)については本研究の基礎的な手法と実装が初年度中できたが、異分野の研究者等が利用するためドキュメンテーションや検証も必要になり、実装の公開は第2年度になると予定している。また、初年度の研究実績を論文で報告する予定だが、lrslibでの新しい並列化と論理ソルバの利用を異なる論文で分ける予定である。次は、(2)については初年度中はlrslib内で計算問題の規模を近似する機能等並列化できると分かり、大規模な計算問題に対し大規模な並列計算機が使えることが重要になるため今後そのような並列化を行いたい。 (3)については本研究の新しいアプローチの有効性と限界を理解するため、幾何計算における様々な計算問題に拡張する。