调优z3以先尝试较低的数字

Question

我有一个包含几个整数的smt模型，所有这些整数都在0和N之间有界，尽管它们远为可能是N或接近N，但它们几乎总是非常接近于0。也许80%的时候，我需要他们是0,1或2...something那样。

另外，如果一些关键整数的值较低，那么很多整数都可以被忽略，因此在我看来，如果我可以从下限开始调优z3，并且首先尝试较小值的较小模型，我就可以提高执行时间。

我试图理解“z3-p”中的选项，但没有找到一种方法来定制解决策略，从而以这种方式处理我的查询。是否有可能首先调优z3以尝试较低的数字？

Answer 1

在Z3的标准使用方面没有真正的解决方案。我目前正在为Z3开发优化特性，它允许提出查询获得最小/最大值。你可以通过多个目标来完成这个任务。不幸的是，获得真正的优化可能会非常昂贵，因此它不会取代一个简单的启发式旋钮。