Как случайным образом (недетерминированно) находить решения в SAT4J?

Question

В примерах кода из документации SAT4J многократный вызов решателя для одной и той же задачи SAT всегда дает одно и то же решение, даже если существует несколько возможных решений, то есть результат является детерминированным.

Я ищу способ получить разные решения при нескольких запусках, то есть недетерминированный / случайный результат. Для каждого возможного решения должна быть ненулевая вероятность того, что решение будет выбрано. В идеале каждое решение следует выбирать с одинаковой вероятностью, но это не строгое требование.

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

Answer 1

Да, Sat4j по умолчанию детерминирован: он всегда найдет одно и то же решение, если вы запустите его несколько раз для одной и той же проблемы из командной строки.

Способ добавить некоторый недетерминизм в эвристику - использовать RandomWalkDecorator, как, например, можно найти в GreedySolver в org.sat4j.minisat.SolverFactory.

Однако обратите внимание, что если вы несколько раз используете такой решатель из командной строки:

java -jar org.sat4j.core.jar GreedySolver file.cnf

вы по-прежнему будете детерминированным, поскольку генератор псевдослучайных чисел засевается константой.

Таким образом, вам нужно задать несколько моделей в вашем Java-коде.

Как упоминалось в вашем вопросе, вы можете использовать декоратор ModelIterator с привязкой к этому:

ISolver solver = SolverFactory.newGreedySolver();
ModelIterator mi = new ModelIterator(solver,10); // look for 10 models