什么是SAT以及它有什么用？

Question

最近我看到一篇关于使用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/

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

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

Answer 1

SAT非常重要,因为它是NP-Complete.要理解这意味着你需要一个明确的复杂性概念.这是一个简短的纲要:

• P是可以在多项式时间(即快速)中求解的所有问题的类.

• NP是可以在多项式时间内验证解的所有问题的类.这意味着给定解决方案非常快,但找到一个通常很慢(通常是指数时间).除非问题出现在NP的P部分当然(如下所述,P是NP的一部分,因为您可以轻松验证).

然后是NP-Complete问题集.这个集合包含所有如此通用的问题,你可以解决这些问题而不是NP中的另一个问题(这称为将问题减少到另一个问题).这意味着您可以将问题从一个域转换为另一个NP-Complete问题,让它得出答案并将答案转换回来.

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

SAT非常好,因为它是NP-Complete,即你可以解决它而不是NP中的任何其他问题,而且减少也不是那么难.TSP是另一个NP-Complete问题,但转换通常要困难得多.

所以,是的,SAT可以用于你提到的所有这些问题.但通常这是不可行的.在可行的情况下,当没有其他快速算法已知时,例如你提到的谜题.在这种情况下,您不必为拼图开发算法,但可以使用任何高度优化的SAT-Solvers,您最终会得到一个合理的快速算法.

例如,遍历树结构非常简单,任何从SAT到SAT的转换都很可能比直接编写遍历要复杂得多.

Answer 2

总而言之,SAT求解器是你给出布尔公式的东西,它告诉你它是否能找到不同变量的值,使得公式为真.

例

假设a,b并且c是布尔变量,并且您想知道是否可以为这些变量分配一个以某种方式使公式生成的值(¬a ? b) ? (¬b ? c).您将此公式发送给SAT求解器,它将返回给您true.SAT解算器通常也会为您提供有效的作业.在这种情况下,这个任务可能是a: false, b:false, c:false.

它可以用于什么？

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

如今,SAT求解器变得越来越普遍,特别是在软件包管理器等软件中.Eclipse嵌入了SAT4j来管理其插件之间的依赖关系.SAT的其他应用通常包括模型检查,计划应用程序,配置程序,调度以及许多其他应用程序.