DPLLアルゴリズム

DPLL

5 回の無駄な試行(赤)の後、変数割り当てa =1、b =1 を選択すると、単位伝播(下)の後に成功(緑)に至ります。左上のCNF式は満たされます。
クラス	ブール充足可能性問題
データ構造	二分木
最悪の場合の パフォーマンス	${\displaystyle O(2^{n})}$
最高の パフォーマンス	${\displaystyle O(1)}$（絶え間ない）
最悪の場合の 空間複雑度	${\displaystyle O(n)}$（基本アルゴリズム）

論理学とコンピュータサイエンスにおいて、デイビス・パトナム・ローゲマン・ラブランド( DPLL )アルゴリズムは、連言標準形の命題論理式の充足可能性を決定する、すなわちCNF-SAT問題を解決するための完全なバックトラッキングベースの検索アルゴリズムです。

このアルゴリズムは 1961 年にマーティン・デイビス、ジョージ・ローゲマン、ドナルド・W・ラブランドによって導入され、 1960 年にデイビスとヒラリー・パトナムによって開発された解像度ベースの手順である以前のデイビス・パトナム アルゴリズムを改良したものです。特に古い出版物では、デイビス・ローゲマン・ラブランド アルゴリズムは「デイビス・パトナム法」または「DP アルゴリズム」と呼ばれることがよくあります。区別を維持する他の一般的な名前は、DLL と DPLL です。

SAT問題は理論的にも実際的観点からも重要です。複雑性理論ではNP 完全であることが証明された最初の問題であり、モデル検査、自動計画およびスケジュール、人工知能の診断など、さまざまなアプリケーションで使用できます。

そのため、効率的なSATソルバーを書くことは何年にもわたって研究テーマとなってきました。GRASP （1996-1999）はDPLLを使用した初期の実装でした。^{[1]国際SATコンテストでは、} zChaff ^[2]やMiniSat ^[3]などのDPLLをベースにした実装が2004年と2005年のコンテストで1位を獲得しました。^[4]

DPLL がよく使用されるもう 1 つのアプリケーションは、自動定理証明または理論を法とする充足可能性(SMT) です。これは、命題変数を別の数学理論の式に置き換えるSAT 問題です。

基本的なバックトラッキング アルゴリズムは、リテラルを選択し、それに真理値を割り当て、式を簡略化してから、簡略化された式が満たされるかどうかを再帰的にチェックすることによって実行されます。満たされる場合、元の式は満たされます。そうでない場合は、反対の真理値を前提として同じ再帰チェックが行われます。これは、問題を 2 つのより単純なサブ問題に分割するため、分割規則として知られています。簡略化の手順では、基本的に、割り当てによって真になるすべての節を式から削除し、偽になるすべてのリテラルを残りの節から削除します。

DPLL アルゴリズムは、各ステップで次のルールを積極的に使用することで、バックトラッキング アルゴリズムを強化します。

ユニット伝播

節がユニット節である場合、つまり、割り当てられていないリテラルが 1 つだけ含まれている場合、この節は、このリテラルを真にするために必要な値を割り当てることによってのみ満たされます。したがって、選択は必要ありません。ユニットの伝播は、ユニット節のリテラルを含むすべての節を削除し、ユニット節のリテラルの補数をその補数を含むすべての節から破棄することで構成されます。実際には、これによりユニットの決定論的なカスケードが発生することが多く、ナイーブな検索空間の大部分が回避されます。

文字通りの排除

命題変数が式の中で1 つの極性のみで出現する場合、それは純粋と呼ばれます。純粋なリテラルは、それを含むすべての節が真となるような方法で常に割り当てることができます。したがって、そのように割り当てられると、これらの節は検索を制約しなくなり、削除できます。

与えられた部分的な代入の不満足性は、1 つの節が空になった場合、つまり、その節のすべての変数が、対応するリテラルを偽にする方法で代入された場合に検出されます。式の満足性は、空の節が生成されることなくすべての変数が代入された場合、または最新の実装ではすべての節が満たされた場合に検出されます。完全な式の不満足性は、徹底的な検索を行った後でのみ検出できます。

DPLL アルゴリズムは次の疑似コードで要約できます。ここで、Φ はCNF式です。

アルゴリズムDPLL
    入力: 節 Φ の集合。
    出力: Φ が満たされるかどうかを示す真理値。

機能 DPLL（Φ）
    // 単位伝播:
    Φ に単位節 { l } がある場合、 
        Φ ← unit-propagate ( l , Φ )を実行します。
    // 純粋なリテラル除去:
    一方、 Φ 内に純粋に出現するリテラルl が存在する場合、do 
        Φ ← pure-literal-assign ( l , Φ ) を実行します。
    // 停止条件:
    Φ が空の場合はtrue
        を返します。Φ
    に空の節が含まれている場合はfalse
        を返します。
    // DPLL 手順:
    l ←リテラルを選択(Φ);
     DPLL (Φ ∧ {l})またはDPLL (Φ ∧ {¬l})を返します 。
 

この擬似コードでは、unit-propagate(l, Φ)と は、それぞれ単位伝播と純粋リテラル規則をリテラルと式pure-literal-assign(l, Φ)に適用した結果を返す関数です。つまり、式 で のすべての を「true」に、 のすべての を「false」に置き換えて、結果の式を簡略化します。ステートメントの は短絡演算子です。は、でを「true」に置き換えた簡略化された結果を表します。 lΦlnot lΦorreturnΦ ∧ {l}lΦ

アルゴリズムは、2 つのケースのいずれかで終了します。CNF 式Φが空、つまり節が含まれない場合です。その場合、すべての節が空虚に真であるため、任意の割り当てによって満たされます。それ以外の場合、式に空の節が含まれる場合、全体のセットが真であるためには、論理和で少なくとも 1 つのメンバーが真である必要があるため、その節は空虚に偽です。この場合、そのような節が存在するということは、式 (すべての節の論理積として評価) が真に評価できず、満たされないことを意味します。

疑似コード DPLL 関数は、最終的な割り当てが式を満たすかどうかのみを返します。実際の実装では、通常、成功した場合は部分的に満たされる割り当ても返されます。これは、分岐リテラルと、単位伝播および純粋なリテラル除去中に行われたリテラル割り当てを追跡することで導き出すことができます。

デイビス・ローゲマン・ラブランドアルゴリズムは、バックトラックステップで考慮されるリテラルである分岐リテラルの選択に依存します。結果として、これは厳密にはアルゴリズムではなく、分岐リテラルを選択する可能性のある方法ごとに1つずつ、アルゴリズムのファミリです。効率は分岐リテラルの選択に大きく影響されます。分岐リテラルの選択に応じて、実行時間が一定または指数関数になるインスタンスが存在します。このような選択関数は、ヒューリスティック関数または分岐ヒューリスティックとも呼ばれます。^[5]

Davis、Logemann、Loveland (1961) がこのアルゴリズムを開発しました。このオリジナルのアルゴリズムの特性は次のとおりです。

• 検索に基づいています。
• これは、ほぼすべての最新の SAT ソルバーの基礎となります。
• 学習や非時系列バックトラッキングは使用しません( 1996 年に導入)。

時系列バックトラッキングを持つ DPLL アルゴリズムの視覚化の例:

• 
  CNF式を構成するすべての節
• 
  変数を選択する
• 
  決定を下すと、変数a = False (0)となり、緑の節はTrueになる。
• 
  いくつかの決定を行った後、矛盾につながる含意グラフが見つかります。
• 
  次に、直近のレベルに戻り、強制的にその変数に反対の値を割り当てます。
• 
  しかし、強制的な決定は新たな紛争を引き起こす
• 
  前のレベルに戻って強制的に決定を下す
• 
  新たな決断を下すが、それが対立につながる
• 
  強引な決断をするが、またもや対立を招く
• 
  前のレベルに戻る
• 
  このように続けると最終的な含意グラフ

1986 年以来、（縮小順序付き）二分決定図も SAT の解決に使用されています。^{[引用が必要]}

1989年から1990年にかけて、ストールマルクの公式検証法が発表され、特許を取得しました。この方法は産業用途で使用されています。^[6]

DPLLは、 DPLL(T)アルゴリズムによって一階論理の断片の定理証明を自動化できるように拡張されている。^[1]

2010年から2019年の10年間で、アルゴリズムの改善作業により、分岐リテラルを選択するためのより良いポリシーと、アルゴリズムを高速化するための新しいデータ構造が見つかりました。特に単位伝播の部分です。しかし、主な改善点は、より強力なアルゴリズムであるConflict-Driven Clause Learning（CDCL）です。これはDPLLに似ていますが、競合に到達した後、競合の根本原因（変数への割り当て）を「学習」し、この情報を使用して非時系列バックトラッキング（別名バックジャンプ）を実行し、同じ競合に再び到達しないようにします。2019年現在、最先端のSATソルバーのほとんどはCDCLフレームワークに基づいています。^[7]

DPLLベースのアルゴリズムを不満足なインスタンスに対して実行すると、ツリー解決反証証明に相当する。^[8]

• 証明の複雑さ
• ハーブブランド化

ウィキメディア・コモンズには、デイビス・パトナム・ローゲマン・ラブランドアルゴリズムに関連するメディアがあります。

一般的な

• デイビス、マーティン;パトナム、ヒラリー( 1960 )。「数量化理論のための計算手順」。ACMジャーナル。7 (3): 201–215。doi : 10.1145/ 321033.321034。S2CID  31888376 。
• デイビス、マーティン; ロゲマン、ジョージ; ラブランド、ドナルド (1961)。「定理証明のための機械プログラム」。Communications of the ACM。5 ( 7): 394–397。doi : 10.1145/368273.368557。hdl : 2027/ mdp.39015095248095。S2CID  15866917 。
• Ouyang, Ming (1998). 「DPLL における分岐規則はどの程度優れているか?」離散応用数学. 89 (1–3): 281–286. doi :10.1016/S0166-218X(98)00045-6.
• ジョン・ハリソン (2009)。『実用論理と自動推論ハンドブック』ケンブリッジ大学出版局。pp. 79–90。ISBN 978-0-521-89957-4。

特定の

• Malay Ganai、Aarti Gupta、Aarti Gupta 博士 (2007)。SATベースのスケーラブルな形式検証ソリューション。Springer。pp. 23–32。ISBN 978-0-387-69166-4。
• Gomes, Carla P.; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008)。「Satisfiability Solvers」。Van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (編)。知識表現ハンドブック。人工知能の基礎。第 3 巻。Elsevier。pp. 89–134。doi :10.1016/S1574-6526(07) 03002-7。ISBN 978-0-444-52211-5。