Как улучшить оптимизацию на основе бинарного поиска в Z3py

Я пытаюсь оптимизировать с помощью Z3py экземпляр Set Covering Problem (SCP41) на основе минимизации.

Результаты следующие:

С использованием

(1) Я знаю, что Z3 поддерживает оптимизацию (https://rise4fun.com/Z3/tutorial/optimization). Много раз я добирался до оптимума в SCP41 и других случаях, но не у всех.

(2) Я понимаю, что если я буду использовать Z3py API без модуля оптимизации, мне придется выполнять типичный последовательный поиск, описанный в (Минимальное и максимальное значения целочисленной переменной) от @Leonardo de Moura. Это никогда не дает мне результатов.

Мой подход

(3) Я попытался улучшить подход к последовательному поиску, внедрив бинарный поиск, аналогичный тому, как он объясняет @Philippe в (Поддерживает ли Z3 проблемы с оптимизацией), когда я запускаю свой алгоритм, он ждет, и я не получаю никакого результата.

Я так понимаю, что бинарный поиск должен быть быстрее и работать в этом случае? Я также знаю, что экземпляр SCP41 — это что-то большое, и что генерируется много ограничений, и он становится чрезвычайно комбинаторным, это мой полный код (Код большого экземпляра), и это мой двоичный поиск:

def min(F, Z, M, LB, UB, C):    
    i = 0
    s = Solver()

    s.add(F[0])
    s.add(F[1])
    s.add(F[2])
    s.add(F[3])
    s.add(F[4])
    s.add(F[5])

    r = s.check()

    if r == sat:
        UB = s.model()[Z]

        while int(str(LB)) <= int(str(UB)):

            C = int(( int(str(LB)) + int(str(UB)) / 2))

            s.push()
            s.add( Z > LB, Z <= C)

            r = s.check()

            if r==sat:
                UB = Z
                return s.model()
            elif r==unsat:
                LB = C
                s.pop()

            i = i + 1
            if (i > M):
                raise Z3Exception("maximum not found, maximum number of iterations was reached")
    return unsat

И это еще один экземпляр (Краткий экземпляр кода), который я использовал в первоначальных тестах, и это работало хорошо в любом случае.

Что такое некорректный бинарный поиск или какая-то концепция Z3 применена неправильно?

С уважением, Алекс


z3 z3py sat-solvers
person afdez    schedule 25.06.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я не думаю, что ваша проблема связана с самой минимизацией. Если вы поместите print r после r = s.check() в свою программу, вы увидите, что z3 просто изо всех сил пытается вернуть результат. Таким образом, ваш цикл даже не выполняется один раз.

Невозможно прочитать вашу программу, так как она очень большая! Но я вижу массу вещей в форме:

 Or(X250 == 0, X500 == 1)

Это говорит о том, что ваши переменные X250 X500 и т. д. (а их очень много) на самом деле являются логическими, а не целыми числами. Если это действительно так, вы должны абсолютно придерживаться логических значений. Решение целочисленных ограничений значительно сложнее, чем решение чисто логических ограничений, и когда вы используете целые числа для моделирования логических значений, подобных этому, базовый решатель просто исследует пространство поиска, которое просто недоступно.

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

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

person alias    schedule 25.06.2019
comment
Я понимаю, что изменение значений Ints на значения Bools устраняет большинство ограничений модели и упрощает решение для Z3, это значительно. Я добавил код с небольшим экземпляром в конце моего первоначального вопроса для лучшего понимания. - person afdez; 25.06.2019
comment
Да, похоже, это просто логические значения; поэтому вы должны сделать их логическими. И похоже, что у вас есть псевдобулевы ограничения; т. е. вещи вида не более чем K из этих N логических значений истинны; которые напрямую моделируются Pb ограничениями. См. этот ответ: stackoverflow.com/questions/43081929/ Как только вы полностью избавитесь от целых чисел, я думаю, что z3 хорошо масштабируется для этой проблемы. Возможно, вам даже не понадобится бинарный поиск. Оптимизатор может работать нормально; но это то, что нужно явно проверить. - person alias; 25.06.2019