Résolution de l'aide DPLL solveur
-
10-10-2019 - |
Question
J'ai trouvé un solveur dans
http://code.google.com/p/aima-java/
J'ai essayé le code suivant pour résoudre une expression à l'aide 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))
CNF transformateur transforme à
( ( ( NOT A ) OR B ) AND ( ( NOT B ) OR A ) )
il ne considère pas les autres parties de la logique, il considère que le premier mandat, comment faire fonctionner correctement?
S'il vous plaît me suggérer si un autre 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);
La solution
Essayez celui-ci sur: http://www.sat4j.org/
Je crois que cette technologie a été intégrée dans le système de provisionnement Eclipse P2 pour résoudre les dépendances du plugin. http://blog.mancoosi.org/index.php/2008/06/01/4-edos-offspring-1-eclipse-p2-will-include-sat-solver-technology -pour-gestion-plugins
Licencié sous: CC-BY-SA avec attribution
Non affilié à StackOverflow