SAT4J含意使用例

Question

私はsat4jライブラリを初めて使用しています。たとえば、私は含意を定義することができます。 (A1 v A2 v A3) => (A1 ∧ A4) sat4jを使用して、すべての変数のブール値を見つけますか？

私はsat4jの単体テストを見つけましたが、私は以下のようなものを試しました。問題は、hasASolution()がtrueを返しますが、solution変数が空であることです。

DependencyHelper<String, String> dependencyHelper = new DependencyHelper<>(SolverFactory.newEclipseP2()); 
dependencyHelper.implication("A1", "A2", "A3").implies("A1").and("A4"); 
// Before get a solution it must be checked 
assertTrue(dependencyHelper.hasASolution()); 
IVec<String> solution = dependencyHelper.getSolution(); 
System.out.println(solution.toString()); 

Answer 1

解決策には「満足」変数のリストがあります。ここで、変数を改ざんすることは、あなたの含意を満足させます。

したがって、空の解集合は、すべての変数が改ざんされていることを意味します。