Комбинация MAxSMT и определяемой пользователем функции стоимости в решателе Z3

@alias ответил на вопрос с технической точки зрения; Я интерпретировал вопрос с точки зрения удобства использования, поэтому добавил ответ с некоторыми подробностями.

Как указано в @alias, использование assert-soft помещает неявную целевую функцию во внутренний стек целей. Ключевой момент, на который следует обратить внимание, заключается в том, что это происходит в месте формулы первого оператора assert-soft каждой группы мягких предложений с общим идентификатором <id>.

Решатель z3 OMT поддерживает 3 многоцелевых комбинированных подхода: коробочный, лексикографический и оптимизация по Парето. Последние два являются достаточно известными многокритериальными подходами к оптимизации. Коробочная (также известная как Многонезависимая) оптимизация похожа на последовательное решение нескольких независимых задач с одной целью, имеющих одну и ту же формулу ввода и разные функции затрат; только то, что это делается намного быстрее за один проход оптимизации-поиска.

Комбинацию оптимизации можно задать прямо внутри формулы, в любой момент времени до вызова (check-sat):

(set-option :opt.priority VALUE)

где VALUE может быть box, lex или pareto.

Многоцелевая комбинация, используемая z3 по умолчанию, – это лексикографическая оптимизация.

В следующих примерах с использованием лексикографической оптимизации показано, как поведение z3 изменяется в зависимости от того, как чередуются команды assert-soft и minimize/maximize.

Пример I: Все операторы assert-soft появляются перед командой minimize. Неявная цель MaxSMT имеет приоритет над целью ЛИРА.

(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(assert-soft (< 2 x) :weight 1 :id pb)
(assert-soft (< 2 y) :weight 1 :id pb)
(minimize (+ x y))
(check-sat)
(get-model)
(get-objectives)

приводит к

~$ z3 example_01.smt2
sat
(model 
  (define-fun y () Int
    3)
  (define-fun x () Int
    3)
)
(objectives
 (pb 0)
 ((+ x y) 6)
)

Пример II: Все операторы assert-soft появляются после команды minimize. Цель ЛИРА имеет приоритет над неявной целью MaxSMT.

(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(minimize (+ x y))
(assert-soft (< 2 x) :weight 1 :id pb)
(assert-soft (< 2 y) :weight 1 :id pb)
(check-sat)
(get-model)
(get-objectives)

приводит к

~$ z3 example_02.smt2
sat
(model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    0)
)
(objectives
 ((+ x y) 0)
 (pb 2)
)

Пример III: Чередование операторов assert-soft с командой minimize. Неявная цель MaxSMT имеет приоритет над целью ЛИРА.

(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(assert-soft (< 2 x) :weight 1 :id pb)
(minimize (+ x y))
(assert-soft (< 2 y) :weight 1 :id pb)
(check-sat)
(get-model)
(get-objectives)

приводит к

~$ z3 example_03.smt2
sat
(model 
  (define-fun y () Int
    3)
  (define-fun x () Int
    3)
)
(objectives
 (pb 0)
 ((+ x y) 6)
)

Примечание. другие решатели OMT используют другие многоцелевые комбинации по умолчанию и по-разному обрабатывают операторы assert-soft, так что об этом следует помнить при использовании различных решателей.

Мягкое утверждение, по сути, рассматривается как ограничение, которое вводит штраф в функцию стоимости, если не выполняется:

(assert-soft F [:weight n | :dweight d ] [:id id ]) - установить мягкое ограничение F, опционально с целым весом n или десятичным весом d . Если вес не указан, вес по умолчанию равен 1 (1,0). Десятичные и целые веса можно свободно смешивать. Кроме того, мягкие ограничения могут быть помечены необязательным идентификатором имени. Это позволяет комбинировать несколько различных программных целей. Рис. 1 иллюстрирует использование с мягкими ограничениями.

Таким образом, в некотором смысле один и тот же движок MaxSMT обрабатывает как общую функцию стоимости, так и мягкие ограничения одним махом. Приведенная выше цитата и подробности приведены в этом документе: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf