与UNSAT核心相似的卫星核心

Question

我知道有可能在Z3获得一个UNSAT核心。但它也有可能得到什么东西，你可以称之为SAT-核心？这意味着，如果我们有一个可满足的实例，那么所有变量都有一个模型。Sat-Core将是子模型的最小大小，它的属性是所有其他变量都通过传播约束来接收它们的值。

Answer 1

我不认为这是一个定义良好的概念；考虑一下有两个变量a和b，其中有约束的a = Not(b)，您可以同时断言a和b。不管你选择哪一种，另一种是由常量传播决定的；但是没有理由选择其中一种而不是另一种。

当然，你可以找一个“任意”的这样的集合，但这使得它不太有用；同样，最小性，就像在未设置核心的情况下，将很难保证在传统的SAT/SMT解决程序。

然而，consequences在z3中有一个相关的概念。详情请参见https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-consequences。这个想法是你想要找出什么文字在任何模型中都是正确的。这是一个有趣的问题，因为它向您展示了在您输入的约束下，变量空间的哪一部分不再相关，因为它总是被迫的。这些文本也称为骨干文本，有关详细信息，请参阅https://sat.inesc-id.pt/~mikolas/bb-aicom-preprint.pdf。