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

Question

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

这是我之前的相关问题：如何获得多个不同的未饱和核心或使核心更小

Answer 1

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

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

以简化的方式说明如何同时检索多个核心（或全部）和多个最大满足集（或全部）。