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 restart schedule
  • Loading branch information
@BenKaufmann
BenKaufmann committed Jul 10, 2024
1 parent 6b4c499 commit 770e8d2
Show file tree
Hide file tree
Showing 11 changed files with 564 additions and 331 deletions.
61 changes: 38 additions & 23 deletions clasp/cli/clasp_cli_options.inl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -357,17 +357,28 @@ OPTION(rand_prob, "", ARG(arg("<n>[,<m>]")), "Do <n> random searches with [<m>=1
#if defined(NOTIFY_SUBGROUPS)
GROUP_BEGIN(SELF)
#endif
OPTION(restarts, "!,r", ARG(arg("<sched>")), "Configure restart policy\n" \
" %A: <type {D|F|L|x|+}>,<n {1..umax}>[,<args>][,<lim>]\n" \
" F,<n> : Run fixed sequence of <n> conflicts\n" \
" L,<n> : Run Luby et al.'s sequence with unit length <n>\n" \
" x,<n>,<f>: Run geometric seq. of <n>*(<f>^i) conflicts (<f> >= 1.0)\n" \
" +,<n>,<m>: Run arithmetic seq. of <n>+(<m>*i) conflicts (<m {0..umax}>)\n"\
" ...,<lim>: Repeat seq. every <lim>+j restarts (<type> != F)\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))
OPTION(restarts, "!,r", ARG_EXT(arg("<sched>"), DEFINE_ENUM_MAPPING(RestartSchedule::Keep, \
MAP("n", RestartSchedule::keep_never), MAP("r", RestartSchedule::keep_restart), \
MAP("b", RestartSchedule::keep_block), MAP("br", RestartSchedule::keep_always), \
MAP("rb", RestartSchedule::keep_always))), "Configure restart policy\n" \
" %A: <type {F|L|x|+}>,<n {1..umax}>[,<args>][,<lim>]\n" \
" F,<n> : Run fixed sequence of <n> conflicts\n" \
" L,<n> : Run Luby et al.'s sequence with unit length <n>\n" \
" x,<n>,<f>: Run geometric seq. of <n>*(<f>^i) conflicts (<f> >= 1.0)\n" \
" +,<n>,<m>: Run arithmetic seq. of <n>+(<m>*i) conflicts (<m {0..umax}>)\n" \
" ...,<lim>: Repeat sequence every <lim>+j restarts (<type> != F)\n" \
" %A: D,<n>,<K>[,<args>]: Dynamic restarts based on moving LBD average\n" \
" <n> : Fast moving average window size\n" \
" <K> : Fast margin (restart if fastAvg * <K> > slowAvg)\n" \
" <L> : LBD average limit [0 = none]\n" \
" <f> : Fast moving average type [d = SMA]\n" \
" d : Default\n" \
" e|l : EMA with alpha = 2/(<n>+1) or 1/log2(<n>)\n" \
" es|ls : e or l with exponentially decreasing alpha for first samples\n" \
" <k> : keep fast moving average on (r)estarts/(b)locks [n = never]\n" \
" <s> : slow moving average type [d = CMA]\n" \
" <w> : slow moving average window size (<s> != d) [200*<n>]\n" \
" no|0 : Disable restarts", FUN(arg) { return ITE(arg.off(), (SELF.disable(),true), arg>>SELF.rsSched);}, GET(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 @@ -380,15 +391,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(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 (see restarts) [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 @@ -427,11 +442,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 @@ -516,7 +531,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
1 change: 1 addition & 0 deletions clasp/solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -868,6 +868,7 @@ class Solver {
Constraint* enum_; // enumeration constraint - set by enumerator
uint64 memUse_; // memory used by learnt constraints (estimate)
Dirty* lazyRem_; // set of watch lists that contain invalid constraints
DynamicLimit* dynLimit_; // active dynamic limit
SmallClauseAlloc smallAlloc_; // allocator object for small clauses
Assignment assign_; // three-valued assignment.
DecisionLevels levels_; // information (e.g. position in trail) on each decision level
Expand Down
171 changes: 149 additions & 22 deletions clasp/solver_strategies.h
View file
Original file line number Diff line number Diff line change
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 @@ -276,30 +275,139 @@ struct SolverParams : SolverStrategies {

typedef Range<uint32> Range32;

struct RestartSchedule : ScheduleStrategy {
typedef MovingAvg::Type AvgType;
enum Keep { keep_never = 0, keep_restart = 1, keep_block = 2, keep_always = 3 };
RestartSchedule() : ScheduleStrategy() {}
//! Creates dynamic sequence.
static RestartSchedule dynamic(uint32 base, float k, uint32 lim, AvgType fast, Keep keep,AvgType slow, uint32 slowW);

bool isDynamic() const { return type == 3u; }
// only valid if isDynamic() is true.
float k() const { return grow; }
uint32 lbdLim() const { return len; }
uint32 adjustLim() const { return lbdLim() != UINT32_MAX ? 16000 : UINT32_MAX; }
AvgType fastAvg() const;
AvgType slowAvg() const;
uint32 slowWin() const;
Keep keepAvg() const;
};

//! Aggregates restart-parameters to configure restarts during search.
/*!
* \see ScheduleStrategy
*/
struct RestartParams {
RestartParams();
enum SeqUpdate { seq_continue = 0, seq_repeat = 1, seq_disable = 2 };
typedef RestartSchedule Schedule;
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:16;/**< Apply counter implication bump every counterRestart restarts (0: disable). */
uint32 counterBump:16; /**< Bump factor for counter implication restarts. */
bool disabled() const { return base() == 0; }
bool local() const { return cntLocal != 0; }
SeqUpdate update() const { return static_cast<SeqUpdate>(upRestart); }
uint32 base() const { return rsSched.base; }
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. */
CLASP_ALIGN_BITFIELD(uint32)
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? */
};

//! 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.
*/
struct DynamicLimit {
typedef RestartSchedule::Keep Keep;
enum Type { lbd_limit, level_limit };
//! Creates new limit with moving average of the given window size.
DynamicLimit(float k, uint32 window, MovingAvg::Type fast, Keep keep, MovingAvg::Type slow, uint32 slowWin = 0, uint32 adjustLimit = 16000);

//! Resets adjust strategy and optionally the moving (fast) average.
void resetAdjust(float k, Type type, uint32 lim, bool resetAvg = false);
//! Resets current run - depending on the Keep strategy this also clears the moving average.
void block();
//! Resets moving and global average.
void reset();
//! Adds an observation and updates the moving average. Typically called on conflict.
void update(uint32 conflictLevel, uint32 lbd);
//! Notifies this object about a restart.
/*!
* The function checks whether to adjust the active margin ratio and/or
* whether to switch from LBD based to conflict level based restarts.
*
* \param maxLBD Threshold for switching between lbd and conflict level queue.
* \param k Lower bound for margin ratio.
*/
uint32 restart(uint32 maxLBD, float k);
//! Returns the number of updates since last restart.
uint32 runLen() const { return num_; }
//! Returns whether it is time to restart.
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); }
uint32 limit; //!< Number of conflicts before an update is forced.
uint32 restarts;//!< Number of restarts since last update.
uint32 samples; //!< Number of samples since last update.
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(const DynamicLimit&);
DynamicLimit& operator=(const DynamicLimit&);
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.
/*!
* \see G. Audemard, L. Simon "Refining Restarts Strategies for SAT and UNSAT"
* \see A. Biere, A. Froehlich "Evaluating CDCL Restart Schemes"
*/
struct BlockLimit {
explicit BlockLimit(uint32 windowSize, double R = 1.4, MovingAvg::Type t = MovingAvg::Type::avg_ema);
bool push(uint32 nAssign) {
avg.push(nAssign);
return ++n >= next;
}
//! Returns the exponential moving average scaled by r.
double scaled() const { return avg.get() * r; }
MovingAvg avg; //!< Moving average.
uint64 next; //!< Enable once n >= next.
uint64 n; //!< Number of data points seen so far.
uint32 inc; //!< Block restart for next inc conflicts.
float r; //!< Scale factor for moving average.
};

//! Reduce strategy used during solving.
Expand Down Expand Up @@ -378,8 +486,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 Expand Up @@ -566,6 +674,25 @@ class BasicSatConfig : public UserConfiguration, public ContextParams {
SearchVec search_;
HeuFactory heu_;
};
///////////////////////////////////////////////////////////////////////////////
// SearchLimits
///////////////////////////////////////////////////////////////////////////////
//! Parameter-Object for managing search limits.
struct SearchLimits {
typedef DynamicLimit* LimitPtr;
typedef BlockLimit* BlockPtr;
SearchLimits();
uint64 used;
struct {
uint64 conflicts; //!< Soft limit on number of conflicts for restart.
LimitPtr dynamic; //!< Use dynamic restarts based on lbd or conflict level.
BlockPtr block; //!< Optional strategy to increase restart limit.
bool local; //!< Apply conflict limit against active branch.
} restart; //!< Restart limits.
uint64 conflicts; //!< Soft limit on number of conflicts.
uint64 memory; //!< Soft memory limit for learnt lemmas (in bytes).
uint32 learnts; //!< Limit on number of learnt lemmas.
};

//! Base class for solving related events.
template <class T>
Expand Down
Loading

0 comments on commit 770e8d2

Please sign in to comment.