问什么是SAT，它有什么好处？

EN

SAT是非常重要的，因为它是NP完全的。要理解这意味着什么，您需要对复杂性类有一个清晰的概念。下面是一个简短的概要：

• P是所有能在多项式时间(即快速)内解决的问题，
• NP是所有能在多项式时间内验证其解的问题。这意味着找到一个给定的解决方案是很快的，但找到一个解决方案通常是很慢的(通常是指数时间)。当然，除非问题出在NP的P部分(正如下面指出的，P是NP的一部分，这一点你可以很容易地验证)。

然后是NP-完全问题集。这个集合包含了所有如此通用的问题，你可以解决这些问题而不是NP中的另一个问题(这称为将一个问题归结到另一个问题上)。这意味着您可以将一个问题从一个领域转换为另一个NP完全问题，让它推导出答案，并将答案转换回来。

然而，通常可以证明一个问题是NP完全的，但是对于另一个给定的问题，转换是不清楚的。

SAT很好，因为它是NP完全的，也就是说，你可以用NP来解决它，而不是用NP来解决任何其他问题，而且归约也不是那么困难。TSP是另一个NP完全问题，但转换通常要困难得多。

所以，是的，SAT可以用来解决你提到的所有这些问题。然而，这通常是不可行的。可行的情况是，当不知道其他快速算法时，例如您提到的拼图。在这种情况下，您不必为拼图开发算法，但可以使用任何高度优化的SAT-Solver，最终将为您的拼图提供合理的快速算法。

例如，遍历树结构是如此简单，以至于从和到SAT的任何转换都很可能比直接编写遍历复杂得多。

长话短说，SAT求解器是您为其提供布尔公式的东西，它告诉您是否可以找到不同变量的值，从而使公式为真。

示例

假设a、b和c是布尔变量，您想知道是否可以为这些变量赋值，使公式成为(¬a ∨ b) ∧ (¬b ∨ c)。您将此公式发送到SAT求解器，它将返回true。SAT解算器通常也会为您提供有效的赋值。在这种情况下，此赋值可能为a: false, b:false, c:false。

它能用来做什么?

我不会使用它来遍历树，也不会用它来解析文本或换行。但是，您可以在遍历树时使用它来检查树上的某些约束是否得到满足。你当然可以使用它来打包，即使一些专门的CSP解算器可能会在这类问题上表现得更好。

SAT求解器现在变得越来越普遍，特别是在包管理器这样的软件中。Eclipse嵌入了SAT4j来管理其插件之间的依赖关系。SAT的其他应用通常包括模型检查、计划应用、配置器、调度和许多其他应用。