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

Question

我正在尝试使用 SAT4J 及其 DependencyHelper 来解决优化问题。寻找单个解决方案工作正常，但现在我需要找到 all 最佳解决方案（或者，或者，按最佳顺序遍历所有解决方案），但我不知道该怎么做那。我能找到的所有解决方案迭代示例都是针对简单的可满足性问题，而不是优化。

看看ModelIterator是怎么做到的，好像要走的路是求一个解决方案，然后用DependencyHelper.discard()（内部用ISolver.addBlockingClause()）加一个排除该解决方案的约束，再次请求解决方案以获得下一个解决方案，同时排除该解决方案，依此类推，直到 hasASolution() returns false。但是当我尝试这样做时，我发现它只给了我一个解决方案的子集（有时是多个，但不是全部）。这里发生了什么？优化过程是否已经在内部排除了其他解决方案？如果是这样，我如何获得这些？

我还在 IOptimizationProblem.forceObjectiveValueTo() 的 API 文档中找到了注释“这对迭代最优解特别有用”，这听起来正是我需要的，但我找不到如何使用它的文档或示例，盲目实验证明是徒劳的。

简单示例：具有三个变量 A、B、C、一个约束 A => B || C 和 objective 函数权重 -3 的问题， 1, 1. 8种可能的取值组合中，有7种是解，其中2种是最优的，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

但是，应用上面的算法只给了我一个解决方案，A,C，忽略了同样最优的 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

我做错了什么？任何人都可以向我展示在上面的示例问题中执行我想要的示例代码吗？ IE。给我

所有最优解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

由于 SAT4J 2.3.5 的 OptToPBSATAdapter 和 PseudoOptDecorator 的组合似乎无法支持对最优解的迭代，过早地从 isSatisfiable() 返回 false（更多更改与 OptimalModelIterator 一起引入似乎是必需的），这是一个似乎适用于 2.3.5 的解决方法：首先使用 OptToPBSATAdapter 找到最佳的 objective 函数值，然后约束解决具有该值的问题并在不使用 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

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

How to iterate over optimal solutions with SAT4J DependencyHelper?

sat4j