SAT4J蕴涵使用情况

我是新来sat4j库。我如何定义蕴含(A1 v A2 v A3) => (A1 ∧ A4)使用sat4j并找到所有变量的布尔值？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());

来源

2017-06-04 Vadym Perepeliak

我发现了另一个框架（[GIMB上的AIMA]（https://github.com/aimacode/aima-java）），可以在几行内完成逻辑操作。你可以找到一些JUnit测试[这里]（https://github.com/aimacode/aima-java/blob/AIMA3e/aima-core/src/test/java/aima/test/core/experiment/logic/propositional/算法/ WalkSATExperiment.java）作为AIMA框架的介绍。 –

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

从而空溶液组意味着所有的变量都篡改。

来源

2017-06-05 06:49:14

有没有办法强制一些变量为“真”？ –

@VadymPerepeliak只是一个变量的约束/子句。像'formula.and（var）' – CaptainTrunky

SAT4J蕴涵使用情况

回答

相关问题