SMT 求解器中约束强化的效率 [英] Efficiency of constraint strengthening in SMT solvers

问题描述

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

One way to solve optimisation problems is to use an SMT solver to ask whether a (bad) solution exists, then to progressively add tighter cost constraints until the proposition is no longer satisfiable. This approach is discussed in, for example, http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf and http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf.

这种方法有效吗?即，当尝试使用附加约束进行求解时，求解器是否会重新使用先前解决方案中的信息?

Is this approach efficient, though? i.e. will the solver re-use information from previous solutions when attempting to solve with additional constraints?

推荐答案

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

The solver can reuse lemmas learned when trying to solve previous queries. Just keep in mind than in Z3 whenever you execute a pop all lemmas (created since the corresponding push) are forgotten. So, to accomplish that you must avoid push and pop commands and use "assumptions" if you need to retract assertions. In the following question, I describe how to use "assumptions" in Z3: Soft/Hard constraints in Z3

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

Regarding efficiency, this approach is not the most efficient one for every problem domain. On the other hand, it can be implemented on top of most SMT solvers. Moreover, Pseudo-Boolean solvers (solver for 0-1 integer problems) successfully use a similar approach for solving optimization problems.

这篇关于SMT 求解器中约束强化的效率的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！