並列充足可能性判定器の実用的基盤の実現

• 研究課題/領域番号: 23K11214
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分61030:知能情報学関連
• 研究機関: 山梨大学
• 研究代表者: 鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
• 研究期間 (年度): 2023-04-01 – 2026-03-31
• 研究課題ステータス: 交付 (2023年度)
• 配分額: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円); 2025年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2024年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2023年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
• キーワード: 充足可能性判定問題 / 並列処理 / 決定的挙動 / 充足不能証明

研究開始時の研究の概要

SATは計算機科学における最も基本的かつ本質的な組み合わせ問題であるとともに，ハードウェア・ソフトウェアの検証やプランニング，スケジューリングなど実社会における様々な応用領域の基盤推論技術として幅広く利用されている．複数のCPUや計算機を利用するSATの並列解法は強力な求解能力を提供できる有望な方法の１つであるが，ほとんどの並列SATソルバーでは挙動に再現性がなく，充足不能の証明がサポートされていないなどの実用上の課題がある．本研究ではこれらの課題の解消を目的とするとともに，その成果を既存の逐次SATソルバーを容易に組み込み可能な汎用フレームワークとして提供することを目指す．