好像已经一年的问题了···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 形

式。