DPLL SATソルバーを使用して解決します

Question

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

Answer 1

これを試してみてください： http://www.sat4j.org/

この技術は、プラグインの依存関係を解決するためにEclipse Provisioning System P2に組み込まれていると思います。 http://blog.mancoosi.org/index.php/2008/06/4-edos-offspring-1-eclipse-p2-include-sat-solver-technology-for-managing-plugins