Оптимизация с ограничением по времени Z3

Question

Я видел, что Z3 поддерживает оптимизацию, например, через assert-soft. Из того, что я понял, если дано достаточно времени, Z3 сообщит оптимальное решение для данной формулы SMT.

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

Если я запускаю Z3 по формуле SMT и ограничиваю время (через параметр -T), он просто сообщит "timeout", если не решит его оптимальным образом. Я читал, что по умолчанию решатель wmax использует простую процедуру для ограничения весов, и мне любопытно, возможно ли связать весовые коэффициенты с верхней, а не нижней границы.

С уважением, Эмир

Answer 1

Параметр тайм-аута -T приводит к завершению процесса, поэтому он не возвращает никаких промежуточных значений. Если вы используете опцию -t (мягкое время ожидания), процесс не завершится. Вместо этого Z3 остановит поиск в некоторой точке, где он проверяет отмену. Затем он дает лучший ответ на данный момент. Это соответствует настройке состояния отмены. Я надеюсь, что это будет работать для вас.