check-sat 返回未知时对部分模型的保证

Posted 2023-03-28

【中文标题】check-sat 返回未知时对部分模型的保证

【英文标题】：Guarantees about partial model when check-sat returns unknown

【发布时间】：2018-09-15 21:44:28

【问题描述】：

我对 z3 的部分模型有疑问。 我在网上查找了有关它们的信息，但遗憾的是我没有找到太多信息，除了有时在验证失败时可以检索到它们。

如果(check-sat) 返回unknown，部分模型的保证是什么（如果可以检索）？是否保证始终完好无损？

我对与量词相关的不完整情况特别感兴趣，但我怀疑这会有所不同。

提前谢谢你。

【参考方案1】：

由于 - 据我所知 - 没有官方保证，我希望（不令人满意的）答案是：部分模型在很大程度上取决于具体问题和“手段”（预处理步骤、启发式、求解器、策略, 随机种子, 超时, ...) Z3 用于解决问题。

因此，我希望只有基本上了解整个代码库和您的具体问题的人才能给您一个令人满意的答案......如果有的话。