使用Z3 Python打印20以内素数异常：仅输出部分素数问题排查

你的代码逻辑本身是正确的，但Z3在处理变量x的存在量词否定约束时，对于较大的素数（如11、13等），默认求解策略难以高效搜索到解。原素数定义中的Not(Exists(y, And(y < x, 1 < y, x % y == 0)))等价于“所有1<y<x的y都不整除x”，这是一个全称性陈述；当x是变量时，Z3需要遍历的y的范围随x增大而扩大，搜索效率骤降，导致无法找到更大的素数解。而单独测试固定x值时，Z3可以直接枚举y的可能值验证，因此能返回sat。

以下是两种可行的解决方法：

方法1：改用全称量词ForAll定义素数 #

直接用全称量词表达“所有1<y<x的y都不整除x”，Z3对这种形式的约束处理更高效：

from z3 import *
def isPrime(x):
    y = Int('y')
    # 素数定义：x>1，且所有满足1<y<x的y都不能整除x
    return And(x > 1, ForAll(y, Implies(And(1 < y, y < x), x % y != 0)))

s = Solver()

x = Int('x')
s.add(isPrime(x))
s.add(x < 20)

while s.check() == sat:
    ans = s.model()[x]
    print(ans)
    s.add(x != ans)

方法2：优化存在量词的搜索范围 #

利用素数的数学性质：若x有因数，则必有一个因数≤√x。缩小y的搜索范围，减少Z3的计算量：

from z3 import *
def isPrime(x):
    y = Int('y')
    # 素数定义：x>1，且不存在2≤y≤√x的y能整除x
    return And(x > 1, Not(Exists(y, And(y >= 2, y * y <= x, x % y == 0))))

s = Solver()

x = Int('x')
s.add(isPrime(x))
s.add(x < 20)

while s.check() == sat:
    ans = s.model()[x]
    print(ans)
    s.add(x != ans)

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