SATとは何ですか？

Question

最近、私はパズルを解くためにSATを使用したRedditの記事を見ました[1]。これは、この「座った」ことについて非常に好奇心をそそりました。ウィキペディアの記事を読みましたが、もっと素人の言葉で私のために説明するようにあなたの誰かに頼みたいと思います。

SATとは何ですか？木構造を横断するために使用できますか？テキストを解析するために？ラインブレイクのために[2]？ビンパッキング[3]？それは一種の最適化技術ですか？

関連することに、NP対Pは、いくつかの数値が合計でゼロになるかどうかを確認するvsのセット合計の数をゼロに選択することを選択していることを読みました - これに関連していますか？

[1] http://www.reddit.com/r/programming/comments/pxpzd/solving_hexiom_really_fast_with_a_sat_solver/

[2] http://en.wikipedia.org/wiki/line_wrap

[3] http://en.wikipedia.org/wiki/bin_packing_problem

Answer 1

SATはNPコンプリートであるため、非常に重要です。これが何を意味するのかを理解するには、複雑さのクラスの明確な概念が必要です。これが短い概要です：

• Pは、多項式時間（すなわち速い）で解決できるすべての問題のクラスです。

• NPは、多項式時間に解決策を検証できるすべての問題のクラスです。これは、特定のソリューションが高速であることを意味しますが、通常は見つけることは遅くなります（ほとんどの場合、指数時間）。もちろん、問題がNPのP部分にある場合を除きます（以下で指摘したように、PはNPの一部です。簡単に検証できます）。

次に、NP不完全な問題のセットがあります。このセットには、非常に一般的なすべての問題が含まれています。NPの別の問題の代わりにこれらの問題を解決できます（これは問題を別の問題に削減すると呼ばれます）。これは、問題をあるドメインから別のNP完全な問題に変換し、答えを導き出し、答えを変換できることを意味します。

しかし、多くの場合、問題がNP不完全であることが証明される可能性がありますが、変換は別の与えられた問題では不明です。

SATはNPが完全であるため、SATはとてもいいです。つまり、NPの他の問題の代わりに解決できることもあります。また、削減はそれほど難しくありません。 TSPは別のNP完全な問題ですが、変換はほとんどの場合ははるかに困難です。

したがって、はい、SATは、あなたが言及しているこれらすべての問題に使用できます。多くの場合、これは実行可能ではありません。実行可能な場合、言及したパズルなど、他の高速アルゴリズムがわからない場合です。この場合、パズルのアルゴリズムを開発する必要はありませんが、そこにある高度に最適化されたSATソルバーのいずれかを使用でき、パズルの合理的な高速アルゴリズムになります。

たとえば、ツリー構造の移動は非常に単純であるため、トラバーサルを直接書き込むよりも、とSATからの変換とSATへの変換はおそらくはるかに複雑です。

Answer 2

長いストーリーを短くするために、SATソルバーはブール式の式を与えるものであり、式が真であるように異なる変数の値を見つけることができるかどうかを示します。

例

仮定 a, b と c ブール変数であり、これらの変数に何らかの形で式を作成する値を割り当てることができるかどうかを知りたい (¬a ∨ b) ∧ (¬b ∨ c). 。この式をSATソルバーに送信すると、返品されます true. 。 SATソルバーは、多くの場合、有効な割り当てを提供します。この場合、この割り当てはそうかもしれません a: false, b:false, c:false.

何のために使用できますか？

私はそれを使用したり、テキストを解析したり、ラインを破ったりするためには使用しません。ただし、ツリーを横断するときに使用して、ツリーの制約が満足しているかどうかを確認できます。一部の専門のCSPソルバーは、おそらくこの種の問題でパフォーマンスを向上させる可能性がありますが、ビンパッキングには確かに使用できます。

最近、SATソルバーは、特にパッケージマネージャーのようなソフトウェアでは、はるかに一般的になりつつあります。 Eclipseは、sat4jを埋め込み、プラグイン間の依存関係を管理します。 SATの他のアプリケーションには、通常、モデルチェック、計画アプリケーション、コンフィギュレータ、スケジューリングなどが含まれます。