デジタル人材の育成

未踏ターゲット事業:2020年度採択プロジェクト概要(小津PJ)

1.担当PM

  • 棚橋 耕太郎(株式会社リクルートコミュニケーションズ リードエンジニア)

2.採択者氏名

  • 小津 泰生(名古屋大学 大学院理学研究科)

3.採択金額

  • 3,600,000円

4.プロジェクト名

  • アニーリングを用いた効率的な制約充足問題ソルバの実装

5.応募枠

  • 応用・実用化枠

6.関連Webサイト

  • なし

7.申請プロジェクト概要

私は、様々な社会的問題を解決するための新たな手段として、アニーリングを用いる方法を普及させたいと考えている。2019年度のプロジェクトで開発したSpoonQは、主に初心者のユーザーがアニーリングに関する専門的な技術を学ぶこと無く、問題をアニーリングによって手軽に解く方法を提供する。しかしながら、SpoonQを用いた方法は、古典コンピュータによる既存の問題解決手法とは全く異なるものであり、既にこのような手法を活用しているユーザーに対して、SpoonQを用いたアニーリングの活用を提案することは困難である。

今年度のプロジェクトでは、SAT問題を論理式に逆エンコードした上で、最適化処理を行い、アニーリングを用いて効率的に求解できるソルバを実装する。SAT問題は古典コンピュータを用いた既存の問題解決手法において広く使われているため、SAT問題のソルバを提供することで、既存の手法を活用しているユーザーに対しても、アニーリングの利用を提案することができるようになる。その結果、2019年度の成果物と合わせて、より広いユーザー層に対して問題解決のためのソリューションを提供できるようになることが期待される。さらに、SpoonQからこのソルバを活用できるようにすることにより、SpoonQを用いる場合でも、より効率的に問題を解くことができるようになると考えられる。

8.採択理由

本提案は前年度のアニーリングマシン用プログラミング言語開発に続く「応用・実用化枠」として、アニーリングマシン用の充足可能性問題(SAT)ソルバを開発するという提案である。前年度開発した言語では、アニーリングで解くべき問題を柔軟に式で定義することができ、内部的な変換によってマシンに入力するイジングモデルが自動的に得られるというものであった。SATの問題をアニーリングマシンで解く場合にも、SATがイジングモデルとしてどのように表現されるかという点が重要になってくる。

提案者は、論理式の最適化をはじめとした従来のSAT分野で培われた技術をアニーリング分野に適用することに情熱を持っているが、このような他分野からの技術移転はアニーリング技術の発展にとって不可欠である。今回開発するSATソルバは前年度開発したアニーリング用言語の内部エンジンとして活用される予定であり、前年度開発した言語の拡張としても意味のある取り組みであると考える。