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))

结果似乎只是随机了一秒钟......然后它就开始给出连续的数字.

The result seems to be only randomed for a second... Then it just started to give consecutive numbers.

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

我怎样才能让它更随机?至少，不是连续数字的列表.我的最佳目标是拥有一个在解决方案空间中分布相当均匀的解决方案列表.

How can I make it more random? At least, not a list of consecutive numbers. My optimal goal is to have a list of solutions that are rather uniformly distributed in the solution space.

推荐答案

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

I think you're conflating what randomization does with sampling. As @JohanC pointed out, you usually fix a random seed to get consistent results in SMT across multiple runs. Just because you change the seed, does not mean you'll get a different result. Sampling is an entirely different (and much more difficult) problem than setting some random numbers. Otherwise, what you're doing is correct; To find all the settable options, run z3 -p > options.txt and look inside options.txt for the keywords seed and random.

这篇关于Z3py，随机不同解生成的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！