我正在试验 Z3(使用 python api)，其中我正在为类分配构建调度模型，其中我必须经常使用模(因为它是周期性的)。 Modulo 似乎已经使 z3 减慢了很多，但是如果我尝试在顶部进行一些优化(最小化成本函数，即总和)，那么对于相当小的问题需要相当长的时间。
如果没有优化，它的工作效果还不错(对于较小的问题只需几秒钟)。话虽这么说，我现在有两个问题:
1)模函数的使用有什么技巧吗？我已经将模值分配给函数。或者还有其他方式来表达周期性/环形行为吗？
2)我对寻找最佳解决方案不感兴趣。一个好的，就够了。有没有办法为成本函数设置一些界限。就像，如果知道它的上限和下限吗？任何其他技巧，我可以使用领域知识来快速找到解决方案。 此外，我认为如果我使用超时选项solver.set("timeout"10000)，那么求解器将使用迄今为止最好的解决方案超时。事实似乎并非如此。它只是超时了。
最佳答案
如果没有看到一些代码，就不可能对 mod 函数进行评论。但根据经验，除法是很困难的。您使用的是 Int 值还是位向量？如果您使用无界整数，您可能想尝试位向量，这可能会受益于更好的内部启发式方法。或者尝试Real值，然后进行适当的减少。
关于如何获得“迄今为止最好的”最优值，请参见这个答案:Finding suboptimal solution (best solution so far) with Z3 command line tool and timeout
关于z3 - 使用取模和优化的 z3py 的性能问题，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/51073642/