CVC4: как получить правильное ядро без присмотра?
Используя этот код:
#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 )
Я предположил, что параметр inUnsatCore из SmtEngine.assertFormula будет так или иначе направлять утверждения. Но это не так.
Как правильно утверждать формулы и запрашивать ненасыщенное ядро, если не так, как показано выше?
Использование версии cvc4 с тегом 1.5 от github.
Решение
qr rs nqs само по себе не является ненасыщенным ядром (оно тривиально выполнимо, если установить для всех трех переменных значение true). Похоже, вы пытаетесь достичь чего-то похожего на именованные утверждения в SMT-LIB v2. Когда используешь (get-unsat-core) в SMT-LIB v2 печатаются только именованные утверждения в ядре 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).
inUnsatCore не имеет никакого эффекта, когда produce-unsat-cores является true насколько я могу судить. Я добавил пункт для улучшения этой документации в наш список обслуживания.
Другие решения
Других решений пока нет …