Z3可满足性求解快速但量词消除卡顿，求解决方案及替代求解器

问题描述 #

使用Z3 Python API编写如下公式：

from z3 import *

xOne = Real('xOne')
xTwo = Real('xTwo')
kOne = Real('kOne')
kTwo = Real('kTwo')
FETCH_xOne = Real('FETCH_xOne')
FETCH_xTwo = Real('FETCH_xTwo')
FETCH_kOne = Real('FETCH_kOne')
FETCH_kTwo = Real('FETCH_kTwo')

quantified_phi = Exists([xTwo, kOne, xOne, kTwo],
       Not(Or(3/2*FETCH_xOne + -kOne*xOne - kTwo*xTwo < xOne,
              Or(xOne <
                 3/2*FETCH_xOne + -kOne*xOne - kTwo*xTwo,
                 Or(1/5*FETCH_xTwo < xTwo,
                    Or(xTwo < 1/5*FETCH_xTwo,
                       Or(Or(Or(FETCH_kOne < kOne,
                                Or(kOne < FETCH_kOne,
                                   Or(FETCH_kTwo < kTwo,
                                      kTwo < FETCH_kTwo))),
                             Not(xTwo < FETCH_xTwo)),
                          Not(xOne < FETCH_xOne))))))))

执行可满足性检查时很快得到sat结果：

solver = Solver()
solver.add(quantified_phi)
print(solver.check())

但调用qe2策略执行量词消除时程序陷入卡顿：

t = Tactic('qe2')
result = t(quantified_phi)

尝试qe-light和qe策略，均无法完成完全量词消除：

• qe-light结果：

[[Exists([xTwo, kOne, xOne, kTwo],
         And(Not(FETCH_xOne <= xOne),
             xOne <=
             3/2*FETCH_xOne + -1*xOne*kOne + -1*kTwo*xTwo,
             3/2*FETCH_xOne + -1*xOne*kOne + -1*kTwo*xTwo <=
             xOne,
             xTwo <= 1/5*FETCH_xTwo,
             1/5*FETCH_xTwo <= xTwo,
             Not(FETCH_xTwo <= xTwo),
             FETCH_kTwo <= kTwo,
             kOne <= FETCH_kOne,
             FETCH_kOne <= kOne,
             kTwo <= FETCH_kTwo))]]

• qe结果：

[[Exists(x!44,
         And(3/2*FETCH_xOne +
             -1*FETCH_kOne*x!44 +
             -1/5*FETCH_kTwo*FETCH_xTwo <=
             x!44,
             x!44 <=
             3/2*FETCH_xOne +
             -1*FETCH_kOne*x!44 +
             -1/5*FETCH_kTwo*FETCH_xTwo,
             Not(0 <= x!44 + -1*FETCH_xOne),
             Not(FETCH_xTwo <= 0)))]][

需要解决的问题：

• 为什么qe2会卡顿？
• 如何实现完全量词消除？
• 有没有其他可替代的求解器？

原因分析 #

1. qe2的算法局限性：qe2基于虚拟替换算法，对线性实数约束效率很高，但你的公式中存在kOne*xOne、kTwo*xTwo这类非线性项（变量相乘），虚拟替换处理非线性约束时会生成大量分支，导致计算量指数级增长，最终引发卡顿。
2. 公式结构冗余：原公式嵌套了多层Or和Not，逻辑结构复杂，没有提前化简，加重了求解器的处理负担。

解决方法 #

1. 先化简公式再执行量词消除 #

利用逻辑等价规则展开原公式，减少嵌套冗余：

from z3 import *

xOne = Real('xOne')
xTwo = Real('xTwo')
kOne = Real('kOne')
kTwo = Real('kTwo')
FETCH_xOne = Real('FETCH_xOne')
FETCH_xTwo = Real('FETCH_xTwo')
FETCH_kOne = Real('FETCH_kOne')
FETCH_kTwo = Real('FETCH_kTwo')

# 拆解原公式的Or分支，将Not(Or(A,B,C,D,E,F))转为And(Not(A), Not(B), ..., Not(F))
A = 3/2*FETCH_xOne + -kOne*xOne - kTwo*xTwo < xOne
B = xOne < 3/2*FETCH_xOne + -kOne*xOne - kTwo*xTwo
C = 1/5*FETCH_xTwo < xTwo
D = xTwo < 1/5*FETCH_xTwo
E = Or(FETCH_kOne < kOne, kOne < FETCH_kOne, FETCH_kTwo < kTwo, kTwo < FETCH_kTwo)
F = Not(xTwo < FETCH_xTwo)
G = Not(xOne < FETCH_xOne)

# 构建化简后的公式
simplified_phi = Exists([xTwo, kOne, xOne, kTwo],
                       And(Not(A), Not(B), Not(C), Not(D), Not(E), Not(F), Not(G)))

# 调用Z3内置化简工具进一步优化
simplified_phi = simplify(simplified_phi)
print(simplified_phi)

化简后的公式约束更清晰，能大幅减少量词消除时的分支数量。

2. 调整量词消除策略 #

• 组合策略预处理：将化简和量词消除结合，先用simplify做逻辑规整，再调用qe：

  t = Then('simplify', 'qe')
  result = t(simplified_phi)
  print(result)
  

• 避开qe2处理非线性约束：如果公式存在变量相乘的非线性项，qe2效率极低，优先使用qe或qe-light。
• 手动完成剩余量词消除：从qe的结果来看，剩余的单个存在量词对应一个等式约束，可以手动求解：
  等式：3/2*FETCH_xOne - FETCH_kOne*x!44 - 1/5*FETCH_kTwo*FETCH_xTwo = x!44
  整理得：x!44 = (3/2*FETCH_xOne - 1/5*FETCH_kTwo*FETCH_xTwo)/(1 + FETCH_kOne)（需满足1 + FETCH_kOne ≠ 0）
  将其代入剩余约束Not(x!44 <= FETCH_xOne)和Not(FETCH_xTwo <= 0)，即可得到完全无量词的公式。

替代求解器 #

如果Z3的量词消除能力无法满足需求，可尝试以下工具：

• CVC5：支持线性和非线性实数理论的量词消除，对复杂公式的处理效率优于Z3部分策略，Python API使用方式与Z3兼容。
• Mathematica：内置Resolve函数，对非线性约束的量词消除能力较强，但属于商业软件。
• Redlog：专为实数/整数理论设计的量词消除工具，集成在Reduce系统中，适合处理代数类约束。

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