From 47c9c2f42696a1e04577c1a79ac78f4186657818 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 23 Apr 2021 17:57:35 -0700 Subject: [PATCH] Add assumption-based unsat cores. (#6427) This PR adds an assumption-based unsat cores option. If enabled it will disable proof logging in the SAT solver and adds input assertions as assumptions to the SAT solver. When an unsat core is requested we extract the unsat core in terms of the unsat assumption in the SAT solver. Assumption-based unsat cores use the proof infrastructure to map the input assumptions back to the original assertions. --- src/expr/proof_rule.h | 8 ++++ src/prop/minisat/core/Solver.cc | 46 +++++++++++++---------- src/prop/minisat/core/Solver.h | 7 ++++ src/prop/minisat/minisat.cpp | 36 +++++++++++++++++- src/prop/minisat/minisat.h | 10 +++++ src/prop/prop_engine.cpp | 54 +++++++++++++++++++++++++-- src/prop/prop_engine.h | 13 +++++++ src/smt/smt_engine.cpp | 16 ++++++-- src/theory/booleans/proof_checker.cpp | 6 +++ 9 files changed, 169 insertions(+), 27 deletions(-) diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 88e344b8a..432ff1f89 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -247,6 +247,14 @@ enum class PfRule : uint32_t // where F is an equality (= t t') that holds by a form of substitution that // could not be determined by the TrustSubstitutionMap. TRUST_SUBS_MAP, + // ========= SAT Refutation for assumption-based unsat cores + // Children: (P1, ..., Pn) + // Arguments: none + // --------------------- + // Conclusion: false + // Note: P1, ..., Pn correspond to the unsat core determined by the SAT + // solver. + SAT_REFUTATION, //================================================= Boolean rules // ======== Resolution diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 40274489b..19f1bff97 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -484,8 +484,8 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // If a literal is false at 0 level (both sat and user level) we also // ignore it, unless we are tracking the SAT solver's reasoning if (value(ps[i]) == l_False) { - if (!options::unsatCores() && !isProofEnabled() - && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) + if (!options::unsatCores() && !needProof() && level(var(ps[i])) == 0 + && user_level(var(ps[i])) == 0) { continue; } @@ -527,7 +527,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { - if (options::unsatCores() || isProofEnabled()) + if (options::unsatCores() || needProof()) { // Take care of false units here; otherwise, we need to // construct the clause below to give to the proof manager @@ -549,7 +549,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) ProofManager::getSatProof()->finalizeProof( cvc5::Minisat::CRef_Lazy); } - if (isProofEnabled()) + if (needProof()) { d_pfManager->finalizeProof(ps[0], true); } @@ -574,7 +574,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) clauses_persistent.push(cr); attachClause(cr); - if (options::unsatCores() || isProofEnabled()) + if (options::unsatCores() || needProof()) { if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) { @@ -596,7 +596,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) { ProofManager::getSatProof()->finalizeProof(cr); } - if (isProofEnabled()) + if (needProof()) { d_pfManager->finalizeProof(ca[cr], true); } @@ -633,7 +633,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // already been registered, as the ProofCnfStream will not register // them and as they are not the result of propagation will be left // hanging in assumptions accumulator - if (isProofEnabled()) + if (needProof()) { d_pfManager->registerSatLitAssumption(ps[0]); } @@ -654,7 +654,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) ProofManager::getSatProof()->finalizeProof(confl); } } - if (isProofEnabled()) + if (needProof()) { if (ca[confl].size() == 1) { @@ -755,7 +755,7 @@ void Solver::removeClause(CRef cr) { // Solver::reason, if it appears in a resolution chain built lazily we // will be unable to do so after the step below. Thus we eagerly justify // this propagation here. - if (isProofEnabled()) + if (needProof()) { Trace("pf::sat") << "Solver::removeClause: eagerly compute propagation of " << c[0] @@ -1001,7 +1001,7 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) { ProofManager::getSatProof()->startResChain(confl); } - if (isProofEnabled()) + if (needProof()) { d_pfManager->startResChain(ca[confl]); } @@ -1066,7 +1066,7 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) { ProofManager::getSatProof()->resolveOutUnit(q); } - if (isProofEnabled()) + if (needProof()) { d_pfManager->addResolutionStep(q); } @@ -1088,7 +1088,7 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) { ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); } - if (isProofEnabled()) + if (needProof()) { d_pfManager->addResolutionStep(ca[confl], p); } @@ -1129,7 +1129,7 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) { ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); } - if (isProofEnabled()) + if (needProof()) { Debug("newproof::sat") << "Solver::analyze: redundant lit " @@ -1677,7 +1677,7 @@ lbool Solver::search(int nof_conflicts) { ProofManager::getSatProof()->finalizeProof(confl); } - if (isProofEnabled()) + if (needProof()) { if (confl == CRef_Lazy) { @@ -1704,7 +1704,7 @@ lbool Solver::search(int nof_conflicts) { ProofManager::getSatProof()->endResChain(learnt_clause[0]); } - if (isProofEnabled()) + if (needProof()) { d_pfManager->endResChain(learnt_clause[0]); } @@ -1723,7 +1723,7 @@ lbool Solver::search(int nof_conflicts) ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT); ProofManager::getSatProof()->endResChain(id); } - if (isProofEnabled()) + if (needProof()) { d_pfManager->endResChain(ca[cr]); } @@ -2219,7 +2219,7 @@ CRef Solver::updateLemmas() { // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { - Assert(!options::unsatCores() && !isProofEnabled()); + Assert(!options::unsatCores() && !needProof()); conflict = CRef_Lazy; backtrackLevel = 0; Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -2249,7 +2249,7 @@ CRef Solver::updateLemmas() { // Last index in the trail int backtrack_index = trail.size(); - Assert(!options::unsatCores() || isProofEnabled() + Assert(!options::unsatCores() || needProof() || lemmas.size() == (int)lemmas_cnf_assertion.size()); // Attach all the clauses and enqueue all the propagations @@ -2320,7 +2320,7 @@ CRef Solver::updateLemmas() { { ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); } - if (isProofEnabled()) + if (needProof()) { d_pfManager->storeUnitConflict(lemma[0]); } @@ -2334,7 +2334,7 @@ CRef Solver::updateLemmas() { } } - Assert(!options::unsatCores() || isProofEnabled() + Assert(!options::unsatCores() || needProof() || lemmas.size() == (int)lemmas_cnf_assertion.size()); // Clear the lemmas lemmas.clear(); @@ -2400,5 +2400,11 @@ std::shared_ptr Solver::getProof() bool Solver::isProofEnabled() const { return d_pfManager != nullptr; } +bool Solver::needProof() const +{ + return isProofEnabled() + && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS; +} + } // namespace Minisat } // namespace cvc5 diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index cd3f38c9e..a9ee25c11 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -160,6 +160,13 @@ public: /** Is proof enabled? */ bool isProofEnabled() const; + /** + * Checks whether we need a proof. + * + * SAT proofs are not required for assumption-based unsat cores. + */ + bool needProof() const; + // Less than for literals in a lemma struct lemma_lt { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 813292a21..611416dbc 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -32,7 +32,7 @@ namespace prop { //// DPllMinisatSatSolver MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry) - : d_minisat(NULL), d_context(NULL), d_statistics(registry) + : d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry) {} MinisatSatSolver::~MinisatSatSolver() @@ -193,6 +193,40 @@ SatValue MinisatSatSolver::solve() { return result; } +SatValue MinisatSatSolver::solve(const std::vector& assumptions) +{ + setupOptions(); + d_minisat->budgetOff(); + + d_assumptions.clear(); + Minisat::vec assumps; + + for (const SatLiteral& lit : assumptions) + { + Minisat::Lit mlit = toMinisatLit(lit); + assumps.push(mlit); + d_assumptions.emplace(lit); + } + + SatValue result = toSatLiteralValue(d_minisat->solve(assumps)); + d_minisat->clearInterrupt(); + return result; +} + +void MinisatSatSolver::getUnsatAssumptions( + std::vector& unsat_assumptions) +{ + for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i) + { + Minisat::Lit mlit = d_minisat->d_conflict[i]; + SatLiteral lit = ~toSatLiteral(mlit); + if (d_assumptions.find(lit) != d_assumptions.end()) + { + unsat_assumptions.push_back(lit); + } + } +} + bool MinisatSatSolver::ok() const { return d_minisat->okay(); } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 42588080d..74b7ab749 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -58,6 +58,8 @@ class MinisatSatSolver : public CDCLTSatSolverInterface SatValue solve() override; SatValue solve(long unsigned int&) override; + SatValue solve(const std::vector& assumptions) override; + void getUnsatAssumptions(std::vector& unsat_assumptions) override; bool ok() const override; @@ -100,6 +102,14 @@ class MinisatSatSolver : public CDCLTSatSolverInterface /** Context we will be using to synchronize the sat solver */ context::Context* d_context; + /** + * Stores assumptions passed via last solve() call. + * + * It is used in getUnsatAssumptions() to determine which of the literals in + * the final conflict clause are assumptions. + */ + std::unordered_set d_assumptions; + void setupOptions(); class Statistics { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index c4d929d35..23377cb0c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -82,7 +82,8 @@ PropEngine::PropEngine(TheoryEngine* te, d_ppm(nullptr), d_interrupted(false), d_resourceManager(rm), - d_outMgr(outMgr) + d_outMgr(outMgr), + d_assumptions(userContext) { Debug("prop") << "Constructing the PropEngine" << std::endl; @@ -262,7 +263,18 @@ void PropEngine::assertInternal( // Assert as (possibly) removable if (isProofEnabled()) { - d_pfCnfStream->convertAndAssert(node, negated, removable, pg); + if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS + && input) + { + Assert(!negated); + d_pfCnfStream->ensureLiteral(node); + d_assumptions.push_back(node); + } + else + { + d_pfCnfStream->convertAndAssert(node, negated, removable, pg); + } + // if input, register the assertion if (input) { @@ -274,6 +286,7 @@ void PropEngine::assertInternal( d_cnfStream->convertAndAssert(node, removable, negated, input); } } + void PropEngine::assertLemmasInternal( theory::TrustNode trn, const std::vector& ppLemmas, @@ -358,7 +371,20 @@ Result PropEngine::checkSat() { d_interrupted = false; // Check the problem - SatValue result = d_satSolver->solve(); + SatValue result; + if (d_assumptions.size() == 0) + { + result = d_satSolver->solve(); + } + else + { + std::vector assumptions; + for (const Node& node : d_assumptions) + { + assumptions.push_back(d_cnfStream->getLiteral(node)); + } + result = d_satSolver->solve(assumptions); + } if( result == SAT_VALUE_UNKNOWN ) { @@ -628,5 +654,27 @@ std::shared_ptr PropEngine::getProof() bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; } +void PropEngine::getUnsatCore(std::vector& core) +{ + Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS); + std::vector unsat_assumptions; + d_satSolver->getUnsatAssumptions(unsat_assumptions); + for (const SatLiteral& lit : unsat_assumptions) + { + core.push_back(d_cnfStream->getNode(lit)); + } +} + +std::shared_ptr PropEngine::getRefutation() +{ + Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS); + std::vector core; + getUnsatCore(core); + CDProof cdp(d_pnm); + Node fnode = NodeManager::currentNM()->mkConst(false); + cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {}); + return cdp.getProofFor(fnode); +} + } // namespace prop } // namespace cvc5 diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index a0496a525..6812a6549 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -286,6 +286,13 @@ class PropEngine /** Is proof enabled? */ bool isProofEnabled() const; + + /** Retrieve unsat core from SAT solver for assumption-based unsat cores. */ + void getUnsatCore(std::vector& core); + + /** Return the prop engine proof for assumption-based unsat cores. */ + std::shared_ptr getRefutation(); + private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); @@ -370,6 +377,12 @@ class PropEngine /** Reference to the output manager of the smt engine */ OutputManager& d_outMgr; + + /** + * Stores assumptions added via assertInternal() if assumption-based unsat + * cores are enabled. + */ + context::CDList d_assumptions; }; } // namespace prop diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8e8a1e062..09b3d64ab 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1419,9 +1419,19 @@ UnsatCore SmtEngine::getUnsatCoreInternal() // generate with new proofs PropEngine* pe = getPropEngine(); Assert(pe != nullptr); - Assert(pe->getProof() != nullptr); - std::shared_ptr pfn = d_pfManager->getFinalProof( - pe->getProof(), *d_asserts, *d_definedFunctions); + + std::shared_ptr pepf; + if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS) + { + pepf = pe->getRefutation(); + } + else + { + pepf = pe->getProof(); + } + Assert(pepf != nullptr); + std::shared_ptr pfn = + d_pfManager->getFinalProof(pepf, *d_asserts, *d_definedFunctions); std::vector core; d_ucManager->getUnsatCore(pfn, *d_asserts, core); return UnsatCore(core); diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 256ccedce..8b2967fe6 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -74,6 +74,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::CNF_ITE_NEG1, this); pc->registerChecker(PfRule::CNF_ITE_NEG2, this); pc->registerChecker(PfRule::CNF_ITE_NEG3, this); + pc->registerTrustedChecker(PfRule::SAT_REFUTATION, this, 1); } Node BoolProofRuleChecker::checkInternal(PfRule id, @@ -950,6 +951,11 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, args[0], args[0][1].notNode(), args[0][2].notNode()}; return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); } + if (id == PfRule::SAT_REFUTATION) + { + Assert(args.empty()); + return NodeManager::currentNM()->mkConst(false); + } // no rule return Node::null(); } -- 2.30.2