1

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] を生成するようです。特定の制約で使用されていない変数のモデル補完でさえ、常に決定論的な結果を生成するようです。

このオプションがどのように機能するかについてのアイデアやヒントはありますか?

4

1 に答える 1

1

キャッチしてくれてありがとう！確かに、ランダム シードが算術理論に渡されないバグがありました。これは現在、不安定版ブランチで修正されています (修正はこちら)。

この例:

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

現在、3 つの異なるモデルを生成しています。

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

このオプションが正しく渡されない別の場所があるようです (たとえば、qflra タクティックを直接呼び出す代わりに set-logic を使用する場合)、それについてはまだ調査中です。

于 2014-06-23T14:55:01.850 に答える