Эффективность усиления ограничений в решателях SMT

Question

Один из способов решения проблем оптимизации состоит в том, чтобы использовать SMT-решатель, чтобы спросить, существует ли (плохое) решение, а затем постепенно добавлять более жесткие ограничения по стоимости, пока предложение больше не будет удовлетворяемым. Этот подход обсуждается, например, в http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf и http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf.

Хотя этот подход эффективен? т.е. будет ли решатель повторно использовать информацию из предыдущих решений при попытке решить проблему с дополнительными ограничениями?

Answer 1

Решатель может повторно использовать леммы, полученные при попытке решить предыдущие запросы. Просто имейте в виду, чем в Z3 всякий раз, когда вы выполняете pop все леммы (созданные с push) забыты. Итак, для достижения этого вы должны избегать push а также pop Команды и используйте "предположения", если вам нужно убрать утверждения. В следующем вопросе я опишу, как использовать "предположения" в Z3: мягкие / жесткие ограничения в Z3

Что касается эффективности, этот подход не самый эффективный для каждой проблемной области. С другой стороны, это может быть реализовано поверх большинства решателей SMT. Кроме того, псевдобулевы решатели (решатель для целых задач 0-1) успешно используют аналогичный подход для решения задач оптимизации.