我找到了一个 SAT 求解器，地址是：

http://code.google.com/p/aima-java/

我尝试了以下代码，使用 dpllsolver 求解一个表达式：

输入是：

(A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E))

CNF 转换器将其转换为：

 (  (  ( NOT A )  OR B ) AND  (  ( NOT B )  OR A ) )

它没有考虑逻辑的其他部分，只考虑了第一个项。如何使其正确工作？

请推荐我其他的 SAT 求解器，如果可以的话。

PEParser parser = new PEParser();
CNFTransformer transformer=new CNFTransformer();
Sentence and;
Sentence transformedAnd;
DPLL dpll = new DPLL();

Sentence sentence = (Sentence) parser.parse("(A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E))");
transformedAnd = transformer.transform(sentence);

System.out.println(transformedAnd.toString());
boolean satisfiable = dpll.dpllSatisfiable(transformedAnd);

System.out.println(satisfiable);

回答：

试试这个：http://www.sat4j.org/

我相信这项技术已经被纳入 Eclipse Provisioning System P2 中，以解决插件依赖关系。http://blog.mancoosi.org/index.php/2008/06/01/4-edos-offspring-1-eclipse-p2-will-include-sat-solver-technology-for-managing-plugins