I am trying to use SAT4J and its DependencyHelper to solve an optimization problem. Finding single solutions works fine, but now I need to find all optimal solutions (or, alternatively, iterate over all solutions in order of optimality), and I can’t figure out how to do that. All examples of iteration over solutions I can find are for simple satisfiability problems, not optimization.
Looking at how ModelIterator does it, it seems like the way to go is to ask for a solution, then use DependencyHelper.discard() (which internally uses ISolver.addBlockingClause()) to add a constraint that excludes that solution, ask for a solution again to get the next one, exclude that as well, and so on until hasASolution() returns false. But when I try that, I find that it only gives me a subset of solutions (sometimes multiple, but not all). What is going on here? Has the optimization process already excluded other solutions internally? If so, how do I get at those?
I have also found the note “This is especially useful to iterate over optimal solutions” in the API documentation of IOptimizationProblem.forceObjectiveValueTo(), which sounds like exactly what I need, but I can find no documentation or example of how to use it, and blind experimentation has proven fruitless.
Simple example: A problem with three variables A, B, C, one constraint A => B || C, and objective function weights -3, 1, 1. Of the 8 possible combinations of values, 7 are solutions, and 2 of them are optimal with cost -2:
A B C cost
----------
0 0 0 0
0 0 1 1
0 1 0 1
0 1 1 2
1 0 0 not a solution
1 0 1 -2
1 1 0 -2
1 1 1 -1
However, applying the algorithm above only gives me one solution, A,C, leaving out the equally optimal A,B (and all the other less optimal ones):
import org.sat4j.core.Vec;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.SolverFactory;
import org.sat4j.pb.tools.DependencyHelper;
import org.sat4j.pb.tools.StringNegator;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.TimeoutException;
public class Optimize {
public static void main(String[] args) {
IPBSolver solver = SolverFactory.newDefaultOptimizer();
DependencyHelper<String, String> helper = new DependencyHelper<>(solver);
helper.setNegator(StringNegator.INSTANCE);
try {
helper.implication("A").implies("B", "C").named("A => B || C");
} catch (ContradictionException e) {
e.printStackTrace();
}
helper.addToObjectiveFunction("A", -3);
helper.addToObjectiveFunction("B", 1);
helper.addToObjectiveFunction("C", 1);
try {
System.out.println(helper.hasASolution()); // true
System.out.println(helper.getSolution()); // A,C
System.out.println(helper.getSolutionCost()); // -2
helper.discard(new Vec<String>(new String[] { "A", "-B", "C" }));
System.out.println(helper.hasASolution()); // false !?! expecting true
System.out.println(helper.getSolution()); // expecting A,B
System.out.println(helper.getSolutionCost()); // expecting -2
helper.discard(new Vec<String>(new String[] { "A", "B", "-C" }));
System.out.println(helper.hasASolution()); // expecting either false (if it stops after optimal ones) or true (continuing with the next-best A,B,C)
} catch (TimeoutException e) {
e.printStackTrace();
} catch (ContradictionException e) {
e.printStackTrace();
}
}
}
$ javac -cp .p2/pool/plugins/org.sat4j.core_2.3.5.v201308161310.jar:.p2/pool/plugins/org.sat4j.pb_2.3.5.v201404071733.jar Optimize.java
$ java -cp .p2/pool/plugins/org.sat4j.core_2.3.5.v201308161310.jar:.p2/pool/plugins/org.sat4j.pb_2.3.5.v201404071733.jar:. Optimize
true
A,C
-2
false
A,C
-2
false
What am I doing wrong? Can anybody show me example code that does what I want in the example problem above? I.e. gives me
- either all the optimal solutions
A,C,A,B - or all solutions in order of optimality
A,C,A,B,A,B,C,∅, …
I am not very familiar with satisfiability solving theory and terminology, I’m just trying to use the library as a black box to solve my problem, which is doing some kind of dependency resolution in an Eclipse application, similar to Eclipse’s (p2’s) own plugin dependency resolution using SAT4J. DependencyHelper looks useful there in particular because of its explanation support.
