SAT 是什么？它有什么用？
最近我在 Reddit 上看到一篇关于使用 SAT 解决难题的文章 [1]。这让我对“SAT”这个东西非常好奇。我读了维基百科的文章，但我想请你们中的某个人用更通俗的术语为我解释一下。
SAT 是什么？它有什么用？可以用来遍历树结构吗？用于解析文本？用于断行[2]？用于垃圾箱包装 [3]？这是一种优化技术吗？
在相关说明中，我读到 NP 与 P 是关于选择一组数字中的哪些数字总和为零与检查某些数字总和是否为零 - SAT 是否与此相关？
[1] http://www.reddit.com/r/programming/comments /pxpzd/solving_hexiom_really_fast_with_a_sat_solver/
Recently I saw a Reddit article on using SAT for solving a puzzle [1]. This got me very curios about this "SAT" thing. I read the Wikipedia article but I would like to ask someone of you to explain it for me in more layman terms.
What is SAT and what is it good for? Can it be used to traverse a tree structure? For parsing texts? For line breaking [2]? For bin packing [3]? Is it a kind of optimization technique?
On related note, I read that NP vs P is about choosing which numbers of a set sum to zero vs checking whether some numbers sum to zero - is SAT somehow related to this?
[1] http://www.reddit.com/r/programming/comments/pxpzd/solving_hexiom_really_fast_with_a_sat_solver/
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
SAT 非常重要，因为它是 NP-Complete。要理解这意味着什么，您需要对复杂性类有一个清晰的概念。以下是一个简短的概述：
P 是可以在多项式时间（即快速）内解决的所有问题的类。
NP 是可以在多项式时间内验证解决方案的所有问题的类别。这意味着找到一个给定的解决方案很快，但找到一个解决方案通常很慢（通常是指数时间）。当然，除非问题是在 NP 的 P 部分（正如下面指出的，P 是 NP 的一部分，您可以轻松验证）。
然后是一组 NP 完全问题。该集合包含所有非常通用的问题，您可以解决这些问题，而不是 NP 中的另一个问题（这称为将一个问题简化为另一个问题）。这意味着您可以将一个问题从一个域转换为另一个 NP 完全问题，让它导出答案并将答案转换回来。
然而，通常可以证明一个问题是 NP 完全问题，但对于另一个给定问题来说，转换是不清楚的。
SAT 非常好，因为它是 NP 完全的，即你可以解决它而不是 NP 中的任何其他问题，而且减少也不那么难。 TSP 是另一个 NP 完全问题，但转换通常要困难得多。
所以，是的，SAT 可以用来解决你提到的所有这些问题。然而，这通常是不可行的。可行的地方是，当不知道其他快速算法时，例如您提到的难题。在这种情况下，您不必为谜题开发算法，但可以使用任何高度优化的 SAT 求解器，最终将为您的谜题找到一个合理的快速算法。
例如，遍历树结构非常简单，任何从 SAT 到 SAT 的转换很可能比直接编写遍历要复杂得多。
SAT is very important because it is NP-Complete. To understand what this means you need a clear notion of Complexity classes. Here is a short rundown:
P is the class of all problems which can be solved in polynomial time (i.e. fast).
NP is the class of all problem for which a solution can be verified in polynomial time. This means veryfing a given solution is fast, but finding one is usually slow (most often exponential time). Unless the problem is in the P part of NP of course (as pointed out below P is part of NP, as you can easily verify).
Then there is the set of NP-Complete problems. This set contains all problem which are so generic, you can solve these Problems instead of another one from NP (this is called reducing a problem onto another). This means you can transform a problem from one domain into another NP-Complete problem, have it derive an answer and transform the answer back.
Often however it can be proven that a problem is NP-Complete, but the transformations are unclear for another given problem.
SAT is so nice, because it is NP-Complete, i.e. you can solve it instead of any other problem in NP, and also the reductions are not so hard to do. TSP is another NP-Complete problem, but the transformations are most often much more difficult.
So, yes, SAT can be used for all these problems you are mentioning. Often however this is not feasible. Where it is feasible is, when no other fast algorithm is known, such as the puzzle you mention. In this case you do not have to develop an algorithm for the puzzle, but can use any of the highly optimized SAT-Solvers out there and you will end up with a reasonable fast algorithm for your puzzle.
Traversing a tree structure is so simple for example, that any transformation from and to SAT will most likely be much more complex than just writing the traversal directly.
长话短说，SAT 求解器就是您提供布尔公式的东西，它会告诉您它是否可以找到不同变量的值以使公式成立。
示例
假设
a、b和c是布尔变量，并且您想知道这些变量是否可以分配一个值，该值以某种方式使公式（Øa∨b）∧（Øb∨c）。您将此公式发送到 SAT 求解器，它会返回true。 SAT 求解器通常还会为您提供有效的作业。在这种情况下，该分配可能是a: false, b:false, c:false。它可以用来做什么？
我不会用它来遍历树、解析文本或换行。但是，您可以在遍历树时使用它来检查树上的某些约束是否得到满足。您当然可以将其用于装箱，尽管某些专门的 CSP 求解器可能在此类问题上表现更好。
如今，SAT 求解器变得越来越普遍，尤其是在包管理器等软件中。 Eclipse 嵌入 SAT4j 来管理其插件之间的依赖关系。 SAT 的其他应用通常包括模型检查、规划应用、配置器、调度等。
To make a long story short, a SAT solver is something you give a boolean formula to, and it tells you whether it can find a value for the different variables such that the formula is true.
Example
suppose that
a,bandcare boolean variables, and you want to know if these variables can be assigned a value that somehow makes the formula(¬a ∨ b) ∧ (¬b ∨ c). You send this formula to the SAT solver, and it will return youtrue. SAT solvers also often give you a valid assignment. In this case this assignment might bea: false, b:false, c:false.What can it be used for ?
I would not use it to traverse trees nor to parse text or to break lines. However, you could use it when traversing a tree to check if some constraints on the tree are satisified. You can certainly use it for bin packing, even though some specialized CSP solvers will probably perform better on this kind of problems.
SAT solvers are becoming much more common these days, especially in software like package managers. Eclipse embeds SAT4j to manage dependencies among its plugins. Other applications of SAT typically include model checking, planning applications, configurators, scheduling, and many others.