sat4j - 如何使用 SAT4J DependencyHelper 迭代最优解决方案？

Question

标签： sat4j

Answer 1

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