ウォークサット

コンピュータサイエンスにおいて、GSATとWalkSAT はブール充足可能性問題を解決するための局所探索 アルゴリズムです。

どちらのアルゴリズムも、ブール論理の式、つまり連言標準形 にあるか、連言標準形に変換された式で動作します。式の各変数にランダムな値を割り当てることから始めます。割り当てがすべての節を満たす場合、アルゴリズムは終了し、割り当てを返します。それ以外の場合は、変数が反転され、すべての節が満たされるまで上記が繰り返されます。WalkSAT と GSAT は、反転する変数を選択する方法が異なります。

• GSAT は、新しい課題で満たされていない節の数を最小限に抑える変更を行うか、またはある程度の確率で変数をランダムに選択します。
• WalkSAT は、まず現在の割り当てで満たされていない節を選択し、次にその節内の変数を反転します。節は満たされていない節の中からランダムに選択されます。変数は、以前に満たされていた節のうち満たされていない節が最も少なくなるように選択され、変数の 1 つがランダムに選択される可能性がいくらかあります。ランダムに選択する場合、WalkSAT では、節内の変数の数のうち少なくとも 1 つが現在の誤った割り当てを修正する可能性が保証されます。最適であると推測される変数を選択する場合、WalkSAT は、考慮する可能性が少ないため、GSAT よりも計算が少なくて済みます。

どちらのアルゴリズムも、解決方法が長い間見つからない場合、満たされていない節の数の 局所的最小値から抜け出す方法として、新しいランダム割り当てで再開することがあります。

GSAT と WalkSAT には多くのバージョンが存在します。WalkSAT は、自動化された計画問題からの変換によって生成された充足可能性問題を解決するのに特に有効であることが証明されています。計画問題をブール充足可能性問題に変換する計画アプローチはsatplanと呼ばれます。

MaxWalkSATは、各節に重みが関連付けられ、その割り当てによって満たされる節の合計重みを最大化する割り当て(式全体を満たす場合も満たさない場合もあります) を見つけることが目標である、重み付け満足度問題を解決するために設計された WalkSAT のバリエーションです。

• Henry Kautz と B. Selman (1996)。限界を押し広げる: 計画、命題論理、確率的探索。第 13 回人工知能全国会議 (AAAI'96) の議事録、1194 ～ 1201 ページ。
• Papadimitriou, Christos H. (1991)、「満足のいく真理値割り当ての選択について」、第 32 回コンピュータ サイエンスの基礎に関する年次シンポジウムの議事録、pp. 163–169、doi :10.1109/SFCS.1991.185365、ISBN 978-0-8186-2445-2、S2CID  206559488。
• Schöning, U. (1999)、「 k -SAT および制約充足問題のための確率的アルゴリズム」、第 40 回コンピュータ サイエンスの基礎に関する年次シンポジウムの議事録、pp. 410–414、CiteSeerX  10.1.1.132.6306、doi :10.1109/SFFCS.1999.814612、ISBN 978-0-7695-0409-4、S2CID  1230959。
• B. セルマンとヘンリー・カウツ (1993)。GSAT へのドメイン非依存拡張: 大規模な構造化満足度問題の解決。第 13 回国際人工知能合同会議 (IJCAI'93) の議事録、290 ～ 295 ページ。
• Bart Selman、Henry Kautz、Bram Cohen。「充足可能性テストのための局所探索戦略」最終版は、1993 年 10 月 11 ～ 13 日に開催された Cliques、Coloring、および Satisfiability: Second DIMACS 実装チャレンジに掲載されています。David S. JohnsonおよびMichael A. Trick編。DIMACS Series in Discrete Mathematics and Theoretical Computer Science、第 26 巻、AMS、1996 年。
• B. セルマン、H. レベスク、D. ミッチェル (1992)。「困難な充足可能性問題を解くための新しい方法」第 10 回全国人工知能会議 (AAAI'92) の議事録、440 ～ 446 ページ。

• WalkSATホームページ