Z3 生成模型值的随机性 [英] Z3 randomness of generated model values

问题描述

我试图影响 Z3 生成的模型值的结果随机性.据我了解，此选项非常有限:在线性算术的情况下，单纯形求解器不允许仍然满足给定约束的随机结果.但是，有一个选项 smt.arith.random_initial_value(在基于单纯形的程序中使用随机初始值进行线性算术(默认:false)")，我似乎无法使用:

I'm trying to influence the randomness of results for model values generated by Z3. As far as I understand, the options for this are very limited: in case of linear arithmetic, the simplex solver does not allow for random results that still satisfy the given constraints. However, there is an option smt.arith.random_initial_value ("use random initial values in the simplex-based procedure for linear arithmetic (default: false)") which I don't seem to get working:

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].即使是在给定约束中未使用的变量的模型完成似乎也一直会产生确定性的结果.

This seems to always produce [y = 0, x = 1] as a result. Even model completion for variables unused in the given constraints seems to produce deterministic results all the time.

有关此选项如何工作的任何想法或提示?

Any ideas or hints about how this option works?

推荐答案

感谢您发现这个问题！确实存在导致随机种子无法传递到算术理论的错误.现在已在不稳定分支中修复此问题(修复此处).

Thanks for catching that! There was indeed a bug that caused the random seed not to be passed through to the arithmetic theory. This is now fixed in the unstable branch (fix here).

这个例子:

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

现在生产三种不同的模型:

Now produces three different models:

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 策略时)，我们仍在调查.

It looks like there may be another place where this option isn't passed through correctly (e.g., when using set-logic instead of calling the qflra tactic directly), we're still looking into that.

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