Z3 SAT求解器的隨機種子

Question

我正在使用Z3作爲SAT solver，因爲在CNF/DIMACS格式中編碼的難以滿足的問題。

會是有意義的隨機輸入，以增加機會找到一個解決辦法：

• 洗牌CNF條款的順序
• 排序/洗牌輸入編號 變量

針對較小問題的測量（每個求解器和分類模式的100次測試運行）Z3，Cryptominisat和Clasp：

對於Z3，整理/隨機不看好我的例子這可能並不能代表。

我還沒有找到影響SAT模塊Z3的隨機種子命令行參數。 參數「random_seed」似乎只能控制SMT解算器。

Answer 1

你提出了一個很好的觀點：座標解算器使用的隨機種子沒有像其他模塊一樣暴露。我更新了不穩定分支，並更新了座標解算器的參數。您現在可以將來自命令行的隨機種子設置爲sat參數的一部分。我希望這有幫助。