DPLLアルゴリズム

3行要約

1. 命題論理式の充足可能性問題（SAT）を解くための、バックトラッキングに基づく完備な手法。
2. 単位伝播や純リテラル除去などの手法を組み合わせ、探索空間を効率的に削減するのが特徴である。
3. 現代の高性能なSATソルバーの多くが、このアルゴリズムを基礎として設計されている。