Z3 SAT求解器的随机种子

Question

我正在使用Z3作为SAT solver，因为在CNF/DIMACS格式中编码的难以满足的问题。

会是有意义的随机输入，以增加机会找到一个解决办法：

• 洗牌CNF条款的顺序
• 排序/洗牌输入编号 变量

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

对于Z3，整理/随机不看好我的例子这可能并不能代表。

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

Answer 1

你提出了一个很好的观点：坐标解算器使用的随机种子没有像其他模块一样暴露。我更新了不稳定分支，并更新了坐标解算器的参数。您现在可以将来自命令行的随机种子设置为sat参数的一部分。我希望这有帮助。