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

求解器可以重用在尝试解决先前查询时学到的引理。请记住，在 Z3 中，每当您执行 pop 时，所有引理(自相应的 push 创建)都会被忘记。因此，要实现这一点，您必须避免 push 和 pop 命令，并在需要撤回断言时使用“假设”。在下面的问题中，我描述了如何在Z3中使用“假设”: Soft/Hard constraints in Z3

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