0

私は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());
4

1 に答える 1

0

ソリューションは、「満足している」変数のリストを提供します。ここで、変数を偽ることはあなたの含意を満たします。

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

于 2017-06-05T06:49:14.823 に答える