Resolver usando DPLL se sentó solucionador

Question

He encontrado un solucionador se sentaron en

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

Me trató el código siguiente para resolver una expresión utilizando dpllsolver

la entrada es

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

CNF transformador transforma a

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

que no considera las otras partes de la lógica, que considera sólo el primer término, la forma de hacer que funcione correctamente?

por favor me sugieren si algún otro se sentó solucionador puede hacerlo

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

Trate de éste hacia fuera: http://www.sat4j.org/

Creo que esta tecnología ha sido incorporada en el sistema de aprovisionamiento de Eclipse P2 para resolver las dependencias plugin. http://blog.mancoosi.org/index.php/2008/06/01/4-edos-offspring-1-eclipse-p2-will-include-sat-solver-technology -para-gestión-plugins