如何在Z3中表达软约束和硬约束？我从API中了解到可能有假设(软约束),但在使用命令行工具时我无法表达这一点.我用z3/smt2/si来调用它
我在UFBV查询上运行Z3.目前查询包含2个调用check-sat.如果放在Z3 push 1之后check-sat在30秒内解决查询.如果不放任何东西push 1- Z3在200秒内解决它.有趣.任何具体原因还是巧合？
解决优化问题的一种方法是使用SMT求解器来询问是否存在(坏)解决方案,然后逐步添加更严格的成本约束,直到命题不再可满足为止.例如,在http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/中讨论了这种方法.08_isvlsi_optprob.pdf.
这种方法有效吗？也就是说,当尝试用额外的约束来解决时,解算器会重复使用先前解决方案中的信息吗？