Z3求解模幂方程报错‘Z3 integer expression expected’的解决方法

错误原因 #

你的代码报错是因为Z3的模运算(%)要求操作数必须都是Z3整数表达式，但你直接用了Python原生整数（n、a、b、c）和Z3变量表达式混合运算，导致类型不匹配。另外，你还遗漏了两个关键约束：

• p、q是512位素数
• m的取值范围应该在[0, n-1]（模n的结果必然在这个区间）

修正后的代码 #

from z3 import *

s = Solver()

# 定义变量
m = Int('m')
p = Int('p')
q = Int('q')

# 将常量转换为Z3整数表达式
n = IntVal(101205131618457490641888226172378900782027938652382007193297646066245321085334424928920128567827889452079884571045344711457176257019858157287424646000972526730522884040459357134430948940886663606586037466289300864147185085616790054121654786459639161527509024925015109654917697542322418538800304501255357308131)
a = IntVal(38686943509950033726712042913718602015746270494794620817845630744834821038141855935687477445507431250618882887343417719366326751444481151632966047740583539454488232216388308299503129892656814962238386222995387787074530151173515835774172341113153924268653274210010830431617266231895651198976989796620254642528)
b = IntVal(83977895709438322981595417453453058400465353471362634652936475655371158094363869813512319678334779139681172477729044378942906546785697439730712057649619691929500952253818768414839548038664187232924265128952392200845425064991075296143440829148415481807496095010301335416711112897000382336725454278461965303477)
c = IntVal(21459707600930866066419234194792759634183685313775248277484460333960658047171300820279668556014320938220170794027117386852057041210320434076253459389230704653466300429747719579911728990434338588576613885658479123772761552010662234507298817973164062457755456249314287213795660922615911433075228241429771610549)

# 添加核心约束
s.add(n == p * q)
s.add(Mod(m ** p, n) == a)
s.add(Mod(m ** q, n) == b)
s.add(Mod(m ** n, n) == c)

# 添加素数与位数约束
s.add(IsPrime(p))
s.add(IsPrime(q))
s.add(2**511 <= p < 2**512)
s.add(2**511 <= q < 2**512)

# 添加m的范围约束（模n的结果必然在0到n-1之间）
s.add(0 <= m < n)

# 求解并输出结果
print(s.check())
model = s.model()
if s.check() == sat:
    print(f"m = {model[m]}")
    print(f"p = {model[p]}")
    print(f"q = {model[q]}")

注意事项 #

1. Z3的局限性：Z3是通用定理证明器，并非专门针对大整数数论问题的求解器。对于512位素数这类超大整数的离散对数/幂模问题，Z3的求解效率会极低，甚至可能无法在合理时间内给出结果。如果这类问题是你的核心需求，建议使用专门的数论工具（如SageMath）或密码学库。
2. 幂运算优化：Z3的**运算符处理大指数时性能很差，你可以尝试用模幂的性质简化约束，比如利用欧拉定理：m^n ≡ m^(n mod φ(n) + φ(n)) mod n（当m与n不互质时），不过这需要额外推导约束。

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