SATとは何ですか？

Question

最近、パズルを解くのにSATを使用するRedditの記事がありました[1]。これは私にこの「SAT」のことを非常に興味深いものにしました。私はWikipediaの記事を読んでいますが、あなたの誰かに私にとってそれをより一般的な言葉で説明するように頼んでみたいと思います。

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

関連するノートでは、NP対Pは、ゼロにセットされた合計の数を選択することと、いくつかの数がゼロになるかどうかをチェックすることです。

[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

それはNP完全であるため、SATは非常に重要です。これが意味するものを理解するには、複雑なクラスの明確な概念が必要です。

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

• NPは、解が多項式時間で検証できるすべての問題のクラスです。これは、与えられた解が高速であることを確かめることを意味するが、1つを見つけるのは通常遅い（指数関数的な時間が多い）。問題がNPのP部分にある場合を除き（PはNPの一部であり、簡単に確認できます）

NP-Completeの問題があります。このセットには非常に一般的な問題がすべて含まれていますので、NPから別の問題を解決することができます（これを問題を別の問題に還元するという）。これは、問題をあるドメインから別のNP完全な問題に変換し、それが回答を導出し、回答を元に戻すことを意味します。

多くの場合、問題はNP-Completeであることが証明できますが、変換は別の問題では不明です。

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

はい、SATはあなたが言及しているこれらの問題すべてに使用できます。しかしながらこれはしばしば実行可能ではない。他の高速アルゴリズムが知られていないとき、例えばあなたが言及したパズルのように、実現可能なところです。この場合、パズルのアルゴリズムを開発する必要はありませんが、高度に最適化されたSAT-Solversを使用すると、パズルの合理的な高速アルゴリズムになります。

ツリー構造をトラバースするのは非常に簡単なことです。たとえば、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の他のアプリケーションには、通常、モデル検査、アプリケーション計画、コンフィギュレータ、スケジューリングなどがあります。