使用 DPLL sat 求解器求解

Question

中找到了一个卫星求解器

我在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 ) )

不考虑逻辑的其他部分，它只考虑第一项，如何使其正常工作？

如果其他卫星解算器可以做到这一点，请建议我

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);

Answer 1

尝试一下这个：http://www.sat4j.org/

我相信这项技术已被纳入Eclipse Provisioning System P2 来解决插件依赖性。