c++ - 以增量方式使用 z3 但会花费更多时间

Question

我正在尝试使用 Z3 通过推送方法解决具有一个增量约束的问题，例如 (< Z 100)，然后 (< Z 90)，然后 ( < Z 80)。

然而，当我在增量方法中使用 Z3 时，我发现如果我们只直接检查 (< Z 80) 有时会花费更少的时间(比上面两次增量检查后的检查时间 (< Z 80) 更快) ).

• 你能告诉我原因吗？
• 是不是学习到的子句太多导致搜索变慢了？
• 有什么策略可以帮助我解决这个问题吗？

Answer 1

这次你走运了

这次您单独使用 (< Z 80) 很快就解决了这个问题，这可能是因为您的算法在寻找较小的 Z 时找到了一个非常好的最优值，在您使用它的特定情况下。。

这可能纯粹是由于您输入的数据。为了表明直接查找 (< Z 80) 更好——显然情况并非如此——您必须对多种输入数据集进行多次尝试。