2021 Fiscal Year Final Research Report
Large-scale parallel logic solvers and applications using complexity
| Project/Area Number |
18K18027
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Otaru University of Commerce (2021)
Hokkaido University (2018-2020) |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | QBF / 並列論理ソルバ / QBFソルバ |
|---|
| Outline of Final Research Achievements |
The rapid development of parallel computers and high performance algorithms has found countless applications in recent years. Formalizing a problem in logic, and then solving the formalized problem has proven to be a particularly powerful approach. The basic goals of this research project were (1) developing parallel logic solvers (in particular for QBF) and (2) applying these logic solvers to mathematical questions via finite model theory.
The main results were (1) development of an initial parallel logic solver cmdqbf, (2) development of a framework for applying QBF solvers via finite model theory (currently under preparation for releasing) and (3) initially unplanned application of logic solvers to questions in computational geometry.
|
| Free Research Field |
アルゴリズム、形式論理
|
| Academic Significance and Societal Importance of the Research Achievements |
近年並列計算機および高速アルゴリズムを様々な分野や問題に適応されている。本研究の成果では、より大規模な並列計算機で高速論理ソルバが利用できるようになったことと、記述計算量に基づくフレームワークを利用することによって、最新QBFソルバを利用する時のより記述しやすい高水準言語が使えるようになった。また、当初想像しなかった幾何計算での応用も量子物理学に応用があり、他の研究者に利用されると期待できる。これらは実装し、フリーソフトとして公開するため、無料で自由に使える研究道具になっている。
|
