Skip to content

Commit

Permalink
Rework dynamic/blocked restarts.
Browse files Browse the repository at this point in the history 
* add support for different moving averages
* add support for keeping ema on restart/block
* drop "User" schedule in favor of dedicated Dynamic options
* fix overflow handling in ScheduleStrategy
  • Loading branch information
@BenKaufmann
BenKaufmann committed Apr 5, 2024
1 parent 67f1793 commit 9b1713b
Show file tree
Hide file tree
Showing 10 changed files with 449 additions and 187 deletions.
35 changes: 20 additions & 15 deletions clasp/cli/clasp_cli_options.inl
View file
Original file line number Diff line number Diff line change
@@ -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/
//
Expand Down Expand Up @@ -352,7 +352,9 @@ OPTION(restarts, "!,r", ARG(arg("<sched>")), "Configure restart policy\n" \
" D,<n>,<f>: Restart based on moving LBD average over last <n> conflicts\n" \
" Mavg(<n>,LBD)*<f> > avg(LBD)\n" \
" use conflict level average if <lim> > 0 and avg(LBD) > <lim>\n"\
" no|0 : Disable restarts", FUN(arg) { return ITE(arg.off(), (SELF.disable(),true), arg>>SELF.sched);}, GET(SELF.sched))
" no|0 : Disable restarts", FUN(arg) { RestartParams::Dynamic dyn = {0}; char s; \
return ITE(arg.off(), (SELF.disable(),true), ITE(arg.peek() == 'd' || arg.peek() == 'D', (arg>>s>>dyn && dyn.base && (SELF.setDynamic(dyn),true)), arg>>SELF.rsSched));},\
GET_FUN(str) { ITE(SELF.disabled(), str<<off, ITE(SELF.dynamic(), str << "d" << SELF.rsDynamic(), str << SELF.rsSched));})
OPTION(reset_restarts , ",@2", ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(RestartParams::SeqUpdate, \
MAP("no",RestartParams::seq_continue), MAP("repeat", RestartParams::seq_repeat), MAP("disable", RestartParams::seq_disable))),\
"Update restart seq. on model {no|repeat|disable}",\
Expand All @@ -365,16 +367,19 @@ OPTION(counter_restarts, "" , ARG(arg("<arg>")), "Use counter implication rest
FUN(arg) { uint32 n = 0; uint32 m = SELF.counterBump; \
return (arg.off() || (arg >> n >> opt(m) && n > 0)) && SET_OR_FILL(SELF.counterRestart, n) && SET_OR_FILL(SELF.counterBump, m); },\
GET_IF(SELF.counterRestart, SELF.counterRestart, SELF.counterBump))
OPTION(block_restarts , "" , ARG(arg("<arg>")), "Use glucose-style blocking restarts\n" \
" %A: <n>[,<R {1.0..5.0}>][,<c>]\n" \
" <n>: Window size for moving average (0=disable blocking)\n" \
" <R>: Block restart if assignment > average * <R> [1.4]\n" \
" <c>: Disable blocking for the first <c> conflicts [10000]\n", FUN(arg) { \
uint32 n = 0; double R = 0.0; uint32 x = 0;\
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_restarts , "" , ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(MovingAvg::Type, \
MAP("d", MovingAvg::avg_sma), MAP("e", MovingAvg::avg_ema), MAP("l", MovingAvg::avg_ema_log), \
MAP("es", MovingAvg::avg_ema_smooth), MAP("ls", MovingAvg::avg_ema_log_smooth))),\
"Use glucose-style blocking restarts\n" \
" %A: <n>[,<R {1.0..5.0}>][,<c>][,<a>]\n" \
" <n>: Window size for moving average (0=disable blocking)\n" \
" <R>: Block restart if assignment > average * <R> [1.4]\n" \
" <c>: Disable blocking for the first <c> conflicts [10000]\n" \
" <a>: Type of moving average [e]\n", \
FUN(arg) { uint32 n = 0; float R = 1.4; uint32 c = 10000; MovingAvg::Type a = MovingAvg::avg_ema; \
return ITE(arg.off(), (SELF.block=RestartParams::Block(), true), arg>>n>>opt(R)>>opt(c)>>opt(a) && SET_GEQ(SELF.block.window, n, 1) \
&& R >= 1.0 && R <= 5.0 && SET(SELF.block.fscale, static_cast<uint32>(R*100.0f)) && SET(SELF.block.first, c) && SET(SELF.block.avg, a)); },\
GET_FUN(str) { ITE(!SELF.block.window, str<<off, str<<SELF.block.window<<SELF.block.scale()<<SELF.block.first<<static_cast<MovingAvg::Type>(SELF.block.avg)); })
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))
Expand Down Expand Up @@ -410,11 +415,11 @@ OPTION(del_grow , "!", NO_ARG, "Configure size-based deletion policy\n" \
" <sched> : Set grow schedule (<type {F|L|x|+}>) [grow on restart]", FUN(arg){ double f; double g; ScheduleStrategy sc = ScheduleStrategy::def();\
return ITE(arg.off(), (SELF.growSched = ScheduleStrategy::none(), SELF.fGrow = 0.0f, true),\
arg>>f>>opt(g = 3.0)>>opt(sc) && SET_R(SELF.fGrow, (float)f, 1.0f, FLT_MAX) && SET_R(SELF.fMax, (float)g, 0.0f, FLT_MAX)\
&& (sc.defaulted() || !sc.user()) && (SELF.growSched=sc, true));},\
&& (SELF.growSched=sc, true));},\
GET_FUN(str) { if (SELF.fGrow == 0.0f) str<<off; else { str<<SELF.fGrow<<SELF.fMax; if (!SELF.growSched.disabled()) str<<SELF.growSched;}})
OPTION(del_cfl , "!", ARG(arg("<sched>")), "Configure conflict-based deletion policy\n" \
" %A: <type {F|L|x|+}>,<args>... (see restarts)", FUN(arg){\
return ITE(arg.off(), (SELF.cflSched=ScheduleStrategy::none()).disabled(), arg>>SELF.cflSched && !SELF.cflSched.user());}, GET(SELF.cflSched))
return ITE(arg.off(), (SELF.cflSched=ScheduleStrategy::none()).disabled(), arg>>SELF.cflSched);}, GET(SELF.cflSched))
OPTION(del_init , "" , ARG(defaultsTo("3.0")->state(Value::value_defaulted)), "Configure initial deletion limit\n"\
" %A: <f>[,<n>,<o>] (<f> > 0)\n" \
" <f> : Set initial limit to P=estimated problem size/<f> [%D]\n" \
Expand Down Expand Up @@ -493,7 +498,7 @@ OPTION(global_restarts, ",@1", ARG(arg("<X>")), "Configure global restart policy
" <n> : Maximal number of global restarts (0=disable)\n" \
" <sched>: Restart schedule [x,100,1.5] (<type {F|L|x|+}>)\n", FUN(arg) {\
return ITE(arg.off(), (SELF.restarts = SolveOptions::GRestarts(), true), arg>>SELF.restarts.maxR>>opt(SELF.restarts.sched = ScheduleStrategy())\
&& SELF.restarts.maxR && !SELF.restarts.sched.user());},\
&& SELF.restarts.maxR);},\
GET_IF(SELF.restarts.maxR, SELF.restarts.maxR, SELF.restarts.sched))
OPTION(distribute, "!,@1", ARG_EXT(defaultsTo("conflict,global,4"), \
DEFINE_ENUM_MAPPING(Distributor::Policy::Types, MAP("all", Distributor::Policy::all), MAP("short", Distributor::Policy::implicit), MAP("conflict", Distributor::Policy::conflict), MAP("loop" , Distributor::Policy::loop))\
Expand Down
66 changes: 42 additions & 24 deletions clasp/solver_strategies.h
View file
Original file line number Diff line number Diff line change
@@ -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/
//
Expand Down Expand Up @@ -68,7 +68,7 @@ namespace Clasp {
struct ScheduleStrategy {
public:
//! Supported strategies.
enum Type { Geometric = 0, Arithmetic = 1, Luby = 2, User = 3 };
enum Type { Geometric = 0, Arithmetic = 1, Luby = 2 };

ScheduleStrategy(Type t = Geometric, uint32 b = 100, double g = 1.5, uint32 o = 0);
//! Creates luby's sequence with unit-length unit and optional outer limit.
Expand All @@ -80,12 +80,11 @@ struct ScheduleStrategy {
//! Creates fixed sequence with length base.
static ScheduleStrategy fixed(uint32 base) { return ScheduleStrategy(Arithmetic, base, 0, 0); }
static ScheduleStrategy none() { return ScheduleStrategy(Geometric, 0); }
static ScheduleStrategy def() { return ScheduleStrategy(User, 0, 0.0); }
static ScheduleStrategy def() { return ScheduleStrategy(Arithmetic, 0); }
uint64 current() const;
bool disabled() const { return base == 0; }
bool defaulted()const { return base == 0 && type == User; }
bool user() const { return base != 0 && type == User; }
void reset() { idx = 0; }
bool defaulted()const { return base == 0 && type == Arithmetic; }
void reset() { idx = 0; }
uint64 next();
void advanceTo(uint32 idx);
uint32 base : 30; // base of sequence (n1)
Expand Down Expand Up @@ -281,26 +280,45 @@ typedef Range<uint32> Range32;
* \see ScheduleStrategy
*/
struct RestartParams {
RestartParams();
typedef ScheduleStrategy Schedule;
enum SeqUpdate { seq_continue = 0, seq_repeat = 1, seq_disable = 2 };
struct Dynamic {
uint32 base;
float k;
uint32 lim;
uint32 fast : 3;
uint32 keep : 2;
uint32 slow : 3;
uint32 sWin : 24;
};
RestartParams();
uint32 prepare(bool withLookback);
void disable();
bool dynamic() const { return sched.user(); }
bool local() const { return cntLocal != 0; }
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. */
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? */
bool disabled() const { return base() == 0; }
bool dynamic() const { return rsSched.type == 3u; }
bool local() const { return cntLocal != 0; }
SeqUpdate update() const { return static_cast<SeqUpdate>(upRestart); }
uint32 base() const { return rsSched.base; }
float dynK() const;
uint32 dynLim() const;
void setDynamic(const Dynamic&);
Schedule schedule() const;
Dynamic rsDynamic()const;
Schedule rsSched;
struct Block {
float scale() const { return static_cast<float>(fscale) / 100.0f; }
uint32 window : 23; /**< Size of moving assignment average for blocking restarts (0: disable). */
uint32 fscale : 9; /**< Scaling factor for blocking restarts. */
uint32 first : 29; /**< Disable blocking restarts for first conflicts. */
uint32 avg : 3; /**< Use avg strategy (see MovingAvg::Type) */
} block; /**< Blocking restarts options. */
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). */
uint32 upRestart : 2; /**< How to update restart sequence after a model was found (one of SeqUpdate). */
uint32 cntLocal : 1; /**< Count conflicts globally or relative to current branch? */
uint32 shuffle :14; /**< Shuffle program after shuffle restarts (0: disable). */
uint32 shuffleNext :14; /**< Re-Shuffle program every shuffleNext restarts (0: disable). */
uint32 upRestart : 2; /**< How to update restart sequence after a model was found (one of SeqUpdate). */
uint32 cntLocal : 1; /**< Count conflicts globally or relative to current branch? */
};

//! Reduce strategy used during solving.
Expand Down Expand Up @@ -379,8 +397,8 @@ struct ReduceParams {
Range32 sizeInit(const SharedContext& ctx) const;
uint32 cflInit(const SharedContext& ctx) const;
uint32 getBase(const SharedContext& ctx) const;
float fReduce() const { return strategy.fReduce / 100.0f; }
float fRestart() const { return strategy.fRestart/ 100.0f; }
float fReduce() const { return static_cast<float>(strategy.fReduce) / 100.0f; }
float fRestart() const { return static_cast<float>(strategy.fRestart)/ 100.0f; }
static uint32 getLimit(uint32 base, double f, const Range<uint32>& r);
ScheduleStrategy cflSched; /**< Conflict-based deletion schedule. */
ScheduleStrategy growSched; /**< Growth-based deletion schedule. */
Expand Down
80 changes: 37 additions & 43 deletions clasp/solver_types.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,19 +70,18 @@ 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 };
//! 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();
enum Type { lbd_limit, level_limit };
enum Keep { keep_never = 0, keep_restart = 1, keep_block = 2, keep_always = 3 };
//! Creates new limit with moving average of the given window size.
DynamicLimit(uint32 window, MovingAvg::Type fast, Keep keep, MovingAvg::Type slow, uint32 slowWin = 0);

//! Resets moving average and adjust limit.
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 init(float k, Type type, uint32 uLimit = 16000);
//! Resets current run - depending on the Keep strategy this also clears the moving average.
void resetBlock();
//! Resets moving and global average.
void reset();
Expand All @@ -99,16 +98,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_.win() && (movingAverage() * adjust.rk) > globalAverage(); }
struct {
//! Returns the average restart length, i.e. number of conflicts between restarts.
double avgRestart() const { return ratio(samples, restarts); }
Expand All @@ -118,20 +109,27 @@ 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 global_.avg(adjust.type); }
double movingAverage() const { return avg_.get(); }
private:
DynamicLimit(uint32 size);
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(MovingAvg::Type type, uint32 size = 0);
//! Returns the global lbd or conflict level average.
double avg(Type t) const { return (t == lbd_limit ? lbd : cfl).get(); }
void reset() {
lbd.clear();
cfl.clear();
}
MovingAvg lbd; //!< Moving average of lbds
MovingAvg cfl; //!< Moving average of conflict levels
} global_; //!< Global lbd/conflict level data.
MovingAvg avg_; //!< (Fast) moving average.
uint32 num_; //!< Number of samples in this run.
Keep keep_; //!< Strategy for keeping fast moving average.
};

//! Type for implementing Glucose-style blocking of restarts.
Expand All @@ -140,22 +138,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, MovingAvg::Type t = MovingAvg::Type::avg_ema);
bool push(uint32 nAssign) {
ema = n >= span
? exponentialMovingAverage(ema, nAssign, alpha)
: cumulativeMovingAverage(ema, nAssign, n);
avg.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 avg.get() * r; }
MovingAvg avg; //!< 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 moving average.
};
///////////////////////////////////////////////////////////////////////////////
// Statistics
Expand Down Expand Up @@ -301,7 +295,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);
Expand Down
Loading

0 comments on commit 9b1713b

Please sign in to comment.