使用Z3的ALLSAT

我使用Z3作爲一個黑匣子找到一些真實世界的所有可能的組合與C＃這樣的代碼對象，但現在我遇到了一個更大的問題，那就是8.5E + 64個可能的組合，沒有限制。使用Z3的ALLSAT

我開始約6000個約束。

我觀察到的情況是，檢查操作在開始時的時間不到0.02秒，並且慢慢地建立起來。 100000找到解決方案後，它每回合已經1秒，130000回合後，我測量2秒。

有沒有簡單的方法來提高性能？

2017-07-12 ChristianJ

爲什麼不使用MathSAT呢？它有一個比天真阻塞條款更好的All-SAT。 – qsp

求解器在每個約束條件下花費的時間越來越長並不是不合理的。但爲了確保它不是C＃部分中的某種內存泄漏，應該檢查while循環所用的時間確實在Check部分中，而不是在invert/assert部分中。如果您確定z3是責任方，則可能在https://github.com/Z3Prover/z3/issues處提交它可能會向開發人員尋求更好的答案。

來源

2017-07-15 05:41:37

感謝您的回答。時間只通過檢查部分，並沒有內存泄漏 – ChristianJ

我不會將它作爲一個問題提交，因爲我認爲我是缺少某些東西的人。 – ChristianJ

回答

相關問題