Tom*_*rry 4 smt z3
解决优化问题的一种方法是使用SMT求解器来询问是否存在(坏)解决方案,然后逐步添加更严格的成本约束,直到命题不再可满足为止.例如,在http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/中讨论了这种方法.08_isvlsi_optprob.pdf.
这种方法有效吗？也就是说,当尝试用额外的约束来解决时,解算器会重复使用先前解决方案中的信息吗？
Leo*_*ura 5
解算器可以重用尝试解决先前查询时学习的词条.只要你执行一个pop所有的lemmas(自相应的创建以来push)被遗忘,请记住,而不是在Z3 中.因此,要实现这一点,您必须避免push并pop命令并使用"假设",如果您需要撤消断言.在下面的问题中,我描述了如何在Z3中使用"假设":Z3中的 软/硬约束
pop
push
关于效率,这种方法对于每个问题域都不是最有效的方法.另一方面,它可以在大多数SMT求解器之上实现.此外,伪布尔求解器(0-1整数问题的求解器)成功地使用类似的方法来解决优化问题.
归档时间：
13 年，8 月 前
查看次数：
879 次
最近记录：
11 年，9 月 前