How to iterate over optimal solutions with SAT4J DependencyHelper?

Question

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.

Answer 1

Using OptimalModelIterator should do the trick: https://gitlab.ow2.org/sat4j/sat4j/-/blob/master/org.sat4j.pb/src/main/java/org/sat4j/pb/tools/OptimalModelIterator.java

See an example to use it here: https://gitlab.ow2.org/sat4j/sat4j/-/blob/master/org.sat4j.pb/src/test/java/org/sat4j/pb/OptimalModelIteratorTest.java

Answer 2

Since the combination of OptToPBSATAdapter and PseudoOptDecorator of SAT4J 2.3.5 seems unable to support iteration over optimal solutions, returning false from isSatisfiable() too soon (more of the changes that were introduced together with OptimalModelIterator seem to be required), here is a workaround that seems to work with 2.3.5: First use OptToPBSATAdapter to find the optimal objective function value, then constrain the problem to solutions with that value and iterate over them without using OptToPBSATAdapter.

import java.math.BigInteger;
import org.sat4j.core.Vec;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.OptToPBSATAdapter;
import org.sat4j.pb.PseudoOptDecorator;
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 Optimize3 {

    public static void main(String[] args) {
        PseudoOptDecorator optimizer = new PseudoOptDecorator(SolverFactory.newDefault());
        DependencyHelper<String, String> helper = new DependencyHelper<>(new OptToPBSATAdapter(optimizer));
        helper.setNegator(StringNegator.INSTANCE);
        try {
            // 1. Find the optimal cost
            helper.implication("A").implies("B", "C").named("A => B || C");
            helper.addToObjectiveFunction("A", -3);
            helper.addToObjectiveFunction("B", 1);
            helper.addToObjectiveFunction("C", 1);
            System.out.println(helper.hasASolution()); // true
            BigInteger cost = helper.getSolutionCost();
            System.out.println(cost); // -2

            // 2. Iterate over solutions with optimal cost

            // In SAT4J 2.3.5, the optimization done by OptToPBSATAdapter in
            // helper.hasASolution() -> OptToPBSATAdapter.isSatisfiable() somehow
            // messed up the OptToPBSATAdapter, making it unable to find some more
            // solutions (isSatisfiable() now returns false). Therefore, start over.

            // helper.reset() doesn't seem to properly reset everything in XplainPB 
            // (it produces wrong solutions afterwards), so make a new helper.
            optimizer.reset();
            // Leave out the OptToPBSATAdapter (that would again be messed up after
            // the first call to isSatisfiable()) here and directly insert the
            // PseudoOptDecorator into the helper. This works because we don't need to
            // do any optimization anymore, just find all satisfying solutions.
            helper = new DependencyHelper<>(optimizer);
            helper.setNegator(StringNegator.INSTANCE);

            helper.implication("A").implies("B", "C").named("A => B || C");
            helper.addToObjectiveFunction("A", -3);
            helper.addToObjectiveFunction("B", 1);
            helper.addToObjectiveFunction("C", 1);
            // restrict to all the optimal solutions
            optimizer.forceObjectiveValueTo(cost);

            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()); // true
            System.out.println(helper.getSolution()); // A,B
            System.out.println(helper.getSolutionCost()); // -2
            helper.discard(new Vec<String>(new String[] { "A", "B", "-C" }));
            System.out.println(helper.hasASolution()); // false
        } 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 Optimize3.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:. Optimize3
true
-2
true
A,C
-2
true
A,B
-2
false