我在 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和 ... 。我应该在这个简单的代码中添加什么？
最佳答案
线性算术求解器基于 Simplex 算法。因此，解决方案不会是随机的。
位向量求解器基于 SAT，您可以通过在位向量算法中对问题进行编码并选择随机相位选择来获得“随机”解决方案。这是一个示例(也可用 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:在求解中提供随机解，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/18770582/