z3 - Z3 SAT Solver 的随机种子

Question

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

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

• 打乱 CNF 子句的顺序
• 对输入变量的编号进行排序/打乱

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

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

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

Answer 1

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