【发布时间】：2014-06-14 11:35:29
【问题描述】：
z3 中的 random-seed 选项有什么用？可以用来生成随机模型吗？在这篇Z3: Offering random solutions in solving 的帖子中，提到LIA 不能有随机模型。那么为什么我们需要随机种子呢？
【问题讨论】：
标签： z3
【发布时间】：2014-06-14 11:35:29
【问题描述】：
您可以使用随机种子来控制 SMT 核心中的命题变量选择启发式。随机种子可用于检查 SAT 搜索组件的性能是否在按照公式编写顺序的扰动下稳定。
【讨论】：
-
感谢 Nikolaj 的回答。有一件事是肯定的，对于 LIA，我们无法获得随机模型。但是对于位向量，相位选择是如何工作的，每次我们使用不同的随机种子执行时，我们能否得到不同的模型。还有Z3可以接受的随机种子值的范围是多少。