我们可以在 z3 中以增量方式使用 MaxSMT 求解器(优化(的先前解决方案吗？另外，有没有办法在优化器上打印出软断言？
如果您问在技术上是否可以z3或OptiMathSAT增量运行 MaxSMT 问题，答案是肯定的。(使用 API(。
所有具有相同id的软子句- 在执行check-sat的那一刻 -都被视为同一MaxSMT目标的一部分。实质上，OMT 求解器懒惰地评估 MaxSMT 目标的相关软子句集。这适用于z3和OptiMathSAT。
在早期阶段找到的最优解可能与迭代过程后期的最优解相去甚远。
处理 MaxSMT 问题时，OMT 求解器重用的能力跨增量调用的学习子句可能取决于所使用的优化算法。
我看到两种可能的情况：
-
一种是使用基于内核的MaxSMT引擎。在这种情况下，探索复杂程度不断增加的问题的表述可能有助于确定原始问题的可处理子集。但是，请注意，涉及在先前迭代中学习的软约束的引理在以后的阶段可能没有用(实际上，OMT 求解器将丢弃所有这些子句，并在必要时重新计算它们(。
-
一种是使用基于卫星的MaxSMT引擎。在这种情况下，我不清楚将问题拆分为更小的块有什么好处，除了将搜索重点放在特定的(可能相关？(软子句组上。OMT求解器可以同时给出所有软约束以及硬超时，并且在警报触发时仍然能够产生部分最优解。(涉及成本函数的 T 引理在增量调用中没有用，因为成本函数会发生变化。在最佳情况下，OMT 求解器会丢弃它们。在最坏的情况下，这些 T-Lemmas 会保留在环境中，在不改变解决方案的情况下使搜索混乱(。
我承认，预测 OMT 求解器的性能有点困难，因为这两种方法都会引入开销。一方面，我们有增量调用的开销，以及优化过程多次从头开始的事实。另一方面，我们有在更大的软子句集上执行 BCP 的开销。我猜天平转向有利于足够大的软条款集的增量方法。[这将是一个有趣的调查主题，我很想阅读一篇关于它的论文！