Блог

Главная - Вопросы по программированию - z3py: Символические выражения не могут быть приведены к конкретным логическим значениям

z3py: Символические выражения не могут быть приведены к конкретным логическим значениям

#optimization #smt #z3py

Вопрос:

У меня возникли проблемы с определением объективной функции в задаче SMT с z3py.

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

У меня есть массив координат (представленный массивом целых чисел длиной 2) и список целых чисел (представляющих высоту размещаемого блока).

     # [x,y] list of integer variables
    P = [[Int("x_%s" % (i   1)), Int("y_%s" % (i   1))]
         for i in range(blocks)]
    
    y = [int(b) for a, b in data[2:]]

Я определил целевую функцию следующим образом:

     obj= Int(max([P[i][1]   y[i] for i in range(blocks)]))

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

В любом случае, если я запущу свой код, в строке целевой функции возникнет следующая ошибка:

«вызовите исключение Z3Exception(«Символические выражения не могут быть приведены к конкретным логическим значениям»)».

Во время отладки я видел, что это P[i][1], которое выдает ошибку, и я думаю, что это потому, что программа читает «y_i 3» (например), и они не могут быть добавлены вместе.

Дело в том, что очевидно, что целевая функция зависит от переменных проблемы, так как же я могу избавиться от этой ошибки? Есть ли другое место, где я должен определить целевую функцию, чтобы она ждала создания экземпляра массива P, прежде чем что-либо делать?

Полный код:

     from z3 import *
    from math import ceil
    
    
    width = 8
    blocks = 4
    x = [3,3,5,5]
    y = [3,5,3,5]
    
    height = ceil(sum([x[i] * y[i] for i in range(blocks)]) / width)   1
    
    # [blocks x 2] list of integer variables
    P = [[Int("x_%s" % (i   1)), Int("y_%s" % (i   1))]
         for i in range(blocks)]
    
    # value/ domain constraint
    values = [And(0 <= P[i][0], P[i][0] <= width - 1, 0 <= P[i][1], P[i][1] <= height - 1)
              for i in range(blocks)]
    
    
    obj = Int(max([P[i][1]   y[i] for i in range(blocks)]))
    
    board_problem = values # other constraints I've not included for brevity
    
    o = Optimize()
    o.add(board_problem)
    o.minimize(obj)
    
    if (o.check == 'unsat'):
        print("The problem is unsatisfiable")
    else:
        print("Solved")

Комментарии:

1. Пожалуйста, опубликуйте свой код, который вызывает проблему, которую люди могут загрузить непосредственно сами, чтобы увидеть ошибку, которую вы видите. Конечно, чем меньше, тем лучше. То есть вся программа, а не только отдельные строки из нее.

2. Без доступа к instancestxtins-1.txt файлу люди не смогут запустить вашу программу. Можете ли вы избавиться от зависимости от этого файла?

Ответ №1:

Проблема здесь в том, что вы вызываете Python max для символьных значений, который не предназначен для работы с символическими выражениями. Вместо этого определите символическую версию max и используйте ее:

 # Return maximum of a vector; error if empty
def symMax(vs):
  m = vs[0]
  for v in vs[1:]:
    m = If(v > m, v, m)
  return m

obj = symMax([P[i][1]   y[i] for i in range(blocks)])

С учетом этого изменения ваша программа будет работать и печататься Solved при запуске.

Метки: