Я заинтересован в том, чтобы Z3 предоставил мне модель, и в то же время я был бы счастлив, если бы он попытался принять во внимание целевую функцию как эвристику, но я не хочу платить штраф за производительность за нахождение фактического (max | мин) имум.
Возможно ли это в Z3?
Это уже возможно в Z3 с мягким тайм-аутом, см. этот ответ: Z3 Time Restricted Optimization
Способ добиться того, чего вы хотите, - использовать пошаговое решение:
check-sat и получите модельНа последнем шаге вы можете настроить, сколько вы хотите ждать, то есть штраф, который вы готовы заплатить.
Примечание по теме: вы также можете поиграть с мягкими ограничениями, которые решатель может «удовлетворить» по желанию, а в противном случае понести штрафные санкции. Возможно, это больше подходит для вашего варианта использования. Узнайте здесь, как это сделать: https://rise4fun.com/Z3/tutorialcontent/optimization#h23
