WIP

potassco · Apr 2, 2024 · 5727211 · 5727211
1 parent db5fce9
commit 5727211
Show file tree

Hide file tree

Showing 10 changed files with 266 additions and 103 deletions.
diff --git a/clasp/cli/clasp_cli_options.inl b/clasp/cli/clasp_cli_options.inl
@@ -1,5 +1,5 @@
 //
-// Copyright (c) 2013-2017 Benjamin Kaufmann
+// Copyright (c) 2013-present Benjamin Kaufmann
 //
 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
 //
@@ -374,7 +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(block_ema       , "!,@3", ARG(implicit("1")->arg("{0..3}")), "Use ema strategy for blocking", STORE_LEQ(SELF.blockEmaQ, 3u), GET(SELF.blockEmaQ))
 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))

diff --git a/clasp/solver_strategies.h b/clasp/solver_strategies.h
@@ -1,5 +1,5 @@
 //
-// Copyright (c) 2006-2017 Benjamin Kaufmann
+// Copyright (c) 2006-present Benjamin Kaufmann
 //
 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
 //
@@ -290,12 +290,12 @@ struct RestartParams {
 	SeqUpdate update()  const { return static_cast<SeqUpdate>(upRestart); }
 	ScheduleStrategy sched;  /**< Restart schedule to use. */
 	float  blockScale;       /**< Scaling factor for blocking restarts. */
-	uint32 blockWindow: 16;  /**< Size of moving assignment average for blocking restarts (0: disable). */
-	uint32 blockFirst : 16;  /**< Enable blocking restarts after blockFirst conflicts. */
+	uint32 blockWindow: 15;  /**< Size of moving assignment average for blocking restarts (0: disable). */
+	uint32 blockFirst : 15;  /**< Enable blocking restarts after blockFirst conflicts. */
+	uint32 blockEmaQ  :  2;  /**< Use EMA strategy (see AvgQueue::EmaFlag) */
 	CLASP_ALIGN_BITFIELD(uint32)
-	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? */
+	uint32 counterRestart:16;/**< Apply counter implication bump every counterRestart restarts (0: disable). */
+	uint32 counterBump:16;   /**< Bump factor for counter implication restarts. */
 	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). */

diff --git a/clasp/solver_types.h b/clasp/solver_types.h
@@ -70,18 +70,19 @@ struct SearchLimits {
 //! Type for implementing Glucose-style dynamic restarts.
 /*!
  * \see  G. Audemard, L. Simon. "Refining Restarts Strategies for SAT and UNSAT"
- * \note In contrast to Glucose's dynamic restarts, this class also implements
- * a heuristic for dynamically adjusting the margin ratio K.
+ * \note In contrast to Glucose's dynamic restarts, this class also implements a heuristic for
+ *       dynamically adjusting the margin ratio K.
  */
 struct DynamicLimit {
-	enum Type   { lbd_limit, level_limit };
-	enum QStrat { keep_never = 0, keep_restart = 1, keep_block = 2, keep_always = 3 };
+	enum Type  { lbd_limit, level_limit };
+	enum Keep  { keep_never = 0, keep_restart = 1, keep_block = 2, keep_always = 3 };
+	enum QType { q_default = 0, q_ema = 1, q_ema_log = 2, q_ema_smooth = 3, q_ema_log_smooth = 4 };
 	//! Creates new limit with bounded queue of the given window size.
-	static DynamicLimit* create(uint32 window);
+	static DynamicLimit* create(uint32 window, Keep keep, QType local, QType global, uint32 globalWin = 0);
 	//! Destroys this object and its bounded queue.
 	void   destroy();
 	//! Resets moving average and adjust limit.
-	void   init(float k, Type type, QStrat strat, uint32 uLimit = 16000);
+	void   init(float k, Type type, uint32 uLimit = 16000);
 	//! Resets current run - depending on the queue strategy this also clears the bounded queue.
 	void   resetBlock();
 	//! Resets moving and global average.
@@ -99,16 +100,8 @@ struct DynamicLimit {
 	uint32 restart(uint32 maxLBD, float k);
 	//! Returns the number of updates since last restart.
 	uint32 runLen()  const { return num_;  }
-	//! Returns the maximal size of the bounded queue.
-	uint32 window()  const { return cap_; }
 	//! Returns whether it is time to restart.
-	bool   reached() const { return runLen() >= window() && (sma(adjust.type) * adjust.rk) > global.avg(adjust.type); }
-	struct {
-		//! Returns the global lbd or conflict level average.
-		double avg(Type t) const { return ratio(sum[t], samples); }
-		uint64 sum[2]; //!< Sum of lbds/conflict levels since last call to resetGlobal().
-		uint64 samples;//!< Samples since last call to resetGlobal().
-	} global; //!< Global lbd/conflict level data.
+	bool   reached() const { return runLen() >= avg_.lim() && (localAverage() * adjust.rk) > globalAverage(); }
 	struct {
 		//! Returns the average restart length, i.e. number of conflicts between restarts.
 		double avgRestart() const { return ratio(samples, restarts); }
@@ -118,20 +111,46 @@ struct DynamicLimit {
 		float  rk;      //!< LBD/CFL dynamic limit factor (typically < 1.0).
 		Type   type;    //!< Dynamic limit based on lbd or conflict level.
 	} adjust; //!< Data for dynamically adjusting margin ratio (rk).
+
+	double globalAverage() const {
+		return globalAverage(adjust.type);
+	}
+
+	double globalAverage(Type t) const {
+		return global_.avg(t);
+	}
+
+	double localAverage() const {
+		return avg_.get();
+	}
 private:
-	DynamicLimit(uint32 size);
+	DynamicLimit(uint32 window, Keep keep, QType local, QType global, uint32 globalWin = 0);
 	DynamicLimit(const DynamicLimit&);
 	DynamicLimit& operator=(const DynamicLimit&);
-	double sma(Type t)  const { return sum_[t] / double(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
+	void resetRun(Keep k);
+	struct Global {
+		explicit Global(QType type, uint32 size = 0);
+		//! Returns the global lbd or conflict level average.
+		double avg(Type t) const {
+			if (cma)
+				return ratio(sum[t], samples);
+			else
+				return (t == lbd_limit ? lbd : cfl).get();
+		}
+		void reset() {
+			sum[0] = sum[1] = samples = 0;
+			lbd.clear();
+			cfl.clear();
+		}
+		uint64   sum[2]; //!< Sum of lbds/conflict levels since last call to resetGlobal().
+		uint64   samples;//!< Samples since last call to resetGlobal().
+		AvgQueue lbd;    //!< EMA of lbds (if cma is false)
+		AvgQueue cfl;    //!< EMA of conflict levels (if cma is false)
+		bool     cma;    //!< Use cumulative moving average or ema?
+	} global_;           //!< Global lbd/conflict level data.
+	AvgQueue avg_;
+	uint32   num_;
+	Keep     keep_;
 };
 
 //! Type for implementing Glucose-style blocking of restarts.
@@ -140,22 +159,18 @@ POTASSCO_WARNING_END_RELAXED
  * \see A. Biere, A. Froehlich "Evaluating CDCL Restart Schemes"
  */
 struct BlockLimit {
-	explicit BlockLimit(uint32 windowSize, double R = 1.4);
+	explicit BlockLimit(uint32 windowSize, double R = 1.4, AvgQueue::EmaFlag flags = AvgQueue::EmaFlag());
 	bool push(uint32 nAssign) {
-		ema = n >= span
-			? exponentialMovingAverage(ema, nAssign, alpha)
-			: cumulativeMovingAverage(ema, nAssign, n);
+		emaQ.push(nAssign);
 		return ++n >= next;
 	}
 	//! Returns the exponential moving average scaled by r.
-	double scaled() const { return ema * r; }
-	double ema;   //!< Current exponential moving average.
-	double alpha; //!< Smoothing factor: 2/(span+1).
-	uint64 next;  //!< Enable once n >= next.
-	uint64 inc;   //!< Block restart for next inc conflicts.
-	uint64 n;     //!< Number of data points seen so far.
-	uint32 span;  //!< Minimum observation window.
-	float  r;     //!< Scale factor for ema.
+	double scaled() const { return emaQ.get() * r; }
+	AvgQueue emaQ; //!< Exponential moving average.
+	uint64   next; //!< Enable once n >= next.
+	uint64   inc;  //!< Block restart for next inc conflicts.
+	uint64   n;    //!< Number of data points seen so far.
+	float    r;    //!< Scale factor for ema.
 };
 ///////////////////////////////////////////////////////////////////////////////
 // Statistics
@@ -183,8 +198,9 @@ struct CoreStats {
 	STAT(uint64 choices;    DOXY(number of choices)     , "choices"           , VALUE(choices)    , LHS.choices    += RHS.choices   )\
 	STAT(uint64 conflicts;  DOXY(number of conflicts)   , "conflicts"         , VALUE(conflicts)  , LHS.conflicts  += RHS.conflicts )\
 	STAT(uint64 analyzed;   DOXY(number of conflicts analyzed), "conflicts_analyzed", VALUE(analyzed)   , LHS.analyzed   += RHS.analyzed  )\
-	STAT(uint64 restarts;   DOXY(number of restarts)    , "restarts"          , VALUE(restarts)   , LHS.restarts   += RHS.restarts  )\
-	STAT(uint64 lastRestart;DOXY(length of last restart), "restarts_last"     , VALUE(lastRestart), LHS.lastRestart = std::max(LHS.lastRestart, RHS.lastRestart))
+	STAT(uint64 restarts;   DOXY(number of restarts)        , "restarts"        , VALUE(restarts)   , LHS.restarts   += RHS.restarts  )\
+	STAT(uint64 lastRestart;DOXY(length of last restart)    , "restarts_last"   , VALUE(lastRestart), LHS.lastRestart = std::max(LHS.lastRestart, RHS.lastRestart)) \
+	STAT(uint64 blRestarts; DOXY(number of blocked restarts), "restarts_blocked", VALUE(blRestarts), LHS.blRestarts = std::max(LHS.blRestarts, RHS.blRestarts))
 
 	CoreStats() { reset(); }
 	void reset();
@@ -300,7 +316,7 @@ struct SolverStats : public CoreStats {
 	~SolverStats();
 	bool enableExtended();
 	bool enable(const SolverStats& o) { return !o.extra || enableExtended(); }
-	void enableLimit(uint32 size);
+	void acquireLimit(DynamicLimit* limit);
 	void reset();
 	void accu(const SolverStats& o);
 	void accu(const SolverStats& o, bool enableRhs);

diff --git a/clasp/util/misc_types.h b/clasp/util/misc_types.h
@@ -1,5 +1,5 @@
 //
-// Copyright (c) 2006-2017 Benjamin Kaufmann
+// Copyright (c) 2006-present Benjamin Kaufmann
 //
 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
 //
@@ -141,16 +141,106 @@ class RNG {
 /*!
  * Computes ema = currentEma + ((double(sample) - currentEma)*alpha);
  */
-template <class T>
-inline double exponentialMovingAverage(double currentEma, T sample, double alpha) {
-	return (static_cast<double>(sample) * alpha) + (currentEma * (1.0 - alpha));
+inline double exponentialMovingAverage(double currentEma, double sample, double alpha) {
+	return currentEma + (alpha * (sample - currentEma));
 }
 //! Updates the given moving average with the given sample.
 template <class T>
 inline double cumulativeMovingAverage(double currentAvg, T sample, uint64 numSeen) {
 	return (static_cast<double>(sample) + (currentAvg * numSeen)) / static_cast<double>(numSeen + 1);
 }
 
+class AvgQueue {
+public:
+	enum EmaFlag { ema_log = 1, ema_smooth = 2 };
+	AvgQueue(uint32 window, bool sma, EmaFlag flags) : avg_(0.0), extra_(), pos_(0), cap_(window), full_(0), cma_(0), sma_(sma) {
+		assert(window > 0 || (!sma && (flags & ema_log) == 0));
+		if (sma) {
+			void* m = ::operator new(sizeof(SmaBuffer) + (window*sizeof(uint32)));
+			extra_.sma = new (m) SmaBuffer();
+			extra_.sma->sum = 0.0;
+		}
+		else {
+			if ((flags & ema_log) == 0)
+				extra_.alpha = 2.0 / static_cast<double>(window + 1);
+			else
+				extra_.alpha = 1.0 / static_cast<double>(1u << log2(window));
+			cma_ = (flags & ema_smooth) == 0;
+		}
+	}
+
+	~AvgQueue() {
+		if (sma_)
+			::operator delete(extra_.sma);
+	}
+
+	bool push(uint32 val) {
+		sma_ ? pushSma(val) : pushEma(val);
+		if (++pos_ == cap_) { pos_ = 0; full_ = 1; }
+		return valid();
+	}
+
+	void clear() {
+		avg_  = 0.0;
+		pos_  = 0;
+		full_ = 0;
+		if (sma_)
+			extra_.sma->sum = 0.0;
+	}
+
+	double get()     const { return avg_; }
+	bool   valid()   const { return full_ != 0; }
+	uint32 lim()     const { return cap_; }
+
+private:
+	AvgQueue(const AvgQueue&);
+	AvgQueue& operator=(const AvgQueue&);
+
+	struct SmaBuffer {
+		double sum;
+		POTASSCO_WARNING_BEGIN_RELAXED
+		uint32 buffer[0];
+		POTASSCO_WARNING_END_RELAXED
+	};
+
+	void pushSma(uint32 val) {
+		assert(pos_ < cap_);
+		SmaBuffer* p = extra_.sma;
+		p->sum += static_cast<double>(val) - (valid() ? static_cast<double>(p->buffer[pos_]) : 0.0);
+		p->buffer[pos_] = val;
+		avg_ = p->sum / cap_;
+	}
+
+	void pushEma(double val) {
+		if (valid()) {
+			avg_ = exponentialMovingAverage(avg_, val, extra_.alpha);
+		}
+		else {
+			if (cma_) {
+				avg_ = cumulativeMovingAverage(avg_, val, pos_);
+			}
+			else if (pos_ < 32) {
+				double a = std::max(extra_.alpha, 1.0 / static_cast<double>(uint32(1) << pos_));
+				avg_ = exponentialMovingAverage(avg_, val, a);
+			}
+			else {
+				avg_ = exponentialMovingAverage(avg_, val, extra_.alpha);
+			}
+		}
+	}
+
+	double avg_;
+	union Extra {
+		SmaBuffer* sma; // Buffer and sum for SMA
+		double   alpha; // Smoothing factor for EMA
+	} extra_;
+	uint32 pos_;
+	uint32 cap_ : 29;
+	uint32 full_:  1; // Enough data points seen?
+	uint32 cma_ :  1; // Use cumulative moving average for first data points
+	uint32 sma_ :  1; // Simple (1) or Exponential (0) Moving Average
+};
+
 //! An unary operator function that calls p->destroy().
 struct DestroyObject {
 	template <class T> void operator()(T* p) const { if (p) p->destroy(); }

diff --git a/src/clasp_options.cpp b/src/clasp_options.cpp
@@ -269,7 +269,21 @@ static int xconvert(const char* x, ScheduleStrategy& out, const char** errPos, i
 	else if (strncmp(x, "x,", 2) == 0 || strncmp(x, "*,", 2) == 0 || strncasecmp(x, "d,", 2) == 0) {
 		std::pair<double, uint32> arg(0, 0);
 		if (*next != ',' || !xconvert(next+1, arg, &next, e)) { return 0; }
-		if      (strncasecmp(x, "d", 1) == 0 && arg.first > 0.0) { out = ScheduleStrategy(ScheduleStrategy::User, base, arg.first, arg.second); }
+		if (strncasecmp(x, "d", 1) == 0 && arg.first > 0.0 && arg.second <= 255u) {
+			uint32 keep    = 0;
+			uint32 local   = 0;
+			uint32 global  = 0;
+			uint32 globWin = 0;
+			if (*next == ',' && (!xconvert(next + 1, keep, &next, e) || keep > 3))                { return 0; }
+			if (*next == ',' && (!xconvert(next + 1, local, &next, e) || local > 4))              { return 0; }
+			if (*next == ',' && (!xconvert(next + 1, global, &next, e) || global > 4))            { return 0; }
+			if (*next == ',' && (!xconvert(next + 1, globWin, &next, e) || globWin > UINT16_MAX)) { return 0; }
+			arg.second |= keep << 8;
+			arg.second |= local << 10;
+			arg.second |= global << 13;
+			arg.second |= globWin << 16;
+			out = ScheduleStrategy(ScheduleStrategy::User, base, arg.first, arg.second);
+		}
 		else if (strncasecmp(x, "d", 1) != 0 && arg.first >= 1.0){ out = ScheduleStrategy::geom(base, arg.first, arg.second); }
 		else { return 0; }
 	}
@@ -297,7 +311,19 @@ static std::string& xconvert(std::string& out, const ScheduleStrategy& sched) {
 			else           { return out; }
 		case ScheduleStrategy::User:
 			out[t] = 'd';
-			return xconvert(out.append(1, ','), std::make_pair((double)sched.grow, sched.len));
+			xconvert(out.append(1, ','), (double)sched.grow);
+			xconvert(out.append(1, ','), sched.len & 255);
+			t = sched.len >> 8u;
+			if (t != 0) {
+				xconvert(out.append(1, ','), t & 3u);
+				t >>= 2u;
+				xconvert(out.append(1, ','), t & 7u);
+				t >>= 3u;
+				xconvert(out.append(1, ','), t & 7u);
+				t >>= 3u;
+				xconvert(out.append(1, ','), t);
+			}
+			return out;
 		default: POTASSCO_ASSERT(false, "xconvert(ScheduleStrategy): unknown type");
 	}
 }

diff --git a/src/clasp_output.cpp b/src/clasp_output.cpp
@@ -1,5 +1,5 @@
 //
-// Copyright (c) 2009-2017 Benjamin Kaufmann
+// Copyright (c) 2009-present Benjamin Kaufmann
 //
 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
 //
@@ -1188,7 +1188,7 @@ void TextOutput::printStats(const Clasp::SolverStats& st) const {
 	printf(" (Analyzed: %" PRIu64")\n", st.backjumps());
 	printKeyValue("Restarts", "%-8" PRIu64"", st.restarts);
 	if (st.restarts) {
-		printf(" (Average: %.2f Last: %" PRIu64")", st.avgRestart(), st.lastRestart);
+		printf(" (Average: %.2f Last: %" PRIu64" Blocked: %" PRIu64")", st.avgRestart(), st.lastRestart, st.blRestarts);
 	}
 	printf("\n");
 	if (!st.extra) return;