4

ウィキペディアで説明されているように、C++でDPLLアルゴリズムを実装しています。

function DPLL(Φ)
   if Φ is a consistent set of literals
       then return true;
   if Φ contains an empty clause
       then return false;
   for every unit clause l in Φ
      Φ ← unit-propagate(l, Φ);
   for every literal l that occurs pure in Φ
      Φ ← pure-literal-assign(l, Φ);
   l ← choose-literal(Φ);
   return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

しかし、ひどいパフォーマンスをしています。このステップでは：

return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

現在、私はのコピーを作成することを避けようとしてΦいますが、代わりに、lまたはnot(l)の唯一のコピーを追加して、/if 'sが戻っΦたときにそれらを削除します。これはアルゴリズムを壊して間違った結果を与えるようです（セットがであるとしても）。DPLL()falseUNSATISFIABLESATISFIABLE

このステップで明示的なコピーを回避する方法に関する提案はありますか？

4

1 に答える 1

1

DPLL へのあまり単純でないアプローチは、変数の割り当てと、ユニット伝播および純粋なリテラルの割り当てステップで句に加えられた変更を記録することによって式をコピーすることを回避し、空の句が生成されたときに変更を元に戻します (バックトラック)。そのため、変数xに true が割り当てられた場合、 xの正のリテラルを含むすべての節を非アクティブとしてマークし (その後、それらは満たされるため無視します)、それを含むすべての節から-xを削除します。後で後戻りできるように、どの句に-xが含まれているかを記録します。同じ理由で、どの条項を非アクティブとマークしたかも記録します。

もう 1 つの方法は、満たされていない節ごとに割り当てられていない変数の数を追跡することです。後で後戻りできるように、数値が減少したときに記録します。カウントが 1 に達した場合はユニットの伝播を行い、数値が 0 に達し、すべてのリテラルが false の場合はバックトラックします。

より良いアプローチがまだあるため、上記で「素朴ではない」と書きました。最新の DPLL タイプの SAT ソルバーは、「2 つの監視されたリテラル」と呼ばれる遅延句更新スキームを使用します。これには、句からリテラルを削除する必要がないため、不適切な代入が見つかったときにそれらを復元する必要がないという利点があります。変数の割り当ては記録してバックトラックする必要がありますが、節に関連する構造を更新する必要がないため、2 つの監視対象リテラルは、SAT ソルバーの他の既知のバックトラッキング スキームよりも高速になります。クラスの後半でこれについて学ぶことは間違いありません。

于 2012-10-25T06:30:39.810 に答える