Solving using DPLL sat solver

I found a sat solver in

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

I tried the following code to solve an expression using dpllsolver

the input is

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

CNF transformer transforms it to

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

it doesn't consider the other parts of the logic, it considers only first term, how to make it work correctly?

please suggest me if some other sat solver can do it

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 A开发者_运维问答ND D AND E))");
transformedAnd = transformer.transform(sentence);

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

System.out.println(satisfiable);

---

Try this one out: http://www.sat4j.org/

I believe that this technology has been incorporated into the Eclipse Provisioning System P2 to solve plugin dependencies. http://blog.mancoosi.org/index.php/2008/06/01/4-edos-offspring-1-eclipse-p2-will-include-sat-solver-technology-for-managing-plugins