时间戳

首页 > 解决方案 > Z3py，随机不同的解决方案生成

python - Z3py，随机不同的解决方案生成

问题描述

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

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

标签： pythonz3z3py

解决方案

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

推荐阅读