什么是SAT求解器

Question

什么是SAT求解器

Answer 1

好像已经一年的问题了···SAT问题就是满足性问题。给你介绍三种SAT求解器：
1. SAT4j。 SAT4j是一个用Java实现的SAT求解器，其支持可满足问题、 部
分极大可满足问题和带权的极大可满足问题。SAT4j目前已经随Eclipse3 一起
发布，并且也在 Linux的发行版 Ubuntu4 的软件仓库中。 SAT4j可以作为一
个Java库来使用，作为一个黑盒可以嵌入到其他的Java程序中。 总体来说，
SAT4j是一个性能和稳定性都比较好的求解器，而且有比较好的团队支持。
2. MSUnCore。MSUNCORE ( Maximum Satisability with UNsatisable COREs)
是一个基于不可满足核的求解器，其中实现几个不同的Max-SAT算法，有能
力处理大型的实例。同时它看作是一种分枝限界算法。在2008年的 MaxSAT
竞赛中，msu1.2获得了工业 MaxSAT 组的第一名和工业部分MaxSAT 组的每
二名。
3. Clone 。 Clone是一个分枝限界的求解器，同时使用了一种称作 d-
DNNF 的易解语言。 一旦实例为 d-DNNF 形式，便可以有效的在多项式时
间内求解。 如果不是，Clone会通过分枝的办法设法把实例变成 d-DNNF 形
式。