最近我看到一篇关于使用 SAT 解决难题的 Reddit 文章 [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/
SAT非常重要，因为它是NP-Complete。要理解这意味着什么，您需要对复杂性类有一个清晰的概念。这是一个简短的概述：
P 是可以在多项式时间内（即快速）解决的所有问题的类别。
NP 是可以在多项式时间内验证解决方案的所有问题的类别。这意味着验证给定解决方案的速度很快，但找到一个解决方案通常很慢（通常是指数时间）。除非问题当然出在 NP 的 P 部分（正如下面指出的 P 是 NP 的一部分，您可以轻松验证）。
然后是一组 NP-Complete 问题。这组包含所有非常通用的问题，您可以解决这些问题而不是来自 NP 的另一个问题（这称为将问题归约到另一个问题上）。这意味着您可以将一个问题从一个域转换为另一个 NP-Complete 问题，让它得出一个答案并将答案转换回来。
然而，通常可以证明一个问题是 NP 完全的，但是对于另一个给定的问题，转换是不清楚的。
SAT 太好了，因为它是 NP-Complete，即你可以解决它而不是 NP 中的任何其他问题，而且减少也不难做到。TSP 是另一个 NP 完全问题，但转换通常要困难得多。
所以，是的，SAT 可以用来解决你提到的所有这些问题。然而，这通常是不可行的。可行的地方是，当没有其他快速算法已知时，例如您提到的难题。在这种情况下，您不必为拼图开发算法，但可以使用任何高度优化的 SAT-Solvers，您最终会为您的拼图找到一个合理的快速算法。
例如，遍历树结构非常简单，以至于任何从 SAT 到 SAT 的转换都可能比直接编写遍历要复杂得多。
长话短说，SAT求解器是一个你给它一个布尔公式的东西，它告诉你它是否可以找到不同变量的值，使得公式为真。
例子
假设a和是布尔变量，b并且c您想知道是否可以为这些变量分配一个值，从而以某种方式生成公式(¬a ∨ b) ∧ (¬b ∨ c)。您将此公式发送给 SAT 求解器，它会返回给您true。SAT 求解器也经常给你一个有效的作业。在这种情况下，这个分配可能是a: false, b:false, c:false.
它可以用来做什么？
我不会用它来遍历树，也不会解析文本或换行。但是，您可以在遍历树时使用它来检查树上的某些约束是否得到满足。您当然可以将它用于装箱，尽管一些专门的 CSP 求解器可能会在此类问题上表现更好。
如今，SAT 求解器变得越来越普遍，尤其是在包管理器等软件中。Eclipse 嵌入了 SAT4j 来管理其插件之间的依赖关系。SAT 的其他应用通常包括模型检查、规划应用、配置器、调度等。