Это альтернативный ответ, который использует команду assert-soft.
Альтернативное кодирование # 1
Я предоставляю кодировку для Сначала OptiMathSAT , а затем объясните, как изменить эти формулы для достижения того же результата в z3 . По сравнению с другим подходом эта кодировка более подходит, когда имеется много логических переменных, имеющих один и тот же уровень приоритета , поскольку она позволяет решателю OMT использовать либо выделенный механизм MaxSAT для каждого шага лексикографического поиска.или Cardinality Networks для улучшения стандартного поиска на основе OMT.
Я соединил два игрушечных примера, которые я показал в другом ответе, в одной пошаговой формуле следующим образом:
(set-option :produce-models true)
(set-option :opt.priority lex)
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(assert (= a true))
(assert (or
(and (= b true) (not (= c true)))
(and (= c true) (not (= b true)))
))
(assert-soft a :weight 1 :id highest_priority)
(assert-soft b :weight 1 :id medium_priority)
(assert-soft c :weight 1 :id lowest_priority)
(minimize highest_priority)
(minimize medium_priority)
(minimize lowest_priority)
; First Solution
(check-sat)
(get-objectives)
(get-model)
; Second Solution
(push 1)
(assert (not (and a b)))
(check-sat)
(get-objectives)
(get-model)
(pop 1)
(exit)
Этовывод:
~$ optimathsat test.smt2
sat
(objectives
(highest_priority 0)
(medium_priority 0)
(lowest_priority 1)
)
( (a true)
(b true)
(c false)
(highest_priority 0)
(medium_priority 0)
(lowest_priority 1) )
sat
(objectives
(highest_priority 0)
(medium_priority 1)
(lowest_priority 0)
)
( (a true)
(b false)
(c true)
(highest_priority 0)
(medium_priority 1)
(lowest_priority 0) )
Чтобы использовать эту кодировку с z3 , достаточно закомментировать следующие три строки:
;(minimize highest_priority)
;(minimize medium_priority)
;(minimize lowest_priority)
Причинапотому что это z3 неявно определяет цель команды assert-soft и неявно минимизирует ее.Его вывод:
~$ z3 test.smt2
sat
(objectives
(highest_priority 0)
(medium_priority 0)
(lowest_priority 1)
)
(model
(define-fun b () Bool
true)
(define-fun c () Bool
false)
(define-fun a () Bool
true)
)
sat
(objectives
(highest_priority 0)
(medium_priority 1)
(lowest_priority 0)
)
(model
(define-fun b () Bool
false)
(define-fun c () Bool
true)
(define-fun a () Bool
true)
)
Обратите внимание, что, поскольку z3 неявно объявляет цели минимизации для вас, команды assert-soft должны отображаться в том же порядке приоритета, который вы хотели быназначить их связанной целевой функции.
Как я уже упоминал в начале статьи, эта кодировка намного лучше, чем в другом ответе в случае, когда некоторые переменные имеют одинаковый уровень приоритета.Чтобы разместить две переменные a1 и a2 на одном уровне приоритета, вы можете использовать одинаковые id для их команды assert-soft.
Например:
(set-option :produce-models true)
(set-option :opt.priority lex)
(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const b1 Bool)
(declare-const b2 Bool)
(declare-const c Bool)
(assert (= a1 true))
(assert (or
(and (= b1 true) (not (= c true)))
(and (= c true) (not (= b1 true)))
))
(assert (or (not a1) (not a2) (not a3) ))
(assert (or (not b1) (not b2) ))
(assert-soft a1 :weight 1 :id highest_priority)
(assert-soft a2 :weight 1 :id highest_priority)
(assert-soft a3 :weight 1 :id highest_priority)
(assert-soft b1 :weight 1 :id medium_priority)
(assert-soft b2 :weight 1 :id medium_priority)
(assert-soft c :weight 1 :id lowest_priority)
(minimize highest_priority)
(minimize medium_priority)
(minimize lowest_priority)
; First Solution
(check-sat)
(get-objectives)
(get-model)
; Second Solution
(push 1)
(assert (not (and a1 b1)))
(check-sat)
(get-objectives)
(get-model)
(pop 1)
(exit)
с выводом
~$ optimathsat test.smt2
sat
(objectives
(highest_priority 1)
(medium_priority 1)
(lowest_priority 0)
)
( (a1 true)
(a2 true)
(a3 false)
(b1 false)
(b2 true)
(c true)
(highest_priority 1)
(medium_priority 1)
(lowest_priority 0) )
sat
(objectives
(highest_priority 1)
(medium_priority 1)
(lowest_priority 0)
)
( (a1 true)
(a2 true)
(a3 false)
(b1 false)
(b2 true)
(c true)
(highest_priority 1)
(medium_priority 1)
(lowest_priority 0) )
Альтернативное кодирование # 2
Интересный факт о assert-soft заключается в том, что его можно использовать для решения лексикографическая оптимизация проблем без какого-либо лексикографического механизма оптимизации: для достижения того же результата достаточно немного поиграть с весами.Это то, что традиционно делается в случае решения SAT / MaxSAT.Единственное предостережение - нужно аккуратно расставлять гири.Помимо этого, этот подход может быть даже более эффективным, чем приведенное выше кодирование, поскольку вся проблема оптимизации решается с помощью одного вызова внутреннего одноцелевого механизма.
(set-option :produce-models true)
(set-option :opt.priority lex)
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(assert (= a true))
(assert (or
(and (= b true) (not (= c true)))
(and (= c true) (not (= b true)))
))
(assert-soft a :weight 4 :id obj) ; highest priority
(assert-soft b :weight 2 :id obj)
(assert-soft c :weight 1 :id obj) ; lowest priority
(minimize obj)
; First Solution
(check-sat)
(get-objectives)
(get-model)
; Second Solution
(push 1)
(assert (not (and a b)))
(check-sat)
(get-objectives)
(get-model)
(pop 1)
(exit)
Это вывод:
~$ optimathsat test.smt2
sat
(objectives
(obj 1)
)
( (a true)
(b true)
(c false)
(obj 1) )
sat
(objectives
(obj 2)
)
( (a true)
(b false)
(c true)
(obj 2) )
Я упоминал об этом в комментарии к другому ответу, но другое потенциально интересное решение могло бы заключаться в том, чтобы попытаться использовать бит-векторную кодировку формулы, а затем использовать OBVBS * 1069.* (см. «Оптимизация по битовому вектору» Наделя и др. ) механизм оптимизации BV по вектору, в котором самый значимый бит представляет переменную с наивысшим приоритетом, а наименее значимый бит представляет наименьшийпеременная приоритета.
Если вы хотите попробовать, некоторое время назад мы представили в OptiMathSAT повторную реализацию механизма OBVBS, описанного в статье.Z3 также поддерживает оптимизацию Bit-Vector.