投射モデル計数のためのグラフ表現を用いた問題分類と計数戦略

Research Project

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	確率や量的な安全尺度の計算への応用を背景にして、論理式の解（モデル）の個数を高速に数える技術の必要性が高まっている。命題論理式のための既存の投射モデル計数ソルバやその計数戦略には一長一短があるが、それらを入力問題ごとに適切に切り替えるための有効な問題分類方法は知られていない。本研究では、論理式のグラフ表現に着目し、その特徴量を用いた投射モデル計数のための問題分類と計数戦略決定を試みる。機械学習を用いたモデル学習を通して、投射モデル計数問題の分類に役立つグラフ表現の特徴量を見いだすことで、高速に解くことができる適切なソルバや計数戦略を問題ごとに決定するシステムを構築する。