投射モデル計数のためのグラフ表現を用いた問題分類と計数戦略
| Project/Area Number |
23K11045
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| Project Period (FY) |
2023-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2025: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2023: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
|
|---|
| Keywords | 投射モデル計数 / 機械学習 / 分類 / 分割 / モデル計数 / SAT |
|---|
| Outline of Research at the Start |
確率や量的な安全尺度の計算への応用を背景にして、論理式の解（モデル）の個数を高速に数える技術の必要性が高まっている。命題論理式のための既存の投射モデル計数ソルバやその計数戦略には一長一短があるが、それらを入力問題ごとに適切に切り替えるための有効な問題分類方法は知られていない。本研究では、論理式のグラフ表現に着目し、その特徴量を用いた投射モデル計数のための問題分類と計数戦略決定を試みる。機械学習を用いたモデル学習を通して、投射モデル計数問題の分類に役立つグラフ表現の特徴量を見いだすことで、高速に解くことができる適切なソルバや計数戦略を問題ごとに決定するシステムを構築する。
|
| Outline of Annual Research Achievements |
我々の研究グループでは、与えられた命題論理式全体を真にする変数への真理値割当て（モデル）のうち、指定された変数集合に関して異なるモデルがいくつか存在するかを計数する問題（投射モデル計数）を解くソルバを開発している。投射モデル計数ソルバは他機関でも開発されており、それらの性能は問題ごとに一長一短がある。令和６年度はまず、与えられた投射モデル計数問題に対して、その命題論理式の特徴量から計数問題を最も速く解くことができるソルバを事前決定するための分類器構築に関する研究に取り組んだ。モデル計数ではなくSAT判定に対し機械学習を利用してソルバ決定を行う既存ソルバとしてSATzillaが知られている。今年度は、SATzillaで利用されている命題論理式の特徴量と、線形回帰モデルを用いた分類器構築のアプローチを採用して、投射モデル計数問題でのソルバ決定に利用できるかを検討した。現状は線形回帰モデルを用いたアプローチでは良い分類性能を達成できておらず、計数対象の命題論理式のグラフの特徴量（グラフ表現の次数等）も一部組み入れたが、現行のアプローチで投射モデル計数問題を解くソルバの特徴をうまく捉えるのは難しいという見通しを得ている。今年度は他に、グラフのパス計数問題や敷詰めパズルの解計数問題をモデル計数ソルバを利用して解く方法についての研究にも取り組んだ。グラフのパス計数問題については、パス計数問題を小さいグラフのパス列挙問題に分解してその結果を組み合わせることで全体のパス計数を行う手法を提案し、単にモデル計数問題に単純に帰着して解く方法よりも多くの問題を解くことができるようになった。2023年に開催されたグラフパス計数競技会<https://afsa.jp/icgca/>に参加し、提案手法を実装したソルバはアイデア部門で1位という結果を得た。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
与えられた投射モデル計数問題を最も速く問題を解くことができるソルバを事前決定するための分類器構築については、分類性能の改善に課題が残っているものの、学習・評価を行う環境を整備できたことや、投射モデル計数問題のためのソルバ決定においては少なくともSATソルバのための既存の特徴量だけでは有効ではない裏付けは得られた。グラフパス計数問題に対しては、有効な分割結合手法を考案でき、グラフパス計数競技会でアイデア部門1位という良い結果を得ることができた。他にも、モデル計数問題一般に利用できる汎用的な分割結合手法の開発のため、タイルの敷き詰め問題を題材に新たに問題の分割結合の方法を提案しその有効性を確認した。
|
| Strategy for Future Research Activity |
ソルバ選択に関する研究については、引き続き、投射モデル計数問題独自の新たな特徴量の検討と、線形回帰モデル以外に深層学習などを利用した方法を検討する。また、ソルバ単体の性能改善のため、機械学習を利用した変数選択ヒューリスティクスや簡単化のための前処理の切り替え手法について検討する予定である。グラフパス計数問題に対する分割結合手法についても引き続き改良を行い、その他にも具体的な計数問題を題材に有効な分割結合手法を検討する。それらを通して、モデル計数問題一般に適用できるように分割結合手法を汎化できるかについても検討する予定である。
|
Report
(1 results)
Research Products
(1 results)
