使用 MAXSMT 进行增量学习答案

【问题标题】：Incremental Learning using MAXSMT使用 MAXSMT 进行增量学习
【发布时间】：2019-12-11 14:52:19
【问题描述】：

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

【问题讨论】：

这在 OptiMathSAT 中通过 API 是可能的，我猜对于 z3 也是一样的。评估最优模型上的每个软子句，然后“使用它”。 - 这是一个相当通用的答案，因此我将其作为评论。你能稍微提炼一下这个问题，以便更好地定义它的范围并理解手头的问题吗？
例如，如果我从一小组软约束开始，检查模型，然后添加另一小组软约束并重复此过程，直到某些停止标准。我的问题是，Is 比同时执行所有软约束更好吗？
您是否在学习以前的软约束一样难？（或其中的一个子集）新的软约束是同一个 MaxSMT 目标的一部分吗？（相同的 ID）
我不知道你的意思是“以前的软约束一样硬”。是的，新的软约束是同一目标的一部分。模型中没有硬性约束。
如果软约束在先前最优解中的值被断言固定，那么它就会变得困难。在您的应用程序中，软约束是完全独立的，还是具有更高权重的新软约束会导致与早期软约束不同的最优分配？

【解决方案1】：

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

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

在早期阶段找到的最优解可能与迭代过程后期的最优解远。

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

我看到两种可能的情况：

其中一个正在使用基于内核的 MaxSMT 引擎。在这种情况下，探索具有越来越复杂程度的问题的公式可能有助于识别原始问题的易处理子集。但是，请注意，涉及在先前迭代中学习的软约束的引理在以后的阶段可能没有用（实际上，OMT 求解器将丢弃所有这些子句并在必要时重新计算它们）。
其中一个正在使用基于卫星的 MaxSMT 引擎。在这种情况下，除了将搜索集中在 （？可能相关？） 软子句的特定组上之外，我不清楚将问题分成更小的块的好处。 OMT 求解器可以一次获得所有软约束以及硬超时，并且在警报触发时仍然能够产生部分最优解。（涉及成本函数的 T-Lemmas 在增量调用中不会有用，因为成本函数会发生变化。在最好的情况下，OMT 求解器会丢弃它们。在最坏的情况下，这些 T-Lemmas 会保留在环境中并在不改变解决方案的情况下使搜索变得混乱）。

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

【讨论】：