Résolution de l'aide DPLL solveur

Question

J'ai trouvé un solveur dans

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

J'ai essayé le code suivant pour résoudre une expression à l'aide dpllsolver

l'entrée est

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

CNF transformateur transforme à

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

il ne considère pas les autres parties de la logique, il considère que le premier mandat, comment faire fonctionner correctement?

S'il vous plaît me suggérer si un autre solveur peut le faire

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

Essayez celui-ci sur: http://www.sat4j.org/

Je crois que cette technologie a été intégrée dans le système de provisionnement Eclipse P2 pour résoudre les dépendances du plugin. http://blog.mancoosi.org/index.php/2008/06/01/4-edos-offspring-1-eclipse-p2-will-include-sat-solver-technology -pour-gestion-plugins