Die Lösung mit DPLL saß Solver
-
10-10-2019 - |
Frage
Ich fand ein Sat-Solver in
http://code.google.com/p/aima-java/
Ich habe versucht, den folgenden Code unter Verwendung eines Ausdrucks dpllsolver
zu lösendie Eingabe
(A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E))
CNF Transformator wandelt es zu
( ( ( NOT A ) OR B ) AND ( ( NOT B ) OR A ) )
es nicht die anderen Teile der Logik betrachten, es hält nur ersten Begriff, wie es richtig funktioniert?
Sie mir empfehlen, wenn ein anderer Solver saß kann es tun
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);
Lösung
Versuchen Sie dieses heraus: http://www.sat4j.org/
Ich glaube, dass diese Technologie in das Eclipse-Provisioning System P2 eingebaut wurde Plugin Abhängigkeiten zu lösen. http://blog.mancoosi.org/index.php/2008/06/01/4-edos-offspring-1-eclipse-p2-will-include-sat-solver-technology -für-Verwaltung-Plugins
Lizenziert unter: CC-BY-SA mit Zuschreibung
Nicht verbunden mit StackOverflow