From: msoos Date: Sun, 18 Apr 2010 15:50:28 +0000 (+0000) Subject: CMS2 now has two types of learnt clause evaluation X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f1e9afd72ba4cecf63e04ea773525a9a0979175c;p=francis%2Fstp.git CMS2 now has two types of learnt clause evaluation CryptoMiniSat2 now has two types of learnt clause activity measures. This means that different type of problems can be effectively solved with the same solver that uses radically different measures of learnt clause effectiveness. There are some rough edges for the moment: it's really difficult which type of instance we are dealing with. So, the 'heuristic' that decides is really dumb. You can find it in RestarTypeChooser.cpp. If you have a more refined heuristic in mind, please share it with me! git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@688 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index 730b62c..0438466 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -67,6 +67,7 @@ protected: uint32_t mySize:20; union {int32_t act; uint32_t abst;} extra; + float oldActivityInter; #ifdef _MSC_VER Lit data[1]; #else @@ -88,8 +89,11 @@ public: isLearnt = learnt; setGroup(_group); for (uint i = 0; i < ps.size(); i++) data[i] = ps[i]; - if (learnt) extra.act = 0; - else calcAbstraction(); + if (learnt) { + extra.act = 0; + oldActivityInter = 0; + } else + calcAbstraction(); } public: @@ -118,6 +122,15 @@ public: const bool learnt () const { return isLearnt; } + float& oldActivity () { + return oldActivityInter; + } + + const float& oldActivity () const { + return oldActivityInter; + } + + const bool getStrenghtened() const { return strenghtened; } diff --git a/src/sat/cryptominisat2/FailedVarSearcher.cpp b/src/sat/cryptominisat2/FailedVarSearcher.cpp index f2de3da..171f9c7 100644 --- a/src/sat/cryptominisat2/FailedVarSearcher.cpp +++ b/src/sat/cryptominisat2/FailedVarSearcher.cpp @@ -142,7 +142,7 @@ const bool FailedVarSearcher::search(uint64_t numProps) uint64_t origProps = solver.propagations; //If failed var searching is going good, do successively more and more of it - if (lastTimeFoundTruths > 500 || (double)lastTimeFoundTruths > (double)solver.order_heap.size() * 0.05) std::max(numPropsMultiplier*1.7, 5.0); + if (lastTimeFoundTruths > 500 || (double)lastTimeFoundTruths > (double)solver.order_heap.size() * 0.03) std::max(numPropsMultiplier*1.7, 5.0); else numPropsMultiplier = 1.0; numProps = (uint64_t) ((double)numProps * numPropsMultiplier); @@ -156,6 +156,9 @@ const bool FailedVarSearcher::search(uint64_t numProps) propValue.resize(solver.nVars(), 0); vector > bothSame; + //For calculating how many variables have really been set + uint32_t origTrailSize = solver.trail.size(); + //For 2-long xor (rule 6 of Equivalent literal propagation in the DLL procedure by Chu-Min Li) set twoLongXors; uint32_t toReplaceBefore = solver.varReplacer->getNewToReplaceVars(); @@ -325,7 +328,7 @@ end: } } - lastTimeFoundTruths = goodBothSame + numFailed; + lastTimeFoundTruths = solver.trail.size() - origTrailSize; solver.var_inc = backup_var_inc; std::copy(backup_activity.getData(), backup_activity.getDataEnd(), solver.activity.getData()); diff --git a/src/sat/cryptominisat2/RestartTypeChooser.cpp b/src/sat/cryptominisat2/RestartTypeChooser.cpp index 9130a1d..739c449 100644 --- a/src/sat/cryptominisat2/RestartTypeChooser.cpp +++ b/src/sat/cryptominisat2/RestartTypeChooser.cpp @@ -56,8 +56,11 @@ void RestartTypeChooser::addInfo() const RestartType RestartTypeChooser::choose() { - if (countVarsDegreeStDev().second < 80 && + pair mypair = countVarsDegreeStDev(); + if ((mypair.second < 80 && (avg() > (double)limit || ((avg() > (double)(limit*0.9) && stdDeviation(sameIns) < 5)))) + || + (mypair.second < 80 && (double)solver.xorclauses.size() > (double)solver.nClauses()*0.1)) return static_restart; else return dynamic_restart; diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index e98bab4..fee91b5 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -99,6 +99,7 @@ Solver::Solver() : , ok (true) , var_inc (128) + , cla_inc (1) , curRestart (1) , nbclausesbeforereduce (NBCLAUSESBEFOREREDUCE) @@ -112,6 +113,7 @@ Solver::Solver() : , remove_satisfied (true) , mtrand((unsigned long int)0) , restartType (static_restart) + , lastSelectedRestartType (static_restart) #ifdef STATS_NEEDED , logger(verbosity) , dynamic_behaviour_analysis(false) //do not document the proof as default @@ -760,7 +762,7 @@ bool subset(const T1& A, const T2& B, vector& seen) | Effect: | Will undo part of the trail, upto but not beyond the assumption of the current decision level. |________________________________________________________________________________________________@*/ -Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int &nbLevels/*, int &merged*/) +Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, int &nbLevels, const bool update) { int pathC = 0; Lit p = lit_Undef; @@ -777,6 +779,9 @@ Clause* Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel, i Clause& c = *confl; if (p != lit_Undef) reverse_binary_clause(c); + + if (update && restartType == static_restart && c.learnt()) + claBumpActivity(c); for (uint j = (p == lit_Undef) ? 0 : 1; j != c.size(); j++) { const Lit& q = c[j]; @@ -1229,30 +1234,39 @@ FoundWatch: | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked | clauses are clauses that are reason to some assignment. Binary clauses are never removed. |________________________________________________________________________________________________@*/ -struct reduceDB_lt { - bool operator () (const Clause* x, const Clause* y) { - const uint xsize = x->size(); - const uint ysize = y->size(); - - // First criteria - if (xsize > 2 && ysize == 2) return 1; - if (ysize > 2 && xsize == 2) return 0; - - // Second criteria - if (x->activity() > y->activity()) return 1; - if (x->activity() < y->activity()) return 0; - - //return x->oldActivity() < y->oldActivity(); - return xsize > ysize; - } -}; +bool reduceDB_ltMiniSat::operator () (const Clause* x, const Clause* y) { + const uint xsize = x->size(); + const uint ysize = y->size(); + + // First criteria + if (xsize > 2 && ysize == 2) return 1; + if (ysize > 2 && xsize == 2) return 0; + + return x->oldActivity() < y->oldActivity(); +} + +bool reduceDB_ltGlucose::operator () (const Clause* x, const Clause* y) { + const uint xsize = x->size(); + const uint ysize = y->size(); + + // First criteria + if (xsize > 2 && ysize == 2) return 1; + if (ysize > 2 && xsize == 2) return 0; + + if (x->activity() > y->activity()) return 1; + if (x->activity() < y->activity()) return 0; + return xsize > ysize; +} void Solver::reduceDB() { uint32_t i, j; nbReduceDB++; - std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt()); + if (lastSelectedRestartType == dynamic_restart) + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose()); + else + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat()); #ifdef VERBOSE_DEBUG std::cout << "Cleaning clauses" << endl; @@ -1284,7 +1298,10 @@ const vec& Solver::get_learnts() const const vec& Solver::get_sorted_learnts() { - std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt()); + if (lastSelectedRestartType == dynamic_restart) + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose()); + else + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat()); return learnts; } @@ -1331,7 +1348,11 @@ void Solver::dumpSortedLearnts(const char* file, const uint32_t maxSize) } fprintf(outfile, "c clauses from learnts\n"); - std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt()); + + if (lastSelectedRestartType == dynamic_restart) + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose()); + else + std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat()); for (int i = learnts.size()-1; i >= 0 ; i--) { if (learnts[i]->size() <= maxSize) learnts[i]->plainPrint(outfile); @@ -1597,7 +1618,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf if (decisionLevel() == 0) return l_False; learnt_clause.clear(); - Clause* c = analyze(confl, learnt_clause, backtrack_level, nbLevels); + Clause* c = analyze(confl, learnt_clause, backtrack_level, nbLevels, update); if (update) { avgBranchDepth.push(decisionLevel()); if (restartType == dynamic_restart) @@ -1722,11 +1743,13 @@ inline void Solver::chooseRestartType(const uint& lastFullRestart) tmp = fixRestartType; if (tmp == dynamic_restart) { + lastSelectedRestartType = dynamic_restart; nbDecisionLevelHistory.fastclear(); nbDecisionLevelHistory.initSize(100); if (verbosity >= 2) printf("c | Decided on dynamic restart strategy |\n"); } else { + lastSelectedRestartType = static_restart; if (verbosity >= 2) printf("c | Decided on static restart strategy |\n"); @@ -1748,10 +1771,13 @@ inline void Solver::setDefaultRestartType() { if (fixRestartType != auto_restart) restartType = fixRestartType; else restartType = static_restart; + if (restartType == dynamic_restart) { nbDecisionLevelHistory.fastclear(); nbDecisionLevelHistory.initSize(100); } + + lastSelectedRestartType = restartType; } const lbool Solver::simplifyProblem(const uint32_t numConfls, const uint64_t numProps) diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 2c232a3..9fcda6a 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -67,6 +67,16 @@ using std::endl; //================================================================================================= // Solver -- the main class: +struct reduceDB_ltMiniSat +{ + bool operator () (const Clause* x, const Clause* y); +}; + +struct reduceDB_ltGlucose +{ + bool operator () (const Clause* x, const Clause* y); +}; + class Solver { @@ -217,6 +227,7 @@ protected: vec learnts; // List of learnt clauses. vec activity; // A heuristic measurement of the activity of a variable. uint32_t var_inc; // Amount to bump next variable with. + double cla_inc; // Amount to bump learnt clause oldActivity with vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses. vec > binwatches; @@ -247,6 +258,7 @@ protected: bqueue avgBranchDepth; // Avg branch depth MTRand mtrand; // random number generaton RestartType restartType; // Used internally to determine which restart strategy to choose + RestartType lastSelectedRestartType; //the last selected restart type friend class Logger; #ifdef STATS_NEEDED Logger logger; // dynamic logging, statistics @@ -279,7 +291,7 @@ protected: Clause* propagate (const bool update = true); // Perform unit propagation. Returns possibly conflicting clause. Clause* propagate_xors (const Lit& p); void cancelUntil (int level); // Backtrack until a certain level. - Clause* analyze (Clause* confl, vec& out_learnt, int& out_btlevel, int &nblevels); // (bt = backtrack) + Clause* analyze (Clause* confl, vec& out_learnt, int& out_btlevel, int &nblevels, const bool update); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') lbool search (int nof_conflicts, int nof_conflicts_fullrestart, const bool update = true); // Search for a given number of conflicts. @@ -289,6 +301,7 @@ protected: // Maintaining Variable/Clause activity: // + void claBumpActivity (Clause& c); void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead. void varBumpActivity (Var v); // Increase a variable with the current 'bump' value. void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead. @@ -397,6 +410,17 @@ inline void Solver::varBumpActivity(Var v) order_heap.decrease(v); } +inline void Solver::claBumpActivity (Clause& c) +{ + if ( (c.oldActivity() += cla_inc) > 1e20 ) { + // Rescale: + for (uint32_t i = 0; i < learnts.size(); i++) + learnts[i]->oldActivity() *= 1e-17; + cla_inc *= 1e-20; + } +} + + inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index f3f456b..01ed823 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,2 +1,2 @@ CryptoMiniSat -GIT revision: 3c04fa48505107a294986a85131b05a67c479ba1 +GIT revision: 3f1c377140a6808fe92a2126eb5ed420dfc6f051