0

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

4

1 回答 1

2

答案是肯定的，如果您询问是否在技术上可以运行z3或OptiMathSAT 增量运行MaxSMT 问题。（使用 API）。

所有具有相同的软子句——id 在一个人执行 a 的那一刻check-sat——被认为是同一个 MaxSMT 目标的一部分。本质上，OMT 求解器懒惰地评估 MaxSMT 目标的相关软子句集。这适用于z3和OptiMathSAT。

早期找到的最优解可能与迭代过程后期的最优解相距甚远。

在处理 MaxSMT 问题时，OMT 求解器在增量调用中重用学习子句的能力可能取决于正在使用的优化算法。

我看到两种可能的情况：

  • 一种是使用基于内核的MaxSMT 引擎。在这种情况下，探索具有越来越复杂程度的问题的公式可能有助于识别原始问题的易处理子集。但是，请注意，涉及在先前迭代中学习的软约束的引理在后期可能没有用（实际上，OMT 求解器将丢弃所有这些子句并在必要时重新计算它们）。

  • 一种是使用基于卫星的MaxSMT 引擎。在这种情况下，除了将搜索集中在（？可能相关的？）软子句的特定组上之外，我不清楚将问题分成更小的块的好处。OMT 求解器可以一次获得所有软约束以及硬超时，并且在警报触发时它仍然能够产生部分最优解。（涉及成本函数的 T-Lemmas 在增量调用中不会有用，因为成本函数会发生变化。在最好的情况下，OMT 求解器会丢弃它们。在最坏的情况下，这些 T-Lemmas 会保留在环境中并弄乱搜索而不改变解决方案）。

    我承认，由于两种方法都引入了开销，因此很难预测 OMT 求解器的性能。一方面，我们有增量调用的开销以及优化过程从头开始多次重新启动的事实。另一方面，我们有在更大的软子句集上执行 BCP 的开销。我猜想对于足够大的软子句集来说，平衡转向有利于增量方法。[这将是一个有趣的调查主题，我很想读一篇关于它的论文！]

于 2019-12-11T16:30:37.577 回答