如何在Z3中断言未知长度数字的最高位为特定值？

要验证一个未知位数的整数最高位为特定值（比如9），核心思路是利用区间约束：对于数字N，存在非负整数k，使得9*10^k ≤ N < 10^(k+1)。这个区间刚好覆盖所有最高位为9的数（从9本身，到90-99、900-999等）。

具体实现（Z3Py） #

直接通过整数变量和存在量词来构建约束：

from z3 import *

# 定义目标数字变量
N = Int('N')

# 创建求解器并添加最高位为9的约束
s = Solver()
# 约束1：N是正整数（最高位为9不可能为0或负数）
s.add(N > 0)
# 约束2：存在非负整数k，使得N落在[9*10^k, 10^(k+1))区间内
s.add(Exists(Int('k'), And(
    Int('k') >= 0,
    9 * (10 ** Int('k')) <= N,
    N < 10 ** (Int('k') + 1)
)))

# 测试示例
# 满足条件的情况
s.push()
s.add(N == 9)
print("N=9：", s.check())  # 输出 sat（满足）
s.pop()

s.push()
s.add(N == 95)
print("N=95：", s.check())  # 输出 sat
s.pop()

s.push()
s.add(N == 9999)
print("N=9999：", s.check())  # 输出 sat
s.pop()

# 不满足条件的情况
s.push()
s.add(N == 8)
print("N=8：", s.check())  # 输出 unsat（不满足）
s.pop()

s.push()
s.add(N == 100)
print("N=100：", s.check())  # 输出 unsat
s.pop()

s.push()
s.add(N == 899)
print("N=899：", s.check())  # 输出 unsat
s.pop()

通用化扩展 #

如果要验证最高位为其他数字（比如d，1≤d≤9），只需把约束中的9替换为d，10^(k+1)替换为(d+1)*10^k即可：

d = 5  # 示例：最高位为5
s.add(Exists(Int('k'), And(
    Int('k') >= 0,
    d * (10 ** Int('k')) <= N,
    N < (d + 1) * (10 ** Int('k'))
)))

原理说明 #

• 10^k表示1后面跟着k个0，9*10^k就是最高位为9、后面k位全0的最小数（比如k=1时是90，k=2时是900）。
• 10^(k+1)是比9*10^k高一位的最小数（比如k=1时是100，k=2时是1000），因此N落在这个区间内时，最高位必然是9。

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