我使用Z3
Python绑定通过z3.And(exprs)创建一个And表达式,其中exprs是一个对布尔变量的48000个相等约束的python列表.在具有2.6GHz处理器的MBP上,此操作需要2秒.

我能做错什么？这是z3 Python绑定的问题吗？关于如何优化这种结构的任何想法？

顺便说一句,在我的实验中,这些表达式的构造花费的时间比解决得到的公式要多:)

最佳答案 在Python上使用Z3通常很慢.它包括参数检查和编组(_coerce_expr等).

对于可伸缩性,您最好使用其他绑定之一或尽可能绕过Python运行时.