使用MAXSMT进行增量学习

Question

我们可以在z3中以增量方式使用MaxSMT求解器的先前解决方案（优化）吗？另外，是否有任何方法可以在优化程序上打印出软断言？

Answer 1

答案为是，如果您询问是否可能[[技术上运行z3或OptiMathSAT 递增出现MaxSMT问题。 （（使用API​​）。

[id相同的所有软子句

-在执行check-sat-的那一刻

]被视为同一MaxSMT目标的一部分。本质上，OMT求解器会懒惰地评估MaxSMT目标的相关软子句集。 z3和OptiMathSAT都适用。

在早期发现的最佳解决方案可能与迭代过程后期的最佳解决方案

相距较远]。

当处理MaxSMT问题时，OMT解算器具有重用能力

incremental调用中的学习子句可能取决于所使用的优化算法。

我看到两种可能的情况：

• [一个正在使用

  基于内核]] MaxSMT引擎。在这种情况下，以复杂程度提高的方式探索问题的表述可能有助于识别原始问题的可处理

  子集。但是，请注意，涉及在先前迭代中学习到的软约束的引理在以后的阶段可能没有用（实际上，OMT解算器将丢弃所有这些子句，并在必要时重新计算它们）。] >
• [一个正在使用

  基于卫星]

MaxSMT引擎。在这种情况下，除了将搜索集中在特定的（？可能相关？）软子句组上之外，我不清楚将问题分成较小的块的好处。可以立即为OMT求解器提供所有软约束以及硬超时，并且在警报触发时，它仍然能够提供部分最优的解决方案。 （涉及成本函数的T-Lemmas在增量调用中将不会有用，因为成本函数会发生变化。在最佳情况下，OMT求解程序会丢弃它们。在最坏的情况下，这些T-Lemmas仍保留在环境中，并且搜索变得混乱，而无需更改解决方案）。我承认，由于两种方法都会带来开销，因此很难预测OMT求解器的性能。一方面，我们有

incremental

调用的开销，而且优化过程会从头开始多次重启。另一方面，我们需要在更大范围的软子句上执行BCP的开销。我猜想，对于足够多的软子句，这种平衡转而倾向于incremental方法。 [[这将是一个有趣的调查主题，我很想读一篇有关它的论文！] >>