pysmt: как равномерно и случайным образом извлечь модели?

Question

В настоящее время я работаю над проектом, в котором мне нужно попробовать решения заданной формулы. Для этого я использую библиотеку pysmt , опираясь на решатель z3. В настоящее время я делаю, учитывая формулу (какpysmt.fnode.FNode), я используюget_modelфункцию для извлечения решения, добавления отрицания в формулу и выполнения итерации.

Проблема этого подхода заключается в том, что в конце процесса значения переменных (которые ограничены конечным числом значений) не распределяются должным образом, и это важно для работы, которую я выполняю.

Есть ли способ получитьnвыборки такие, что значения всех переменных примерно равномерно распределены в пространстве значений?

Спасибо!

Вот код для выборки:

      solutions = []

for s in range(n_samples):
        solution = []
        model = get_model(formula)

       if model is None:
            print("Not enough solutions")
            break

        sample = []
        for o in self.objects:
            attributes = {
                attr: [
                    x
                    for x in self.values[attr]
                    if model[self.get_attribute(attr, o, x)].is_true()
                ][0]
                for attr in self.values
            }
            sample.append(attributes)

        solutions.append(sample)

        # Exclude the current model by adding a negation of its assertions
        # to the problem, so the next iteration finds a different solution.
        negation = Not(And(EqualsOrIff(x, y) for (x, y) in model))
        formula = And(formula, negation)

Answer 1

Если количество решений достаточно мало, вы можете перечислить все решения описанным способом, а затем выбрать из них случайную выборку.

Если вы можете сформулировать свою проблему напрямую как задачу SAT, вы можете использовать unigen, который также имеет привязки к Python. Полученные выборки, очевидно, почти однородны (точные математические гарантии см. в статье).

Answer 2

Равномерная выборка не поддерживается z3. См. /questions/9988580/obrazets-ravnomerno-iz-mnozhestva-udovletvoryayuschih-zadanij-v-z3/9988595#9988595 для некоторых комментариев 2012 года; и я считаю, что это все еще так.

Равномерная выборка (или выборка по некоторому распределению) является сложной проблемой для SMT. Хотя есть некоторые исследования в этом направлении. Например, см.: https://github.com/RafaelTupynamba/SMTSampler .

Еще один проект, на который стоит посмотреть: https://github.com/RafaelTupynamba/GuidedSampler .

Таким образом, на данный момент этого нельзя просто достичь с помощью z3 или любого другого решателя SMT. По крайней мере, не из коробки.