Solving using DPLL sat solver

Question

I found a sat solver in

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

I tried the following code to solve an expression using DPLL solver

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 the first term, how to make it work correctly?

please suggest to 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 AND D AND E))");

transformedAnd = transformer.transform(sentence);

System.out.println(transformedAnd.toString());

boolean satisfiable = dpll.dpllSatisfiable(transformedAnd);

System.out.println(satisfiable);

Answer 1

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking the satisfiability of Boolean formulas. Many state-of-the-art SAT solvers are based on the DPLL algorithm and need the input formula to be in conjunctive normal form (CNF).

Refer to the following link for more information regarding the same: https://ieeexplore.ieee.org/document/5227064

You can try this one out: http://www.sat4j.org/