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