SATアルゴリズムとその形式的検証への応用

摘要

まず、論理式の充足可能性判定問題（SAT問題）を解くアルゴリズム（SAT手法と呼ぶ）について、DPLL法を中心にその歴史と現状について解説する。 次に、SAT手法を特に形式的な設計検証に適用する技術について、現状を解説する。 近年のSAT手法の大きな進歩により、実用規模のハードウェア設計検証や、ソフトウェアのバグハンティングが可能になってきている。 本稿はその状況を平易に解説することを目標としている。