From 240dad8784b4c9743ff6153a18daa7ae388f03e3 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 14 Dec 2020 20:39:58 -0300 Subject: [PATCH] [proof-new] Making the CDCL(T) Minisat proof producing (#5669) This closely follows the old proof code in terms of where Minisat is hooked to the SatProofManager, other than a few places like registering removed clauses and removal of redundant literals. Note that this together with the thorough handling from SatProofManager makes the new SAT proofs perceptibly more robust than the old ones. This PR also adds some traces to better track what Minisat does. --- src/prop/minisat/core/Solver.cc | 340 +++++++++++++++++++++++++------- src/prop/minisat/core/Solver.h | 3 + 2 files changed, 275 insertions(+), 68 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index c5158bb4f..7e4954d36 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -55,7 +55,8 @@ namespace { */ bool assertionLevelOnly() { - return options::unsatCores() && options::incrementalSolving(); + return (options::proofNew() || options::unsatCores()) + && options::incrementalSolving(); } //================================================================================================= @@ -221,6 +222,12 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, propagation_budget(-1), asynch_interrupt(false) { + if (pnm) + { + d_pfManager.reset( + new SatProofManager(this, proxy->getCnfStream(), userContext, pnm)); + } + if (options::unsatCores()) { ProofManager::currentPM()->initSatProof(this); @@ -310,10 +317,30 @@ void Solver::resizeVars(int newSize) { } CRef Solver::reason(Var x) { - Debug("pf::sat") << "Solver::reason(" << x << ")" << std::endl; + Trace("pf::sat") << "Solver::reason(" << x << ")" << std::endl; // If we already have a reason, just return it - if (vardata[x].d_reason != CRef_Lazy) return vardata[x].d_reason; + if (vardata[x].d_reason != CRef_Lazy) + { + if (Trace.isOn("pf::sat")) + { + Trace("pf::sat") << " Solver::reason: " << vardata[x].d_reason << ", "; + if (vardata[x].d_reason == CRef_Undef) + { + Trace("pf::sat") << "CRef_Undef"; + } + else + { + for (unsigned i = 0, size = ca[vardata[x].d_reason].size(); i < size; + ++i) + { + Trace("pf::sat") << ca[vardata[x].d_reason][i] << " "; + } + } + Trace("pf::sat") << "\n"; + } + return vardata[x].d_reason; + } // What's the literal we are trying to explain Lit l = mkLit(x, value(x) != l_True); @@ -326,7 +353,7 @@ CRef Solver::reason(Var x) { vec explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); - Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl + Trace("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl; // Sort the literals by trail index level @@ -377,12 +404,12 @@ CRef Solver::reason(Var x) { } explanation.shrink(i - j); - Debug("pf::sat") << "Solver::reason: explanation = "; + Trace("pf::sat") << "Solver::reason: explanation = "; for (int k = 0; k < explanation.size(); ++k) { - Debug("pf::sat") << explanation[k] << " "; + Trace("pf::sat") << explanation[k] << " "; } - Debug("pf::sat") << std::endl; + Trace("pf::sat") << std::endl; // We need an explanation clause so we add a fake literal if (j == 1) @@ -396,7 +423,8 @@ CRef Solver::reason(Var x) { CRef real_reason = ca.alloc(explLevel, explanation, true); // FIXME: at some point will need more information about where this explanation // came from (ie. the theory/sharing) - Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl; + Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" + << std::endl; if (options::unsatCores()) { ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, @@ -453,8 +481,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 if (value(ps[i]) == l_False) { - if (!options::unsatCores() && level(var(ps[i])) == 0 - && user_level(var(ps[i])) == 0) + if (!options::unsatCores() && !isProofEnabled() + && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { continue; } @@ -474,11 +502,11 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // If we are in solve_ or propagate if (minisat_busy) { - Debug("pf::sat") << "Add clause adding a new lemma: "; + Trace("pf::sat") << "Add clause adding a new lemma: "; for (int k = 0; k < ps.size(); ++k) { - Debug("pf::sat") << ps[k] << " "; + Trace("pf::sat") << ps[k] << " "; } - Debug("pf::sat") << std::endl; + Trace("pf::sat") << std::endl; lemmas.push(); ps.copyTo(lemmas.last()); @@ -496,7 +524,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { - if (options::unsatCores()) + if (options::unsatCores() || isProofEnabled()) { // Take care of false units here; otherwise, we need to // construct the clause below to give to the proof manager @@ -518,6 +546,10 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) ProofManager::getSatProof()->finalizeProof( CVC4::Minisat::CRef_Lazy); } + if (isProofEnabled()) + { + d_pfManager->finalizeProof(ps[0], true); + } return ok = false; } } @@ -539,21 +571,32 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) clauses_persistent.push(cr); attachClause(cr); - if (options::unsatCores()) + if (options::unsatCores() || isProofEnabled()) { - ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind() - ? INPUT - : THEORY_LEMMA; - id = ProofManager::getSatProof()->registerClause(cr, ck); - // map id to assertion, which may be required if looking for - // lemmas in unsat core - if (ck == THEORY_LEMMA) + if (options::unsatCores()) { - ProofManager::getCnfProof()->registerConvertedClause(id); + ClauseKind ck = + ProofManager::getCnfProof()->getCurrentAssertionKind() + ? INPUT + : THEORY_LEMMA; + id = ProofManager::getSatProof()->registerClause(cr, ck); + // map id to assertion, which may be required if looking for + // lemmas in unsat core + if (ck == THEORY_LEMMA) + { + ProofManager::getCnfProof()->registerConvertedClause(id); + } } if (ps.size() == falseLiteralsCount) { - ProofManager::getSatProof()->finalizeProof(cr); + if (options::unsatCores()) + { + ProofManager::getSatProof()->finalizeProof(cr); + } + if (isProofEnabled()) + { + d_pfManager->finalizeProof(ca[cr], true); + } return ok = false; } } @@ -580,6 +623,15 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) ProofManager::getCnfProof()->registerConvertedClause(id); } } + // 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 (isProofEnabled() && ps.size() == 1) + { + d_pfManager->registerSatLitAssumption(ps[0]); + } CRef confl = propagate(CHECK_WITHOUT_THEORY); if(! (ok = (confl == CRef_Undef)) ) { if (options::unsatCores()) @@ -596,6 +648,17 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) ProofManager::getSatProof()->finalizeProof(confl); } } + if (isProofEnabled()) + { + if (ca[confl].size() == 1) + { + d_pfManager->finalizeProof(ca[confl][0]); + } + else + { + d_pfManager->finalizeProof(ca[confl]); + } + } } return ok; } else { @@ -614,7 +677,15 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) void Solver::attachClause(CRef cr) { const Clause& c = ca[cr]; - Debug("minisat") << "Solver::attachClause(" << c << "): level " << c.level() << std::endl; + if (Debug.isOn("minisat")) + { + Debug("minisat") << "Solver::attachClause(" << c << "): "; + for (unsigned i = 0, size = c.size(); i < size; ++i) + { + Debug("minisat") << c[i] << " "; + } + Debug("minisat") << ", level " << c.level() << "\n"; + } Assert(c.size() > 1); watches[~c[0]].push(Watcher(cr, c[1])); watches[~c[1]].push(Watcher(cr, c[0])); @@ -625,12 +696,23 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { const Clause& c = ca[cr]; + Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; + if (Debug.isOn("minisat")) + { + Debug("minisat") << "Solver::detachClause(" << c << "), CRef " << cr + << ", clause "; + for (unsigned i = 0, size = c.size(); i < size; ++i) + { + Debug("minisat") << c[i] << " "; + } + + Debug("minisat") << "\n"; + } + assert(c.size() > 1); if (options::unsatCores()) { ProofManager::getSatProof()->markDeleted(cr); } - Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; - assert(c.size() > 1); if (strict){ remove(watches[~c[0]], Watcher(cr, c[1])); @@ -647,10 +729,40 @@ void Solver::detachClause(CRef cr, bool strict) { void Solver::removeClause(CRef cr) { Clause& c = ca[cr]; - Debug("minisat::remove-clause") << "Solver::removeClause(" << c << ")" << std::endl; + if (Debug.isOn("minisat")) + { + Debug("minisat") << "Solver::removeClause(" << c << "), CRef " << cr + << ", clause "; + for (unsigned i = 0, size = c.size(); i < size; ++i) + { + Debug("minisat") << c[i] << " "; + } + Debug("minisat") << "\n"; + } detachClause(cr); // Don't leave pointers to free'd memory! - if (locked(c)) vardata[var(c[0])].d_reason = CRef_Undef; + if (locked(c)) + { + // a locked clause c is one whose first literal c[0] is true and is + // propagated by c itself, i.e. vardata[var(c[0])].d_reason == c. Because + // of this if we need to justify the propagation of c[0], via + // 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()) + { + Trace("pf::sat") + << "Solver::removeClause: eagerly compute propagation of " << c[0] + << "\n"; + d_pfManager->startResChain(c); + for (unsigned i = 1, size = c.size(); i < size; ++i) + { + d_pfManager->addResolutionStep(c[i]); + } + d_pfManager->endResChain(c[0]); + } + vardata[var(c[0])].d_reason = CRef_Undef; + } c.mark(1); ca.free(cr); } @@ -880,6 +992,10 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) { ProofManager::getSatProof()->startResChain(confl); } + if (isProofEnabled()) + { + d_pfManager->startResChain(ca[confl]); + } do{ assert(confl != CRef_Undef); // (otherwise should be UIP) @@ -920,9 +1036,16 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) } // FIXME: can we do it lazily if we actually need the proof? - if (options::unsatCores() && level(var(q)) == 0) + if (level(var(q)) == 0) { - ProofManager::getSatProof()->resolveOutUnit(q); + if (options::unsatCores()) + { + ProofManager::getSatProof()->resolveOutUnit(q); + } + if (isProofEnabled()) + { + d_pfManager->addResolutionStep(q); + } } } } @@ -934,13 +1057,30 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) seen[var(p)] = 0; pathC--; - if (options::unsatCores() && pathC > 0 && confl != CRef_Undef) + if (pathC > 0 && confl != CRef_Undef) { - ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); + if (options::unsatCores()) + { + ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); + } + if (isProofEnabled()) + { + d_pfManager->addResolutionStep(ca[confl], p); + } } }while (pathC > 0); out_learnt[0] = ~p; + if (Debug.isOn("newproof::sat")) + { + Debug("newproof::sat") << "finished with learnt clause "; + for (unsigned i = 0, size = out_learnt.size(); i < size; ++i) + { + prop::SatLiteral satLit = toSatLiteral(out_learnt[i]); + Debug("newproof::sat") << satLit << " "; + } + Debug("newproof::sat") << "\n"; + } // Simplify conflict clause: int i, j; @@ -963,6 +1103,13 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) { ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); } + if (isProofEnabled()) + { + Debug("newproof::sat") + << "Solver::analyze: redundant lit " + << toSatLiteral(out_learnt[i]) << "\n"; + d_pfManager->addResolutionStep(out_learnt[i], true); + } // Literal is redundant, to be safe, mark the level as current assertion level // TODO: maybe optimize max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i]))); @@ -1096,22 +1243,44 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) seen[var(p)] = 0; } - void Solver::uncheckedEnqueue(Lit p, CRef from) { - Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl; - assert(value(p) == l_Undef); - assert(var(p) < nVars()); - assigns[var(p)] = lbool(!sign(p)); - vardata[var(p)] = VarData(from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size()); - trail.push_(p); - if (theory[var(p)]) { - // Enqueue to the theory - d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); + if (Debug.isOn("minisat")) + { + Debug("minisat") << "unchecked enqueue of " << p << " (" + << trail_index(var(p)) << ") trail size is " + << trail.size() << " cap is " << trail.capacity() + << ", reason is " << from << ", "; + if (from == CRef_Lazy) + { + Debug("minisat") << "CRef_Lazy"; + } + else if (from == CRef_Undef) + { + Debug("minisat") << "CRef_Undef"; + } + else + { + for (unsigned i = 0, size = ca[from].size(); i < size; ++i) + { + Debug("minisat") << ca[from][i] << " "; + } } + Debug("minisat") << "\n"; + } + assert(value(p) == l_Undef); + assert(var(p) < nVars()); + assigns[var(p)] = lbool(!sign(p)); + vardata[var(p)] = VarData( + from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size()); + trail.push_(p); + if (theory[var(p)]) + { + // Enqueue to the theory + d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); + } } - CRef Solver::propagate(TheoryCheckType type) { CRef confl = CRef_Undef; @@ -1375,7 +1544,7 @@ void Solver::removeSatisfied(vec& cs) // store a resolution of the literal c propagated ProofManager::getSatProof()->storeUnitResolution(c[0]); } - removeClause(cs[i]); + removeClause(cs[i]); } else cs[j++] = cs[i]; @@ -1472,11 +1641,23 @@ lbool Solver::search(int nof_conflicts) conflicts++; conflictC++; - if (decisionLevel() == 0) { + if (decisionLevel() == 0) + { if (options::unsatCores()) { ProofManager::getSatProof()->finalizeProof(confl); } + if (isProofEnabled()) + { + if (confl == CRef_Lazy) + { + d_pfManager->finalizeProof(); + } + else + { + d_pfManager->finalizeProof(ca[confl]); + } + } return l_False; } @@ -1488,11 +1669,14 @@ lbool Solver::search(int nof_conflicts) // Assert the conflict clause and the asserting literal if (learnt_clause.size() == 1) { uncheckedEnqueue(learnt_clause[0]); - if (options::unsatCores()) { ProofManager::getSatProof()->endResChain(learnt_clause[0]); } + if (isProofEnabled()) + { + d_pfManager->endResChain(learnt_clause[0]); + } } else { CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level, @@ -1508,6 +1692,10 @@ lbool Solver::search(int nof_conflicts) ProofManager::getSatProof()->registerClause(cr, LEARNT); ProofManager::getSatProof()->endResChain(id); } + if (isProofEnabled()) + { + d_pfManager->endResChain(ca[cr]); + } } varDecayActivity(); @@ -1560,17 +1748,17 @@ lbool Solver::search(int nof_conflicts) check_type = CHECK_WITH_THEORY; } - if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) - || !withinBudget(ResourceManager::Resource::SatConflictStep)) - { - // Reached bound on number of conflicts: - progress_estimate = progressEstimate(); - cancelUntil(0); - // [mdeters] notify theory engine of restarts for deferred - // theory processing - d_proxy->notifyRestart(); - return l_Undef; - } + if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) + || !withinBudget(ResourceManager::Resource::SatConflictStep)) + { + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + // [mdeters] notify theory engine of restarts for deferred + // theory processing + d_proxy->notifyRestart(); + return l_Undef; + } // Simplify the set of problem clauses: if (decisionLevel() == 0 && !simplify()) { @@ -1891,6 +2079,9 @@ void Solver::pop() // Pop the trail below the user level --assertionLevel; + Debug("minisat") << "in user pop, decreasing assertion level to " + << assertionLevel << "\n" + << CVC4::push; while (true) { Debug("minisat") << "== unassigning " << trail.last() << std::endl; Var x = var(trail.last()); @@ -1905,16 +2096,19 @@ void Solver::pop() break; } } + // The head should be at the trail top qhead = trail.size(); // Remove the clauses removeClausesAboveLevel(clauses_persistent, assertionLevel); removeClausesAboveLevel(clauses_removable, assertionLevel); - + Debug("minisat") << CVC4::pop; // Pop the SAT context to notify everyone d_context->pop(); // SAT context for CVC4 + Debug("minisat") << "MINISAT POP assertionLevel is " << assertionLevel + << ", trail.size is " << trail.size() << "\n"; // Pop the created variables resizeVars(assigns_lim.last()); assigns_lim.pop(); @@ -1949,15 +2143,15 @@ CRef Solver::updateLemmas() { // The current lemma vec& lemma = lemmas[i]; - Debug("pf::sat") << "Solver::updateLemmas: working on lemma: "; + Trace("pf::sat") << "Solver::updateLemmas: working on lemma: "; for (int k = 0; k < lemma.size(); ++k) { - Debug("pf::sat") << lemma[k] << " "; + Trace("pf::sat") << lemma[k] << " "; } - Debug("pf::sat") << std::endl; + Trace("pf::sat") << std::endl; // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { - Assert(!options::unsatCores()); + Assert(!options::unsatCores() && !isProofEnabled()); conflict = CRef_Lazy; backtrackLevel = 0; Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -2037,13 +2231,17 @@ CRef Solver::updateLemmas() { { Node cnf_assertion = lemmas_cnf_assertion[j]; - Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) " + Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) " << cnf_assertion << value(lemma[0]) << std::endl; ClauseId id = ProofManager::getSatProof()->registerUnitClause( lemma[0], THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); } - + if (CVC4::options::proofNew()) + { + Trace("pf::sat") << "Solver::updateLemmas: unit theory lemma: " + << lemma[0] << std::endl; + } if (value(lemma[0]) == l_False) { // We have a conflict if (lemma.size() > 1) { @@ -2056,6 +2254,10 @@ CRef Solver::updateLemmas() { { ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); } + if (isProofEnabled()) + { + d_pfManager->storeUnitConflict(lemma[0]); + } } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; @@ -2085,7 +2287,7 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::TSatProof* proof) { - + Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl; // FIXME what is this CRef_lazy if (cr == CRef_Lazy) return; @@ -2123,13 +2325,15 @@ inline bool Solver::withinBudget(ResourceManager::Resource r) const SatProofManager* Solver::getProofManager() { - return d_pfManager ? d_pfManager.get() : nullptr; + return isProofEnabled() ? d_pfManager.get() : nullptr; } std::shared_ptr Solver::getProof() { - return d_pfManager ? d_pfManager->getProof() : nullptr; + return isProofEnabled() ? d_pfManager->getProof() : nullptr; } +bool Solver::isProofEnabled() const { return d_pfManager != nullptr; } + } /* CVC4::Minisat namespace */ } /* CVC4 namespace */ diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 270cc9308..00d68cf80 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -158,6 +158,9 @@ public: /** Retrive the refutation proof */ std::shared_ptr getProof(); + /** Is proof enabled? */ + bool isProofEnabled() const; + // Less than for literals in a lemma struct lemma_lt { -- 2.30.2