SAT4J Implication use case

Question

I'm new to sat4j library. How I can define implication e.g. (A1 v A2 v A3) => (A1 ∧ A4) using sat4j and find boolean values for all variables?

I had found unit test for sat4j than I have tried something like in listing below. Problem is that hasASolution() returns true but solution variable is empty.

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

solution provides you a list of "satisfied" variables. Here, falsifying the variables satisfy your implication.

thus the empty solution set means that all the variables are falsified.