最近、パズルを解くための SAT の使用に関する Reddit の記事を見ました [1]。これは、この「SAT」のことについて非常に興味をそそられました。私はウィキペディアの記事を読みましたが、誰かにもっと素人の言葉で説明してもらいたいと思います.
SAT とは何ですか？ツリー構造をトラバースするために使用できますか? テキストを解析するには？改行用 [2]? ビン梱包の場合[3]? 一種の最適化手法ですか？
関連するメモとして、NP と P は、セットのどの数値の合計がゼロになるかを選択することと、いくつかの数値の合計がゼロになるかどうかを確認することについて書かれていることを読みました。
[1] http://www.reddit.com/r/programming/comments/pxpzd/solving_hexiom_really_fast_with_a_sat_solver/
SAT は NP-Complete であるため、非常に重要です。これが何を意味するのかを理解するには、Complexity クラスの明確な概念が必要です。ここに短い要約があります：
P は、多項式時間 (つまり高速) で解けるすべての問題のクラスです。
NP は、解が多項式時間で検証できるすべての問題のクラスです。これは、与えられた解を検証するのは高速ですが、通常、解を見つけるのは遅い (ほとんどの場合、指数関数的な時間) ことを意味します。もちろん、問題が NP の P 部分にある場合を除きます (以下で指摘されているように、簡単に確認できるように、P は NP の一部です)。
次に、NP完全問題のセットがあります。このセットには非常に一般的なすべての問題が含まれているため、NP から別の問題を解決する代わりに、これらの問題を解決できます (これは、問題を別の問題に還元することと呼ばれます)。これは、問題をあるドメインから別の NP-Complete 問題に変換し、その問題に答えを導出させ、その答えを元に戻すことができることを意味します。
しかし、多くの場合、問題が NP 完全であることは証明できますが、別の問題については変換が不明確です。
SAT は NP-Complete であるため、非常に優れています。つまり、NP の他の問題の代わりにそれを解くことができ、還元もそれほど難しくありません。TSP は別の NP 完全問題ですが、ほとんどの場合、変換ははるかに困難です。
そうです、SAT はあなたが言及しているこれらすべての問題に使用できます。ただし、多くの場合、これは実現不可能です。あなたが言及したパズルなど、他の高速なアルゴリズムが知られていない場合は、それが実行可能です。この場合、パズルのアルゴリズムを開発する必要はありませんが、高度に最適化された SAT-Solver のいずれかを使用することができ、パズルの合理的な高速アルゴリズムが得られます。
たとえば、ツリー構造のトラバースは非常に単純であるため、SAT との間の変換は、トラバーサルを直接記述するよりもはるかに複雑になる可能性があります。