--- /dev/null
+/*****************************************************************************************[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 T>
+class bqueue {
+ vec<T> 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<size;i++) elems[i]=0;
+ }
+
+ void fastclear() {first = 0; last = 0; queuesize=0; sumofqueue=0;} // to be called after restarts... Discard the queue
+
+ int size(void) { return queuesize; }
+
+ void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;}
+
+
+};
+
+//=================================================================================================
+#endif
return;
if (varnames.size() <= var) {
- varnames.resize(var+1);
+ varnames.resize(var+1, "Noname");
times_var_propagated.resize(var+1, 0);
times_var_guessed.resize(var+1, 0);
depths_of_assigns_for_var.resize(var+1);
}
- std::stringstream ss;
- ss << var + 1;
- varnames[var] = ss.str();
}
// Resizes the groupnames and other, related vectors to accomodate for a new group
new_var(var);
cut_name_to_size(name);
- std::stringstream ss;
- ss << var + 1;
- if (varnames[var] == ss.str()) {
+ if (varnames[var] == "Noname") {
varnames[var] = name;
} else if (varnames[var] != name) {
printf("Error! Variable no. %d has been named twice. First, as '%s', then second as '%s'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line\n", var+1, varnames[var].c_str(), name.c_str());
cout << "+" << std::setfill('=') << std::setw(fullwidth) << "=" << std::setfill(' ') << "+" << endl;
cout.setf(std::ios_base::left);
- cout.precision(4);
+ cout.precision(2);
print_statistics_note();
print_times_var_guessed();
print_times_group_caused_propagation();
assert(size == b.size);
#endif
- return (std::equal(b.mp-1, b.mp+size, mp-1));
-}
-
-bool PackedRow::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++) {
- popcount += tmp & 1;
- if (popcount > 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
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) {
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<Lit>& tmp_clause, const vec<lbool>& assigns, const vector<Var>& col_to_var_original) const
{
bool final = xor_clause_inverted;
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
{
{
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;
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
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);
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;
}
, xorFinder (true)
, performReplace (true)
, greedyUnbound (false)
+ , dynamicRestarts (false)
// Statistics: (formerly in 'SolverStats')
//
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:
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);
learnts.push(c);
c->setActivity(nbLevels); // LS
if (nbLevels <= 2) nbDL2++;
+ if (c->size() == 2) nbBin++;
attachClause(*c);
uncheckedEnqueue(learnt_clause[0], c);
model.clear();
conflict.clear();
+ if (dynamicRestarts) {
+ nbDecisionLevelHistory.fastclear();
+ nbDecisionLevelHistory.initSize(100);
+ totalSumOfDecisionLevel = 0;
+ }
if (!ok) return l_False;
#include "GaussianConfig.h"
#include "Logger.h"
#include "constants.h"
+#include "BoundedQueue.h"
#ifdef _MSC_VER
#include <ctime>
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<class T>
void removeWatchedCl(vec<T> &ws, const Clause *c);
template<class T>
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 };
Heap<VarOrderLt> 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<unsigned int> nbDecisionLevelHistory; // Set of last decision level in conflict clauses
+ float totalSumOfDecisionLevel;
MTRand mtrand; // random number generator
Logger logger; // dynamic logging, statistics
friend class Logger;
CryptoMiniSat
-SVN revision: 586
-GIT revision: 8b5929ba71ceaf5bf6c905436cde96e640bee4b7
+SVN revision: 594
+GIT revision: 4b4477ffe685caf5a034f65063c93c20929440f8
projects / francis / stp.git / commitdiff