4
je trouve un solveur assis dansRésolution en utilisant DPLL sat solveur
http://code.google.com/p/aima-java/
I essayé le code suivant à résoudre une expression en utilisant dpllsolver
l'entrée est
(A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E))
transformateur CNF le transforme en
( ( (NOT A) OR B) AND ( (NOT B) OR A))
il ne considère pas les autres parties de la logique, il considère seulement le premier terme, comment le faire fonctionner correctement?
s'il vous plaît me suggérer si un autre assis solveur peut le faire
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);