解决优化问题的一种方法是使用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使用“假设”： 在Z3软/硬约束
关于效率，这种方法是不是最有效的一个为每一个问题域。 在另一方面，它可以在大多数SMT求解器的顶部来实现。 此外，伪布尔求解器（求解0-1整数问题）成功地用于解决优化问题类似的方法。
文章来源: Efficiency of constraint strengthening in SMT solvers
