Есть ли инкрементальный решатель Max-SMT?

Question

• 1000 Я обнаружил, что лучше всего задаю ограничения для каждого временного шага, вместо того, чтобы Z3 назначал их все сразу, но это по-прежнему занимает очень много времени. Мне было интересно, можно ли использовать Max-SMT для решения этой проблемы, явно указав, что предыдущие назначения временных рядов должны оставаться такими же, насколько это возможно, и, кроме того, возвращая самую близкую возможную модель, если определенный временной порог достигнут и точное решение не найдено. Однако я не думаю, что Z3 обеспечивает комбинацию инкрементальности и Max-SMT. Вдобавок я не думаю, что возможно заставить Z3 предоставлять «максимально приближенную модель» в режиме решателя.

Кто-нибудь знает об инструменте, который предоставляет эти функции?

Спасибо !

Answer 1

Это правда, что оптимизатор z3 не является инкрементальным. Он также не поддерживает идею «достаточно близкой возможности». (Хотя вы можете запросить некоторые внутренние значения для подбора диапазонов, они не гарантируют, что они даже удовлетворят вашим ограничениям.) : http://optimathsat.disi.unitn.it/. Цитата с их веб-страницы:

OptiMathSAT допускает инкрементную многоцелевую оптимизацию по линейным арифметическим c целевым функциям, он поддерживает широкий спектр теорий (включая, например, равенство и неинтерпретированные функции, линейную арифметику c, бит-векторы, массивы).