Инкрементальное обучение с использованием MAXSMT

Question

Можем ли мы использовать предыдущее решение решателя MaxSMT (оптимизировать) поэтапно в z3? Кроме того, есть ли способ распечатать мягкие утверждения в оптимизаторе?

Answer 1

Ответ ДА, если вы спрашиваете, технически возможно ли запустить либоz3 или OptiMathSAT постепенно с проблемой MaxSMT. (Используйте API).

Все мягкие предложения с одинаковыми id - в момент выполнения check-sat- считаются частью той же цели MaxSMT. По сути, решатель OMT лениво вычисляет соответствующий набор мягких предложений цели MaxSMT. Это справедливо как дляz3 а также OptiMathSAT.

Оптимальное решение, найденное на ранней стадии, может быть далеко от оптимального решения более поздних стадий итерационного процесса.

При работе с проблемой MaxSMT способность решателя OMT повторно использовать изученные предложения в инкрементальных вызовах может зависеть от используемого алгоритма оптимизации.

Я вижу два возможных случая:

• Один из них использует движок MaxSMT на основе ядра. В этом случае, исследуя формулировку проблемы с увеличением уровня сложности может помочь идентификациям послушного подмножества исходной задачи. Однако обратите внимание, что леммы, включающие мягкие ограничения, изученные на предыдущих итерациях, могут оказаться бесполезными на более поздних этапах (на самом деле, решатель OMT собирается отбросить все эти предложения и при необходимости пересчитать их).

• Один из них использует движок MaxSMT на базе спутниковой системы. В этом случае мне не ясно, в чем польза разделения проблемы на более мелкие части, кроме сосредоточения поиска на определенных группах ("возможно связанных?") Мягких предложений. Решателю OMT можно задать все мягкие ограничения сразу вместе с жестким таймаутом, и он все равно сможет дать частичное оптимальное решение при срабатывании сигнала тревоги. (T-леммы, включающие функцию стоимости, не будут полезны для дополнительных вызовов, потому что функция стоимости изменяется. В лучшем сценарии решатели OMT отбрасывают их. В худшем сценарии эти T-леммы остаются в среде и загромождают поиск без изменения решения).

  Я признаю, что довольно сложно предсказать производительность решателя OMT из-за накладных расходов, связанных с любым подходом. С одной стороны, у нас есть накладные расходы на дополнительные вызовы и тот факт, что процесс оптимизации перезапускается с нуля несколько раз. С другой стороны, у нас есть накладные расходы на выполнение BCP по гораздо большему набору мягких предложений. Я предполагаю, что баланс складывается в пользу инкрементного подхода для достаточно больших наборов мягких предложений. [Это было бы интересным предметом исследования, я бы с удовольствием прочитал об этом статью!]