SAT4J隐含用例

Question

我是sat4j库的新手。如何使用sat4j定义隐含(例如(A1 v A2 v A3) => (A1 ∧ A4) )并找到所有变量的布尔值？

我已经找到了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

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

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