我正在处理位向量数组的问题，该数组在不同时间尺度上对不同时间序列数据之间的逻辑关系进行编码，以生成具有任意属性的合成数据。我发现我最好通过逐步为每个时间步提供约束，而不是让Z3一次全部分配约束来做到最好，但这仍然很耗时。我想知道是否有可能使用Max-SMT来处理此问题，即明确指出以前的时间序列分配应尽可能保持相同，此外，如果确定某个时间阈值，则返回最可能的模型已到达，但找不到确切的解决方案。但是，我不认为Z3提供增量和Max-SMT的组合。另外，我认为Z3不可能在求解器模式下提供“可能的最接近模型”。
有人知道提供这些功能的工具吗？
谢谢！
确实，z3的优化器不是增量的。它也不支持“足够接近”的任何概念。 （尽管您可以查询一些内部值以收集范围，但不能保证它们甚至满足您的约束。）
我将使用@PatrickTrenton以获得确切的功能，但您可能需要研究OptiMathSAT：http://optimathsat.disi.unitn.it/。从他们的网页上报价：
OptiMathSAT允许在线性算术目标函数，它支持广泛的理论（包括等式和未解释的函数，线性算术，位向量，数组）。