z3 - SMT求解器中约束加强的效率

Question

解决优化问题的一种方法是使用 SMT 求解器来询问是否存在（坏）解决方案，然后逐步添加更严格的成本约束，直到该命题不再可满足。例如，http: //www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/讨论了这种方法08_isvlsi_optprob.pdf。

但是，这种方法有效吗？即，求解器在尝试使用附加约束求解时是否会重用来自先前解决方案的信息？

Answer 1

求解器可以重用在尝试解决以前的查询时学到的引理。请记住，每当您执行pop所有引理（自相应push的 . 因此，要实现这一点，如果您需要撤回断言，您必须避免push和命令并使用“假设”。pop在下面的问题中，我描述了如何在 Z3 中使用“假设”： Z3 中的 软/硬约束

关于效率，这种方法并不是对每个问题域最有效的方法。另一方面，它可以在大多数 SMT 求解器之上实现。此外，伪布尔求解器（0-1 整数问题的求解器）成功地使用了类似的方法来解决优化问题。