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 AND D AND E))");
transformedAnd = transformer.transform(sentence);
System.out.println(transformedAnd.toString());
boolean satisfiable = dpll.dpllSatisfiable(transformedAnd);
System.out.println(satisfiable);