From 4fd5c00ae877b6202254c401a438e322ce584e16 Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Mon, 19 Aug 2024 12:31:54 +0200 Subject: [PATCH] Add option for stopping optimization at given bound. * Add option '--opt-stop' for stopping optimization once a model M with cost(M) less or equal to the given bound is found. --- clasp/cli/clasp_cli_options.inl | 3 +++ clasp/enumerator.h | 1 + clasp/solve_algorithms.h | 4 ++++ src/clasp_facade.cpp | 16 +++++++++------- src/solve_algorithms.cpp | 34 +++++++++++++++++++++++++-------- tests/cli_test.cpp | 26 +++++++++++++++++++++++++ 6 files changed, 69 insertions(+), 15 deletions(-) diff --git a/clasp/cli/clasp_cli_options.inl b/clasp/cli/clasp_cli_options.inl index 45ae3e8..d1733e0 100644 --- a/clasp/cli/clasp_cli_options.inl +++ b/clasp/cli/clasp_cli_options.inl @@ -601,6 +601,9 @@ OPTION(opt_mode , "", ARG_EXT(arg(""), DEFINE_ENUM_MAPPING(MinimizeMode_t " : Set initial bound for objective function(s)", \ FUN(arg) { MinimizeMode_t::Mode m = MinimizeMode_t::optimize; SumVec B; return (arg >> m >> opt(B)) && SET(SELF.optMode, m) && (SELF.optBound.swap(B), true); }, \ GET_FUN(str) { str << SELF.optMode; if (!SELF.optBound.empty()) str << SELF.optBound; }) +OPTION(opt_stop, "", ARG(arg("...")), "Stop optimization on model with cost <= \n", + FUN(arg) { SumVec B; return ITE(arg.peek() != '0' && arg.off(), true, arg >> B) && (SELF.optStop = B, true); }, + GET_FUN(str) { ITE(SELF.optStop.empty(), str << off, str << SELF.optStop); }) GROUP_END(SELF) #undef CLASP_SOLVE_OPTIONS #undef SELF diff --git a/clasp/enumerator.h b/clasp/enumerator.h index b30fab9..f56daf6 100644 --- a/clasp/enumerator.h +++ b/clasp/enumerator.h @@ -92,6 +92,7 @@ struct EnumOptions { ProjMode proMode; /*!< Projection mode to use. */ uint32 project; /*!< Options for projection. */ SumVec optBound; /*!< Initial bound for optimize statements. */ + SumVec optStop; /*!< Optional stop bound for optimization. */ }; const char* modelType(const Model& m); diff --git a/clasp/solve_algorithms.h b/clasp/solve_algorithms.h index bedadec..319432c 100644 --- a/clasp/solve_algorithms.h +++ b/clasp/solve_algorithms.h @@ -150,6 +150,7 @@ class SolveAlgorithm { void setEnumerator(Enumerator& e); void setEnumLimit(uint64 m) { enumLimit_= m; } void setLimits(const SolveLimits& x) { limits_ = x; } + void setOptLimit(const SumVec& bound); //! If set to false, SharedContext::report() is not called for models. /*! * \note The default is true, i.e. models are reported via SharedContext::report(). @@ -240,6 +241,8 @@ class SolveAlgorithm { enum { value_stop = value_false|value_true }; bool attach(SharedContext& ctx, ModelHandler* onModel); void detach(); + bool hasLimit(const Model& m) const; + bool reportModel(Solver& s, bool sym) const; SolveLimits limits_; SharedContext* ctx_; EnumPtr enum_; @@ -247,6 +250,7 @@ class SolveAlgorithm { PathPtr path_; CorePtr core_; uint64 enumLimit_; + SumVec optLimit_; double time_; int last_; bool reportM_; diff --git a/src/clasp_facade.cpp b/src/clasp_facade.cpp index 8274477..bb41060 100644 --- a/src/clasp_facade.cpp +++ b/src/clasp_facade.cpp @@ -470,7 +470,7 @@ struct ClaspFacade::SolveData { ~SolveData() { reset(); } void init(SolveAlgorithm* algo, Enumerator* en); void reset(); - void prepareEnum(SharedContext& ctx, int64 numM, EnumOptions::OptMode opt, EnumMode mode, ProjectMode prj); + void prepareEnum(SharedContext& ctx, EnumMode mode, const EnumOptions& options); bool interrupt(int sig) { if (solving()) { return active->interrupt(sig); } if (!qSig && sig != SolveStrategy::SIGCANCEL) { qSig = sig; } @@ -522,18 +522,20 @@ void ClaspFacade::SolveData::reset() { if (en.get()) { en->reset(); } prepared = solved = false; } -void ClaspFacade::SolveData::prepareEnum(SharedContext& ctx, int64 numM, EnumOptions::OptMode opt, EnumMode mode, ProjectMode proj) { +void ClaspFacade::SolveData::prepareEnum(SharedContext& ctx, EnumMode mode, const EnumOptions& options) { POTASSCO_REQUIRE(!active, "Solve operation still active"); if (ctx.ok() && !ctx.frozen() && !prepared) { if (mode == enum_volatile && ctx.solveMode() == SharedContext::solve_multi) { ctx.requestStepVar(); } - ctx.output.setProjectMode(proj); - int lim = en->init(ctx, opt, (int)Range(-1, INT_MAX).clamp(numM)); - if (lim == 0 || numM < 0) { + ctx.output.setProjectMode(options.proMode); + int64 numM = options.numModels; + int lim = en->init(ctx, options.optMode, (int)Range(-1, INT_MAX).clamp(numM)); + if (lim == 0 || options.numModels < 0) { numM = lim; } algo->setEnumLimit(numM ? static_cast(numM) : UINT64_MAX); + algo->setOptLimit(options.optStop); prepared = true; } } @@ -979,7 +981,7 @@ void ClaspFacade::prepare(EnumMode enumMode) { EnumOptions& en = config_->solve; if (solved()) { doUpdate(0, false, SIG_DFL); - solve_->prepareEnum(ctx, en.numModels, en.optMode, enumMode, en.proMode); + solve_->prepareEnum(ctx, enumMode, en); ctx.endInit(); } if (prepared()) { return; } @@ -1003,7 +1005,7 @@ void ClaspFacade::prepare(EnumMode enumMode) { ctx.setPreserveHeuristic(true); } POTASSCO_REQUIRE(!ctx.ok() || !ctx.frozen()); - solve_->prepareEnum(ctx, en.numModels, en.optMode, enumMode, en.proMode); + solve_->prepareEnum(ctx, enumMode, en); if (!solve_->keepPrg) { builder_ = 0; } else if (isAsp()) { static_cast(builder_.get())->dispose(false); } if (!builder_.get() && !ctx.heuristic.empty()) { diff --git a/src/solve_algorithms.cpp b/src/solve_algorithms.cpp index 53f1e96..4e516e0 100644 --- a/src/solve_algorithms.cpp +++ b/src/solve_algorithms.cpp @@ -254,6 +254,23 @@ void SolveAlgorithm::setEnumerator(Enumerator& e) { enum_.reset(&e); enum_.release(); } +void SolveAlgorithm::setOptLimit(const SumVec& bound) { + optLimit_ = bound; +} +bool SolveAlgorithm::hasLimit(const Model& m) const { + if (!enum_->tentative() && m.num >= enumLimit_) return true; + if (enum_->optimize() && m.costs && !optLimit_.empty()) { + for (std::size_t i = 0, end = std::min(optLimit_.size(), m.costs->size()); i != end; ++i) { + if (optLimit_[i] != (*m.costs)[i]) { + return (*m.costs)[i] < optLimit_[i]; + } + } + return true; + } + return false; +} + + const Model& SolveAlgorithm::model() const { return enum_->lastModel(); } @@ -347,10 +364,7 @@ bool SolveAlgorithm::next() { last_ = doNext(last_); } if (last_ == value_true) { - Solver& s = *ctx_->solver(model().sId); - if (onModel_ && !onModel_->onModel(s, model())) { last_ = value_stop; } - if (reportM_ && !ctx_->report(s, model())) { last_ = value_stop; } - if (!enum_->tentative() && model().num >= enumLimit_) { last_ = value_stop; } + if (!reportModel(*ctx_->solver(model().sId), false)) { last_ = value_stop; } return true; } else { @@ -367,14 +381,18 @@ void SolveAlgorithm::stop() { detach(); } } -bool SolveAlgorithm::reportModel(Solver& s) const { - for (const Model& m = enum_->lastModel();;) { +bool SolveAlgorithm::reportModel(Solver& s, bool sym) const { + for (const Model& m = model();;) { bool r1 = !onModel_ || onModel_->onModel(s, m); bool r2 = !reportM_ || s.sharedContext()->report(s, m); - bool res= r1 && r2 && (enumLimit_ > m.num || enum_->tentative()); - if (!res || (res = !interrupted()) == false || !enum_->commitSymmetric(s)) { return res; } + if (!r1 || !r2 || hasLimit(m) || interrupted()) { return false; } + if (!sym || !enum_->commitSymmetric(s)) { return true; } } } + +bool SolveAlgorithm::reportModel(Solver& s) const { + return reportModel(s, true); +} bool SolveAlgorithm::reportUnsat(Solver& s) const { const Model& m = enum_->lastModel(); EventHandler* h = s.sharedContext()->eventHandler(); diff --git a/tests/cli_test.cpp b/tests/cli_test.cpp index 98fd10c..dbc8af4 100644 --- a/tests/cli_test.cpp +++ b/tests/cli_test.cpp @@ -614,6 +614,32 @@ TEST_CASE("Cli options", "[cli]") { REQUIRE(b.avg == uint32(MovingAvg::Type::avg_sma)); } + SECTION("test opt-stop option") { + SumVec exp; + REQUIRE(config.getValue("solve.opt_stop") == "no"); + REQUIRE(config.solve.optStop.empty()); + + REQUIRE(config.setValue("solve.opt_stop", "10,17")); + REQUIRE(config.getValue("solve.opt_stop") == "10,17"); + exp.push_back(10); + exp.push_back(17); + REQUIRE(config.solve.optStop == exp); + + REQUIRE(config.setValue("solve.opt_stop", "-4")); + REQUIRE(config.getValue("solve.opt_stop") == "-4"); + exp.assign(1, -4); + REQUIRE(config.solve.optStop == exp); + + REQUIRE(config.setValue("solve.opt_stop", "off")); + REQUIRE(config.getValue("solve.opt_stop") == "no"); + REQUIRE(config.solve.optStop.empty()); + + REQUIRE(config.setValue("solve.opt_stop", "0")); + REQUIRE(config.getValue("solve.opt_stop") == "0"); + exp.assign(1, 0); + REQUIRE(config.solve.optStop == exp); + } + SECTION("test get values") { std::string out; REQUIRE(config.getValue(config.getKey(ClaspCliConfig::KEY_TESTER, "configuration"), out) == -1);