Случайность Z3 сгенерированных значений модели

Я пытаюсь повлиять на случайность результатов для значений модели, сгенерированных Z3. Насколько я понимаю, возможности для этого очень ограничены: в случае линейной арифметики симплексный решатель не допускает случайных результатов, которые по-прежнему удовлетворяют заданным ограничениям. Однако есть опция smt.arith.random_initial_value ("использовать случайные начальные значения в симплексной процедуре для линейной арифметики (по умолчанию: false)"), которая, похоже, не работает:

from z3 import *
set_option('smt.arith.random_initial_value',True)
x = Int('x')
y = Int('y')
s = Solver()
s.add( x+y > 0)
s.check()
s.model()

Кажется, что в результате всегда получается [y = 0, x = 1]. Даже завершение модели для переменных, не используемых в данных ограничениях, кажется, все время дает детерминированные результаты.

Любые идеи или подсказки о том, как работает этот вариант?


z3 z3py
person Carsten Rütz    schedule 20.06.2014    source источник
comment
Вы были бы заинтересованы в итеративном способе получения случайных моделей? Вы можете уточнить данную модель, добавляя случайные ограничения, такие как x >= rand(), пока вы не потеряете контроль.   -  person usr    schedule 20.06.2014

Ответы (1)


arrow_upward
1
arrow_downward

Спасибо, что поймали это! Действительно, была ошибка, из-за которой случайное начальное число не передавалось в арифметическую теорию. Теперь это исправлено в нестабильной ветке (исправьте здесь).

Этот пример:

(set-option :smt.arith.random_initial_value true)
(declare-const x Int)
(declare-const y Int)
(assert (> (+ x y) 0))
(check-sat-using (using-params qflra :random_seed 1))
(get-model)
(check-sat-using (using-params qflra :random_seed 2))
(get-model)
(check-sat-using (using-params qflra :random_seed 3))
(get-model)

Сейчас выпускает три разные модели:

sat
model
  (define-fun y () Int
    4294966763)
  (define-fun x () Int
    4294966337)
)
sat
(model
  (define-fun y () Int
    216)
  (define-fun x () Int
    4294966341)
)
sat
(model
  (define-fun y () Int
    196)
  (define-fun x () Int
    4294966344)
)

Похоже, что может быть еще одно место, где эта опция не передается правильно (например, при использовании set-logic вместо прямого вызова тактики qflra), мы все еще изучаем это.

person Christoph Wintersteiger    schedule 23.06.2014
comment
Как я могу указать check-sat-using (using-params qflra: random_seed 2) в python при использовании z3py? Я искал везде и не мог найти... Я мог найти только эквивалент check-sat, который является просто Solver.check(). - person Jack Feng; 03.02.2020