Z3-Solver变量替换报错：invalid substitution, expression pairs expected

问题重现 #

为复杂Z3布尔公式的特定变量赋值时，触发错误：

raise Z3Exception(msg)
z3.z3types.Z3Exception: Z3 invalid substitution, expression pairs expected.

用户代码如下：

def create_z3_formula_bdd(dimacs_file):
    variable_names = {
        1: 'inflow1', 2: "inflow1'",
        3: 'inflow2', 4: "inflow2'",
        5: 'level@0.3.107', 6: "level@0.3.107'",
        7: 'level@1', 8: "level@1'",
        9: 'level@2', 10: "level@2'",
        11: 'level@3', 12: "level@3'",
        13: 'level@4', 14: "level@4'",
        15: 'level@5', 16: "level@5'",
        17: 'level@6', 18: "level@6'",
        19: 'outflow', 20: "outflow'",
        21: '_jx_b0'
    }
    with open(dimacs_file, 'r') as f:
        dimacs_lines = f.readlines()

    # Parse variables and clauses
    variables = set()
    clauses = []
    for line in dimacs_lines:
        tokens = line.split()
        if tokens[0] == 'p':
            num_vars = int(tokens[2])
        elif tokens[0] != 'c' and tokens[0] != '0':
            clause = [int(var) for var in tokens[:-1]]
            variables.update(map(abs, clause))
            clauses.append(clause)

    z3_variables = {var: Bool(variable_names[abs(var)]) for var in variables}

    # Create Z3 clauses
    z3_clauses = [Or([z3_variables[abs(literal)] if literal > 0 else Not(z3_variables[abs(literal)]) for literal in clause]) for clause in clauses]

    return And(z3_clauses)

formula_bdd = create_z3_formula_bdd('neg_water_reservoir.cnf')
substitution_map = {variable_names[1]: False}
formula_with_substitution = substitute(formula_bdd, substitution_map)

错误原因 #

Z3的substitute函数不接受字符串作为替换目标，它需要Z3表达式对象与替换值的配对；同时substitute要求参数是列表形式的表达式对，而非字典。你传入的字典键是变量名字符串（如'inflow1'），不是实际创建的Bool变量对象，这直接导致了错误。

修复方案 #

方案1：使用substitute并传入表达式对列表 #

先修改函数返回公式和变量映射，再构建正确的替换配对：

def create_z3_formula_bdd(dimacs_file):
    variable_names = {
        1: 'inflow1', 2: "inflow1'",
        3: 'inflow2', 4: "inflow2'",
        5: 'level@0.3.107', 6: "level@0.3.107'",
        7: 'level@1', 8: "level@1'",
        9: 'level@2', 10: "level@2'",
        11: 'level@3', 12: "level@3'",
        13: 'level@4', 14: "level@4'",
        15: 'level@5', 16: "level@5'",
        17: 'level@6', 18: "level@6'",
        19: 'outflow', 20: "outflow'",
        21: '_jx_b0'
    }
    with open(dimacs_file, 'r') as f:
        dimacs_lines = f.readlines()

    variables = set()
    clauses = []
    for line in dimacs_lines:
        tokens = line.split()
        if tokens[0] == 'p':
            num_vars = int(tokens[2])
        elif tokens[0] != 'c' and tokens[0] != '0':
            clause = [int(var) for var in tokens[:-1]]
            variables.update(map(abs, clause))
            clauses.append(clause)

    z3_variables = {var: Bool(variable_names[abs(var)]) for var in variables}
    z3_clauses = [Or([z3_variables[abs(literal)] if literal > 0 else Not(z3_variables[abs(literal)]) for literal in clause]) for clause in clauses]

    return And(z3_clauses), z3_variables  # 返回公式和变量映射

# 获取公式和变量映射
formula_bdd, z3_vars = create_z3_formula_bdd('neg_water_reservoir.cnf')
# 找到目标变量对应的Z3对象
target_var = z3_vars[1]  # 变量1对应的Z3布尔变量
# 构建替换配对列表
substitution_pairs = [(target_var, False)]
# 执行替换
formula_with_substitution = substitute(formula_bdd, substitution_pairs)

方案2：使用substitute_vars（支持字典格式） #

Z3提供了substitute_vars函数，可以直接接受以Z3变量为键的字典，写法更简洁：

def create_z3_formula_bdd(dimacs_file):
    # 函数内容同方案1，返回公式和变量映射
    variable_names = {
        1: 'inflow1', 2: "inflow1'",
        3: 'inflow2', 4: "inflow2'",
        5: 'level@0.3.107', 6: "level@0.3.107'",
        7: 'level@1', 8: "level@1'",
        9: 'level@2', 10: "level@2'",
        11: 'level@3', 12: "level@3'",
        13: 'level@4', 14: "level@4'",
        15: 'level@5', 16: "level@5'",
        17: 'level@6', 18: "level@6'",
        19: 'outflow', 20: "outflow'",
        21: '_jx_b0'
    }
    with open(dimacs_file, 'r') as f:
        dimacs_lines = f.readlines()

    variables = set()
    clauses = []
    for line in dimacs_lines:
        tokens = line.split()
        if tokens[0] == 'p':
            num_vars = int(tokens[2])
        elif tokens[0] != 'c' and tokens[0] != '0':
            clause = [int(var) for var in tokens[:-1]]
            variables.update(map(abs, clause))
            clauses.append(clause)

    z3_variables = {var: Bool(variable_names[abs(var)]) for var in variables}
    z3_clauses = [Or([z3_variables[abs(literal)] if literal > 0 else Not(z3_variables[abs(literal)]) for literal in clause]) for clause in clauses]

    return And(z3_clauses), z3_variables

formula_bdd, z3_vars = create_z3_formula_bdd('neg_water_reservoir.cnf')
# 构建以Z3变量为键的替换字典
substitution_map = {z3_vars[1]: False}
# 使用substitute_vars执行替换
formula_with_substitution = substitute_vars(formula_bdd, substitution_map)

核心要点 #

• 替换的目标必须是Z3表达式对象（如Bool实例），不能是变量名字符串。
• substitute要求参数是(变量, 值)的列表；substitute_vars支持直接传入字典，更适合批量替换场景。

内容的提问来源于stack exchange，提问作者flessent