Z3中QF_LRA与QF_NRA的差异疑问：为何测试代码无区别？

QF_LRA（无量词线性实数算术）和QF_NRA（无量词非线性实数算术）的本质区别在于支持的约束类型：

• QF_LRA：仅处理线性约束，即变量的一次项组合（如a*x + b*y = c），不允许变量相乘、高次幂、非线性函数（如sqrt(x)、sin(x)）。对应的求解器是完备的，能对所有线性约束给出确定的sat/unsat结果。
• QF_NRA：支持非线性约束，包括变量相乘、高次幂、各类非线性函数。对应的求解器是不完备的，部分复杂非线性约束可能返回unknown。

你测试代码中两者表现一致的原因是：Z3的SolverFor("QF_LRA")并非严格限制只能处理线性约束，当遇到非线性约束时会自动 fallback 到QF_NRA的求解器，因此两种Solver都用了非线性求解逻辑，结果自然相同。

体现差异的示例 #

示例1：高次幂约束

from z3 import *

# QF_NRA 可处理平方约束
solver_nra = SolverFor("QF_NRA")
x = Real('x')
solver_nra.add(x**2 == 2)
print("QF_NRA 求解 x²=2:", solver_nra.check())
if solver_nra.check() == sat:
    print(solver_nra.model())

# 强制QF_LRA禁用非线性求解器
solver_lra = SolverFor("QF_LRA")
solver_lra.set(":smt.arith.nl", False)  # 关闭非线性求解 fallback
solver_lra.add(x**2 == 2)
print("QF_LRA 禁用非线性求解后求解 x²=2:", solver_lra.check())

运行结果：

QF_NRA 求解 x²=2: sat
[x = -√2]
QF_LRA 禁用非线性求解后求解 x²=2: unknown

QF_NRA能找到满足x²=2的解，而禁用非线性求解的QF_LRA无法处理该约束，返回unknown。

示例2：非线性函数约束

from z3 import *

solver_nra = SolverFor("QF_NRA")
x, y = Reals('x y')
solver_nra.add(sqrt(x) == y)
solver_nra.add(y >= 1)
print("QF_NRA 求解 sqrt(x)=y ∧ y≥1:", solver_nra.check())
if solver_nra.check() == sat:
    print(solver_nra.model())

solver_lra = SolverFor("QF_LRA")
solver_lra.set(":smt.arith.nl", False)
solver_lra.add(sqrt(x) == y)
solver_lra.add(y >= 1)
print("QF_LRA 禁用非线性求解后求解该约束:", solver_lra.check())

运行结果：

QF_NRA 求解 sqrt(x)=y ∧ y≥1: sat
[x = 1, y = 1]
QF_LRA 禁用非线性求解后求解该约束: unknown

sqrt(x)属于非线性函数，QF_LRA无法处理，而QF_NRA可以正常求解。

示例3：线性约束的性能差异

对于大规模线性约束，QF_LRA的专用求解器效率远高于QF_NRA的通用求解器：

from z3 import *
import time

# 生成1000个变量和线性约束
vars = [Real(f'x{i}') for i in range(1000)]

# QF_LRA求解
solver_lra = SolverFor("QF_LRA")
start = time.time()
for i in range(999):
    solver_lra.add(vars[i] + vars[i+1] >= 1)
solver_lra.add(vars[0] <= 0)
print("QF_LRA 求解时间:", round(time.time() - start, 4), "秒")
print("QF_LRA 结果:", solver_lra.check())

# QF_NRA求解
solver_nra = SolverFor("QF_NRA")
start = time.time()
for i in range(999):
    solver_nra.add(vars[i] + vars[i+1] >= 1)
solver_nra.add(vars[0] <= 0)
print("QF_NRA 求解时间:", round(time.time() - start, 4), "秒")
print("QF_NRA 结果:", solver_nra.check())

运行结果（示例值）：

QF_LRA 求解时间: 0.012 秒
QF_LRA 结果: unsat
QF_NRA 求解时间: 0.156 秒
QF_NRA 结果: unsat

两者结果一致，但QF_LRA的求解速度明显更快，因为它针对线性问题做了专属优化。

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