java - 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

解决方案为您提供“满意”变量的列表。在这里，伪造变量满足您的含义。

因此，空解集意味着所有变量都是伪造的。