SATローカル検索のデータ構造をサポートします

Question

WalksatとGSAT ブールの満足度の問題を解決するためのよく知られたシンプルなローカル検索アルゴリズムです。 GSATアルゴリズムの擬似コードは質問からコピーされます GSATアルゴリズムの実装 - フリップするリテラルを選択する方法は？ 以下に示します。

procedure GSAT(A,Max_Tries,Max_Flips)
  A: is a CNF formula
  for i:=1 to Max_Tries do
    S <- instantiation of variables
    for j:=1 to Max_Iter do
      if A satisfiable by S then
        return S
      endif
      V <- the variable whose flip yield the most important raise in the number of satisfied clauses;
      S <- S with V flipped;
    endfor
  endfor
  return the best instantiation found
end GSAT

ここでは、満たされた条項の数を最大化する変数をひっくり返します。これはどのように効率的に行われますか？素朴な方法は、すべての変数をフリップし、各ステップですべての条項を通過し、それらの数が満足するものを計算することです。一定の時間で条項を満たすために節を照会できたとしても、素朴な方法は$ o（vc）$時間で実行されます。ここで、$ v $は変数の数、$ c $は条項の数です。私たちはより良いことができると確信しているので、質問は次のとおりです。

多くのローカル検索アルゴリズムは、満足した句の数を最大化する変数の割り当てをフリップします。実際には、この操作はどのようなデータ構造で効率的にサポートされていますか？

これは、教科書がしばしば省略するように感じるものです。一例は有名です ラッセル＆ノーヴィグの本.

Answer 1

必要なデータ構造は次のとおりです リストリスト, 、変数が発生する句を含む各変数のリスト。これらのリストは、CNFが最初に読み取られるときに一度構築されます。それらは、満足した条項をカウントするためにCNF式全体をスキャンすることを避けるために、以下の手順3および5で使用されています。

すべての変数をフリップするよりも優れたアルゴリズムは次のとおりです。

1. 不満の条項で発生する変数のみのリストを作成します。
2. このリストから変数$ x $を選択します。
3. $ x $を含む句の数を数えます。
4. フリップ$ x $。
5. $ x $を含む句の数を数えます。
6. $ x $を薄切っています。
7. ステップ5のステップ3の結果を減算し、$ x $で記録します。
8. ステップ1で見つかった残りの変数について、手順2-7を繰り返します。
9. ステップ7に記録された最高の数で変数を反転します。

たとえば、データ構造のリファレンス（隣接リストとも呼ばれます）は LynceとMarques-Silva、SATソルバーのバックトラッキングのための効率的なデータ構造、2004年。