如何让Z3 Python中的存在性命题始终简化为True/False？

问题背景 #

需要借助Z3求解器判断向量b是否处于向量组a的张成空间中，期望结果始终是True或False。使用存在性命题Exists()实现逻辑时，部分场景能正确简化为布尔值，但有些场景结果仍以Exists()表达式形式呈现，无法直接得到布尔值。

示例代码与问题现象 #

示例1：输出正常布尔值 #

import numpy as np
from z3 import *
solver = Solver()
a=np.array([[0,1,1],[0,0,1]])
b=np.array([1,1,1])
Coefficient=[Int('c_%s' %i) for i in range(2)]
linear_combination = np.dot(Coefficient,a)
answer = Bool('answer')
solver.add(answer == Exists(Coefficient,And([linear_combination[i]==b[i] for i in range(len(b))])))
solver.check()
solver.model().evaluate(answer)

输出：

Out[4]: False

示例2：输出Exists表达式 #

import numpy as np
from z3 import *
solver = Solver()
a=np.array([[1,1,1],[1,1,1]])
b=np.array([1,1,1])
Coefficient=[Int('c_%s' %i) for i in range(2)]
linear_combination = np.dot(Coefficient,a)
answer = Bool('answer')
solver.add(answer == Exists(Coefficient,And([linear_combination[i]==b[i] for i in range(len(b))])))
solver.check()
solver.model().evaluate(answer)

输出：

Out[6]: Exists([c_0, c_1], c_0 + c_1 == 1)

解决方案 #

出现这种差异的原因是：当存在性命题的真值可直接判定（比如无解），Z3会简化为布尔值；但当命题有无限多解时，Z3不会自动将Exists表达式简化为True。要始终得到布尔值，推荐直接利用Z3的求解能力判断线性方程组是否有解，无需使用Exists表达式。

方法：直接判断方程组的可满足性 #

核心思路是将线性组合等于b的约束添加到求解器，通过solver.check()的返回结果直接得到布尔值：

• 返回sat：存在符合条件的系数，即b在a的张成空间中，结果为True
• 返回unsat：不存在符合条件的系数，结果为False

修改后的示例代码：

import numpy as np
from z3 import *

a = np.array([[1,1,1],[1,1,1]])
b = np.array([1,1,1])
Coefficient = [Int(f'c_{i}') for i in range(2)]
solver = Solver()

# 添加线性组合等于b的约束
linear_combination = np.dot(Coefficient, a)
for i in range(len(b)):
    solver.add(linear_combination[i] == b[i])

# 直接获取布尔结果
is_in_span = solver.check() == sat
print(is_in_span)  # 输出：True

可选方法：通过判定命题真假获取布尔值 #

如果一定要使用Exists表达式，可以通过判断命题的否定是否不可满足来得到布尔值：

import numpy as np
from z3 import *

a = np.array([[1,1,1],[1,1,1]])
b = np.array([1,1,1])
Coefficient = [Int(f'c_{i}') for i in range(2)]
linear_combination = np.dot(Coefficient, a)

# 构造存在性命题
prop = Exists(Coefficient, And([linear_combination[i]==b[i] for i in range(len(b))]))

# 判断命题是否为真
solver = Solver()
solver.add(Not(prop))
is_in_span = solver.check() == unsat
print(is_in_span)  # 输出：True

总结 #

最简洁可靠的方式是直接将线性方程组作为约束添加到求解器，通过solver.check()的结果得到布尔值，这种方法避免了Exists表达式带来的简化问题，能始终输出True或False。

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