Z3 SAT Solver 的随机种子答案

【问题标题】：Random seed for Z3 SAT SolverZ3 SAT Solver 的随机种子
【发布时间】：2014-09-13 10:19:58
【问题描述】：

我使用 Z3 作为SAT solver 来解决以CNF/DIMACS 格式编码的棘手可满足性问题。

将输入随机化以增加找到解决方案的机会是否有意义：

Z3、Cryptominisat 和 Clasp 的较小问题的测量（每个求解器和排序模式运行 100 次测试）：

对于 Z3，排序/随机化对于我的示例来说看起来并不乐观，这可能不具有代表性。

我没有找到影响Z3 SAT 模块的随机种子命令行参数。参数“random_seed”似乎只控制 SMT 求解器。

【问题讨论】：

【解决方案1】：

您提出了一个很好的观点：sat 求解器使用的随机种子与其他模块的暴露方式不同。我已经更新了不稳定的分支，更新了 sat 求解器的参数。您现在可以从命令行将随机种子设置为 sat 参数的一部分。我希望这会有所帮助。

【讨论】：