高速SATソルバーの原理と応用高速SATソルバーの原理 鍋島 英知 nabesima@yamanashi.ac.jp 山梨大学 湊離散構造処理系プロジェクトERATO セミナー はじめに SAT = 命題論理式の充足可能性を判定する問題 計算機科学における最も基本的で本質的な組合せ問題 90年代末頃からSAT ソルバーの性能が飛躍的に向上 数百万変数からなる大規模な問題が求解可能に システム検証，プランニング，スケジューリング，定理証 明，制約充足問題など様々な分野で SAT が活用 2 SAT を利用した問題解決手法 3 SAT 問題 SAT の解 原問題 原問題の解 高速 SAT ソルバー 面倒 符号化 復号化 解決策の1つとして SAT 型 CSP ソルバーを利用 4 SAT 問題 SAT の解 CSP CSP の解 符号化 復号化 高速 SAT ソルバー 原問題 モデリング 原問題の解 解釈
