A Novel Hardware SAT Solver Using Non-chronological Backtracking and Clause Recording

平本 新哉 (0551102)


充足可能性問題(Boolean satisfiability problem, SAT)はNP完全問題と知られ,多くのアプリケーションを持つ.

現在のソフトウェアSATソルバはnon-chronologicalバックトラッキング,clauseレコーディングを用いて,大幅な速度増加を 実現している.しかしながら,これらの手法は複雑な処理を必要とするため,多くのハードウェアSATソルバでは実装されていない. 現在のソフトウェアSATソルバより処理速度を上げるにはこれらの手法をハードウェアSATソルバにも実装する事が必要である.

本研究は,これらの手法を複雑な処理を用いずに実装する方法を示し,この方法を用いたハードウェアSATソルバを実装する. 実験により,EDAに関する問題において現在のソフトウェアSATソルバに比べ32-197倍の処理速度増加を 見積もる事ができた.

本発表では,提案手法と設計したSATソルバのアーキテクチャ,実験結果について述べる.