Как перебирать оптимальные решения с помощью SAT4J DependencyHelper?

Question

Как перебирать оптимальные решения с помощью SAT4J DependencyHelper?

Я пытаюсь использовать SAT4J и его DependencyHelper для решения проблемы оптимизации. Поиск отдельных решений работает нормально, но теперь мне нужно найти все оптимальные решения (или, наоборот, перебрать все решения в порядке оптимальности), и я не могу понять, как это сделать. Все примеры перебора решений, которые я могу найти, относятся к простым задачам выполнимости, а не к оптимизации.

Глядя на то, как делает этоModelIterator , кажется, что лучше всего попросить решение, а затем использовать DependencyHelper.discard() (который внутренне использует ISolver.addBlockingClause()), чтобы добавить ограничение, исключающее это решение, снова запросите решение, чтобы получить следующее, исключите и это, и так далее, пока hasASolution()возвращает false. Но когда я пытаюсь это сделать, я обнаруживаю, что это дает мне только подмножество решений (иногда несколько, но не все). Что здесь происходит? Исключены ли из процесса оптимизации другие внутренние решения? Если да, то как мне добраться до них?

Я также нашел примечание «Это особенно полезно для перебора оптимальных решений» в документации API IOptimizationProblem.forceObjectiveValueTo() , которая звучит как именно то, что мне нужно, но я не могу найти никакой документации или примера того, как ее использовать, а слепые эксперименты оказались бесплодными.

Простой пример: задача с тремя переменными 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

Однако применение приведенного выше алгоритма дает мне только одно решение, не считая столь же оптимального (и всех остальных менее оптимальных):

      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,B,C, ∅,…

Я не очень знаком с теорией и терминологией решения выполнимости, я просто пытаюсь использовать библиотеку как черный ящик для решения моей проблемы, которая выполняет какое-то разрешение зависимостей в приложении Eclipse, подобное собственному Eclipse (p2) разрешение зависимостей плагина с использованием SAT4J. DependencyHelper выглядит здесь полезным, в частности, из-за поддержки объяснений.

0

sat4j

Источник

user2725327 13 сен '21 в 19:05

2 ответа

Другие вопросы по тегам sat4j

user2725327 16 сен '21 в 09:37 2021-09-16 09:37 · Answer 1 · 2021-09-16 09:37

Поскольку сочетание и PseudoOptDecoratorSAT4J 2.3.5 кажется неспособным поддерживать итерацию оптимальных решений, возвращая false из isSatisfiable()слишком рано (больше изменений, которые были введены вместе с OptimalModelIteratorкажется необходимым), вот обходной путь, который, кажется, работает с 2.3.5: сначала используйте, чтобы найти оптимальное значение целевой функции, затем ограничьте проблему решениями с этим значением и повторите их, не используя 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

user3867609 14 сен '21 в 18:28 2021-09-14 18:28 · Answer 2 · 2021-09-14 18:28

Использование 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

0

Источник

user3867609 14 сен '21 в 18:28