From d9b7b5d9668d5941f9427f6e74ff0de7243328d9 Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Thu, 4 Apr 2024 18:11:45 +0200 Subject: [PATCH] Rework dynamic/blocked restarts. * add support for different moving averages * add support for keeping ema on restart/block * drop "User" schedule in favor of dedicated restart schedule * fix overflow handling in ScheduleStrategy --- clasp/cli/clasp_app.h | 4 +- clasp/cli/clasp_cli_options.inl | 63 +++++++----- clasp/shared_context.h | 4 +- clasp/solve_algorithms.h | 2 +- clasp/solver.h | 10 +- clasp/solver_strategies.h | 173 +++++++++++++++++++++++++++----- clasp/solver_types.h | 114 --------------------- clasp/util/misc_types.h | 90 +++++++++++++++-- src/clasp_options.cpp | 84 ++++++++++++---- src/solve_algorithms.cpp | 68 ++++++------- src/solver.cpp | 10 +- src/solver_strategies.cpp | 122 ++++++++++++++++++++-- src/solver_types.cpp | 93 +---------------- tests/cli_test.cpp | 83 +++++++++++++-- tests/solver_test.cpp | 16 +++ 15 files changed, 590 insertions(+), 346 deletions(-) diff --git a/clasp/cli/clasp_app.h b/clasp/cli/clasp_app.h index 14ca64c..0f896eb 100644 --- a/clasp/cli/clasp_app.h +++ b/clasp/cli/clasp_app.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/ // @@ -42,7 +42,7 @@ namespace Clasp { namespace Cli { // clasp exit codes ///////////////////////////////////////////////////////////////////////////////////////// enum ExitCode { - E_UNKNOWN = 0, /*!< Satisfiablity of problem not knwon; search not started. */ + E_UNKNOWN = 0, /*!< Satisfiability of problem not known; search not started. */ E_INTERRUPT = 1, /*!< Run was interrupted. */ E_SAT = 10, /*!< At least one model was found. */ E_EXHAUST = 20, /*!< Search-space was completely examined. */ diff --git a/clasp/cli/clasp_cli_options.inl b/clasp/cli/clasp_cli_options.inl index 9659f47..2d51f8d 100644 --- 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/ // @@ -342,17 +342,28 @@ OPTION(rand_prob, "", ARG(arg("[,]")), "Do random searches with [=1 #if defined(NOTIFY_SUBGROUPS) GROUP_BEGIN(SELF) #endif -OPTION(restarts, "!,r", ARG(arg("")), "Configure restart policy\n" \ - " %A: ,[,][,]\n" \ - " F, : Run fixed sequence of conflicts\n" \ - " L, : Run Luby et al.'s sequence with unit length \n" \ - " x,,: Run geometric seq. of *(^i) conflicts ( >= 1.0)\n" \ - " +,,: Run arithmetic seq. of +(*i) conflicts ()\n"\ - " ...,: Repeat seq. every +j restarts ( != F)\n" \ - " D,,: Restart based on moving LBD average over last conflicts\n" \ - " Mavg(,LBD)* > avg(LBD)\n" \ - " use conflict level average if > 0 and avg(LBD) > \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(""), 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: ,[,][,]\n" \ + " F, : Run fixed sequence of conflicts\n" \ + " L, : Run Luby et al.'s sequence with unit length \n" \ + " x,,: Run geometric seq. of *(^i) conflicts ( >= 1.0)\n" \ + " +,,: Run arithmetic seq. of +(*i) conflicts ()\n" \ + " ...,: Repeat sequence every +j restarts ( != F)\n" \ + " %A: D,,[,]: Dynamic restarts based on moving LBD average\n" \ + " : Fast moving average window size\n" \ + " : Fast margin (restart if fastAvg * > slowAvg)\n" \ + " : LBD average limit [0 = none]\n" \ + " : Fast moving average type [d = SMA]\n" \ + " d : Default\n" \ + " e|l : EMA with alpha = 2/(+1) or 1/log2()\n" \ + " es|ls : e or l with exponentially decreasing alpha for first samples\n" \ + " : keep fast moving average on (r)estarts/(b)locks [n = never]\n" \ + " : slow moving average type [d = CMA]\n" \ + " : slow moving average window size ( != d) [200*]\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(""), 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}",\ @@ -365,15 +376,19 @@ OPTION(counter_restarts, "" , 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("")), "Use glucose-style blocking restarts\n" \ - " %A: [,][,]\n" \ - " : Window size for moving average (0=disable blocking)\n" \ - " : Block restart if assignment > average * [1.4]\n" \ - " : Disable blocking for the first 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(""), 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" \ + " : Window size for moving average (0=disable blocking)\n" \ + " : Block restart if assignment > average * [1.4]\n" \ + " : Disable blocking for the first conflicts [10000]\n" \ + " : 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(R*100.0f)) && SET(SELF.block.first, c) && SET(SELF.block.avg, a)); },\ + GET_FUN(str) { ITE(!SELF.block.window, str<(SELF.block.avg)); }) OPTION(shuffle , "!" , ARG(arg(",")), "Shuffle problem after +(*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)) @@ -409,11 +424,11 @@ OPTION(del_grow , "!", NO_ARG, "Configure size-based deletion policy\n" \ " : Set grow schedule () [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<")), "Configure conflict-based deletion policy\n" \ " %A: ,... (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: [,,] ( > 0)\n" \ " : Set initial limit to P=estimated problem size/ [%D]\n" \ @@ -492,7 +507,7 @@ OPTION(global_restarts, ",@1", ARG(arg("")), "Configure global restart policy " : Maximal number of global restarts (0=disable)\n" \ " : Restart schedule [x,100,1.5] ()\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))\ diff --git a/clasp/shared_context.h b/clasp/shared_context.h index fc3ae48..0f49478 100644 --- a/clasp/shared_context.h +++ b/clasp/shared_context.h @@ -1,5 +1,5 @@ // -// Copyright (c) 2010-2017 Benjamin Kaufmann +// Copyright (c) 2010-present Benjamin Kaufmann // // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ // @@ -693,7 +693,7 @@ class SharedContext { bool isShared() const { return frozen() && concurrency() > 1; } //! Returns whether the problem is more than a simple CNF. bool isExtended() const { return stats_.vars.frozen != 0; } - //! Returns whether this object has a solver associcated with the given id. + //! Returns whether this object has a solver associated with the given id. bool hasSolver(uint32 id) const { return id < solvers_.size(); } //! Returns the master solver associated with this object. Solver* master() const { return solver(0); } diff --git a/clasp/solve_algorithms.h b/clasp/solve_algorithms.h index bfc534c..bedadec 100644 --- a/clasp/solve_algorithms.h +++ b/clasp/solve_algorithms.h @@ -45,7 +45,7 @@ struct SolveLimits { , restarts(r) { } bool reached() const { return conflicts == 0 || restarts == 0; } - bool enabled() const { return conflicts != UINT64_MAX || restarts != UINT32_MAX; } + bool enabled() const { return conflicts != UINT64_MAX || restarts != UINT64_MAX; } uint64 conflicts; /*!< Number of conflicts. */ uint64 restarts; /*!< Number of restarts. */ }; diff --git a/clasp/solver.h b/clasp/solver.h index d0130e5..e906836 100644 --- a/clasp/solver.h +++ b/clasp/solver.h @@ -631,10 +631,12 @@ class Solver { return *learnts_[ idx ]; } - mutable RNG rng; //!< Random number generator for this object. - ValueVec model; //!< Stores the last model (if any). - LowerBound lower; //!< Stores the last lower bound found (if any). - SolverStats stats; //!< Stores statistics about the solving process. + typedef SingleOwnerPtr DynLimPtr; + mutable RNG rng; //!< Random number generator for this object. + ValueVec model; //!< Stores the last model (if any). + LowerBound lower; //!< Stores the last lower bound found (if any). + SolverStats stats; //!< Stores statistics about the solving process. + DynLimPtr dynamic; //!< Optional dynamic limit. //@} /*! diff --git a/clasp/solver_strategies.h b/clasp/solver_strategies.h index 46e5cea..3f73831 100644 --- 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/ // @@ -59,7 +59,7 @@ namespace Clasp { * \ is the initial outer-limit and j is the number of times the * sequence was already repeated. * - * \note For luby's seqeuence, j is not a repetition counter + * \note For luby's sequence, j is not a repetition counter * but the index where the sequence grows to the next power of two. * * \see Luby et al. "Optimal speedup of las vegas algorithms." @@ -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. @@ -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) @@ -276,30 +275,137 @@ struct SolverParams : SolverStrategies { typedef Range 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; } + 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(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(upRestart); } + uint32 base() const { return rsSched.base; } + Schedule rsSched; + struct Block { + float scale() const { return static_cast(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 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); + void resetAdjust(float k, Type type, uint32 lim); + 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. @@ -378,8 +484,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(strategy.fReduce) / 100.0f; } + float fRestart() const { return static_cast(strategy.fRestart)/ 100.0f; } static uint32 getLimit(uint32 base, double f, const Range& r); ScheduleStrategy cflSched; /**< Conflict-based deletion schedule. */ ScheduleStrategy growSched; /**< Growth-based deletion schedule. */ @@ -568,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 diff --git a/clasp/solver_types.h b/clasp/solver_types.h index f451aec..010aca5 100644 --- a/clasp/solver_types.h +++ b/clasp/solver_types.h @@ -45,117 +45,6 @@ class SharedLiterals; */ //@{ /////////////////////////////////////////////////////////////////////////////// -// SearchLimits -/////////////////////////////////////////////////////////////////////////////// -struct DynamicLimit; -struct BlockLimit; - -//! 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. -}; - -//! 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 { - enum Type { lbd_limit, level_limit }; - //! 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(); - //! 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 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. - 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). -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(sum_[t] / cap_); } - uint64 sum_[2]; - uint32 cap_; - uint32 pos_; - uint32 num_; -POTASSCO_WARNING_BEGIN_RELAXED - uint32 buffer_[0]; -POTASSCO_WARNING_END_RELAXED -}; - -//! 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); - bool push(uint32 nAssign) { - ema = n >= span - ? exponentialMovingAverage(ema, nAssign, alpha) - : cumulativeMovingAverage(ema, nAssign, n); - 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. -}; -/////////////////////////////////////////////////////////////////////////////// // Statistics /////////////////////////////////////////////////////////////////////////////// class StatisticObject; @@ -299,7 +188,6 @@ struct SolverStats : public CoreStats { ~SolverStats(); bool enableExtended(); bool enable(const SolverStats& o) { return !o.extra || enableExtended(); } - void enableLimit(uint32 size); void reset(); void accu(const SolverStats& o); void accu(const SolverStats& o, bool enableRhs); @@ -322,7 +210,6 @@ struct SolverStats : public CoreStats { inline void addIntegrated(uint32 num = 1); inline void removeIntegrated(uint32 num = 1); inline void addPath(const LitVec::size_type& sz); - DynamicLimit* limit; /**< Optional dynamic limit. */ ExtendedStats* extra; /**< Optional extended statistics. */ SolverStats* multi; /**< Not owned: set to accu stats in multishot solving. */ private: SolverStats& operator=(const SolverStats&); @@ -343,7 +230,6 @@ inline void SolverStats::addIntegratedAsserting(uint32 rDL, uint32 jDL) { } inline void SolverStats::addConflict(uint32 dl, uint32 uipLevel, uint32 bLevel, uint32 lbd) { ++analyzed; - if (limit) { limit->update(dl, lbd); } if (extra) { extra->jumps.update(dl, uipLevel, bLevel); } } #undef CLASP_STAT_DEFINE diff --git a/clasp/util/misc_types.h b/clasp/util/misc_types.h index 3677873..2e9a1e8 100644 --- 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,92 @@ class RNG { /*! * Computes ema = currentEma + ((double(sample) - currentEma)*alpha); */ -template -inline double exponentialMovingAverage(double currentEma, T sample, double alpha) { - return (static_cast(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 -inline double cumulativeMovingAverage(double currentAvg, T sample, uint64 numSeen) { +//! Updates the given cumulative moving average with the given sample. +inline double cumulativeMovingAverage(double currentAvg, double sample, uint64 numSeen) { return (static_cast(sample) + (currentAvg * numSeen)) / static_cast(numSeen + 1); } +//! Updates the given simple moving average with the given sample. +inline double simpleMovingAverage(double currentAvg, uint32 sample, uint32* buffer, uint32 cap, uint32 pos, bool full) { + assert(pos < cap); + double oldS = static_cast(buffer[pos]); + double newS = static_cast(sample); + buffer[pos] = sample; + return full ? currentAvg + ((newS - oldS) / cap) : cumulativeMovingAverage(currentAvg, newS, pos); +} + +class MovingAvg { +public: + enum Type { avg_sma = 0, avg_ema = 1, avg_ema_log = 2, avg_ema_smooth = 3, avg_ema_log_smooth = 4 }; + + MovingAvg(uint32 window, Type type) + : avg_(0.0), extra_(), pos_(0), win_(window), full_(window == 0), cma_(0), ema_(type != avg_sma) { + assert(window > 0 || type == avg_sma); + if (ema_) { + cma_ = (type < avg_ema_smooth); + extra_.alpha = (type & 1u) != 0 ? 2.0 / (window + 1) : 1.0 / (1u << log2(window)); + } + else if (window) { + extra_.sma = new uint32[window]; + } + else { + extra_.num = 0; + } + } + + ~MovingAvg() { + if (!ema_ && win_) + delete [] extra_.sma; + } + + bool push(uint32 val) { + if (cumulative()) avg_ = cumulativeMovingAverage(avg_, val, extra_.num++); + else if (ema_ == 0) avg_ = simpleMovingAverage(avg_, val, extra_.sma, win_, pos_, valid()); + else if (valid()) avg_ = exponentialMovingAverage(avg_, val, extra_.alpha); + else if (cma_) avg_ = cumulativeMovingAverage(avg_, val, pos_); + else avg_ = exponentialMovingAverage(avg_, val, smoothAlpha(extra_.alpha, pos_)); + if (++pos_ == win_) { pos_ = 0; full_ = 1; } + return valid(); + } + + void clear() { + avg_ = 0.0; + pos_ = 0; + if (cumulative()) + extra_.num = 0; + else + full_ = 0; + } + + double get() const { return avg_; } + bool valid() const { return full_ != 0; } + uint32 win() const { return win_; } + +private: + MovingAvg(const MovingAvg&); + MovingAvg& operator=(const MovingAvg&); + bool cumulative() const { return !ema_ && !win_; } + + static double smoothAlpha(double alpha, uint32 pos) { + return pos < 32 ? std::max(alpha, 1.0 / static_cast(uint32(1) << pos)) : alpha; + } + + double avg_; + union Extra { + uint32* sma; // Buffer for SMA + double alpha; // Smoothing factor for EMA + uint64 num; // Number of data points for CMA + } extra_; + uint32 pos_; // Number of data points % window size + uint32 win_ : 29; // Window size (for SMA/EMA) + uint32 full_: 1; // Enough data points seen? + uint32 cma_ : 1; // Use cumulative moving average for first data points + uint32 ema_ : 1; // Exponential Moving Average? +}; + //! An unary operator function that calls p->destroy(). struct DestroyObject { template void operator()(T* p) const { if (p) p->destroy(); } diff --git a/src/clasp_options.cpp b/src/clasp_options.cpp index 948750a..71a4b5b 100644 --- a/src/clasp_options.cpp +++ b/src/clasp_options.cpp @@ -245,37 +245,38 @@ DEFINE_ENUM_MAPPING(ConfigKey, \ ///////////////////////////////////////////////////////////////////////////////////////// // Conversion functions for complex clasp types ///////////////////////////////////////////////////////////////////////////////////////// +static int convertRet(int res, const char* in, const char** next) { + if (next) *next = in; + return res; +} + static int xconvert(const char* x, ScheduleStrategy& out, const char** errPos, int e) { using Potassco::xconvert; - if (!x) { return 0; } - const char* next = std::strchr(x, ','); + const char* next = std::strchr(x ? x : "", ','); uint32 base = 0; - int tok = 1; - if (errPos) { *errPos = x; } - if (!next || !xconvert(next+1, base, &next, e) || base == 0) { return 0; } - if (strncasecmp(x, "f,", 2) == 0 || strncasecmp(x, "fixed,", 6) == 0){ + if (!next || !xconvert(next+1, base, &next, e) || base == 0) { return convertRet(0, x, errPos); } + if (strncasecmp(x, "f,", 2) == 0 || strncasecmp(x, "fixed,", 6) == 0) { out = ScheduleStrategy::fixed(base); } else if (strncasecmp(x, "l,", 2) == 0 || strncasecmp(x, "luby,", 5) == 0) { uint32 lim = 0; - if (*next == ',' && !xconvert(next+1, lim, &next, e)) { return 0; } + if (*next == ',' && !xconvert(next+1, lim, &next, e)) { return convertRet(0, next, errPos); } out = ScheduleStrategy::luby(base, lim); } else if (strncmp(x, "+,", 2) == 0 || strncasecmp(x, "add,", 4) == 0) { std::pair arg(0, 0); - if (*next != ',' || !xconvert(next+1, arg, &next, e)) { return 0; } + if (*next != ',' || !xconvert(next+1, arg, &next, e)) { return convertRet(0, next, errPos); } out = ScheduleStrategy::arith(base, arg.first, arg.second); } - else if (strncmp(x, "x,", 2) == 0 || strncmp(x, "*,", 2) == 0 || strncasecmp(x, "d,", 2) == 0) { + else if (strncmp(x, "x,", 2) == 0 || strncmp(x, "*,", 2) == 0) { std::pair 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); } - else if (strncasecmp(x, "d", 1) != 0 && arg.first >= 1.0){ out = ScheduleStrategy::geom(base, arg.first, arg.second); } - else { return 0; } + if (*next != ',' || !xconvert(next+1, arg, &next, e) || arg.first < 1.0) { return convertRet(0, next, errPos); } + out = ScheduleStrategy::geom(base, arg.first, arg.second); } - else { next = x; tok = 0; } - if (errPos) { *errPos = next; } - return tok; + else { + return convertRet(0, x, errPos); + } + return convertRet(1, next, errPos); } static std::string& xconvert(std::string& out, const ScheduleStrategy& sched) { using Potassco::xconvert; @@ -295,12 +296,55 @@ static std::string& xconvert(std::string& out, const ScheduleStrategy& sched) { out[t] = 'l'; if (sched.len) { return xconvert(out.append(1, ','), sched.len); } else { return out; } - case ScheduleStrategy::User: - out[t] = 'd'; - return xconvert(out.append(1, ','), std::make_pair((double)sched.grow, sched.len)); default: POTASSCO_ASSERT(false, "xconvert(ScheduleStrategy): unknown type"); } } +static int xconvert(const char* x, RestartSchedule& out, const char** errPos, int e) { + if (!x || (*x != 'd' && *x != 'D')) + return xconvert(x, static_cast(out), errPos, e); + using Potassco::xconvert; + std::pair req(0, 0); + uint32 lim = 0, sWin = 0; + MovingAvg::Type fast = MovingAvg::Type::avg_sma; + MovingAvg::Type slow = MovingAvg::Type::avg_sma; + DynamicLimit::Keep keep = RestartSchedule::keep_never; + const char* next = 0; + if (x[1] != ',' || !xconvert(x + 2, req, &x, e) || req.first == 0 || req.second <= 0.0) + return convertRet(0, x, errPos); + if (*x == ',' && !xconvert(x + 1, lim, &x, e)) + return convertRet(0, x, errPos); + if (*x == ',' && !xconvert(x + 1, fast, &x, e)) + return convertRet(0, x, errPos); + if (*x == ',' && fast != MovingAvg::Type::avg_sma && xconvert(x + 1, keep, &next, e)) + x = next; + if (*x == ',' && !xconvert(x + 1, slow, &x, e)) + return convertRet(0, x, errPos); + if (*x == ',' && slow != MovingAvg::Type::avg_sma && !xconvert(x + 1, sWin, &x, e)) + return convertRet(0, x, errPos); + out = RestartSchedule::dynamic(req.first, static_cast(req.second), lim, fast, keep, slow, sWin); + return convertRet(1, x, errPos); +} +static std::string& xconvert(std::string& out, const RestartSchedule& in) { + if (in.disabled() || !in.isDynamic()) + return xconvert(out, static_cast(in)); + using Potassco::xconvert; + xconvert(out.append("d,"), std::make_pair(in.base, in.grow)); + uint32 lbdLim = in.lbdLim(); + MovingAvg::Type fast = in.fastAvg(); + MovingAvg::Type slow = in.slowAvg(); + if (lbdLim || fast != MovingAvg::avg_sma || slow != MovingAvg::avg_sma) + xconvert(out.append(1, ','), lbdLim); + if (fast != MovingAvg::avg_sma || slow != MovingAvg::avg_sma) + xconvert(out.append(1, ','), fast); + if (fast != MovingAvg::avg_sma && in.keepAvg()) + xconvert(out.append(1, ','), static_cast(in.keepAvg())); + if (slow != MovingAvg::avg_sma) { + xconvert(out.append(1, ','), slow); + if (in.slowWin()) xconvert(out.append(1, ','), in.slowWin()); + } + return out; +} + static bool setOptLegacy(OptParams& out, uint32 n) { if (n >= 20) { return false; } out.type = n < 4 ? OptParams::type_bb : OptParams::type_usc; @@ -1178,7 +1222,7 @@ const char* validate(const SolverParams& solver, const SolveParams& search) { const ReduceParams& reduce = search.reduce; if (solver.search == SolverParams::no_learning) { if (Heuristic_t::isLookback(solver.heuId)) return "Heuristic requires lookback strategy!"; - if (!search.restart.sched.disabled() && !search.restart.sched.defaulted()) return "'no-lookback': restart options disabled!"; + if (!search.restart.disabled()) return "'no-lookback': restart options disabled!"; if (!reduce.cflSched.disabled() || (!reduce.growSched.disabled() && !reduce.growSched.defaulted()) || search.reduce.fReduce() != 0) return "'no-lookback': deletion options disabled!"; } bool hasSched = !reduce.cflSched.disabled() || !reduce.growSched.disabled() || reduce.maxRange != UINT32_MAX; diff --git a/src/solve_algorithms.cpp b/src/solve_algorithms.cpp index ee0fd2d..d379297 100644 --- a/src/solve_algorithms.cpp +++ b/src/solve_algorithms.cpp @@ -34,7 +34,7 @@ struct BasicSolve::State { typedef BasicSolveEvent EventType; typedef SingleOwnerPtr BlockPtr; State(Solver& s, const SolveParams& p); - ValueRep solve(Solver& s, const SolveParams& p, SolveLimits* lim); + ValueRep solve(Solver& s, const SolveParams& p, SolveLimits& lim); uint64 dbGrowNext; double dbMax; double dbHigh; @@ -78,34 +78,29 @@ ValueRep BasicSolve::solve() { if (limits_.reached()) { return value_free; } if (!state_ && !params_->randomize(*solver_)){ return value_false; } if (!state_) { state_ = new State(*solver_, *params_); } - return state_->solve(*solver_, *params_, hasLimit() ? &limits_ : 0); + return state_->solve(*solver_, *params_, limits_); } bool BasicSolve::satisfiable(const LitVec& path, bool init) { if (!solver_->clearAssumptions() || !solver_->pushRoot(path)){ return false; } if (init && !params_->randomize(*solver_)) { return false; } State temp(*solver_, *params_); - return temp.solve(*solver_, *params_, 0) == value_true; + SolveLimits limits; + return temp.solve(*solver_, *params_, limits) == value_true; } bool BasicSolve::assume(const LitVec& path) { return solver_->pushRoot(path); } -BasicSolve::State::State(Solver& s, const SolveParams& p) { +BasicSolve::State::State(Solver& s, const SolveParams& p) + : dbGrowNext(p.reduce.growSched.current()), dbRed(p.reduce.cflSched), nRestart(0), nGrow(0) + , dbRedInit(p.reduce.cflInit(*s.sharedContext())), dbPinned(0), rsShuffle(p.restart.shuffle), resetState(false) { Range32 dbLim= p.reduce.sizeInit(*s.sharedContext()); - dbGrowNext = p.reduce.growSched.current(); dbMax = dbLim.lo; dbHigh = dbLim.hi; - dbRed = p.reduce.cflSched; - nRestart = 0; - nGrow = 0; - dbRedInit = p.reduce.cflInit(*s.sharedContext()); - dbPinned = 0; - rsShuffle = p.restart.shuffle; - resetState = false; if (dbLim.lo < s.numLearntConstraints()) { - dbMax = std::min(dbHigh, double(s.numLearntConstraints() + p.reduce.initRange.lo)); + dbMax = std::min(dbHigh, double(s.numLearntConstraints() + p.reduce.initRange.lo)); } if (dbRedInit && dbRed.type != ScheduleStrategy::Luby) { if (dbRedInit < dbRed.base) { @@ -115,20 +110,22 @@ BasicSolve::State::State(Solver& s, const SolveParams& p) { } dbRedInit = 0; } - if (p.restart.dynamic()) { - s.stats.enableLimit(p.restart.sched.base); - s.stats.limit->reset(); + if (p.restart.rsSched.isDynamic()) { + const RestartSchedule& r = p.restart.rsSched; + uint32 adjustLim = r.lbdLim() != UINT32_MAX ? 16000 : UINT32_MAX; + s.dynamic.reset(new DynamicLimit(r.k(), r.base, r.fastAvg(), r.keepAvg(), r.slowAvg(), r.slowWin(), adjustLim)); } - if (p.restart.blockScale > 0.0f && p.restart.blockWindow > 0) { - rsBlock.reset(new BlockLimit(p.restart.blockWindow, p.restart.blockScale)); - rsBlock->inc = std::max(p.restart.sched.base, uint32(50)); - rsBlock->next = std::max(p.restart.blockWindow, p.restart.blockFirst); + if (p.restart.block.fscale > 0 && p.restart.block.window > 0) { + const RestartParams::Block& block = p.restart.block; + rsBlock.reset(new BlockLimit(block.window, block.scale(), static_cast(block.avg))); + rsBlock->inc = std::max(p.restart.base(), uint32(50)); + rsBlock->next = std::max(block.window, block.first); } s.stats.lastRestart = s.stats.analyzed; } -ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits* lim) { - assert(!lim || !lim->reached()); +ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits& lim) { + assert(!lim.reached()); const uint32 resetMode = s.enumerationConstraint() ? static_cast(s.enumerationConstraint())->resetMode() : 0u; if (s.hasConflict() && s.decisionLevel() == s.rootLevel()) { resetState = resetState || (resetMode & value_false) != 0; @@ -147,21 +144,20 @@ ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits* new (this) State(s, p); } WeightLitVec inDegree; - SearchLimits sLimit; - ScheduleStrategy rs = p.restart.sched; + SearchLimits sLimit; + RestartSchedule rs = p.restart.rsSched; ScheduleStrategy dbGrow = p.reduce.growSched; - Solver::DBInfo db = {0,0,dbPinned}; - ValueRep result = value_free; - ConflictLimits cLimit = {dbRed.current() + dbRedInit, dbGrowNext, UINT64_MAX, lim ? lim->conflicts : UINT64_MAX}; - uint64 limRestarts = lim ? lim->restarts : UINT64_MAX; + Solver::DBInfo db = {0,0,dbPinned}; + ValueRep result = value_free; + ConflictLimits cLimit = {dbRed.current() + dbRedInit, dbGrowNext, UINT64_MAX, lim.conflicts}; + uint64 limRestarts = lim.restarts; if (!dbGrow.disabled()) { dbGrow.advanceTo(nGrow); } if (nRestart == UINT32_MAX && p.restart.update() == RestartParams::seq_disable) { sLimit = SearchLimits(); } - else if (p.restart.dynamic() && s.stats.limit) { - if (!nRestart) { s.stats.limit->init((float)p.restart.sched.grow, DynamicLimit::lbd_limit); } - 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); + else if (rs.isDynamic() && s.dynamic.get()) { + sLimit.restart.dynamic = s.dynamic.get(); + sLimit.restart.conflicts = s.dynamic->adjust.limit - std::min(s.dynamic->adjust.samples, s.dynamic->adjust.limit - 1); } else { rs.advanceTo(!rs.disabled() ? nRestart : 0); @@ -202,7 +198,7 @@ ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits* } if (sLimit.restart.dynamic) { n = sLimit.restart.dynamic->runLen(); - sLimit.restart.conflicts = sLimit.restart.dynamic->restart(rs.len ? rs.len : UINT32_MAX, (float)rs.grow); + sLimit.restart.conflicts = sLimit.restart.dynamic->restart(rs.lbdLim(), rs.k()); } else { sLimit.restart.conflicts = n = rs.next(); @@ -239,9 +235,9 @@ ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits* dbPinned = db.pinned; resetState = (resetMode & result) != 0u; s.stats.lastRestart = s.stats.analyzed - s.stats.lastRestart; - if (lim) { - if (lim->conflicts != UINT64_MAX) { lim->conflicts = cLimit.global; } - if (lim->restarts != UINT64_MAX) { lim->restarts = limRestarts; } + if (lim.enabled()) { + if (lim.conflicts != UINT64_MAX) { lim.conflicts = cLimit.global; } + if (lim.restarts != UINT64_MAX) { lim.restarts = limRestarts; } } return result; } diff --git a/src/solver.cpp b/src/solver.cpp index 7cffcd0..0619745 100644 --- a/src/solver.cpp +++ b/src/solver.cpp @@ -224,7 +224,7 @@ void Solver::startInit(uint32 numConsGuess, const SolverParams& params) { if (!strategy_.hasConfig) { uint32 id = this->id(); uint32 hId = strategy_.heuId; // remember active heuristic - strategy_ = params; + strategy_ = static_cast(params); strategy_.id = id; // keep id strategy_.hasConfig = 1; // strategy is now "up to date" if (!params.ccMinRec) { delete ccMin_; ccMin_ = 0; } @@ -942,7 +942,9 @@ bool Solver::resolveConflict() { if (decisionLevel() > rootLevel()) { if (decisionLevel() != backtrackLevel() && searchMode() != SolverStrategies::no_learning) { uint32 uipLevel = analyzeConflict(); - stats.addConflict(decisionLevel(), uipLevel, backtrackLevel(), ccInfo_.lbd()); + uint32 dl = decisionLevel(); + stats.addConflict(dl, uipLevel, backtrackLevel(), ccInfo_.lbd()); + if (dynamic.get()) { dynamic.get()->update(dl, ccInfo_.lbd()); } if (shared_->reportMode()) { sharedContext()->report(NewConflictEvent(*this, cc_, ccInfo_)); } @@ -1650,7 +1652,7 @@ Solver::DBInfo Solver::reduceLinear(uint32 maxR, const CmpScore& sc) { scoreSum += sc.score(learnts_[i]->activity()); } double avgAct = (scoreSum / (double) numLearntConstraints()); - // constraints with socre > 1.5 times the average are "active" + // constraints with score > 1.5 times the average are "active" double scoreThresh = avgAct * 1.5; double scoreMax = (double)sc.score(makeScore(Clasp::ACT_MAX, 1)); if (scoreThresh > scoreMax) { @@ -1830,7 +1832,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->block(); } else { limit.restart.conflicts += block->inc; } block->next = block->n + block->inc; ++stats.blRestarts; diff --git a/src/solver_strategies.cpp b/src/solver_strategies.cpp index eb57bb0..9538a9d 100644 --- a/src/solver_strategies.cpp +++ b/src/solver_strategies.cpp @@ -97,17 +97,19 @@ ScheduleStrategy::ScheduleStrategy(Type t, uint32 b, double up, uint32 lim) : base(b), type(t), idx(0), len(lim), grow(0.0) { if (t == Geometric) { grow = static_cast(std::max(1.0, up)); } else if (t == Arithmetic) { grow = static_cast(std::max(0.0, up)); } - else if (t == User) { grow = static_cast(std::max(0.0, up)); } else if (t == Luby && lim){ len = std::max(uint32(2), (static_cast(std::pow(2.0, std::ceil(log(double(lim))/log(2.0)))) - 1)*2); } } +static uint64_t saturate(double d) { + return d < static_cast(UINT64_MAX) ? static_cast(d) : UINT64_MAX; +} + uint64 ScheduleStrategy::current() const { - enum { t_add = ScheduleStrategy::Arithmetic, t_luby = ScheduleStrategy::Luby }; - if (base == 0) return UINT64_MAX; - else if (type == t_add) return static_cast(addR(idx, grow) + base); - else if (type == t_luby)return static_cast(lubyR(idx)) * base; - uint64 x = static_cast(growR(idx, grow) * base); - return x + !x; + if (base == 0) return UINT64_MAX; + else if (type == Geometric) return saturate(growR(idx, grow) * base); + else if (type == Arithmetic) return static_cast(addR(idx, grow) + base); + else if (type == Luby) return static_cast(lubyR(idx)) * base; + else return base; } uint64 ScheduleStrategy::next() { if (++idx != len) { return current(); } @@ -134,12 +136,25 @@ void ScheduleStrategy::advanceTo(uint32 n) { } idx = n; } +RestartSchedule RestartSchedule::dynamic(uint32 base, float k, uint32 lim, AvgType fast, Keep keep, AvgType slow, uint32 slowW) { + RestartSchedule sched; + sched.base = base; + sched.type = 3u; + sched.grow = k; + sched.len = lim; + sched.idx = uint32(fast) | (uint32(slow) << 3u) | ((keep & 3u) << 6u) | (std::min(slowW, (1u<<24)-1) << 8u); + return sched; +} +MovingAvg::Type RestartSchedule::fastAvg() const { return static_cast(idx & 7u); } +MovingAvg::Type RestartSchedule::slowAvg() const { return static_cast((idx >> 3u) & 7u); } +RestartSchedule::Keep RestartSchedule::keepAvg() const { return static_cast((idx >> 6u) & 3u); } +uint32 RestartSchedule::slowWin() const { return idx >> 8u; } ///////////////////////////////////////////////////////////////////////////////////////// // RestartParams ///////////////////////////////////////////////////////////////////////////////////////// RestartParams::RestartParams() - : sched() - , blockScale(1.4f), blockWindow(0), blockFirst(0) + : rsSched() + , block() , counterRestart(0), counterBump(9973) , shuffle(0), shuffleNext(0) , upRestart(0), cntLocal(0) { @@ -147,15 +162,90 @@ RestartParams::RestartParams() } void RestartParams::disable() { std::memset(this, 0, sizeof(RestartParams)); - sched = ScheduleStrategy::none(); } uint32 RestartParams::prepare(bool withLookback) { - if (!withLookback || sched.disabled()) { + if (!withLookback || disabled()) { disable(); } return 0; } ///////////////////////////////////////////////////////////////////////////////////////// +// DynamicLimit +///////////////////////////////////////////////////////////////////////////////////////// +DynamicLimit::Global::Global(MovingAvg::Type type, uint32 size) + : lbd(size, type) + , cfl(size, type) { +} + +static uint32 verifySize(uint32 size) { + POTASSCO_REQUIRE(size != 0, "size must be > 0"); + return size; +} + +DynamicLimit::DynamicLimit(float k, uint32 size, MovingAvg::Type fast, Keep keep, MovingAvg::Type slow, uint32 slowSize, uint32 adjustLim) + : global_(slow, slowSize || slow == MovingAvg::avg_sma ? slowSize : 200 * verifySize(size)) + , avg_(verifySize(size), fast) + , num_(0) + , keep_(keep) { + resetAdjust(k, lbd_limit, adjustLim); +} + +void DynamicLimit::resetAdjust(float k, Type t, uint32 uLimit) { + std::memset(&adjust, 0, sizeof(adjust)); + adjust.limit = uLimit; + adjust.rk = k; + adjust.type = t; +} +void DynamicLimit::block() { + resetRun(Keep::keep_block); +} + +void DynamicLimit::resetRun(Keep k) { + num_ = 0; + if ((keep_ & k) == 0) + avg_.clear(); +} +void DynamicLimit::reset() { + global_.reset(); + resetRun(Keep::keep_never); +} +void DynamicLimit::update(uint32 dl, uint32 lbd) { + // update global avg + ++adjust.samples; + global_.cfl.push(dl); + global_.lbd.push(lbd); + // update moving avg + ++num_; + uint32 v = adjust.type == lbd_limit ? lbd : dl; + avg_.push(v); +} +uint32 DynamicLimit::restart(uint32 maxLBD, float k) { + ++adjust.restarts; + if (adjust.limit != UINT32_MAX && adjust.samples >= adjust.limit) { + Type nt = maxLBD && global_.avg(lbd_limit) > maxLBD ? level_limit : lbd_limit; + float rk = adjust.rk; + uint32 uLim = adjust.limit; + if (nt == adjust.type) { + double rLen = adjust.avgRestart(); + bool sx = num_ >= adjust.limit; + if (rLen >= 16000.0) { rk += 0.1f; uLim = 16000; } + else if (sx) { rk += 0.05f; uLim = std::max(uint32(16000), uLim-10000); } + else if (rLen >= 4000.0) { rk += 0.05f; } + else if (rLen >= 1000.0) { uLim += 10000u; } + else if (rk > k) { rk -= 0.05f; } + } + resetAdjust(rk, nt, uLim); + } + resetRun(Keep::keep_restart); + return adjust.limit; +} +BlockLimit::BlockLimit(uint32 windowSize, double R, MovingAvg::Type at) + : avg(windowSize, at) + , next(windowSize), inc(50), n(0) + , r(static_cast(R)) { + static_assert(sizeof(BlockLimit) == 12*sizeof(uint32), "unexpected size"); +} +///////////////////////////////////////////////////////////////////////////////////////// // ReduceParams ///////////////////////////////////////////////////////////////////////////////////////// uint32 ReduceParams::getLimit(uint32 base, double f, const Range32& r) { @@ -301,6 +391,16 @@ void BasicSatConfig::resize(uint32 solver, uint32 search) { void BasicSatConfig::setHeuristicCreator(HeuristicCreator* hc, Ownership_t::Type owner) { HeuFactory(hc, owner).swap(heu_); } +/////////////////////////////////////////////////////////////////////////////// +// SearchLimits +/////////////////////////////////////////////////////////////////////////////// +SearchLimits::SearchLimits() { + std::memset(this, 0, sizeof(SearchLimits)); + restart.conflicts = UINT64_MAX; + conflicts = UINT64_MAX; + memory = UINT64_MAX; + learnts = UINT32_MAX; +} ///////////////////////////////////////////////////////////////////////////////////////// // Heuristics ///////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/solver_types.cpp b/src/solver_types.cpp index 1b3a5bf..887f9af 100644 --- a/src/solver_types.cpp +++ b/src/solver_types.cpp @@ -30,89 +30,6 @@ #pragma GCC diagnostic ignored "-Wclass-memaccess" #endif namespace Clasp { -/////////////////////////////////////////////////////////////////////////////// -// SearchLimits -/////////////////////////////////////////////////////////////////////////////// -SearchLimits::SearchLimits() { - std::memset(this, 0, sizeof(SearchLimits)); - restart.conflicts = UINT64_MAX; - conflicts = UINT64_MAX; - memory = UINT64_MAX; - learnts = UINT32_MAX; -} -///////////////////////////////////////////////////////////////////////////////////////// -// DynamicLimit -///////////////////////////////////////////////////////////////////////////////////////// -DynamicLimit* DynamicLimit::create(uint32 size) { - POTASSCO_REQUIRE(size != 0, "size must be > 0"); - void* m = ::operator new(sizeof(DynamicLimit) + (size*sizeof(uint32))); - return new (m)DynamicLimit(size); -} -DynamicLimit::DynamicLimit(uint32 sz) : cap_(sz), pos_(0), num_(0) { - std::memset(&global, 0, sizeof(global)); - init(0.7f, lbd_limit); -} -void DynamicLimit::init(float k, Type t, uint32 uLimit) { - resetRun(); - std::memset(&adjust, 0, sizeof(adjust)); - adjust.limit = uLimit; - adjust.rk = k; - adjust.type = t; -} -void DynamicLimit::destroy() { - this->~DynamicLimit(); - ::operator delete(this); -} -void DynamicLimit::resetRun() { - sum_[0] = sum_[1] = pos_ = num_ = 0; -} -void DynamicLimit::reset() { - std::memset(&global, 0, sizeof(global)); - resetRun(); -} -void DynamicLimit::update(uint32 dl, uint32 lbd) { - // update global avg - ++adjust.samples; - ++global.samples; - global.sum[lbd_limit] += lbd; - global.sum[level_limit] += dl; - // update moving avg - sum_[lbd_limit] += lbd; - sum_[level_limit] += dl; - if (++num_ > cap_) { - sum_[lbd_limit] -= (buffer_[pos_] & 127u); - sum_[level_limit] -= (buffer_[pos_] >> 7u); - } - buffer_[pos_++] = ((dl << 7) + lbd); - if (pos_ == cap_) { pos_ = 0; } -} -uint32 DynamicLimit::restart(uint32 maxLBD, float k) { - ++adjust.restarts; - if (adjust.samples >= adjust.limit) { - Type nt = global.avg(lbd_limit) > maxLBD ? level_limit : lbd_limit; - if (nt == adjust.type) { - double rLen = adjust.avgRestart(); - bool sx = num_ >= adjust.limit; - float rk = adjust.rk; - uint32 uLim = adjust.limit; - if (rLen >= 16000.0) { rk += 0.1f; uLim = 16000; } - else if (sx) { rk += 0.05f; uLim = std::max(uint32(16000), uLim-10000); } - 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); - } - else { init(k, nt); } - } - else { resetRun(); } - return adjust.limit; -} -BlockLimit::BlockLimit(uint32 windowSize, double R) - : ema(0.0), alpha(2.0/(windowSize+1)) - , next(windowSize), inc(50), n(0) - , span(windowSize) - , r(static_cast(R)) {} - ///////////////////////////////////////////////////////////////////////////////////////// // Statistics ///////////////////////////////////////////////////////////////////////////////////////// @@ -174,24 +91,18 @@ void ExtendedStats::reset() { ///////////////////////////////////////////////////////////////////////////////////////// // SolverStats ///////////////////////////////////////////////////////////////////////////////////////// -SolverStats::SolverStats() : limit(0), extra(0), multi(0) {} -SolverStats::SolverStats(const SolverStats& o) : CoreStats(o), limit(0), extra(0), multi(0) { +SolverStats::SolverStats() : extra(0), multi(0) {} +SolverStats::SolverStats(const SolverStats& o) : CoreStats(o), extra(0), multi(0) { if (o.extra && enableExtended()) { extra->accu(*o.extra); } } SolverStats::~SolverStats() { delete extra; - if (limit) limit->destroy(); } bool SolverStats::enableExtended() { return extra != 0 || (extra = new (std::nothrow) ExtendedStats()) != 0; } -void SolverStats::enableLimit(uint32 size) { - if (limit && limit->window() != size) { limit->destroy(); limit = 0; } - if (!limit) { limit = DynamicLimit::create(size); } -} void SolverStats::reset() { CoreStats::reset(); - if (limit) limit->reset(); if (extra) extra->reset(); } void SolverStats::accu(const SolverStats& o) { diff --git a/tests/cli_test.cpp b/tests/cli_test.cpp index 53ce512..8d5b81b 100644 --- a/tests/cli_test.cpp +++ b/tests/cli_test.cpp @@ -58,6 +58,7 @@ TEST_CASE("Cli options", "[cli]") { std::string val; REQUIRE(config.numSolver() == 1); REQUIRE(config.testerConfig() == 0); + REQUIRE_FALSE(config.solve.limit.enabled()); SECTION("test init from argv") { REQUIRE(config.solve.numSolver() == 1); REQUIRE(config.solve.numModels != 0); @@ -108,7 +109,7 @@ TEST_CASE("Cli options", "[cli]") { REQUIRE(config.getValue("configuration") == tempName); REQUIRE(config.solve.numModels == 0); REQUIRE(config.solver(0).heuId == Heuristic_t::Berkmin); - REQUIRE(config.search(0).restart.sched == ScheduleStrategy::geom(100, 1.5)); + REQUIRE(config.search(0).restart.rsSched == ScheduleStrategy::geom(100, 1.5)); std::remove(tempName); REQUIRE(config.setValue(config.getKey(ClaspCliConfig::KEY_ROOT, "configuration"), tempName) == -2); } @@ -156,7 +157,7 @@ TEST_CASE("Cli options", "[cli]") { // search option REQUIRE(config.setValue("solver.2.restarts", "+,100,10")); REQUIRE(config.numSearch() == 3); - REQUIRE(config.search(2).restart.sched == ScheduleStrategy::arith(100, 10)); + REQUIRE(config.search(2).restart.rsSched == ScheduleStrategy::arith(100, 10)); REQUIRE(config.numSolver() == 3); REQUIRE(config.setValue("solver.17.heuristic", "unit")); @@ -439,11 +440,13 @@ TEST_CASE("Cli options", "[cli]") { REQUIRE(config.getValue(limit, val) > 0); REQUIRE(std::string("0,umax") == val); REQUIRE(config.solve.limit.conflicts == 0); + REQUIRE(config.solve.limit.enabled()); REQUIRE(1 == config.setValue(limit, "no")); REQUIRE(config.getValue(limit, val) > 0); REQUIRE(config.solve.limit.conflicts == UINT64_MAX); REQUIRE(std::string("umax,umax") == val); + REQUIRE_FALSE(config.solve.limit.enabled()); } SECTION("test opt-mode option") { @@ -464,6 +467,71 @@ TEST_CASE("Cli options", "[cli]") { REQUIRE(config.getValue("solve.opt_mode") == "opt,50,20"); } + SECTION("test dynamic restart option") { + REQUIRE(config.getValue("solver.restarts") == "x,100,1.5,0"); + REQUIRE_FALSE(config.setValue("solver.restarts", "D,100")); + REQUIRE_FALSE(config.setValue("solver.restarts", "D,0")); + + REQUIRE(config.setValue("solver.restarts", "D,50,0.8")); + REQUIRE(config.getValue("solver.restarts") == "d,50,0.8"); + + REQUIRE(config.setValue("solver.restarts", "D,100,0.9,20")); + REQUIRE(config.getValue("solver.restarts") == "d,100,0.9,20"); + REQUIRE(config.search(0).restart.rsSched.isDynamic()); + REQUIRE(config.search(0).restart.rsSched.lbdLim() == 20); + + REQUIRE(config.setValue("solver.restarts", "D,100,0.9,0,es,r")); + REQUIRE(config.getValue("solver.restarts") == "d,100,0.9,0,es,r"); + const RestartSchedule& rs = config.search(0).restart.rsSched; + REQUIRE(rs.isDynamic()); + REQUIRE(rs.lbdLim() == 0); + REQUIRE(rs.fastAvg() == MovingAvg::Type::avg_ema_smooth); + REQUIRE(rs.keepAvg() == RestartSchedule::keep_restart); + + REQUIRE(config.setValue("solver.restarts", "D,100,0.9,255,ls,rb,e,1234")); + REQUIRE(config.getValue("solver.restarts") == "d,100,0.9,255,ls,br,e,1234"); + REQUIRE(rs.isDynamic()); + REQUIRE(rs.lbdLim() == 255); + REQUIRE(rs.fastAvg() == MovingAvg::Type::avg_ema_log_smooth); + REQUIRE(rs.keepAvg() == RestartSchedule::keep_always); + REQUIRE(rs.slowAvg() == MovingAvg::Type::avg_ema); + REQUIRE(rs.slowWin() == 1234); + + REQUIRE_FALSE(config.setValue("solver.restarts", "D,100,0.9,255,ls,rb,e,1234,12")); + + REQUIRE(config.setValue("solver.restarts", "D,50,0.8,0,ls,es,10000")); + REQUIRE(config.getValue("solver.restarts") == "d,50,0.8,0,ls,es,10000"); + REQUIRE(rs.isDynamic()); + REQUIRE(rs.lbdLim() == 0); + REQUIRE(rs.fastAvg() == MovingAvg::Type::avg_ema_log_smooth); + REQUIRE(rs.keepAvg() == RestartSchedule::keep_never); + REQUIRE(rs.slowAvg() == MovingAvg::Type::avg_ema_smooth); + REQUIRE(rs.slowWin() == 10000); + } + + SECTION("test block restart option") { + REQUIRE(config.getValue("solver.block_restarts") == "no"); + REQUIRE_FALSE(config.setValue("solver.block_restarts", "0,1.3")); + + REQUIRE(config.setValue("solver.block_restarts", "5000")); + REQUIRE(config.getValue("solver.block_restarts") == "5000,1.4,10000,e"); + RestartParams::Block b = config.search(0).restart.block; + REQUIRE(b.window == 5000); + REQUIRE(b.first == 10000); + REQUIRE(b.scale() == 1.4f); + REQUIRE(b.avg == uint32(MovingAvg::Type::avg_ema)); + + REQUIRE_FALSE(config.setValue("solver.block_restarts", "5000,0.8")); + REQUIRE_FALSE(config.setValue("solver.block_restarts", "5000,5.1")); + + REQUIRE(config.setValue("solver.block_restarts", "10000,1.1,0,d")); + b = config.search(0).restart.block; + REQUIRE(b.window == 10000); + REQUIRE(b.scale() == 1.1f); + REQUIRE(b.first == 0); + REQUIRE(b.avg == uint32(MovingAvg::Type::avg_sma)); + } + SECTION("test get values") { std::string out; REQUIRE(config.getValue(config.getKey(ClaspCliConfig::KEY_TESTER, "configuration"), out) == -1); @@ -547,15 +615,18 @@ TEST_CASE("Cli mt options", "[cli][mt]") { REQUIRE(config.getValue("configuration") == tempName); REQUIRE(config.solve.numModels == 0); REQUIRE(config.solver(0).heuId == Heuristic_t::Berkmin); - REQUIRE(config.search(0).restart.sched == ScheduleStrategy::geom(100, 1.5)); + REQUIRE(config.search(0).restart.rsSched == ScheduleStrategy::geom(100, 1.5)); REQUIRE(config.solve.numSolver() == 4); REQUIRE(config.numSolver() == 4); REQUIRE(config.solver(1).heuId == Heuristic_t::Vsids); REQUIRE(config.solver(2).heuId == Heuristic_t::Vmtf); REQUIRE(config.solver(3).heuId == Heuristic_t::None); - REQUIRE(config.search(1).restart.sched == ScheduleStrategy::luby(128)); - REQUIRE(config.search(2).restart.sched == ScheduleStrategy(ScheduleStrategy::User, 100, 0.7, 0)); - REQUIRE(config.search(3).restart.sched == ScheduleStrategy::fixed(1000)); + REQUIRE(config.search(1).restart.rsSched == ScheduleStrategy::luby(128)); + REQUIRE(config.search(2).restart.rsSched.isDynamic()); + REQUIRE(config.search(2).restart.base() == 100); + REQUIRE(config.search(2).restart.rsSched.k() == 0.7f); + REQUIRE(config.search(2).restart.rsSched.lbdLim() == 0); + REQUIRE(config.search(3).restart.rsSched == ScheduleStrategy::fixed(1000)); std::remove(tempName); REQUIRE(config.setValue(config.getKey(ClaspCliConfig::KEY_ROOT, "configuration"), tempName) == -2); } diff --git a/tests/solver_test.cpp b/tests/solver_test.cpp index 5897c20..1bd5458 100644 --- a/tests/solver_test.cpp +++ b/tests/solver_test.cpp @@ -1773,6 +1773,22 @@ TEST_CASE("once", "[.once]") { REQUIRE((r1.idx == r2.idx && r1.len == r2.len)); } } + SECTION("testScheduleOverflow") { + ScheduleStrategy g = ScheduleStrategy::geom(100, 0.0); + REQUIRE(g.grow == 1.0); + REQUIRE(g.current() == 100); + + g = ScheduleStrategy::geom(1, 2.0); + REQUIRE(g.current() == 1); + REQUIRE(g.next() == 2); + REQUIRE(g.next() == 4); + g.advanceTo(12); + REQUIRE(g.current() == 4096); + g.advanceTo(63); + REQUIRE(g.current() == (uint64(1) << 63)); + g.advanceTo(64); + REQUIRE(g.current() == UINT64_MAX); + } } #if CLASP_HAS_THREADS