Решение с использованием решателя SAT DPLL

Question

Я нашел решатель SAT в

http://code.google.com/p/aima-java/

Я попробовал следующий код, чтобы решить выражение с помощью dpllsolver

Вход есть

(A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E))

Трансформатор CNF преобразует его в

 (  (  ( NOT A )  OR B ) AND  (  ( NOT B )  OR A ) )

Он не учитывает другие части логики, он рассматривает только первый термин, как заставить ее работать правильно?

Пожалуйста, предложите мне, если какой -то другой решатель SAT может сделать это

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);

Answer 1

Попробуйте это: http://www.sat4j.org/

Я полагаю, что эта технология была включена в систему обеспечения Eclipse Provisioning P2 для решения зависимостей плагина. http://blog.mancoosi.org/index.php/2008/06/01/4-edos-ftspring-1-eclipse-p2-will-include-sat-solver-technology-for-madaging-plugins