ブール充足可能性問題（SAT）

定式化と基本概念

論理式は一般に連言標準形（CNF）で記述される。CNFは節の論理積（AND）であり、各節はリテラルの論理和（OR）からなる。リテラルは変数（x）またはその否定（¬x）である。CNFの例として、(x OR ¬y OR z) AND (¬x OR y) AND (z OR w OR ¬y) がある。充足割り当てとは、すべての節に少なくとも一つの真のリテラルが含まれるよう、各変数に真または偽を割り当てることである。

変種と特殊な場合

• k-SAT：各節が高々k個のリテラルを持つ問題。各節が三つのリテラルを持つ3-SATは、標準的なNP完全変種である。
• 2-SAT：各節が高々二つのリテラルを持つ問題。2-SATは多項式時間で解くことができ、線形時間アルゴリズムも存在する。
• Horn-SAT：各節が高々一つの正のリテラルを持つCNF論理式を対象とする。Horn-SATも線形時間で解くことができ、論理プログラミングにおいて重要である。
• Max-SAT：充足される節の数を最大にする割り当てを求める最適化版である。

複雑性と歴史

SATは、NP完全であることが最初に証明された問題である。クック＝レヴィンの定理（1971年頃）は、NPに属する任意の問題が多項式時間でSATへ変換できることを示した。これにより、SATは標準的なNP完全決定問題として位置づけられた。その直後、多くの自然な組合せ論的問題がNP完全であることが示され、3-SATは帰着や複雑性の証明で用いられる標準的な困難な問題となった。

アルゴリズムと実用的な求解

最悪の場合の計算量は指数的であるにもかかわらず、現代のSATソルバーは実用上生じる非常に大規模なインスタンスを扱える。古典的な完全手法は、単位伝播と純粋リテラル除去を強化したDPLL（Davis–Putnam–Logemann–Loveland）バックトラック枠組みに基づく。現代のソルバーでは、競合駆動節学習（CDCL）、高度な分岐ヒューリスティクス、再スタート、前処理が利用される。また、多くのベンチマークで良好に機能する不完全ヒューリスティクスや局所探索法もある。

応用と注目すべき事実

SATは、ハードウェアおよびソフトウェアの検証、計画、スケジューリング、組合せ設計、自動推論の問題を符号化するために広く使われる。多くの検証課題は、効率的なソルバーを活用するためSATへ変換される。研究分野には、ベンチマーク、SAT競技会、ならびに充足可能な領域と充足不能な領域の間で相転移を示すランダムSATインスタンスの研究が含まれる。SATソルバーの実用的な成功により、この問題は理論上の基礎であると同時に強力な工学的手段でもある。

区別と関連概念

SATは命題論理に属する。量化ブール式（QBF）への拡張では、複雑性は多項式階層のより高いクラスへ上がる。充足可能性は論理的含意と区別しなければならない。SATがある論理式を満たすモデルの存在を問うのに対し、含意は一つの論理式のすべてのモデルが別の論理式も満たすかを問う。これらの関係を理解することは、論理学、複雑性理論、自動定理証明において中心的である。