如何将Sympy布尔表达式树自动转换为Z3Py布尔约束？

需求背景 #

我通过Sympy逻辑模块生成了CNF格式的布尔表达式，需要将这些表达式自动转换为Z3Py可识别的约束，替代手动逐个转换的低效方式。核心转换要求：

• 将sympy.Symbol转换为z3.Bool
• 将Sympy的And/Or/Not逻辑算子对应转换为Z3的同名算子

最优实现方案：递归遍历表达式树 #

利用Sympy表达式的树形结构特性，通过递归遍历完成转换，这是最简洁且可扩展的实现方式，代码如下：

from sympy import Symbol
from sympy.logic.boolalg import And, Or, Not
import z3

def sympy_to_z3(sympy_expr, symbol_map=None):
    # 初始化符号映射字典，确保同一个Sympy符号对应唯一的Z3符号
    if symbol_map is None:
        symbol_map = {}
    
    # 处理原子符号：Sympy Symbol -> Z3 Bool
    if isinstance(sympy_expr, Symbol):
        if sympy_expr not in symbol_map:
            symbol_map[sympy_expr] = z3.Bool(str(sympy_expr))
        return symbol_map[sympy_expr]
    
    # 处理非运算：Sympy Not -> Z3 Not
    elif isinstance(sympy_expr, Not):
        child = sympy_to_z3(sympy_expr.args[0], symbol_map)
        return z3.Not(child)
    
    # 处理与运算：Sympy And -> Z3 And
    elif isinstance(sympy_expr, And):
        z3_children = [sympy_to_z3(child, symbol_map) for child in sympy_expr.args]
        return z3.And(*z3_children)
    
    # 处理或运算：Sympy Or -> Z3 Or
    elif isinstance(sympy_expr, Or):
        z3_children = [sympy_to_z3(child, symbol_map) for child in sympy_expr.args]
        return z3.Or(*z3_children)
    
    # 其他布尔类型可按需扩展
    else:
        raise TypeError(f"不支持的Sympy布尔表达式类型: {type(sympy_expr)}")

# 测试示例
if __name__ == "__main__":
    # 定义Sympy表达式
    expr_1 = And(Or(Symbol('a'), Not(Symbol('c'))), Or(Symbol('a'), Not(Symbol('e'))), Or(Symbol('c'), Symbol('e'), Not(Symbol('a'))))
    expr_2 = And(Or(Symbol('b'), Not(Symbol('d'))), Or(Symbol('b'), Not(Symbol('e'))), Or(Symbol('d'), Symbol('e'), Not(Symbol('b'))))
    
    # 转换为Z3约束
    const_1 = sympy_to_z3(expr_1)
    const_2 = sympy_to_z3(expr_2)
    
    # 验证转换结果并求解
    solver = z3.Solver()
    solver.add(const_1, const_2)
    if solver.check() == z3.sat:
        print("可满足，解为：")
        print(solver.model())
    else:
        print("不可满足")

方案优势 #

• 自动化无差错：避免手动转换复杂表达式时容易出现的语法错误或逻辑遗漏
• 通用性强：不仅支持CNF格式，还能处理任意嵌套的Sympy布尔表达式
• 符号一致性：通过symbol_map字典确保同一个Sympy符号始终对应同一个Z3布尔变量，避免符号冲突
• 可扩展性高：如需支持其他Sympy布尔算子（如Implies、Xor），只需在函数中添加对应类型的处理分支即可

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