핵심 개념
本研究では、SAT問題を回路形式に変換し、強化学習ベースのロジック合成手法と新しいコスト最適化LUTマッピング手法を用いて、SAT問題の解決時間を大幅に削減する前処理フレームワークを提案する。
초록
本論文は、SAT問題解決のための新しい前処理フレームワークを提案している。
まず、入力のCNF形式のSAT問題をAIG回路に変換する。次に、強化学習ベースのロジック合成手法を用いて、回路を最適化する。この際、SAT解決時間の削減を目的関数とする。さらに、コスト最適化LUTマッピング手法を用いて、SAT解決がより容易な回路に変換する。最後に、最適化された回路をCNF形式に変換して出力する。
実験の結果、提案手法は、論理等価性検査問題において平均96.14%の解決時間削減を達成し、SAT競争ベンチマークにおいても平均52.42%の削減を実現した。これは、従来手法と比べて大幅な性能向上を示している。
提案手法の主な特徴は以下の通り:
- CNF形式からAIG回路への変換と、回路最適化、LUTマッピングを組み合わせた新しい前処理フレームワーク
- 強化学習ベースのロジック合成手法により、SAT解決時間の最小化を直接的に目的とした最適化
- コスト最適化LUTマッピング手法により、SAT解決がより容易な回路への変換
통계
SAT競争ベンチマークのインスタンスC1では、提案手法により解決時間が968.73秒から270.05秒に削減された。
SAT競争ベンチマークのインスタンスC2では、提案手法により解決時間がタイムアウトから764.84秒に削減された。
인용구
"本研究では、SAT問題を回路形式に変換し、強化学習ベースのロジック合成手法と新しいコスト最適化LUTマッピング手法を用いて、SAT問題の解決時間を大幅に削減する前処理フレームワークを提案する。"
"実験の結果、提案手法は、論理等価性検査問題において平均96.14%の解決時間削減を達成し、SAT競争ベンチマークにおいても平均52.42%の削減を実現した。"