3

今、私はSAT解法について書いていますが、ある時点で立ち往生しています。あなたが私を助けてくれることを願っています。

SAT-Problems を解決するいくつかの方法について説明したいと思います。現在、次の 3 つの方法があります。

  1. 強引な
  2. ランダム (ナイーブ)
  3. DPLL (ヒューリスティックが異なる)
  4. ? ない ？
  5. ...

私の問題は、唯一の効果的なアルゴリズムが DPLL (および DPLL とはわずかに異なる他のアルゴリズム) であることです。したがって、DPLL と比較するものは何もありません。

私の質問: 比較できる DPLL (DP) に基づいていないアルゴリズムをいくつか教えていただければ幸いです。

以下は私が見つけたもののいくつかです。

  • モニエン・スペッケンマイヤー
  • ダンツィン、ゲルト、ヒルシュ、シェーニング
  • Paturi-Pudlák-Zane-アルゴリズム
  • ホフマイスター、シェーニング、シューラー、渡辺

ご協力いただきありがとうございます。

4

2 に答える 2

4

最先端の sat ソルバーは現在、DPLL に基づく CDCL (Conflict Drive Clause Learning) を使用しています。

于 2015-06-23T14:30:33.400 に答える
1

あなたが提案したSAT解決アルゴリズムのうち、ブルートフォースとDPLLはどちらも完全なアルゴリズムであり、十分な時間があれば、満足のいく割り当てを見つけるか、問題を解決できないことを証明することが保証されています。ミリオンが言及しているように、DPLLの進歩であるCDCLも完成しています。

代替案について話し合う場合は、不完全なアルゴリズムを検討することをお勧めします。これらは多くの場合、確率的ローカル検索に基づいており、GSAT と WalkSAT が含まれます。これらのアルゴリズムは答えを見つけることが保証されていませんが、伝統的にランダムな (産業用に比べて) SAT 問題を解決するのに非常に優れています。また、DPLL ベースのアルゴリズムを実装するどのソルバーよりも大きな SAT 問題を解決するためにも使用されています。

さらなる調査のために、Biere のすばらしい本「Handbook of Satisfiability」をお勧めします。

于 2016-12-20T15:47:32.173 に答える