From: msoos Date: Tue, 8 Dec 2009 20:28:16 +0000 (+0000) Subject: Updating CryptoMiniSat to r594. dynamicRestarts is now an option X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=953bc629e8276e624ef417a6a5862b80023b291a;p=francis%2Fstp.git Updating CryptoMiniSat to r594. dynamicRestarts is now an option git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@488 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/BoundedQueue.h b/src/sat/cryptominisat2/BoundedQueue.h new file mode 100644 index 0000000..595da0b --- /dev/null +++ b/src/sat/cryptominisat2/BoundedQueue.h @@ -0,0 +1,78 @@ +/*****************************************************************************************[Queue.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + 2008 - Gilles Audemard, Laurent Simon + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef BoundedQueue_h +#define BoundedQueue_h + +#include "Vec.h" + +//================================================================================================= + + +template +class bqueue { + vec elems; + int first; + int last; + unsigned long long sumofqueue; + int maxsize; + int queuesize; // Number of current elements (must be < maxsize !) + +public: + bqueue(void) : first(0), last(0), sumofqueue(0), maxsize(0), queuesize(0) { } + + void initSize(int size) {growTo(size);} // Init size of bounded size queue + + void push(T x) { + if (queuesize==maxsize) { + assert(last==first); // The queue is full, next value to enter will replace oldest one + sumofqueue -= elems[last]; + if ((++last) == maxsize) last = 0; + } else + queuesize++; + sumofqueue += x; + elems[first] = x; + if ((++first) == maxsize) first = 0; + } + + T peek() { assert(queuesize>0); return elems[last]; } + void pop() {sumofqueue-=elems[last]; queuesize--; if ((++last) == maxsize) last = 0;} + + unsigned long long getsum() const {return sumofqueue;} + unsigned int getavg() const {return (unsigned int)(sumofqueue/((unsigned long long)queuesize));} + int isvalid() const {return (queuesize==maxsize);} + + void growTo(int size) { + elems.growTo(size); + first=0; maxsize=size; queuesize = 0; + for(int i=0;i 1) return false; - tmp >>= 1; - } - } - return popcount; -} - -bool PackedRow::popcnt_is_one(uint from) const -{ - from++; - for (uint i = from/64; i < size; i++) if (mp[i]) { - uint64_t tmp = mp[i]; - uint i2; - if (i == from/64) { - i2 = from%64; - tmp >>= i2; - } else - i2 = 0; - for (; i2 < 64; i2++) { - if (tmp & 1) return false; - tmp >>= 1; - } - } - return true; + return (!std::equal(b.mp-1, b.mp+size, mp-1)); } uint PackedRow::popcnt() const @@ -99,7 +66,7 @@ uint PackedRow::popcnt() const uint PackedRow::popcnt(const uint from) const { uint popcnt = 0; - for (uint i = from/64; i < size; i++) if (mp[i]) { + for (uint i = from/64; i != size; i++) if (mp[i]) { uint64_t tmp = mp[i]; uint i2; if (i == from/64) { @@ -115,33 +82,6 @@ uint PackedRow::popcnt(const uint from) const return popcnt; } -PackedRow& PackedRow::operator=(const PackedRow& b) -{ - #ifdef DEBUG_ROW - assert(size > 0); - assert(b.size > 0); - assert(size == b.size); - #endif - - memcpy(mp-1, b.mp-1, size+1); - return *this; -} - -PackedRow& PackedRow::operator^=(const PackedRow& b) -{ - #ifdef DEBUG_ROW - assert(size > 0); - assert(b.size > 0); - assert(b.size == size); - #endif - - for (uint i = 0; i < size; i++) { - mp[i] ^= b.mp[i]; - } - xor_clause_inverted ^= !b.xor_clause_inverted; - return *this; -} - void PackedRow::fill(vec& tmp_clause, const vec& assigns, const vector& col_to_var_original) const { bool final = xor_clause_inverted; diff --git a/src/sat/cryptominisat2/PackedRow.h b/src/sat/cryptominisat2/PackedRow.h index cad82b3..aa94192 100644 --- a/src/sat/cryptominisat2/PackedRow.h +++ b/src/sat/cryptominisat2/PackedRow.h @@ -45,11 +45,84 @@ class PackedRow public: bool operator ==(const PackedRow& b) const; bool operator !=(const PackedRow& b) const; - PackedRow& operator=(const PackedRow& b); + + PackedRow& operator=(const PackedRow& b) + { + #ifdef DEBUG_ROW + assert(size > 0); + assert(b.size > 0); + assert(size == b.size); + #endif + + memcpy(mp-1, b.mp-1, size+1); + return *this; + } + + PackedRow& operator^=(const PackedRow& b) + { + #ifdef DEBUG_ROW + assert(size > 0); + assert(b.size > 0); + assert(b.size == size); + #endif + + uint64_t * __restrict mp1 = mp; + uint64_t * __restrict mp2 = b.mp; + + for (uint i = 0; i != size; i++) { + *(mp1 + i) ^= *(mp2 + i); + } + xor_clause_inverted ^= !b.xor_clause_inverted; + return *this; + } + + uint popcnt() const; uint popcnt(uint from) const; - bool popcnt_is_one() const; - bool popcnt_is_one(uint from) const; + + bool popcnt_is_one() const + { + char popcount = 0; + for (uint i = 0; i != size; i++) if (mp[i]) { + uint64_t tmp = mp[i]; + for (uint i2 = 0; i2 != 64; i2 += 4) { + popcount += tmp & 1; + popcount += tmp & 2; + popcount += tmp & 4; + popcount += tmp & 8; + if (popcount > 1) return false; + tmp >>= 4; + } + } + return popcount; + } + + bool popcnt_is_one(uint from) const + { + from++; + + uint64_t tmp = mp[from/64]; + tmp >>= from%64; + for (uint i2 = from%64; i2 < 64; i2 += 4) { + if (tmp & 1) return false; + if (tmp & 2) return false; + if (tmp & 4) return false; + if (tmp & 8) return false; + tmp >>= 4; + } + + for (uint i = from/64+1; i != size; i++) if (mp[i]) { + tmp = mp[i]; + for (uint i2 = 0; i2 != 64; i2 += 4) { + if (tmp & 1) return false; + if (tmp & 2) return false; + if (tmp & 4) return false; + if (tmp & 8) return false; + tmp >>= 4; + } + } + return true; + } inline const uint64_t& get_xor_clause_inverted() const { @@ -60,7 +133,7 @@ public: { const uint64_t* mp2 = (const uint64_t*)mp; - for (uint i = 0; i < size; i++) { + for (uint i = 0; i != size; i++) { if (mp2[i]) return false; } return true; @@ -94,15 +167,16 @@ public: assert(b.size == size); #endif + uint64_t * __restrict mp1 = mp; + uint64_t * __restrict mp2 = b.mp; + for (int i = -1; i != size; i++) { - uint64_t tmp(*(b.mp + i)); - *(b.mp + i) = *(mp + i); + uint64_t tmp(*(mp2 + i)); + *(mp2 + i) = *(mp + i); *(mp + i) = tmp; } } - PackedRow& operator^=(const PackedRow& b); - inline const bool operator[](const uint& i) const { #ifdef DEBUG_ROW @@ -118,7 +192,7 @@ public: assert(size == (matrix_size/64) + ((bool)(matrix_size % 64))); //mp = new uint64_t[size]; setZero(); - for (uint i = 0; i < v.size(); i++) { + for (uint i = 0; i != v.size(); i++) { const uint toset_var = var_to_col[v[i].var()]; assert(toset_var != UINT_MAX); @@ -136,7 +210,7 @@ public: assert(size > 0); #endif - for(uint i = var; i < size*64; i++) + for(uint i = var; i != size*64; i++) if (this->operator[](i)) return i; return ULONG_MAX; } diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index 490d6c5..e76028c 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -61,6 +61,7 @@ Solver::Solver() : , xorFinder (true) , performReplace (true) , greedyUnbound (false) + , dynamicRestarts (false) // Statistics: (formerly in 'SolverStats') // @@ -1131,14 +1132,27 @@ lbool Solver::search(int nof_conflicts) llbool Solver::new_decision(int& nof_conflicts, int& conflictC) { - if (nof_conflicts >= 0 && conflictC >= nof_conflicts) { - // Reached bound on number of conflicts: - progress_estimate = progressEstimate(); - cancelUntil(0); - if (dynamic_behaviour_analysis) { - logger.end(Logger::restarting); + + // Reached bound on number of conflicts? + if (dynamicRestarts) { + if (nbDecisionLevelHistory.isvalid() && + ((nbDecisionLevelHistory.getavg()*0.7) > (totalSumOfDecisionLevel / conf4Stats))) { + nbDecisionLevelHistory.fastclear(); + progress_estimate = progressEstimate(); + cancelUntil(0); + if (dynamic_behaviour_analysis) { + logger.end(Logger::restarting); + } + return l_Undef; + } + } else { + if (nof_conflicts >= 0 && conflictC >= nof_conflicts) { + progress_estimate = progressEstimate(); + cancelUntil(0); + if (dynamic_behaviour_analysis) + logger.end(Logger::restarting); + return l_Undef; } - return l_Undef; } // Simplify the set of problem clauses: @@ -1223,6 +1237,10 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf learnt_clause.clear(); analyze(confl, learnt_clause, backtrack_level, nbLevels); conf4Stats++; + if (dynamicRestarts) { + nbDecisionLevelHistory.push(nbLevels); + totalSumOfDecisionLevel += nbLevels; + } if (dynamic_behaviour_analysis) logger.conflict(Logger::simple_confl_type, backtrack_level, confl->group, learnt_clause); @@ -1255,6 +1273,7 @@ llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conf learnts.push(c); c->setActivity(nbLevels); // LS if (nbLevels <= 2) nbDL2++; + if (c->size() == 2) nbBin++; attachClause(*c); uncheckedEnqueue(learnt_clause[0], c); @@ -1319,6 +1338,11 @@ lbool Solver::solve(const vec& assumps) model.clear(); conflict.clear(); + if (dynamicRestarts) { + nbDecisionLevelHistory.fastclear(); + nbDecisionLevelHistory.initSize(100); + totalSumOfDecisionLevel = 0; + } if (!ok) return l_False; diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index 9cba2cf..5c407d9 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -36,6 +36,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "GaussianConfig.h" #include "Logger.h" #include "constants.h" +#include "BoundedQueue.h" #ifdef _MSC_VER #include @@ -98,6 +99,7 @@ public: void needRealUnknowns(); // Uses the "real unknowns" set by setRealUnknown void setRealUnknown(const uint var); //sets a variable to be 'real', i.e. to preferentially branch on it during solving (when useRealUnknown it turned on) void setMaxRestarts(const uint num); //sets the maximum number of restarts to given value + void set_gaussian_decision_until(const uint to); template void removeWatchedCl(vec &ws, const Clause *c); template @@ -140,9 +142,8 @@ public: bool xorFinder; // Automatically find xor-clauses and convert them bool performReplace; // Should var-replacing be performed? friend class FindUndef; - bool greedyUnbound; //If set to TRUE, then we will greedily unbound variables (set them to l_Undef) - void set_gaussian_decision_until(const uint to); - void set_gaussian_decision_from(const uint from); + bool greedyUnbound; //If set, then variables will be greedily unbounded (set to l_Undef) + bool dynamicRestarts; // If set to true, the restart strategy will be dynamic enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 }; @@ -223,6 +224,8 @@ protected: Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. double progress_estimate;// Set by 'search()'. bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. + bqueue nbDecisionLevelHistory; // Set of last decision level in conflict clauses + float totalSumOfDecisionLevel; MTRand mtrand; // random number generator Logger logger; // dynamic logging, statistics friend class Logger; diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 7de8163..9476115 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,3 +1,3 @@ CryptoMiniSat -SVN revision: 586 -GIT revision: 8b5929ba71ceaf5bf6c905436cde96e640bee4b7 +SVN revision: 594 +GIT revision: 4b4477ffe685caf5a034f65063c93c20929440f8