From ca9b88f79611caed3e03c64a64b96ec65ea62dfa Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 25 Mar 2022 18:25:04 -0300 Subject: [PATCH] [proofs] [sat] Have SAT solver communicate whether it has optimized the assertion level of a clause (#8399) This way both the SAT proof manager and the Proof Cnf Stream can properly track proofs for clauses added at assertion levels below their original user level. This commit, besides some minor tweaks, adds the hooks in the places where a clause can be created with an optimized level and we need to track: when the explanation of a propagation is requested when a clause/lemma is added when a lemma is added (from the backlog of lemmas added when Minisat was busy) For clauses derived via resolution, this information is computed directly in the SAT proof manager. This commit also reverts a change from #7790 where whether to optimize clauses was computed only once for the SAT solver. This cannot be the case because between different check-sat calls the state can change. Finally, this commit enables proofs for several regressions that were previously incompatible with proofs. Since now proofs are compatible with optimizing the level of clauses during incremental solving, this commit should lead to performance improvements. Fixes cvc5/cvc5-projects#314 --- src/prop/minisat/core/Solver.cc | 170 ++++++++++++------ src/prop/minisat/core/Solver.h | 23 ++- src/prop/proof_post_processor.cpp | 13 +- src/prop/prop_engine.cpp | 3 + src/prop/sat_proof_manager.cpp | 4 +- .../regress/cli/regress0/cores/issue3455.smt2 | 2 +- .../regress/cli/regress0/cores/issue4925.smt2 | 1 - .../cli/regress1/push-pop/fuzz_3_1.smt2 | 2 +- .../cli/regress1/push-pop/fuzz_3_11.smt2 | 2 +- .../cli/regress1/push-pop/fuzz_3_9.smt2 | 2 +- 10 files changed, 145 insertions(+), 77 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 1294b9d33..64d77e97a 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -142,9 +142,6 @@ Solver::Solver(Env& env, d_context(context), assertionLevel(0), d_pfManager(nullptr), - d_assertionLevelOnly( - (options().smt.produceProofs || options().smt.unsatCores) - && options().base.incrementalSolving), d_enable_incremental(enableIncremental), minisat_busy(false) // Parameters (user settable): @@ -256,7 +253,8 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo setDecisionVar(v, dvar); - Trace("minisat") << "new var " << v << std::endl; + Trace("minisat") << "new var " << v << " with assertion level " + << assertionLevel << std::endl; // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks if (preRegister) @@ -342,15 +340,15 @@ CRef Solver::reason(Var x) { // Compute the assertion level for this clause int explLevel = 0; - if (d_assertionLevelOnly) + if (assertionLevelOnly()) { explLevel = assertionLevel; } else { - int i, j; + int i, j, size; Lit prev = lit_Undef; - for (i = 0, j = 0; i < explanation.size(); ++i) + for (i = 0, j = 0, size = explanation.size(); i < size; ++i) { // This clause is valid theory propagation, so its level is the level of // the top literal @@ -383,13 +381,6 @@ CRef Solver::reason(Var x) { } explanation.shrink(i - j); - Trace("pf::sat") << "Solver::reason: explanation = "; - for (int k = 0; k < explanation.size(); ++k) - { - Trace("pf::sat") << explanation[k] << " "; - } - Trace("pf::sat") << std::endl; - // We need an explanation clause so we add a fake literal if (j == 1) { @@ -398,6 +389,14 @@ CRef Solver::reason(Var x) { } } + Trace("pf::sat") << "..adding in lvl " << explLevel + << " (assertion lvl: " << assertionLevel << ")\n"; + if (needProof() && explLevel < assertionLevel) + { + Trace("pf::sat") << "..user level is " << userContext()->getLevel() << "\n"; + Assert(userContext()->getLevel() == (assertionLevel + 1)); + d_proxy->notifyCurrPropagationInsertedAtLevel(explLevel); + } // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); vardata[x] = VarData( @@ -417,13 +416,13 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) Lit p; int i, j; // Which user-level to assert this clause at - int clauseLevel = (removable && !d_assertionLevelOnly) ? 0 : assertionLevel; + int clauseLevel = (removable && !assertionLevelOnly()) ? 0 : assertionLevel; // Check the clause for tautologies and similar int falseLiteralsCount = 0; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { // Update the level - clauseLevel = d_assertionLevelOnly + clauseLevel = assertionLevelOnly() ? assertionLevel : std::max(clauseLevel, intro_level(var(ps[i]))); // Tautologies are ignored @@ -465,12 +464,15 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // If we are in solve_ or propagate if (minisat_busy) { - Trace("pf::sat") << "Add clause adding a new lemma: "; - for (int k = 0; k < ps.size(); ++k) { - Trace("pf::sat") << ps[k] << " "; + if (TraceIsOn("pf::sat")) + { + Trace("pf::sat") << "Add clause adding a new lemma: "; + for (int k = 0, size = ps.size(); k < size; ++k) + { + Trace("pf::sat") << ps[k] << " "; + } + Trace("pf::sat") << std::endl; } - Trace("pf::sat") << std::endl; - lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); @@ -509,7 +511,22 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) cr = ca.alloc(clauseLevel, ps, false); clauses_persistent.push(cr); attachClause(cr); - + if (needProof() && clauseLevel < assertionLevel) + { + if (TraceIsOn("pf::sat")) + { + Trace("pf::sat") << "addClause_: "; + for (int k = 0, size = ps.size(); k < size; ++k) + { + Trace("pf::sat") << ps[k] << " "; + } + Trace("pf::sat") << " clause/assert levels " << clauseLevel << " / " + << assertionLevel << "\n"; + } + SatClause satClause; + MinisatSatSolver::toSatClause(ca[cr], satClause); + d_proxy->notifyClauseInsertedAtLevel(satClause, clauseLevel); + } if (options().smt.unsatCores || needProof()) { if (ps.size() == falseLiteralsCount) @@ -524,45 +541,48 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) } // Check if it propagates - if (ps.size() == falseLiteralsCount + 1) { - if(assigns[var(ps[0])] == l_Undef) { - Assert(assigns[var(ps[0])] != l_False); - uncheckedEnqueue(ps[0], cr); - Trace("cores") << "i'm registering a unit clause, maybe input" + if (ps.size() == falseLiteralsCount + 1 && assigns[var(ps[0])] == l_Undef) + { + Assert(assigns[var(ps[0])] != l_False); + uncheckedEnqueue(ps[0], cr); + Trace("pf::sat") << "Registering a unit clause " << ps[0] + << ", maybe input, with assigned var value " + << (assigns[var(ps[0])] == l_True + ? "true" + : (assigns[var(ps[0])] == l_False ? "false" + : "undef")) + << ", user_level(" << user_level(var(ps[0])) << ")" << std::endl; - if (ps.size() == 1) + if (ps.size() == 1) + { + // We need to do this so that the closedness check, if being done, + // goes through when we have unit assumptions whose literal has + // 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 (needProof()) { - // We need to do this so that the closedness check, if being done, - // goes through when we have unit assumptions whose literal has - // 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 (needProof()) + d_pfManager->registerSatLitAssumption(ps[0]); + } + } + CRef confl = propagate(CHECK_WITHOUT_THEORY); + if (!(ok = (confl == CRef_Undef))) + { + if (needProof()) + { + if (ca[confl].size() == 1) { - d_pfManager->registerSatLitAssumption(ps[0]); + d_pfManager->finalizeProof(ca[confl][0]); } - } - CRef confl = propagate(CHECK_WITHOUT_THEORY); - if(! (ok = (confl == CRef_Undef)) ) { - if (needProof()) + else { - if (ca[confl].size() == 1) - { - d_pfManager->finalizeProof(ca[confl][0]); - } - else - { - d_pfManager->finalizeProof(ca[confl]); - } + d_pfManager->finalizeProof(ca[confl]); } } - return ok; - } else { - return ok; } + return ok; } } - return true; } @@ -1140,6 +1160,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) Trace("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() + << ", assertion level is " << assertionLevel << ", reason is " << from << ", "; if (from == CRef_Lazy) { @@ -1443,7 +1464,11 @@ void Solver::removeClausesAboveLevel(vec& cs, int level) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (c.level() > level) { - Assert(!locked(c)); + SatClause satClause; + vec clauseLits; + MinisatSatSolver::toSatClause(c, satClause); + MinisatSatSolver::toMinisatClause(satClause, clauseLits); + Assert(!locked(c)) << "Locked " << clauseLits; removeClause(cs[i]); } else { cs[j++] = cs[i]; @@ -1559,7 +1584,7 @@ lbool Solver::search(int nof_conflicts) } else { - CRef cr = ca.alloc(d_assertionLevelOnly ? assertionLevel : max_level, + CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level, learnt_clause, true); clauses_removable.push(cr); @@ -1569,6 +1594,12 @@ lbool Solver::search(int nof_conflicts) if (needProof()) { d_pfManager->endResChain(ca[cr]); + if (TraceIsOn("pf::sat") && ca[cr].level() < assertionLevel) + { + Trace("pf::sat") + << "learnt_clause: " << ca[cr] << " clause/assert levels " + << ca[cr].level() << " / " << assertionLevel << "\n"; + } } } @@ -1961,7 +1992,12 @@ void Solver::pop() Assert(d_enable_incremental); Assert(decisionLevel() == 0); - + // Notify sat proof manager that we have popped and now potentially we need to + // retrieve the proofs for the clauses inserted into optimized levels + if (needProof()) + { + d_pfManager->notifyPop(); + } // Pop the trail below the user level --assertionLevel; Trace("minisat") << "in user pop, decreasing assertion level to " @@ -2078,7 +2114,7 @@ CRef Solver::updateLemmas() { if (lemma.size() > 1) { // If the lemmas is removable, we can compute its level by the level int clauseLevel = assertionLevel; - if (removable && !d_assertionLevelOnly) + if (removable && !assertionLevelOnly()) { clauseLevel = 0; for (int k = 0; k < lemma.size(); ++k) @@ -2088,6 +2124,24 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); + // notify cnf stream that this clause's proof must be saved to resist + // context-popping + if (needProof() && clauseLevel < assertionLevel) + { + if (TraceIsOn("pf::sat")) + { + Trace("pf::sat") << "updateLemmas: "; + for (int k = 0, size = lemma.size(); k < size; ++k) + { + Trace("pf::sat") << lemma[k] << " "; + } + Trace("pf::sat") << " clause/assert levels " << clauseLevel << " / " + << assertionLevel << "\n"; + } + SatClause satClause; + MinisatSatSolver::toSatClause(ca[lemma_ref], satClause); + d_proxy->notifyClauseInsertedAtLevel(satClause, clauseLevel); + } if (removable) { clauses_removable.push(lemma_ref); } else { @@ -2184,5 +2238,11 @@ bool Solver::needProof() const && options().smt.proofMode != options::ProofMode::PP_ONLY; } +bool Solver::assertionLevelOnly() const +{ + return options().smt.unsatCores && !needProof() + && options().base.incrementalSolving; +} + } // namespace Minisat } // namespace cvc5 diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 2f19c6e16..2f027788e 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -74,7 +74,7 @@ class Solver : protected EnvObj /** The pointer to the proxy that provides interfaces to the SMT engine */ cvc5::prop::TheoryProxy* d_proxy; - /** The context from the SMT solver */ + /** The contexts from the SMT solver */ cvc5::context::Context* d_context; /** The current assertion level (user) */ @@ -94,17 +94,6 @@ class Solver : protected EnvObj int getAssertionLevel() const { return assertionLevel; } protected: - /* - * Returns true if the solver should add all clauses at the current assertion - * level. - * - * FIXME: This is a workaround. Currently, our resolution proofs do not - * handle clauses with a lower-than-assertion-level correctly because the - * resolution proofs get removed when popping the context but the SAT solver - * keeps using them. - */ - const bool d_assertionLevelOnly; - /** Do we allow incremental solving */ bool d_enable_incremental; @@ -176,6 +165,16 @@ public: */ bool needProof() const; + /* + * Returns true if the solver should add all clauses at the current assertion + * level. + * + * FIXME (cvc5-projects/issues/503): This is a workaround. While proofs are now + * compatible with the assertion level optimization, it has to be seen for + * non-sat-proofs-based unsat cores. + */ + bool assertionLevelOnly() const; + // Less than for literals in a lemma struct lemma_lt { diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp index b85265427..890ad662c 100644 --- a/src/prop/proof_post_processor.cpp +++ b/src/prop/proof_post_processor.cpp @@ -34,6 +34,11 @@ bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr pn, { bool result = pn->getRule() == PfRule::ASSUME && d_proofCnfStream->hasProofFor(pn->getResult()); + if (TraceIsOn("prop-proof-pp") && !result && pn->getRule() == PfRule::ASSUME) + { + Trace("prop-proof-pp") << "- Ignoring no-proof assumption " + << pn->getResult() << "\n"; + } // check if should continue traversing if (d_proofCnfStream->isBlocked(pn)) { @@ -50,8 +55,9 @@ bool ProofPostprocessCallback::update(Node res, CDProof* cdp, bool& continueUpdate) { - Trace("prop-proof-pp-debug") - << "- Post process " << id << " " << children << " / " << args << "\n"; + Trace("prop-proof-pp") << "- Post process " << id << " " << res << " : " + << children << " / " << args << "\n" + << push; Assert(id == PfRule::ASSUME); // we cache based on the assumption node, not the proof node, since there // may be multiple occurrences of the same node. @@ -61,7 +67,7 @@ bool ProofPostprocessCallback::update(Node res, d_assumpToProof.find(f); if (it != d_assumpToProof.end()) { - Trace("prop-proof-pp-debug") << "...already computed" << std::endl; + Trace("prop-proof-pp") << "...already computed" << std::endl; pfn = it->second; } else @@ -77,6 +83,7 @@ bool ProofPostprocessCallback::update(Node res, } d_assumpToProof[f] = pfn; } + Trace("prop-proof-pp") << pop; // connect the proof cdp->addProof(pfn); // do not recursively process the result diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 678ef2107..12116344c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -652,6 +652,9 @@ std::shared_ptr PropEngine::getProof() { return nullptr; } + Trace("sat-proof") << "PropEngine::getProof: getting proof with cnfStream's " + "lazycdproof cxt lvl " + << userContext()->getLevel() << "\n"; return d_ppm->getProof(); } diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index d31b1273a..63967a23f 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -149,9 +149,9 @@ void SatProofManager::endResChain(const Minisat::Clause& clause) } Node conclusion = getClauseNode(clause); int clauseLevel = clause.level() + 1; - if (clauseLevel < userContext()->getLevel()) + if (clauseLevel < userContext()->getLevel() + && !d_resChains.hasGenerator(conclusion)) { - Assert(!d_optResLevels.count(conclusion)); d_optResLevels[conclusion] = clauseLevel; Trace("sat-proof") << "SatProofManager::endResChain: ..clause's lvl " << clause.level() + 1 << " below curr user level " diff --git a/test/regress/cli/regress0/cores/issue3455.smt2 b/test/regress/cli/regress0/cores/issue3455.smt2 index 7050e8c7d..b922bb7fa 100644 --- a/test/regress/cli/regress0/cores/issue3455.smt2 +++ b/test/regress/cli/regress0/cores/issue3455.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -q --incremental --no-check-proofs +; COMMAND-LINE: -q --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat diff --git a/test/regress/cli/regress0/cores/issue4925.smt2 b/test/regress/cli/regress0/cores/issue4925.smt2 index 62428b565..f1002ed75 100644 --- a/test/regress/cli/regress0/cores/issue4925.smt2 +++ b/test/regress/cli/regress0/cores/issue4925.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-proofs ; EXPECT: sat ; EXPECT: unsat ; EXPECT: unsat diff --git a/test/regress/cli/regress1/push-pop/fuzz_3_1.smt2 b/test/regress/cli/regress1/push-pop/fuzz_3_1.smt2 index 1f3488b16..bf2d2a8c3 100644 --- a/test/regress/cli/regress1/push-pop/fuzz_3_1.smt2 +++ b/test/regress/cli/regress1/push-pop/fuzz_3_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-produce-proofs +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat diff --git a/test/regress/cli/regress1/push-pop/fuzz_3_11.smt2 b/test/regress/cli/regress1/push-pop/fuzz_3_11.smt2 index 4e3ebb625..81fe3b046 100644 --- a/test/regress/cli/regress1/push-pop/fuzz_3_11.smt2 +++ b/test/regress/cli/regress1/push-pop/fuzz_3_11.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-produce-proofs +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat diff --git a/test/regress/cli/regress1/push-pop/fuzz_3_9.smt2 b/test/regress/cli/regress1/push-pop/fuzz_3_9.smt2 index f7d2ae60e..96aaf9f51 100644 --- a/test/regress/cli/regress1/push-pop/fuzz_3_9.smt2 +++ b/test/regress/cli/regress1/push-pop/fuzz_3_9.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-produce-proofs +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat -- 2.30.2