如何从 Microsoft Z3 中获取随机结果？答案

【问题标题】：How to get random results from Microsoft Z3?如何从 Microsoft Z3 中获取随机结果？
【发布时间】：2016-02-12 00:17:36
【问题描述】：

在 Microsoft Z3 中，当我们尝试求解一个公式时，当有两个或多个可满足的解决方案时，Z3 总是以相同的顺序返回结果。

是否可以从 Z3 中得到随机结果，这样对于相同的输入，在不同的执行中会产生不同的输出序列。

请注意，我使用的是 C 或 C# API。我没有使用 smt2lib 使用 Z3。所以如果你能给我一个可以添加随机化的C或C# API函数示例，那会更有用。

【问题讨论】：

听起来你需要设置种子。

标签： z3

【解决方案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)

取自here。

【讨论】：

这是什么语言？看起来方案-y
是smt2，Z3的正常输入，没有任何API。看看这个rise4fun.com/Z3。
我使用 C API 代码尝试了上述参数 ... cfg = Z3_mk_config(); Z3_set_param_value（cfg，“模型”，“真”）； Z3_set_param_value(cfg, "TIMEOUT", TIME_OUT); Z3_set_param_value(cfg, "SMT.ARITH.RANDOM_INITIAL_VALUE", "true"); Z3_set_param_value(cfg, "RANDOM_SEED", "1");求解器 = Z3_mk_context(cfg); ......不幸的是我无法让它工作。当我运行代码时，我收到这样的警告......警告：未知参数'smt.arith.random_initial_value'警告：未知参数'random_seed'知道我做错了什么吗？

【解决方案2】：

您可以编写一个 while 循环来查找所有解决方案，如果您希望它们随机，您可以编写一个简单的约束来隐藏（在现实世界中“否定”）它之前获得的解决方案。喜欢：

int numSolution = 0;
while (true)
{
 do something;.....
 BoolExpr[] args = new BoolExpr[];
 args[i] = your solution variable;
 numSolution++;
 if (numSolution == MAX_NUM_SOLUTION)
  {               
    break;
   }                
 slvr.Assert(z3.MkNot(z3.MkAnd(args)));
}

【讨论】：