我正在尝试制作一个 Z3 程序(在 Python 中),它生成执行某些任务的布尔电路(例如,添加两个 n 位数字),但性能非常糟糕,以至于对整个解决方案空间进行强力搜索将导致快一点。这是我第一次使用 Z3,所以我可能会做一些影响我性能的事情,但我的代码看起来不错。
以下是从我的代码复制的here https://github.com/leoadberg/smt_fun/blob/master/adder.py:
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 位输入的布尔 OR 值,并且电路中提供了 OR 函数,因此解决方案很简单。
我的解空间只有 5*5*2*2*2*2=400:
- 5 可能的功能(两个功能节点)
- 每个函数有 2 个输入,每个输入有两个可能的值
这段代码需要几秒钟的时间才能运行并提供正确的答案,但我觉得它应该立即运行,因为只有 400 种可能的解决方案,其中相当多的解决方案是有效的。如果我将输入增加到两位长,则解决方案空间的大小为 (5^4)*(4^8)=40,960,000 并且永远不会在我的计算机上完成,尽管我觉得这应该可以使用 Z3 轻松实现。
我还有效地尝试了相同的代码,但用 Arrays/Store/Select 替换了 Python 列表,并使用我在 choiceFunc() 中使用的相同技巧“选择”了变量。代码是here https://github.com/leoadberg/smt_fun/blob/master/adder2.py它的运行时间与原始代码的运行时间大致相同,因此没有加速。
我是否做了一些会大大减慢求解器速度的事情?谢谢!