CVC4：如何获得合适的未饱和核心？

Question

使用此代码：

#include <cvc4/cvc4.h>

using namespace std;
using namespace CVC4;

int main() {
  ExprManager em;
  SmtEngine smt(&em);
  smt.setOption("produce-unsat-cores","true");

  Type boolean_type = em.booleanType();

  Expr p = em.mkVar("p", boolean_type);
  Expr q = em.mkVar("q", boolean_type);
  Expr r = em.mkVar("r", boolean_type);
  Expr s = em.mkVar("s", boolean_type);
  Expr t = em.mkVar("t", boolean_type);

  Expr pq = em.mkVar("pq", boolean_type);
  Expr qr = em.mkVar("qr", boolean_type);
  Expr rs = em.mkVar("rs", boolean_type);
  Expr st = em.mkVar("st", boolean_type);
  Expr nqs = em.mkVar("nqs", boolean_type);

  smt.assertFormula(em.mkExpr(kind::IMPLIES, pq, em.mkExpr(kind::IMPLIES, p, q)),false);
  smt.assertFormula(em.mkExpr(kind::IMPLIES, qr, em.mkExpr(kind::IMPLIES, q, r)),false);
  smt.assertFormula(em.mkExpr(kind::IMPLIES, rs, em.mkExpr(kind::IMPLIES, r, s)),false);
  smt.assertFormula(em.mkExpr(kind::IMPLIES, st, em.mkExpr(kind::IMPLIES, s, t)),false);
  smt.assertFormula(em.mkExpr(kind::IMPLIES, nqs, em.mkExpr(kind::NOT, em.mkExpr(kind::IMPLIES, q, s))),false);

  smt.assertFormula(pq,true);
  smt.assertFormula(qr,true);
  smt.assertFormula(rs,true);
  smt.assertFormula(st,true);
  smt.assertFormula(nqs,true);

  Result result = smt.checkSat();
  enum Result::Sat sat_result = result.isSat();
  if (sat_result == Result::SAT) {
    printf("sat\n");
  } else if (sat_result == Result::UNSAT) {
    printf("unsat (");
    UnsatCore unsat_core = smt.getUnsatCore();
    std::vector<Expr>::const_iterator it = unsat_core.begin();
    std::vector<Expr>::const_iterator it_end = unsat_core.end();
    for (; it != it_end; ++it) {
      printf("%s ", Expr(*it).toString().c_str());
    }
    printf(")\n");
  } else {
    printf("unknown\n");
  }

  return 0;
}

我收到以下回复：

unsat (qr rs nqs qr => (q => r) rs => (r => s) nqs => NOT(q => s) )

但我希望是这样的：

unsat (qr rs nqs )

我假设SmtEngine.assertFormula 的参数inUnsatCore 会以某种方式引导断言。但事实并非如此。

如果不是如上所示，断言公式和要求未饱和核心的正确方法是什么？

使用来自 github 的带有标签 1.5 的 cvc4 版本。

Answer 1

qr rs nqs 本身并不是一个 unsat 核心（通过将所有三个变量都设置为 true 可以轻松满足）。您似乎正在尝试实现类似于 SMT-LIB v2 中的命名断言的东西。在 SMT-LIB v2 中使用 (get-unsat-core) 时，仅打印 unsat 核心中的命名断言。

你的例子可以翻译如下：

(set-option :produce-unsat-cores true)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Bool)
(declare-fun pq () Bool)
(declare-fun qr () Bool)
(declare-fun rs () Bool)
(declare-fun st () Bool)
(declare-fun nqs () Bool)
(assert (implies pq (implies p q)))
(assert (implies qr (implies q r)))
(assert (implies rs (implies r s)))
(assert (implies st (implies s t)))
(assert (implies nqs (not (implies q s))))
(assert (! pq :named _pq))
(assert (! qr :named _qr))
(assert (! rs :named _rs))
(assert (! st :named _st))
(assert (! nqs :named _nqs))
(check-sat)
(get-unsat-core)

CVC4 在这个例子中的输出：

unsat
(
_nqs
_rs
_qr
)

这在内部工作的方式是 CVC4 跟踪命名的断言，并且仅在跳过未命名的断言时将其打印出来。如果 unsat 核心的成员属于您的相关断言集（pq、qr、rs、st、nqs），您可以在代码中执行相同的操作。

据我所知，produce-unsat-cores 是 true 时，inUnsatCore 无效。我已将用于改进该文档的项目添加到我们的维护列表中。