Z3py,随机不同的解决方案生成

Z3py, random different solution generation

from z3 import *
import random
a = Int('a')
b = Int('b')

s = Tactic('qflra').solver()
s.add(a > 10)
set_option('smt.arith.random_initial_value', True)
set_option('smt.random_seed', random.randint(0, 2 ** 8))

while s.check() == sat:
    m = s.model()
    print m[a]
    s.add(a != m[a])
    set_option('smt.random_seed', random.randint(0, 2 ** 8))

结果好像只随机了一秒...然后就开始连续给数字了

4294966399
4294966398
4294966397
4294966396
4294966395
4294966394
4294966393
11
12
13
14
4294966400
15
16
17
18
19

如何让它更随机?至少,不是连续数字的列表。我的最佳目标是在解决方案 space 中有一个相当均匀分布的解决方案列表。

我认为您将随机化与抽样混为一谈。正如@JohanC 指出的那样,您通常会修复一个随机种子,以便在多个 运行 的 SMT 中获得一致的结果。 而不是 仅仅因为您更改了种子,就意味着您会得到不同的结果。与设置一些随机数相比,采样是一个完全不同(并且困难得多)的问题。否则,你所做的是正确的;要找到所有可设置的选项,运行 z3 -p > options.txt 并在 options.txt 中查找关键字 seed 和 random。