迭代 unsat 核心

【问题标题】：Iterating over unsat cores迭代 unsat 核心
【发布时间】：2018-06-16 09:48:54
【问题描述】：

我在Z3 中使用(get-unsat-core) 来提取一组不可满足的约束的unsat-core。然而，一些约束可能有不止一个未饱和核心。在这种情况下，有没有办法迭代 unsat-cores？

【问题讨论】：

【解决方案1】：

是的，但这并不完全直截了当。 Mark Liffiton 及其合作者和变体的 MARCO 算法是提取多核的好方法。 Z3 发行版附带一个简化 MARCO 算法的 Python 示例。 http://theory.stanford.edu/~nikolaj/mod.html#/sec-cores-correction-sets-satisfying-assignments上还描述了其他变种

【讨论】：