Как улучшить бинарный поиск в Z3py - PullRequest
Новая
       73

Как улучшить бинарный поиск в Z3py

0 голосов
/ 25 июня 2019

Я пытаюсь оптимизировать с помощью 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 не применяется правильно?

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

1 Ответ

0 голосов
/ 25 июня 2019

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

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

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

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

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

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

...