Z3py, генерация случайных различных решений - PullRequest
Новая
       8

Z3py, генерация случайных различных решений

0 голосов
/ 03 февраля 2020 
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

Как я могу сделать его более случайным? По крайней мере, не список последовательных номеров. Моя оптимальная цель - иметь список решений, которые достаточно равномерно распределены в пространстве решений.

1 Ответ

1 голос
/ 03 февраля 2020

Я думаю, вы смешиваете то, что делает рандомизация с выборкой. Как отметил @ Johan C, вы обычно исправляете случайное начальное число, чтобы получить последовательные результаты в SMT при нескольких запусках. не означает, что вы получите другой результат только потому, что вы меняете семя. Выборка - это совсем другая (и гораздо более сложная) проблема, чем установка случайных чисел. В противном случае то, что вы делаете, правильно; Чтобы найти все настраиваемые параметры, запустите z3 -p > options.txt и посмотрите в options.txt ключевые слова seed и random.

...