DPLLアルゴリズムとは

DPLLアルゴリズムは、ブール論理式を連言標準形（CNF）に変換した後、効率的な探索、含意伝播、およびバックトラックの技術を用いて、その論理式の充足可能性（SAT）を決定するための、古典的な手続き型アルゴリズムのことです。

DPLLアルゴリズムの概要と背景

DPLL（Davis-Putnam-Logemann-Loveland）アルゴリズムは、1960年代初頭に開発された、充足可能性問題（SAT）を解くための基本的なアルゴリズムです。これは、その後のSATソルバーの発展における基礎的な枠組みを提供しました。

当初のDavis-Putnam（DP）アルゴリズムは、再帰的な手順の中で変数を消去するリゾリューション（Resolution、導出原理）を使用していましたが、計算量が大きくなる問題がありました。DPLLアルゴリズムは、リゾリューションをより効率的なバックトラック探索と含意伝播（Unit Propagation）に置き換えることで、大規模な問題にも適用可能な実用性を獲得しました。

主な目的は、与えられた論理式を真（True）にするような変数の真偽値割り当て（解）が存在するかどうかを体系的に判断することです。

DPLLアルゴリズムの基本的な手続き

DPLLアルゴリズムは、与えられたCNF形式の論理式 F を入力として受け取り、以下の主要な規則を繰り返し適用することで、論理式の充足可能性を決定します。

1. 単位節規則（Unit Propagation）

単位節とは、リテラルが一つだけ含まれる節のことです。例えば、(¬x1​∨x2​)∧(x3​) という論理式において、(x3​) が単位節です。

• 処理: 論理式 F に単位節 C=(l) が含まれている場合、C を充足させるために、リテラル l は必ず真でなければなりません。
• 含意伝播: この割り当て（l←True）が確定すると、この割り当てが他の節の充足にどのように影響するかを論理的に伝播させます。
  • l を含む節は、すでに真が確定したため、論理式から除去されます。
  • ¬l を含む節からは、¬l が偽と確定したため、そのリテラルが除去されます。

このプロセスを、論理式中に単位節が存在しなくなるまで繰り返します。

2. 純粋リテラル規則（Pure Literal Elimination）

純粋リテラルとは、論理式 F の中で、その否定形（¬l）が全く出現しないリテラルのことです。

• 処理: 純粋リテラル l は、論理式全体を充足させるために、必ず真と割り当てることができます。なぜなら、その否定形が存在しないため、 l を真にしても矛盾が発生するリスクがないためです。
• 効果: l が真と確定することで、 l を含むすべての節が充足され、論理式から除去されます。

3. 分割規則（Splitting Rule）

単位節規則と純粋リテラル規則を適用しても、論理式が充足されない、あるいは矛盾が発生しない場合、残っている未決定の変数 x を一つ選びます。

• 処理: x に暫定的に真（True）または偽（False）の値を割り当て、再帰的にDPLLアルゴリズムを適用します。
• バックトラック: x←True の割り当てで充足可能性が得られなかった場合（矛盾した場合）、バックトラック（後戻り）を行い、逆の割り当て x←False を試みます。逆の割り当ても失敗した場合、元の論理式は充足不可能（Unsatisfiable）であると結論づけられます。

DPLLアルゴリズムの結論

DPLLアルゴリズムの実行結果は、以下の3つのケースのいずれかになります。

1. 充足可能（Satisfiable）:
   • すべての節が充足され、論理式全体が真となる変数の割り当てが見つかった場合（Yes）。
2. 充足不可能（Unsatisfiable）:
   • 単位節規則の適用中や分割規則のバックトラック中に、空の節（リテラルが一つも含まれていない節）が生成された場合。空の節は常に偽であるため、論理式全体も偽となります（No）。
3. 未決定:
   • 通常、アルゴリズムが終了すれば上記のいずれかの結論が出ます。

現代のSATソルバーは、このDPLLの枠組みを基礎としつつ、CDCL（矛盾駆動節学習）やより洗練されたヒューリスティクスを取り入れることで、飛躍的な性能向上を果たしています。

関連用語

お問い合わせ

システム開発・アプリ開発に関するご相談がございましたら、APPSWINGBYまでお気軽にご連絡ください。