CODEWITHSUNDEEP
javaartificial-intelligencelogicfirst-order-logicsat-solvers
karthi
karthi

Reputation: 2911

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 AND D AND E))");
transformedAnd = transformer.transform(sentence);

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

System.out.println(satisfiable);

Upvotes: 4

Views: 4131

Answers (1)

James Branigan
James Branigan

Reputation: 1154

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

Upvotes: 5

Related Questions