| 研究課題/領域番号 |
23K11045
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| 研究期間 (年度) |
2023-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2025年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2024年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2023年度: 2,470千円 (直接経費: 1,900千円、間接経費: 570千円)
|
|---|
| キーワード | 投射モデル計数 / 機械学習 / 分類 / 分割 / モデル計数 / SAT |
|---|
| 研究開始時の研究の概要 |
確率や量的な安全尺度の計算への応用を背景にして、論理式の解（モデル）の個数を高速に数える技術の必要性が高まっている。命題論理式のための既存の投射モデル計数ソルバやその計数戦略には一長一短があるが、それらを入力問題ごとに適切に切り替えるための有効な問題分類方法は知られていない。本研究では、論理式のグラフ表現に着目し、その特徴量を用いた投射モデル計数のための問題分類と計数戦略決定を試みる。機械学習を用いたモデル学習を通して、投射モデル計数問題の分類に役立つグラフ表現の特徴量を見いだすことで、高速に解くことができる適切なソルバや計数戦略を問題ごとに決定するシステムを構築する。
|
| 研究実績の概要 |
我々の研究グループでは、与えられた命題論理式全体を真にする変数への真理値割当て（モデル）のうち、指定された変数集合に関して異なるモデルがいくつか存在するかを計数する問題（投射モデル計数）を解くソルバを開発している。投射モデル計数ソルバは他機関でも開発されており、それらの性能は問題ごとに一長一短がある。令和６年度はまず、与えられた投射モデル計数問題に対して、その命題論理式の特徴量から計数問題を最も速く解くことができるソルバを事前決定するための分類器構築に関する研究に取り組んだ。モデル計数ではなくSAT判定に対し機械学習を利用してソルバ決定を行う既存ソルバとしてSATzillaが知られている。今年度は、SATzillaで利用されている命題論理式の特徴量と、線形回帰モデルを用いた分類器構築のアプローチを採用して、投射モデル計数問題でのソルバ決定に利用できるかを検討した。現状は線形回帰モデルを用いたアプローチでは良い分類性能を達成できておらず、計数対象の命題論理式のグラフの特徴量（グラフ表現の次数等）も一部組み入れたが、現行のアプローチで投射モデル計数問題を解くソルバの特徴をうまく捉えるのは難しいという見通しを得ている。今年度は他に、グラフのパス計数問題や敷詰めパズルの解計数問題をモデル計数ソルバを利用して解く方法についての研究にも取り組んだ。グラフのパス計数問題については、パス計数問題を小さいグラフのパス列挙問題に分解してその結果を組み合わせることで全体のパス計数を行う手法を提案し、単にモデル計数問題に単純に帰着して解く方法よりも多くの問題を解くことができるようになった。2023年に開催されたグラフパス計数競技会<https://afsa.jp/icgca/>に参加し、提案手法を実装したソルバはアイデア部門で1位という結果を得た。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
与えられた投射モデル計数問題を最も速く問題を解くことができるソルバを事前決定するための分類器構築については、分類性能の改善に課題が残っているものの、学習・評価を行う環境を整備できたことや、投射モデル計数問題のためのソルバ決定においては少なくともSATソルバのための既存の特徴量だけでは有効ではない裏付けは得られた。グラフパス計数問題に対しては、有効な分割結合手法を考案でき、グラフパス計数競技会でアイデア部門1位という良い結果を得ることができた。他にも、モデル計数問題一般に利用できる汎用的な分割結合手法の開発のため、タイルの敷き詰め問題を題材に新たに問題の分割結合の方法を提案しその有効性を確認した。
|
| 今後の研究の推進方策 |
ソルバ選択に関する研究については、引き続き、投射モデル計数問題独自の新たな特徴量の検討と、線形回帰モデル以外に深層学習などを利用した方法を検討する。また、ソルバ単体の性能改善のため、機械学習を利用した変数選択ヒューリスティクスや簡単化のための前処理の切り替え手法について検討する予定である。グラフパス計数問題に対する分割結合手法についても引き続き改良を行い、その他にも具体的な計数問題を題材に有効な分割結合手法を検討する。それらを通して、モデル計数問題一般に適用できるように分割結合手法を汎化できるかについても検討する予定である。
|
