java 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

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

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