From: msoos Date: Fri, 16 Apr 2010 15:54:30 +0000 (+0000) Subject: Importing new version of CMS2 X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=6e40aa67ff034d57c93b66076f71506fb1520acc;p=francis%2Fstp.git Importing new version of CMS2 * bug with Conglomerate fixed. Conglomerate will in the future be callable in the middle of solving * variable activity is now uint32_t. No more floating point code. This change also means a more conservative variable activity heuristic. Should help on most problems (but not crypto, I believe) * Removed useless code around logging * No more warnings on (deprecated) const char* to string conversion git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@687 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index 43caf21..683f558 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -92,10 +92,13 @@ void Conglomerate::fillVarToXor() void Conglomerate::removeVar(const Var var) { - solver.setDecisionVar(var, false); solver.activity[var] = 0.0; solver.order_heap.update(var); removedVars[var] = true; + if (solver.decision_var[var]) { + madeVarNonDecision.push(var); + solver.setDecisionVar(var, false); + } found++; } @@ -461,52 +464,24 @@ void Conglomerate::clearLearntsFromToRemove() solver.learnts.shrink(r-a); } -void Conglomerate::doCalcAtFinish() +void Conglomerate::extendModel(Solver& solver2) { #ifdef VERBOSE_DEBUG cout << "Executing doCalcAtFinish" << endl; #endif - vector toAssign; - for (XorClause** it = calcAtFinish.getData() + calcAtFinish.size()-1; it != calcAtFinish.getData()-1; it--) { - toAssign.clear(); - XorClause& c = **it; + vec ps; + for (int i = (int)(calcAtFinish.size())-1; i >= 0; i--) { + XorClause& c = *calcAtFinish[i]; assert(c.size() > 2); - #ifdef VERBOSE_DEBUG - cout << "doCalcFinish for xor-clause:"; - c.plainPrint(); - #endif - - bool final = c.xor_clause_inverted(); - for (int k = 0, size = c.size(); k < size; k++ ) { - const lbool& val = solver.assigns[c[k].var()]; - if (val == l_Undef) - toAssign.push_back(c[k].var()); - else - final ^= val.getBool(); - } - #ifdef VERBOSE_DEBUG - if (toAssign.size() == 0) { - cout << "ERROR: toAssign.size() == 0 !!" << endl; - for (int k = 0, size = c.size(); k < size; k++ ) { - cout << "Var: " << c[k].var() + 1 << " Level: " << solver.level[c[k].var()] << endl; - } - } - if (toAssign.size() > 1) { - cout << "Double assign!" << endl; - for (uint i = 1; i < toAssign.size(); i++) { - cout << "-> extra Var " << toAssign[i]+1 << endl; - } + ps.clear(); + for (Lit *l = c.getData(), *end = c.getDataEnd(); l != end; l++) { + ps.push(l->unsign()); } - #endif - assert(toAssign.size() > 0); - for (uint i = 1; i < toAssign.size(); i++) { - solver.uncheckedEnqueue(Lit(toAssign[i], true), &c); - } - solver.uncheckedEnqueue(Lit(toAssign[0], final), &c); - assert(solver.clauseCleaner->satisfied(c)); + solver2.addXorClause(ps, c.xor_clause_inverted(), c.getGroup()); + assert(solver2.ok); } } @@ -516,9 +491,6 @@ const bool Conglomerate::addRemovedClauses() cout << "Executing addRemovedClauses" << endl; #endif - char tmp[100]; - tmp[0] = '\0'; - vec ps; for(uint i = 0; i < calcAtFinish.size(); i++) { XorClause& c = *calcAtFinish[i]; @@ -527,31 +499,22 @@ const bool Conglomerate::addRemovedClauses() c.plainPrint(); #endif - ps.clear(); - for(uint i2 = 0; i2 != c.size() ; i2++) { - ps.push(Lit(c[i2].var(), false)); - } - if (!solver.addXorClause(ps, c.xor_clause_inverted(), c.getGroup(), tmp)) + for(Lit *l = c.getData(), *end = c.getDataEnd(); l != end ; l++) + *l = l->unsign(); + + if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) return false; free(&c); } calcAtFinish.clear(); - for (uint i = 0; i < removedVars.size(); i++) { - if (removedVars[i]) { - removedVars[i] = false; - solver.setDecisionVar(i, true); - #ifdef VERBOSE_DEBUG - std::cout << "Inserting Var " << i+1 << " back into the order_heap" << std::endl; - #endif //VERBOSE_DEBUG - } + + std::fill(removedVars.getData(), removedVars.getDataEnd(), false); + for (Var *v = madeVarNonDecision.getData(), *end = madeVarNonDecision.getDataEnd(); v != end; v++) { + solver.setDecisionVar(*v, true); } + madeVarNonDecision.clear(); return true; } -void Conglomerate::newVar() -{ - removedVars.resize(removedVars.size()+1, false); -} - }; //NAMESPACE MINISAT diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h index 15fcb0b..50972d4 100644 --- a/src/sat/cryptominisat2/Conglomerate.h +++ b/src/sat/cryptominisat2/Conglomerate.h @@ -50,11 +50,12 @@ public: const bool conglomerateXorsFull(); const bool heuleProcessFull(); const bool addRemovedClauses(); ///& getCalcAtFinish() const; vec& getCalcAtFinish(); - const vector& getRemovedVars() const; + const vec& getRemovedVars() const; + const bool needCalcAtFinish() const; void newVar(); @@ -84,7 +85,9 @@ private: varToXorMap varToXor; vector blocked; vector toRemove; - vector removedVars; + + vec removedVars; + vec madeVarNonDecision; vec calcAtFinish; uint found; @@ -92,7 +95,12 @@ private: Solver& solver; }; -inline const vector& Conglomerate::getRemovedVars() const +inline void Conglomerate::newVar() +{ + removedVars.push(false); +} + +inline const vec& Conglomerate::getRemovedVars() const { return removedVars; } @@ -107,6 +115,11 @@ inline vec& Conglomerate::getCalcAtFinish() return calcAtFinish; } +inline const bool Conglomerate::needCalcAtFinish() const +{ + return calcAtFinish.size(); +} + }; //NAMESPACE MINISAT #endif //CONGLOMERATE_H diff --git a/src/sat/cryptominisat2/FailedVarSearcher.cpp b/src/sat/cryptominisat2/FailedVarSearcher.cpp index 227875e..f2de3da 100644 --- a/src/sat/cryptominisat2/FailedVarSearcher.cpp +++ b/src/sat/cryptominisat2/FailedVarSearcher.cpp @@ -125,10 +125,9 @@ const bool FailedVarSearcher::search(uint64_t numProps) //Saving Solver state Heap backup_order_heap(solver.order_heap); vector backup_polarities = solver.polarity; - vec backup_activity; - backup_activity.growTo(solver.activity.size()); + vec backup_activity(solver.activity.size()); std::copy(solver.activity.getData(), solver.activity.getDataEnd(), backup_activity.getData()); - double backup_var_inc = solver.var_inc; + uint32_t backup_var_inc = solver.var_inc; uint32_t origHeapSize = solver.order_heap.size(); //General Stats diff --git a/src/sat/cryptominisat2/PartHandler.cpp b/src/sat/cryptominisat2/PartHandler.cpp index dddc7ff..c7f666a 100644 --- a/src/sat/cryptominisat2/PartHandler.cpp +++ b/src/sat/cryptominisat2/PartHandler.cpp @@ -64,7 +64,6 @@ const bool PartHandler::handle() Solver newSolver; newSolver.mtrand.seed(solver.mtrand.randInt()); newSolver.random_var_freq = solver.random_var_freq; - newSolver.var_decay = solver.var_decay; newSolver.verbosity = solver.verbosity; newSolver.restrictedPickBranch = solver.restrictedPickBranch; newSolver.greedyUnbound = solver.greedyUnbound; diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 552b2a8..e98bab4 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -61,7 +61,7 @@ using namespace MINISAT; Solver::Solver() : // Parameters: (formerly in 'SearchParams') - var_decay(1 / 0.95), random_var_freq(0.02) + random_var_freq(0.02) , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1) // More parameters: @@ -98,7 +98,7 @@ Solver::Solver() : , ok (true) - , var_inc (1) + , var_inc (128) , curRestart (1) , nbclausesbeforereduce (NBCLAUSESBEFOREREDUCE) @@ -203,6 +203,10 @@ Var Solver::newVar(bool dvar) template XorClause* Solver::addXorClauseInt(T& ps, bool xor_clause_inverted, const uint32_t group) { + if (ps.size() > (0x01UL << 18)) { + std::cout << "Too long clause!" << std::endl; + exit(-1); + } std::sort(ps.getData(), ps.getData()+ps.size()); Lit p; uint32_t i, j; @@ -1755,11 +1759,10 @@ const lbool Solver::simplifyProblem(const uint32_t numConfls, const uint64_t num Heap backup_order_heap(order_heap); vector backup_polarities = polarity; RestartType backup_restartType= restartType; - double backup_random_var_freq = random_var_freq; - vec backup_activity; - backup_activity.growTo(activity.size()); + uint32_t backup_random_var_freq = random_var_freq; + vec backup_activity(activity.size()); std::copy(activity.getData(), activity.getDataEnd(), backup_activity.getData()); - double backup_var_inc = var_inc; + uint32_t backup_var_inc = var_inc; if (verbosity >= 2) std::cout << "c | " << std::setw(24) << " " @@ -2015,7 +2018,7 @@ lbool Solver::solve(const vec& assumps) //checkSolution(); #endif - if (subsumer->getNumElimed() > 0) { + if (subsumer->getNumElimed() > 0 || conglomerate->needCalcAtFinish()) { Solver s; s.doSubsumption = false; s.performReplace = false; @@ -2025,8 +2028,10 @@ lbool Solver::solve(const vec& assumps) s.conglomerateXors = false; s.greedyUnbound = greedyUnbound; for (Var var = 0; var < nVars(); var++) { - s.newVar(decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var)); + s.newVar(decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var) || conglomerate->getRemovedVars()[var]); + assert(!(conglomerate->getRemovedVars()[var] && (decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var)))); + if (value(var) != l_Undef) { assert(!conglomerate->getRemovedVars()[var]); vec tmp; @@ -2036,18 +2041,22 @@ lbool Solver::solve(const vec& assumps) } varReplacer->extendModelImpossible(s); subsumer->extendModel(s); + conglomerate->extendModel(s); status = s.solve(); - assert(status == l_True); + if (status != l_True) { + printf("c ERROR! Extension of model failed!\n"); + assert(status == l_True); + exit(-1); + } for (Var var = 0; var < nVars(); var++) { if (assigns[var] == l_Undef && s.model[var] != l_Undef) uncheckedEnqueue(Lit(var, s.model[var] == l_False)); } } - conglomerate->doCalcAtFinish(); - // Extend & copy model: #ifndef NDEBUG //checkSolution(); #endif + //Copy model: model.growTo(nVars()); for (Var var = 0; var != nVars(); var++) model[var] = value(var); diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index be234d4..2c232a3 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -25,7 +25,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include #include - #ifdef _MSC_VER #include #else @@ -118,7 +117,6 @@ public: // Mode of operation: // - double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95) double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) int restart_first; // The initial restart limit. (default 100) double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5) @@ -194,11 +192,11 @@ protected: // Helper structures: // struct VarOrderLt { - const vec& activity; + const vec& activity; bool operator () (Var x, Var y) const { return activity[x] > activity[y]; } - VarOrderLt(const vec& act) : activity(act) { } + VarOrderLt(const vec& act) : activity(act) { } }; friend class VarFilter; @@ -217,8 +215,8 @@ protected: vec binaryClauses; // Binary clauses are regularly moved here vec xorclauses; // List of problem xor-clauses. Will be freed vec learnts; // List of learnt clauses. - vec activity; // A heuristic measurement of the activity of a variable. - double var_inc; // Amount to bump next variable with. + vec activity; // A heuristic measurement of the activity of a variable. + uint32_t var_inc; // Amount to bump next variable 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; @@ -370,18 +368,19 @@ inline void Solver::insertVarOrder(Var x) inline void Solver::varDecayActivity() { - var_inc *= var_decay; + var_inc *= 11; + var_inc /= 10; } inline void Solver::varBumpActivity(Var v) { - if ( (activity[v] += var_inc) > 1e100 ) { + if ( (activity[v] += var_inc) > (0x1U) << 24 ) { //printf("RESCALE!!!!!!\n"); //std::cout << "var_inc: " << var_inc << std::endl; // Rescale: for (Var var = 0; var != nVars(); var++) { - activity[var] *= 1e-95; + activity[var] >>= 14; } - var_inc *= 1e-100; + var_inc >>= 14; //var_inc = 1; //std::cout << "var_inc: " << var_inc << std::endl; diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp index f0c9492..40152cd 100644 --- a/src/sat/cryptominisat2/Subsumer.cpp +++ b/src/sat/cryptominisat2/Subsumer.cpp @@ -701,7 +701,7 @@ void Subsumer::fillCannotEliminate() cannot_eliminate[c[i2].var()] = true; } - const vector& tmp2 = solver.conglomerate->getRemovedVars(); + const vec& tmp2 = solver.conglomerate->getRemovedVars(); for (uint32_t i = 0; i < tmp2.size(); i++) { if (tmp2[i]) cannot_eliminate[i] = true; } diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 053ca7f..f3f456b 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,3 +1,2 @@ CryptoMiniSat -GIT revision: fb3f0713d5864d50cae28535b577fb74fd65899c - +GIT revision: 3c04fa48505107a294986a85131b05a67c479ba1 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index 9e36ca3..e499ac4 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -93,7 +93,7 @@ const bool VarReplacer::performReplaceInternal() #endif Var var = 0; - const vector& removedVars = solver.conglomerate->getRemovedVars(); + const vec& removedVars = solver.conglomerate->getRemovedVars(); const vec& removedVars2 = solver.partHandler->getSavedState(); const vec& removedVars3 = solver.subsumer->getVarElimed(); for (vector::const_iterator it = table.begin(); it != table.end(); it++, var++) { @@ -105,8 +105,8 @@ const bool VarReplacer::performReplaceInternal() solver.setDecisionVar(var, false); solver.setDecisionVar(it->var(), true); - double& activity1 = solver.activity[var]; - double& activity2 = solver.activity[it->var()]; + uint32_t& activity1 = solver.activity[var]; + uint32_t& activity2 = solver.activity[it->var()]; if (wasDecisionVar && activity1 > activity2) { activity2 = activity1; solver.order_heap.update(it->var());