Python中如何高效求解含大型三维数组的Z3查询？

问题背景 #

需要对尺寸为480×200×3的三维数组的连续实例进行属性校验，当前实现是生成包含数组声明、288000个元素等式断言的SMT字符串，再通过Z3求解，但因断言数量过大导致求解耗时极长。

当前使用的SMT规格模板：

(declare-const {varname} (Array Int (Array Int (Array Int Int))))
(assert (and
    (= (select (select (select {varname} 0) 0) 0) varvalue[0][0][0])
    (= (select (select (select {varname} 0) 0) 1) varvalue[0][0][1])
    (= (select (select (select {varname} 0) 0) 2) varvalue[0][0][2])
    ...
    (= (select (select (select {varname} 479) 199) 0) varvalue[479][199][0])
    (= (select (select (select {varname} 479) 199) 1) varvalue[479][199][1])
    (= (select (select (select {varname} 479) 199) 2) varvalue[479][199][2])
))
[formula]

当前Python执行代码：

temp_solver = z3.Solver()
temp_solver.from_string(spec)
negation_is_sat = (z3.sat == temp_solver.check())

优化方案 #

1. 用嵌套Store直接构造常量数组 #

Z3的数组理论支持通过Store操作嵌套构造完整的三维数组，替代逐个元素的等式断言。这种方式将数组视为单一约束，Z3能利用数组层面的优化，大幅减少推理开销。

示例代码：

import z3

def build_3d_const_array(value_array):
    # 构造最内层一维数组（长度3）
    def build_1d(row_vals):
        arr = z3.Array('tmp_row', z3.IntSort(), z3.IntSort())
        for idx, val in enumerate(row_vals):
            arr = z3.Store(arr, idx, val)
        return arr
    
    # 构造二维层（长度200）
    def build_2d(layer_vals):
        arr = z3.Array('tmp_layer', z3.IntSort(), z3.ArraySort(z3.IntSort(), z3.IntSort()))
        for row_idx, row in enumerate(layer_vals):
            arr = z3.Store(arr, row_idx, build_1d(row))
        return arr
    
    # 构造完整三维数组（长度480）
    full_arr = z3.Array('target_arr', z3.IntSort(), z3.ArraySort(z3.IntSort(), z3.ArraySort(z3.IntSort(), z3.IntSort())))
    for layer_idx, layer in enumerate(value_array):
        full_arr = z3.Store(full_arr, layer_idx, build_2d(layer))
    return full_arr

# 使用示例
# 假设varvalue是预先定义的480×200×3数值数组
target_array = build_3d_const_array(varvalue)
solver = z3.Solver()
# 添加你的属性校验公式
solver.add(your_property_formula(target_array))
negation_is_sat = (z3.sat == solver.check())

2. 直接使用Z3 API构造约束，避免字符串解析 #

原方法通过生成SMT字符串再解析，额外增加了字符串处理和解析的性能损耗。直接用Z3 Python API构造数组和约束，既能减少中间开销，也让代码更易维护。

3. 利用Z3的常量数组优化 #

完全实例化的常量数组会被Z3识别为单一固定值结构，在后续属性校验中，Z3可直接使用数组的固定值进行推理，无需处理数千个独立的等式约束，大幅提升求解效率。

内容的提问来源于stack exchange，提问作者Carlos Gustavo Lopez Pombo