У меня есть куча ограничений на переменные, и я ищу способ эффективной выборки в этом ограниченном пространстве. Я попробовал Z3, и, похоже, он может сказать мне, является ли пространство нетривиальным (т. Е. Выполнимы ли ограничения), но я не вижу способа получить примеры из пространства, если только я не минимизирую или максимизирую что-то .
Я что-то упустил или Z3 просто не для этого?
Z3 может предоставить вам модель, т. е. один пример назначения переменных, удовлетворяющих ограничениям (попробуйте команду (get-model) в SMT2 или Solver.Model в .NET API (и команды с аналогичными именами в других API)). Затем вы можете подтвердить отрицание модели, чтобы заставить решатель произвести другое назначение для следующего запроса. Такая схема используется многими приложениями, но она не обязательно «эффективна», но это действительно зависит от того, какую выборку вы пытаетесь достичь (например, модели Z3 не будут случайным образом распределяться по пространству поиска).
Существуют методы, которые вы можете использовать для выборки из пространства решений SAT. См. https://simons.berkeley.edu/sites/default/files/docs/4393/moshevardi.pdf
Возможно, некоторые из этих методов можно реализовать поверх Z3.
Существует также существующая реализация алгоритма UniGen для почти равномерной выборки пространства решений SAT на github, но он основан на другом решателе SAT, и не уверен, что он поддерживает решение SMT.
РЕДАКТИРОВАТЬ: кажется, что здесь есть сэмплер SMT на основе Z3: https://github.com/RafaelTupynamba/SMTSampler
