Add support for keeping dynamic restart lbd queue.

clasp/cli/clasp_cli_options.inl

@@ -374,6 +374,7 @@ OPTION(block_restarts  , ""   , ARG(arg("<arg>")), "Use glucose-style blocking r
        return (arg.off() || (arg>>n>>opt(R = 1.4)>>opt(x = 10000) && n && R >= 1.0 && R <= 5.0))\
          && SET(SELF.blockWindow, n) && SET(SELF.blockScale, (float)R) && SET_OR_FILL(SELF.blockFirst, x);},\
        GET_IF(SELF.blockWindow, SELF.blockWindow, SELF.blockScale, SELF.blockFirst))
+OPTION(dyn_queue_keep  , ",@3", ARG(arg("0..3")->implicit("0")), "Keep dynamic lbd/cfl queue", STORE_LEQ(SELF.dynStrat, 3u), GET(SELF.dynStrat))
 OPTION(shuffle         , "!"  , ARG(arg("<n1>,<n2>")), "Shuffle problem after <n1>+(<n2>*i) restarts\n", FUN(arg) { uint32 n1 = 0; uint32 n2 = 0;\
        return (arg.off() || (arg>>n1>>opt(n2) && n1)) && SET_OR_FILL(SELF.shuffle, n1) && SET_OR_FILL(SELF.shuffleNext, n2);},\
        GET_IF(SELF.shuffle, SELF.shuffle, SELF.shuffleNext))

clasp/solver_strategies.h

@@ -293,8 +293,9 @@ struct RestartParams {
 	uint32 blockWindow: 16;  /**< Size of moving assignment average for blocking restarts (0: disable). */
 	uint32 blockFirst : 16;  /**< Enable blocking restarts after blockFirst conflicts. */
 	CLASP_ALIGN_BITFIELD(uint32)
-	uint32 counterRestart:16;/**< Apply counter implication bump every counterRestart restarts (0: disable). */
-	uint32 counterBump:16;   /**< Bump factor for counter implication restarts. */
+	uint32 counterRestart:15;/**< Apply counter implication bump every counterRestart restarts (0: disable). */
+	uint32 counterBump:15;   /**< Bump factor for counter implication restarts. */
+	uint32 dynStrat   :2;    /**< Keep lbd/cfl queue on restart/block? */
 	CLASP_ALIGN_BITFIELD(uint32)
 	uint32 shuffle    :14;   /**< Shuffle program after shuffle restarts (0: disable). */
 	uint32 shuffleNext:14;   /**< Re-Shuffle program every shuffleNext restarts (0: disable). */

clasp/solver_types.h

@@ -74,15 +74,16 @@ struct SearchLimits {
  * a heuristic for dynamically adjusting the margin ratio K.
  */
 struct DynamicLimit {
-	enum Type { lbd_limit, level_limit };
+	enum Type   { lbd_limit, level_limit };
+	enum QStrat { keep_never = 0, keep_restart = 1, keep_block = 2, keep_always = 3 };
 	//! Creates new limit with bounded queue of the given window size.
 	static DynamicLimit* create(uint32 window);
 	//! Destroys this object and its bounded queue.
 	void   destroy();
 	//! Resets moving average and adjust limit.
-	void   init(float k, Type type, uint32 uLimit = 16000);
-	//! Resets moving average, i.e. clears the bounded queue.
-	void   resetRun();
+	void   init(float k, Type type, QStrat strat, uint32 uLimit = 16000);
+	//! Resets current run - depending on the queue strategy this also clears the bounded queue.
+	void   resetBlock();
 	//! Resets moving and global average.
 	void   reset();
 	//! Adds an observation and updates the moving average. Typically called on conflict.
@@ -115,18 +116,19 @@ struct DynamicLimit {
 		uint32 restarts;//!< Number of restarts since last update.
 		uint32 samples; //!< Number of samples since last update.
 		float  rk;      //!< BD/CFL dynamic limit factor (typically < 1.0).
-		Type   type;    //!< Dynamic limit based on lbd or confllict level.
+		Type   type;    //!< Dynamic limit based on lbd or conflict level.
 	} adjust; //!< Data for dynamically adjusting margin ratio (rk).
 private:
 	DynamicLimit(uint32 size);
 	DynamicLimit(const DynamicLimit&);
 	DynamicLimit& operator=(const DynamicLimit&);
 	double sma(Type t)  const { return sum_[t] / double(cap_); }
-	uint32 smaU(Type t) const { return static_cast<uint32>(sum_[t] / cap_); }
+	void resetRun(bool keepQ);
 	uint64 sum_[2];
 	uint32 cap_;
 	uint32 pos_;
 	uint32 num_;
+	QStrat qStrat_;
 POTASSCO_WARNING_BEGIN_RELAXED
 	uint32 buffer_[0];
 POTASSCO_WARNING_END_RELAXED

src/solve_algorithms.cpp

@@ -159,7 +159,7 @@ ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits*
 		sLimit = SearchLimits();
 	}
 	else if (p.restart.dynamic() && s.stats.limit) {
-		if (!nRestart) { s.stats.limit->init((float)p.restart.sched.grow, DynamicLimit::lbd_limit); }
+		if (!nRestart) { s.stats.limit->init((float)p.restart.sched.grow, DynamicLimit::lbd_limit, static_cast<DynamicLimit::QStrat>(p.restart.dynStrat)); }
 		sLimit.restart.dynamic   = s.stats.limit;
 		sLimit.restart.conflicts = s.stats.limit->adjust.limit - std::min(s.stats.limit->adjust.samples, s.stats.limit->adjust.limit - 1);
 	}

src/solver.cpp

@@ -1830,7 +1830,7 @@ ValueRep Solver::search(SearchLimits& limit, double rf) {
 				uint32 n = 1, ts;
 				do {
 					if (block && block->push(ts = numAssignedVars()) && ts > block->scaled()) {
-						if (limit.restart.dynamic) { limit.restart.dynamic->resetRun(); }
+						if (limit.restart.dynamic) { limit.restart.dynamic->resetBlock(); }
 						else                       { limit.restart.conflicts += block->inc; }
 						block->next = block->n + block->inc;
 					}

src/solver_types.cpp

@@ -48,27 +48,33 @@ DynamicLimit* DynamicLimit::create(uint32 size) {
 	void* m = ::operator new(sizeof(DynamicLimit) + (size*sizeof(uint32)));
 	return new (m)DynamicLimit(size);
 }
-DynamicLimit::DynamicLimit(uint32 sz) : cap_(sz), pos_(0), num_(0) {
+DynamicLimit::DynamicLimit(uint32 sz) : cap_(sz), pos_(0), num_(0), qStrat_(keep_never) {
 	std::memset(&global, 0, sizeof(global));
-	init(0.7f, lbd_limit);
+	init(0.7f, lbd_limit, keep_never);
 }
-void DynamicLimit::init(float k, Type t, uint32 uLimit) {
-	resetRun();
+void DynamicLimit::init(float k, Type t, QStrat strat, uint32 uLimit) {
+	resetRun((strat & keep_restart) != 0);
 	std::memset(&adjust, 0, sizeof(adjust));
 	adjust.limit = uLimit;
 	adjust.rk = k;
 	adjust.type = t;
+	qStrat_ = strat;
+}
+void DynamicLimit::resetBlock() {
+	resetRun((qStrat_ & keep_block) != 0);
 }
 void DynamicLimit::destroy() {
 	this->~DynamicLimit();
 	::operator delete(this);
 }
-void DynamicLimit::resetRun() {
-	sum_[0] = sum_[1] = pos_ = num_ = 0;
+void DynamicLimit::resetRun(bool keepQ) {
+	num_ = 0;
+	if (!keepQ)
+		sum_[0] = sum_[1] = pos_ = 0;
 }
 void DynamicLimit::reset() {
 	std::memset(&global, 0, sizeof(global));
-	resetRun();
+	resetRun(false);
 }
 void DynamicLimit::update(uint32 dl, uint32 lbd) {
 	// update global avg
@@ -100,11 +106,11 @@ uint32 DynamicLimit::restart(uint32 maxLBD, float k) {
 			else if (rLen >= 4000.0)  { rk += 0.05f; }
 			else if (rLen >= 1000.0)  { uLim += 10000u; }
 			else if (rk > k)          { rk -= 0.05f; }
-			init(rk, nt, uLim);
+			init(rk, nt, qStrat_, uLim);
 		}
-		else { init(k, nt); }
+		else { init(k, nt, qStrat_); }
 	}
-	else { resetRun(); }
+	else { resetRun((qStrat_ & keep_restart) != 0); }
 	return adjust.limit;
 }
 BlockLimit::BlockLimit(uint32 windowSize, double R)