是否有增量 Max-SMT 求解器？

Question

我正在处理一个问题，即位向量数组编码不同时间尺度的不同时间序列数据之间的逻辑关系，以生成具有任意属性的合成数据。我发现我最好通过增量地为每个时间步提供约束而不是让 Z3 一次分配所有约束，但这仍然非常耗时。我想知道是否可以使用 Max-SMT 来处理这个问题，方法是明确说明以前的时间序列分配应该尽可能保持相同，此外，如果某个时间阈值是，则返回最接近的可能模型达到，但没有找到确切的解决方案。但是，我不认为 Z3 提供了增量和 Max-SMT 的组合。另外，我认为不可能让 Z3 在求解器模式下提供“最接近的模型”。

有人知道提供这些功能的工具吗？

谢谢！

Answer 1

z3 的优化器确实不是增量的。它也不支持任何“尽可能接近”的概念。 （虽然您可以查询一些内部值以收集范围，但它们甚至不能保证满足您的约束。）

我会向@PatrickTrenton 了解确切的功能，但您可能需要查看 OptiMathSAT：http://optimathsat.disi.unitn.it/。引用他们的网页：

OptiMathSAT 允许在 线性算术目标函数，它支持广泛的 理论（包括例如相等和未解释的函数，线性 算术、位向量、数组）。