SAT4J Сценарий использования импликации

Question

Я новичок в библиотеке sat4j. Как я могу определить значение, например, (A1 v A2 v A3) => (A1 ∧ A4) используя sat4j и найти логические значения для всех переменных?

Я нашел модульный тест для Sat4j, чем я пытался что-то вроде в листинге ниже. Проблема в том, что hasASolution() возвращает истину, но 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

Решение предоставляет вам список "удовлетворенных" переменных. Здесь фальсификация переменных удовлетворит ваше мнение.

таким образом, пустой набор решений означает, что все переменные фальсифицированы.