使用Z3Py的all_smt生成模型全解时结果错误的问题排查

我直接使用《Programming Z3》手册中的all_smt函数生成所有有效解的迭代器，同时实现了功能相同的朴素版本all_smt_slow_method。针对如下约束问题：

• x、y、z为0到11之间的整数
• x与y的差值≤8
• y与z的差值≤8

求解有效(x,y,z)对的数量时，all_smt_slow_method得到正确结果1468，但all_smt仅返回111个结果，怀疑是all_smt的调用方式有误，相关代码如下：

from z3 import *


def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))

    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))

    def all_smt_rec(terms):
        if sat == s.check():
            m = s.model()
            yield m
            for i in range(len(terms)):
                s.push()
                block_term(s, m, terms[i])
                for j in range(i):
                    fix_term(s, m, terms[j])
                yield from all_smt_rec(terms[i:])
                s.pop()

    yield from all_smt_rec(list(initial_terms))


def all_smt_slow_method(s, initial_terms, x, y, z):
    s.add(initial_terms)
    manual_counter = 0
    while s.check() == sat:
        s.add(Or(x != s.model()[x], y != s.model()[y], z != s.model()[z]))
        manual_counter += 1
    return manual_counter


def main():
    maximum_delta = 8
    range = 12
    x, y, z = Ints("x y z")
    initial_terms = [
        0 <= x,
        x < range,
        0 <= y,
        y < range,
        0 <= z,
        z < range,
    ]
    initial_terms += [
        x - y <= maximum_delta,
        y - x <= maximum_delta,
        y - z <= maximum_delta,
        z - y <= maximum_delta,
    ]

    manual_counter = all_smt_slow_method(Solver(), initial_terms, x, y, z)

    all_smt_generator = all_smt(Solver(), initial_terms)
    all_smt_counter = sum(1 for x in all_smt_generator)

    print(f"{range ** 3 = } {manual_counter = } {all_smt_counter = }")


if __name__ == "__main__":
    main()

all_smt函数的设计初衷是接收变量列表作为initial_terms参数，它通过递归固定前面的变量值、枚举后面变量的方式生成所有解。但你现在传入的是约束条件列表，完全不符合函数的预期用法，导致逻辑混乱，只生成了部分解。

1. 调用all_smt前，先将约束条件添加到求解器中
2. 调用all_smt时传入变量列表[x, y, z]而非约束条件

修改后的main函数如下：

def main():
    maximum_delta = 8
    range = 12
    x, y, z = Ints("x y z")
    initial_terms = [
        0 <= x,
        x < range,
        0 <= y,
        y < range,
        0 <= z,
        z < range,
    ]
    initial_terms += [
        x - y <= maximum_delta,
        y - x <= maximum_delta,
        y - z <= maximum_delta,
        z - y <= maximum_delta,
    ]

    manual_counter = all_smt_slow_method(Solver(), initial_terms, x, y, z)

    # 修正all_smt的调用方式
    s = Solver()
    s.add(initial_terms)
    all_smt_generator = all_smt(s, [x, y, z])
    all_smt_counter = sum(1 for _ in all_smt_generator)

    print(f"{range ** 3 = } {manual_counter = } {all_smt_counter = }")

运行修改后的代码，all_smt_counter会输出正确的1468，与manual_counter结果一致。

内容的提问来源于stack exchange，提问作者My other car is a cadr