如何使用Z3求解计算结果为整数的整数除法问题

问题原因 #

你遇到的问题核心来自两点：

1. Z3中两个Int类型值做/运算时，默认执行向零截断的整数除法，比如Int(-1)/Int(2)的运算结果是0（整数类型），和你预期的数学精确除法结果-0.5完全不符，这是你觉得原有约束结果不正确的核心原因。
2. Z3的模运算符%仅支持整数类型输入，所以你将c改为Real类型后调用%会直接抛出类型错误。

正确实现方案 #

方案1：使用实数运算建模（推荐，无歧义） #

直接按照需求的数学语义建模：先做精确实数除法，再约束结果为整数，完全规避整数除法的语义歧义：

from z3 import *
# 如果要求c本身是整数，就用Int("c")，允许实数就用Real("c")
c = Int("c")
s = Solver()
# Int转Real做精确除法，约束结果为整数
expr = ToReal(-c) / 2
s.add(IsInt(expr))

# 测试反例：添加c==1的约束会返回unsat，符合预期
# s.add(c == 1)

print(s.check())
if s.check() == sat:
    # 打印一个可行解
    print(s.model())

方案2：整数域直接约束整除关系 #

如果确定c是整数，也可以直接在整数域建模「-c是2的整数倍」的逻辑，避免实数运算开销：

from z3 import *
c = Int("c")
s = Solver()
# 直接约束c是偶数，等价于-c能被2整除
s.add(c % 2 == 0)

print(s.check())
if s.check() == sat:
    print(s.model())

所有满足条件的c的通用解为：c = -2 * k，其中k为任意整数。

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