Поиск субоптимального решения (пока что лучшего) с помощью инструмента командной строки Z3 и времени ожидания

Question

Я видел пост, в котором говорилось о том, как Python API Z3 можно использовать для получения неоптимального решения для проблемы минимизации

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

Использует -t:timeout один вариант предположить, чтобы дать мне неоптимальное решение?

Решателю Z3 потребовалось 150 секунд, чтобы найти оптимальное решение для моей проблемы MaxSMT

я использовал z3 -t:140000 smt2 <filename> установить время ожидания 140 секунд. Но решатель z3 возвращает неизвестное (вместо sat и ненулевое объективное значение). Я также попытался с тайм-аутом 145 секунд и увидел аналогичный результат. Когда я установил тайм-аут> 150, я получил оптимальное решение

Должен ли я добавить что-то еще, чтобы получить неоптимальные решения?

Answer 1

maxres Движок, представленный в νZ - максимальное удовлетворение с Z3 и максимальное удовлетворение с использованием Core-Guided MaxSAT Resolution, приближается к оптимальному решению из неудовлетворительной области через последовательность релаксаций. Следовательно maxres двигатель не должен быть в состоянии найти какую - либо неоптимальную модель: первая модель входной формулы, которую он находит, также является оптимальной моделью.

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

Из командной строки кажется, что можно сделать maxres вывести любое улучшение нижней / верхней границы, включив verbose опция:

~$ ./z3 -v:1 smtlib2_maxsmt.smt2 
(optimize:check-sat)
(optimize:sat)
(maxsmt)
(opt.maxsat mutex size: 2 weight: 1)
(opt.maxres [1:2])
(opt.maxres [1:1])
found optimum
is-sat: l_true
Satisfying soft constraints
1: |(not (<= y 0))!1| |-> true 
1: |(not (<= y 0))!2| |-> true 
1: |(not (<= 0 y))!3| |-> false 
sat
(objectives
 (goal 1)
)
(model 
  (define-fun y () Int
    1)
  (define-fun x () Int
    (- 1))
)

Если я правильно понимаю, в (opt.maxres [1:2]), 1 последняя нижняя граница и 2 это последняя верхняя граница для данной цели. Обратите внимание, что в связанном посте Николай Бьорнер утверждает, что maxres может обновить верхнюю границу вдоль maxres поиск, но я не могу сказать, как часто это происходит, поэтому это решение может быть не очень эффективным на практике.

В качестве альтернативы вы можете попытаться использовать какой-то другой механизм MaxSMT, который приближается к оптимальному решению из удовлетворительной области, например wmax хотя это может быть медленнее, чем maxres,

Двигатель MaxSAT используется z3 можно выбрать, используя следующую опцию:

(set-option:opt.maxsat_engine [wmax|maxres|pd-maxres])

Можно также установить его через командную строку следующим образом:

~$ ./z3 -v:1 opt.maxsat_engine=wmax smtlib2_maxsmt.smt2 
(optimize:check-sat)
(optimize:sat)
(maxsmt)
(opt.maxsat mutex size: 2 weight: 1)
(opt.wmax [1:2])
(opt.wmax [1:1])
is-sat: l_true
Satisfying soft constraints
1: |(not (<= y 0))!1| |-> true 
1: |(not (<= y 0))!2| |-> true 
1: |(not (<= 0 y))!3| |-> false 
sat
(objectives
 (goal 1)
)
(model 
  (define-fun y () Int
    1)
  (define-fun x () Int
    (- 1))
)

Обратите внимание, что есть также возможность включить wmax в пределах maxres двигатель, хотя я не уверен, что он должен делать, так как вывод не меняется:

(set-option:opt.maxres.wmax true)