解决优化问题的一种方法是使用SMT求解器来询问是否存在（坏）解决方案，然后逐步添加更严格的成本约束，直到命题不再可满足为止 . 例如，http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf讨论了这种方法 .
这种方法有效吗？也就是说，当试图用额外的约束解决时，解算器会重复使用先前解决方案中的信息吗？
解决优化问题的一种方法是使用SMT求解器来询问是否存在（坏）解决方案，然后逐步添加更严格的成本约束，直到命题不再可满足为止 . 例如，http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf讨论了这种方法 .
这种方法有效吗？也就是说，当试图用额外的约束解决时，解算器会重复使用先前解决方案中的信息吗？
1 回答
解算器可以重用尝试解决先前查询时学习的词条 . 只要你执行一个
pop所有的lemmas（自相应的push以来创建）被遗忘，请记住比Z3中的情况 . 因此，要实现这一点，您必须避免使用push和pop命令，并在需要撤消断言时使用"assumptions" . 在下面的问题中，我描述了如何在Z3中使用"assumptions"：Soft/Hard constraints in Z3关于效率，这种方法对于每个问题域都不是最有效的方法 . 另一方面，它可以在大多数SMT求解器之上实现 . 此外，伪布尔求解器（0-1整数问题的求解器）成功地使用类似的方法来解决优化问题 .