Z3:在求解中提供随机解 [英] Z3: Offering random solutions in solving

问题描述

我在 http://rise4fun.com/z3/tutorial

(declare-const a Int)
(assert (> a 100))
(check-sat)
(get-model)

结果总是a=101.我在答案中需要一些随机性，它会产生 [101,MAXINT) 范围内的随机数.例如获取 seed=1000 并提供 a=12344.对于 seed=2323 提供 a=9088765 和 ... .

the result is always a=101. I need some randomness in the answer that it produce a random number in the range [101,MAXINT). for example gets a seed=1000 and offers the a=12344. for seed=2323 offers a=9088765 and ... .

我应该在这个简单的代码中添加什么?

what should i add to this simple code?

推荐答案

线性算术求解器基于 Simplex 算法.因此，解决方案不会是随机的.位向量求解器基于 SAT，您可以通过在位向量算法中对问题进行编码并选择随机相位选择来获得随机"解决方案.这是一个示例(也可以在此处获得):

The linear arithmetic solver is based on the Simplex algorithm. So, the solutions will not be random. The bit-vector solver is based on SAT, you can get "random" solutions by encoding your problem in bit-vector arithmetic and selecting random phase selection. Here is an example (also available here):

(set-option :auto-config false)
(set-option :phase-selection 5) ;; select random phase selection
(declare-const a (_ BitVec 32))
(assert (bvugt a (_ bv100 32))) ;; a > 100 as a bitvector constraint
(check-sat)
(get-model)
;; try again
(check-sat)
(get-model)
;; try again
(check-sat)
(get-model)

这篇关于Z3:在求解中提供随机解的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！