From 62f5fb8db269e12f13ce5c4e1c3f975776737836 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 9 Apr 2021 17:30:44 -0300 Subject: [PATCH] [proof-new] Optimizing sat proof (#6324) For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR. --- src/expr/lazy_proof_chain.cpp | 13 +++++++++++-- src/expr/proof_rule.h | 12 ++++++++---- src/prop/sat_proof_manager.cpp | 18 ++++++++---------- src/prop/sat_proof_manager.h | 3 ++- src/smt/proof_manager.cpp | 1 + src/smt/proof_post_processor.cpp | 3 ++- src/theory/booleans/proof_checker.cpp | 7 +++++++ 7 files changed, 39 insertions(+), 18 deletions(-) diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index 7f14adc38..5e638b55f 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -67,7 +67,7 @@ std::shared_ptr LazyCDProofChain::getProofFor(Node fact) std::vector>, NodeHashFunction> assumptionsToExpand; - // invariant of the loop below, the first iteration notwhistanding: + // invariant of the loop below, the first iteration notwithstanding: // visit = domain(assumptionsToExpand) \ domain(toConnect) std::vector visit{fact}; std::unordered_map visited; @@ -121,13 +121,22 @@ std::shared_ptr LazyCDProofChain::getProofFor(Node fact) expr::getFreeAssumptionsMap(curPfn, famap); if (Trace.isOn("lazy-cdproofchain")) { + unsigned alreadyToVisit = 0; Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: free assumptions:\n"; + << "LazyCDProofChain::getProofFor: " << famap.size() + << " free assumptions:\n"; for (auto fap : famap) { Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: - " << fap.first << "\n"; + alreadyToVisit += + std::find(visit.begin(), visit.end(), fap.first) != visit.end() + ? 1 + : 0; } + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: " << alreadyToVisit + << " already to visit\n"; } // mark for post-traversal if we are controlling cycles if (d_cyclic) diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 7e0fc31fe..cec85cc99 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -320,6 +320,8 @@ enum class PfRule : uint32_t // The result of the chain resolution is C, which is equal, in its set // representation, to C_n' MACRO_RESOLUTION, + // As above but not checked + MACRO_RESOLUTION_TRUST, // ======== Split // Children: none @@ -1048,8 +1050,9 @@ enum class PfRule : uint32_t // its ki is negative). >< is always one of <, <= // NB: this implies that lower bounds must have negative ki, // and upper bounds must have positive ki. - // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * poly_n) - // t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n * const_n) + // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * + // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n + // * const_n) ARITH_SCALE_SUM_UPPER_BOUNDS, // ======== Sum Upper Bounds @@ -1134,8 +1137,9 @@ enum class PfRule : uint32_t // Arguments: (t, x, y, a, b, sgn) // --------------------- // Conclusion: - // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y b))) - // sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) (>= y b))) + // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y + // b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) + // (>= y b))) // Where x,y are real terms (variables or extended terms), t = (* x y) // (possibly under rewriting), a,b are real constants, and sgn is either -1 // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index da9354c2f..0d075de45 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -35,6 +35,7 @@ SatProofManager::SatProofManager(Minisat::Solver* solver, d_assumptions(userContext), d_conflictLit(undefSatVariable) { + d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } @@ -169,7 +170,6 @@ void SatProofManager::endResChain(Node conclusion, } d_redundantLits.clear(); // build resolution chain - NodeManager* nm = NodeManager::currentNM(); // the conclusion is stored already in the arguments because of the // possibility of reordering std::vector children, args{conclusion}; @@ -212,7 +212,7 @@ void SatProofManager::endResChain(Node conclusion, Trace("sat-proof") << " : "; if (i > 0) { - args.push_back(nm->mkConst(posFirst)); + args.push_back(posFirst ? d_true : d_false); args.push_back(pivot); Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] "; } @@ -249,7 +249,7 @@ void SatProofManager::endResChain(Node conclusion, // step, which bypasses these. Note that we could generate a chain resolution // rule here by explicitly computing the detailed steps, but leave this for // post-processing. - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(conclusion, ps); // the premises of this resolution may not have been justified yet, so we do // not pass assumptions to check closedness @@ -369,7 +369,6 @@ void SatProofManager::explainLit( // SAT solver, we directly get the literals we need to explain so we no // longer depend on the reference to reason std::vector toExplain{children.back().begin(), children.back().end()}; - NodeManager* nm = NodeManager::currentNM(); Trace("sat-proof") << push; for (unsigned i = 0; i < size; ++i) { @@ -397,7 +396,7 @@ void SatProofManager::explainLit( // note this is the opposite of what is done in addResolutionStep. This is // because here the clause, which contains the literal being analyzed, is // the first clause rather than the second - args.push_back(nm->mkConst(!negated)); + args.push_back(!negated ? d_true : d_false); args.push_back(negated ? currLitNode[0] : currLitNode); // add child premises and the child itself premises.insert(childPremises.begin(), childPremises.end()); @@ -429,7 +428,7 @@ void SatProofManager::explainLit( Trace("sat-proof") << pop; // create step args.insert(args.begin(), litNode); - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(litNode, ps); // the premises in the limit of the justification may correspond to other // links in the chain which have, themselves, literals yet to be justified. So @@ -490,7 +489,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // get resolution Node cur = link.first; std::shared_ptr pfn = link.second; - while (pfn->getRule() != PfRule::MACRO_RESOLUTION) + while (pfn->getRule() != PfRule::MACRO_RESOLUTION_TRUST) { Assert(pfn->getChildren().size() == 1 && pfn->getChildren()[0]->getRule() == PfRule::ASSUME) @@ -539,7 +538,6 @@ void SatProofManager::finalizeProof(Node inConflictNode, // arguments for the resolution step to conclude false. std::vector children{inConflictNode}, args; std::unordered_set premises; - NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = inConflict.size(); i < size; ++i) { Assert(d_cnfStream->getNodeCache().find(inConflict[i]) @@ -555,7 +553,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // note this is the opposite of what is done in addResolutionStep. This is // because here the clause, which contains the literal being analyzed, is // the first clause rather than the second - args.push_back(nm->mkConst(!negated)); + args.push_back(!negated ? d_true : d_false); args.push_back(negated ? litNode[0] : litNode); // add child premises and the child itself premises.insert(childPremises.begin(), childPremises.end()); @@ -578,7 +576,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, } // create step args.insert(args.begin(), d_false); - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(d_false, ps); // not yet ready to check closedness because maybe only now we will justify // literals used in resolutions diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 4d45ce3b7..6407939c7 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -561,7 +561,8 @@ class SatProofManager /** The proof generator for resolution chains */ BufferedProofGenerator d_resChainPg; - /** The false node */ + /** The true/false nodes */ + Node d_true; Node d_false; /** All clauses added to the SAT solver, kept in a context-dependent manner. diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 846df7e41..549f10008 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -64,6 +64,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO); d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_ELIM); d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM); + d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION_TRUST); d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION); if (options::proofGranularityMode() != options::ProofGranularityMode::REWRITE) diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a27a5697e..19ca089d3 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -648,7 +648,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {}); return args[0]; } - else if (id == PfRule::MACRO_RESOLUTION) + else if (id == PfRule::MACRO_RESOLUTION + || id == PfRule::MACRO_RESOLUTION_TRUST) { // first generate the naive chain_resolution std::vector chainResArgs{args.begin() + 1, args.end()}; diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index d6600f14d..6b9d3e44e 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -25,6 +25,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::SPLIT, this); pc->registerChecker(PfRule::RESOLUTION, this); pc->registerChecker(PfRule::CHAIN_RESOLUTION, this); + pc->registerTrustedChecker(PfRule::MACRO_RESOLUTION_TRUST, this, 3); pc->registerChecker(PfRule::MACRO_RESOLUTION, this); pc->registerChecker(PfRule::FACTORING, this); pc->registerChecker(PfRule::REORDERING, this); @@ -299,6 +300,12 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, : clauseNodes.size() == 1 ? clauseNodes[0] : nm->mkNode(kind::OR, clauseNodes); } + if (id == PfRule::MACRO_RESOLUTION_TRUST) + { + Assert(children.size() > 1); + Assert(args.size() == 2 * (children.size() - 1) + 1); + return args[0]; + } if (id == PfRule::MACRO_RESOLUTION) { Assert(children.size() > 1); -- 2.30.2