z3 - 在逻辑 QF_LRA 上使用 z3 时如何获得不同的 unsat 内核

Question

我正在使用 z3 提取不可满足的线性约束集的 unsat 核心。我发现当将“auto-config”选项设置为 false 时，z3 可能会为同一问题提供不同的 unsat 核心。是否存在其他选项可能使 z3 为同一问题提供不同的 unsat 核心？

这是我之前的相关问题:How to get multiple different unsat cores or make the core smaller

Answer 1

没有特定的API来获取不同的unsatisfiable cores，但您可以使用现有的 API 来检索部分或全部最小核心。以下教程

http://rise4fun.com/Z3Py/tutorial/musmss

以简化的方式说明如何同时检索多个核心(或所有)和多个最大满足集(或所有)。