Почему Z3 медленный для крошечного пространства поиска? - PullRequest
Новая
       20

Почему Z3 медленный для крошечного пространства поиска?

2 голосов
/ 04 мая 2019

Я пытаюсь создать программу Z3 (на Python), которая генерирует логические схемы, которые выполняют определенные задачи (например, добавление двух n-битных чисел), но производительность ужасна до такой степени, что поиск методом полного перебора всегоПространство решения будет быстрее.Я впервые использую Z3, поэтому могу делать что-то, что влияет на мою производительность, но мой код выглядит нормально.

Следующее скопировано из моего кода здесь : 

from z3 import *

BITLEN = 1 # Number of bits in input
STEPS = 1 # How many steps to take (e.g. time)
WIDTH = 2 # How many operations/values can be stored in parallel, has to be at least BITLEN * #inputs

# Input variables
x = BitVec('x', BITLEN)
y = BitVec('y', BITLEN)

# Define operations used
op_list = [BitVecRef.__and__, BitVecRef.__or__, BitVecRef.__xor__, BitVecRef.__xor__]
unary_op_list = [BitVecRef.__invert__]
for uop in unary_op_list:
    op_list.append(lambda x, y : uop(x))

# Chooses a function to use by setting all others to 0
def chooseFunc(i, x, y):
    res = 0
    for ind, op in enumerate(op_list):
        res = res + (ind == i) * op(x, y)
    return res

s = Solver()
steps = []

# First step is just the bits of the input padded with constants
firststep = Array("firststep", IntSort(), BitVecSort(1))
for i in range(BITLEN):
    firststep = Store(firststep, i * 2, Extract(i, i, x))
    firststep = Store(firststep, i * 2 + 1, Extract(i, i, y))
for i in range(BITLEN * 2, WIDTH):
    firststep = Store(firststep, i, BitVec("const_0_%d" % i, 1))
steps.append(firststep)

# Generate remaining steps
for i in range(1, STEPS + 1):
    this_step = Array("step_%d" % i, IntSort(), BitVecSort(1))
    last_step = steps[-1]

    for j in range(WIDTH):
        func_ind = Int("func_%d_%d" % (i,j))
        s.add(func_ind >= 0, func_ind < len(op_list))

        x_ind = Int("x_%d_%d" % (i,j))
        s.add(x_ind >= 0, x_ind < WIDTH)

        y_ind = Int("y_%d_%d" % (i,j))
        s.add(y_ind >= 0, y_ind < WIDTH)

        node = chooseFunc(func_ind, Select(last_step, x_ind), Select(last_step, y_ind))
        this_step = Store(this_step, j, node)

    steps.append(this_step)

# Set the result to the first BITLEN bits of the last step
if BITLEN == 1:
    result = Select(steps[-1], 0)
else:
    result = Concat(*[Select(steps[-1], i) for i in range(BITLEN)])

# Set goal
goal = x | y
s.add(ForAll([x, y], goal == result))

print(s)
print(s.check())
print(s.model())

Код в основном распределяет входные данные как отдельные биты, тогда на каждом «шаге» одна из 5 булевых функций может работать со значениями из предыдущего шага, где последний шаг представляет конечный результат.

В этом примере я генерирую схему для вычисления логического ИЛИ двух 1-битных входов, и в схеме доступна функция ИЛИ, поэтому решение тривиально.

У меня естьпространство решения всего 5 * 5 * 2 * 2 * 2 * 2 = 400:

  • 5 Возможные функции (два функциональных узла)
  • 2 Входы для каждой функции, каждая изкоторый имеет два возможных значения

Этот код занимает несколько секунд для запуска и дает правильный ответ, но я чувствую, что он должен работать мгновенно, так как существует только 400 возможных решений, из которых довольно многодействительный.Если я увеличу входные данные до двух битов, пространство решения будет иметь размер (5 ^ 4) * (4 ^ 8) = 40 960 000 и никогда не завершится на моем компьютере, хотя я считаю, что это легко сделать с Z3.

Я также попытался эффективно использовать тот же код, но заменил Arrays / Store / Select для списков Python и «выбрал» переменные, используя тот же прием, который я использовал в chooseFunc ().Код здесь , и он работает примерно в то же время, что и исходный код, так что никакого ускорения не происходит.

Я делаю что-то, что резко замедлит работу решателя?Спасибо!

1 Ответ

1 голос
/ 05 мая 2019

У вас есть дубликат __xor__ в вашем op_list; но это не совсем главная проблема. Замедление неизбежно, так как вы увеличиваете размер в битах, но на первый взгляд вы можете (и следует ) избегать смешивания целочисленных рассуждений с логическими значениями здесь. Я бы кодировал ваш chooseFunc следующим образом: 

def chooseFunc(i, x, y):
    res = False;
    for ind, op in enumerate(op_list):
        res = If(ind == i, op (x, y), res)
    return res

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

...