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 中使用“假设”： Soft/Hard constraints in Z3

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