Инкрементное SAT-решение: сохранить экземпляр решения - изменить модель между прогонами

Question

Насколько я понимаю, инкрементальное SAT-решение помогает оценить различные модели, которые достаточно близки друг к другу.

Я хочу использовать это, чтобы оценить модель, и если я изменю ее позже, повторно оцените ее снова, используя предыдущее решение для более быстрого результата. Однако после изучения различных SAT Solvers (Sat4J, Minisat, mathsat5) кажется, что они способны решать только постепенно, когда все модели представлены в одном прогоне.

Я совершенно новичок в решении SAT, поэтому я могу что-то упустить. Нет ли способа сохранить экземпляр решения для последующего использования? Все обучение теряется при закрытии экземпляра?

Answer 1

В инкрементном режиме вы можете передать решателю новые ограничения.

В зависимости от настроек решатель может забыть или не забыть предыдущие изученные предложения и эвристику.

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

См., Например, это обсуждение в группе новостей minisat: https://groups.google.com/forum/.

Answer 2

SAT4J предоставляет механизм, который позволяет вводить решатель, а затем удалять части предложений и добавлять новые предложения для следующей проверки на удовлетворенность. Пункты, которые необходимо удалить, необходимо добавить в ConstGroup. К сожалению, это немного сложнее, поскольку предложения единиц требуют особой обработки. Это работает примерно так:

solver = initialize it with clauses which are not to be removed
boolean satisfiable;
ConstrGroup group = new ConstrGroup();
IVecInt unit = new VecInt();
try {
    for (all clauses to be added and removed) {
        if (unit clause) {
            unit.push(variable from clause);
        } else {
            group.add(solver.addClause(clause));
        }
        satisfiable = solver.isSatisfiable(unit);
    } catch (ContradictionException e) {
        satisfiable = false;
    } finally {
        group.removeFrom(solver);
    }

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

В то время как это решение работает в FeatureIDE (см. IsSatisfiable(узел Node) в https://github.com/FeatureIDE/FeatureIDE/blob/develop/plugins/de.ovgu.featureide.fm.core/src/org/prop4j/SatSolver.java), вполне вероятно, что есть более эффективные решения там.

Другое решение с допущениями не работает в нашем случае, так как мы имеем миллионы запросов к одному экземпляру решателя SAT с максимум 20000 переменных. Предположения позволят увеличить количество переменных с 20 тысяч до миллиона, что вряд ли поможет.