如何用SAT4J DependencyHelper迭代最优解？

Question

我试图使用SAT4J和它的DependencyHelper来解决优化问题。找到单一的解决方案很好，但是现在我需要找到所有的最优解(或者，或者，按照最优性顺序迭代所有的解决方案)，而我不知道如何做到这一点。我所能找到的所有迭代的例子都是简单的可满足性问题，而不是优化问题。

看看ModelIterator是如何做到的，似乎要做的就是请求一个解决方案，然后使用DependencyHelper.discard() (内部使用ISolver.addBlockingClause())添加一个约束，该约束不包括该解决方案，再次请求一个解决方案以获得下一个解决方案，并排除该解决方案，等等，直到hasASolution()返回false为止。但是当我尝试的时候，我发现它只给了我一个解决方案的子集(有时是多重的，但不是全部的)。这里发生什么事情？优化过程是否已经在内部排除了其他解决方案？如果是的话，我怎么能得到这些呢？

我还发现了IOptimizationProblem.forceObjectiveValueTo()的API文档中的注释“这对于迭代优化解决方案特别有用”，这听起来就像我所需要的，但是我找不到文档或者如何使用它的例子，盲目的实验已经证明是徒劳的。

简单的例子:三个变量A、B、C、一个约束A => B || C和目标函数权重-3、1、1的问题。在8种可能的值组合中，有7种是解，其中2种是最优的，成本-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

然而，应用上述算法只给出了一个解决方案，A,C，忽略了同样最优的A,B (以及其他所有较不优化的A,B)：

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

我做错了什么？有人能给我看一下在上面的示例问题中做我想要的示例代码吗？也就是给我

• 无论是所有最优解A,C，A,B
• 或按最优性A,C、A,B、A,B,C、∅、…顺序排列的所有解

我不太熟悉可满足性解决理论和术语，我只是尝试使用这个库作为一个黑匣子来解决我的问题，这就是在Eclipse应用程序中执行某种依赖解析，类似于Eclipse(P2)使用SAT4J自己的插件依赖解析。DependencyHelper在那里看起来很有用，特别是因为它支持解释。

Answer 1

使用OptimalModelIterator应该能做到这一点：https://gitlab.ow2.org/sat4j/sat4j/-/blob/master/org.sat4j.pb/src/main/java/org/sat4j/pb/tools/OptimalModelIterator.java

请参见此处使用它的示例：https://gitlab.ow2.org/sat4j/sat4j/-/blob/master/org.sat4j.pb/src/test/java/org/sat4j/pb/OptimalModelIteratorTest.java

Answer 2

由于OptToPBSATAdapter和PseudoOptDecorator of SAT4J 2.3.5的组合似乎无法支持最优解的迭代，因此返回isSatisfiable()的false太快(似乎需要更多的与OptimalModelIterator一起引入的更改)，因此这里有一个解决方法似乎适用于2.3.5:首先使用OptToPBSATAdapter找到最优目标函数值，然后将问题约束为具有该值的解，然后在不使用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