From 4d9321af4f6cf3459a4ef809a98bf3b48d6de9a6 Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Tue, 3 Nov 2026 17:36:52 +0100 Subject: [PATCH 1/2] Make the FlatZinc float improvement cut strict in the objective bound The cut obj < best - step was posted as obj <= best - step plus a disequality that only fails once the objective is assigned. The incumbent value therefore stayed inside the objective bounds, and proving optimality could require splitting the other float variables down to single ulps. The model in MiniZinc/MiniZincIDE#220 found its optimum at once and then did not finish proving it. Post obj <= pred(lo(best - step)) when minimizing and obj >= succ(hi(best + step)) when maximizing instead. On assigned objectives this admits exactly the solutions the old cut admitted, so step 0 stays exact, but the incumbent value is pruned immediately. The issue model now proves optimality in 358 nodes instead of running indefinitely. Also initialize the step in the default constructor and read it before the Gist branch, which previously used it uninitialized. --- changelog.in | 12 +++++++++ gecode/flatzinc/flatzinc.cpp | 40 ++++++++++++++++++++++-------- test/flatzinc.cpp | 48 ++++++++++++++++++++++++++++++++++++ 3 files changed, 90 insertions(+), 10 deletions(-) diff --git a/changelog.in b/changelog.in index e757356aa0..4924ae9e8b 100755 --- a/changelog.in +++ b/changelog.in @@ -75,6 +75,18 @@ Date: unreleased [DESCRIPTION] This is the development changelog for the next Gecode release. +[ENTRY] +Module: flatzinc +What: bug +Rank: minor +Thanks: Hillel Wayne +[DESCRIPTION] +Make the improvement cut for float objectives strict in the objective bound. +The cut kept the incumbent objective value until the objective was assigned, +so proving optimality could split other float variables down to single ulps +and fail to finish. Assigned objectives are accepted exactly as before, also +with step 0. + [RELEASE] Version: 6.5.0 Date: 2026-10-31 diff --git a/gecode/flatzinc/flatzinc.cpp b/gecode/flatzinc/flatzinc.cpp index 0d525dd1f0..8f1a11a87c 100644 --- a/gecode/flatzinc/flatzinc.cpp +++ b/gecode/flatzinc/flatzinc.cpp @@ -49,6 +49,7 @@ #include #include #include +#include #include #include @@ -865,7 +866,11 @@ namespace Gecode { namespace FlatZinc { intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1), _optVar(-1), _optVarIsInt(true), _lns(0), _lnsInitialSolution(0), _random(random), - _solveAnnotations(nullptr), needAuxVars(true) { + _solveAnnotations(nullptr), +#ifdef GECODE_HAS_FLOAT_VARS + step(0.0), +#endif + needAuxVars(true) { branchInfo.init(); } @@ -1871,6 +1876,9 @@ namespace Gecode { namespace FlatZinc { void FlatZincSpace::runMeta(std::ostream& out, const Printer& p, const FlatZincOptions& opt, Support::Timer& t_total) { +#ifdef GECODE_HAS_FLOAT_VARS + step = opt.step(); +#endif #ifdef GECODE_HAS_GIST if (opt.mode() == SM_GIST) { BlackBoxContextHandle& black_box_context = BlackBoxAccess::context(*this); @@ -1917,9 +1925,6 @@ namespace Gecode { namespace FlatZinc { #endif -#ifdef GECODE_HAS_FLOAT_VARS - step = opt.step(); -#endif o.threads = opt.threads(); o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0; if (opt.restart() != RM_NONE) @@ -2068,12 +2073,27 @@ namespace Gecode { namespace FlatZinc { static_cast(&s)->iv[_optVar].val()); } else { #ifdef GECODE_HAS_FLOAT_VARS - if (_method == MIN) - rel(*this, fv[_optVar], FRT_LE, - static_cast(&s)->fv[_optVar].val()-step); - else if (_method == MAX) - rel(*this, fv[_optVar], FRT_GR, - static_cast(&s)->fv[_optVar].val()+step); + FloatVal best = static_cast(&s)->fv[_optVar].val(); + // When minimizing, an assigned objective is below best - step + // exactly when its upper bound is below the lower bound of that + // interval (symmetrically when maximizing). Posting this strict + // bound prunes the incumbent value before the objective is + // assigned, and also guarantees progress when it never is. + if (_method == MIN) { + FloatNum n = (best-step).min(); + if (n <= Float::Limits::min) + fail(); + else + rel(*this, fv[_optVar], FRT_LQ, + std::nextafter(n, Float::Limits::min)); + } else if (_method == MAX) { + FloatNum n = (best+step).max(); + if (n >= Float::Limits::max) + fail(); + else + rel(*this, fv[_optVar], FRT_GQ, + std::nextafter(n, Float::Limits::max)); + } #endif } } diff --git a/test/flatzinc.cpp b/test/flatzinc.cpp index c1845f8522..3430570d6c 100755 --- a/test/flatzinc.cpp +++ b/test/flatzinc.cpp @@ -65,6 +65,54 @@ namespace Test { namespace FlatZinc { TupleSetAutoRepresentation tuple_set_auto_representation; +#ifdef GECODE_HAS_FLOAT_VARS + /// Verify that the float improvement cut prunes the incumbent value + /// before the objective is assigned. + class FloatCutExcludesIncumbent : public Base { + private: + /// Return the objective bound after constraining by an incumbent + /// with objective 0.5 + static bool cutBound(const std::string& source, + Gecode::FloatNum& bound) { + using Gecode::FlatZinc::FlatZincSpace; + Gecode::FlatZinc::Printer p; + std::stringstream ss(source); + std::unique_ptr + fg(Gecode::FlatZinc::parse(ss, p, olog)); + if (!fg || (fg->status() == Gecode::SS_FAILED)) + return false; + std::unique_ptr + best(static_cast(fg->clone())); + Gecode::rel(*best, best->fv[0], Gecode::FRT_EQ, 0.5); + if (best->status() == Gecode::SS_FAILED) + return false; + std::unique_ptr + s(static_cast(fg->clone())); + s->constrain(*best); + if ((s->status() == Gecode::SS_FAILED) || s->fv[0].assigned()) + return false; + bound = (source.find("minimize") != std::string::npos) ? + s->fv[0].max() : s->fv[0].min(); + return true; + } + public: + FloatCutExcludesIncumbent(void) + : Base("FlatZinc::Float::CutExcludesIncumbent") {} + + virtual bool run(void) { + Gecode::FloatNum minBound, maxBound; + return + cutBound("var 0.0..1.0: x :: output_var;\nsolve minimize x;\n", + minBound) && + cutBound("var 0.0..1.0: x :: output_var;\nsolve maximize x;\n", + maxBound) && + (minBound < 0.5) && (maxBound > 0.5); + } + }; + + FloatCutExcludesIncumbent float_cut_excludes_incumbent; +#endif + /// Verify that statistics do not override an explicit Gist mode. class GistStatisticsMode : public Base { private: From 6de487988033abae1ecdd4f190aa8aac8c3985ab Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Tue, 3 Nov 2026 18:19:05 +0100 Subject: [PATCH 2/2] Make the MiniModel float improvement cuts strict in the cost bound FloatMinimizeSpace and FloatMaximizeSpace posted cost < best - step as cost <= best - step plus a disequality that fails only once the cost is assigned, so the incumbent cost stayed inside the cost bounds until then, as in the FlatZinc cut fixed by the previous commit. Post cost <= pred(lo(best - step)) when minimizing and cost >= succ(hi(best + step)) when maximizing, computing the difference with outward rounding. With step 0 this accepts exactly the assigned costs the old cut accepted; with a positive step it no longer admits an improvement smaller than the step through rounding. The float spiral and folium examples find the same solutions in 3 to 4 percent fewer nodes. --- changelog.in | 11 ++++++ gecode/minimodel/optimize.cpp | 18 ++++++++-- test/float/basic.cpp | 63 +++++++++++++++++++++++++++++++++++ 3 files changed, 90 insertions(+), 2 deletions(-) diff --git a/changelog.in b/changelog.in index 4924ae9e8b..a4cfdd05f9 100755 --- a/changelog.in +++ b/changelog.in @@ -87,6 +87,17 @@ so proving optimality could split other float variables down to single ulps and fail to finish. Assigned objectives are accepted exactly as before, also with step 0. +[ENTRY] +Module: minimodel +What: bug +Rank: minor +[DESCRIPTION] +Make the improvement cuts of FloatMinimizeSpace and FloatMaximizeSpace strict +in the cost bound, so the incumbent cost is pruned before the cost is +assigned. A new solution must now improve by at least the step, without the +rounding of the step subtraction admitting a smaller improvement. With step 0, +assigned costs are accepted exactly as before. + [RELEASE] Version: 6.5.0 Date: 2026-10-31 diff --git a/gecode/minimodel/optimize.cpp b/gecode/minimodel/optimize.cpp index 6442ada179..9e0afca3b8 100755 --- a/gecode/minimodel/optimize.cpp +++ b/gecode/minimodel/optimize.cpp @@ -33,6 +33,8 @@ #include +#include + namespace Gecode { void @@ -89,7 +91,15 @@ namespace Gecode { dynamic_cast(&_best); if (best == nullptr) throw DynamicCastFailed("FloatMinimizeSpace::constrain"); - rel(*this, cost(), FRT_LE, best->cost().max()-step); + // An assigned cost is below the bound of the best solution minus the + // step exactly when its upper bound is below the lower bound of that + // difference. Posting this strict bound prunes the incumbent value + // before the cost is assigned. + FloatNum n = (FloatVal(best->cost().max())-step).min(); + if (n <= Float::Limits::min) + fail(); + else + rel(*this, cost(), FRT_LQ, std::nextafter(n, Float::Limits::min)); } @@ -99,7 +109,11 @@ namespace Gecode { dynamic_cast(&_best); if (best == nullptr) throw DynamicCastFailed("FloatMaximizeSpace::constrain"); - rel(*this, cost(), FRT_GR, best->cost().min()+step); + FloatNum n = (FloatVal(best->cost().min())+step).max(); + if (n >= Float::Limits::max) + fail(); + else + rel(*this, cost(), FRT_GQ, std::nextafter(n, Float::Limits::max)); } #endif diff --git a/test/float/basic.cpp b/test/float/basic.cpp index 7e747821bb..ec75979cbd 100644 --- a/test/float/basic.cpp +++ b/test/float/basic.cpp @@ -35,7 +35,10 @@ #include "test/float.hh" +#include + #include +#include namespace Test { namespace Float { @@ -116,6 +119,66 @@ namespace Test { namespace Float { namespace { Median median; } + + /// Space minimizing or maximizing a single float variable + template + class OptimizeSpace : public Optimize { + public: + /// The cost variable + Gecode::FloatVar x; + /// Create space with cost variable in [0,1] + OptimizeSpace(void) : x(*this,0.0,1.0) {} + /// Constructor for cloning \a s + OptimizeSpace(OptimizeSpace& s) : Optimize(s) { + x.update(*this,s.x); + } + /// Copy during cloning + virtual Gecode::Space* copy(void) { + return new OptimizeSpace(*this); + } + /// Return cost + virtual Gecode::FloatVar cost(void) const { + return x; + } + }; + + /// Test that the MiniModel float cuts prune the incumbent value + class OptimizeCut : public Base { + private: + /// Return whether constraining by an incumbent with cost 0.5 leaves + /// an unassigned cost and store its remaining domain in \a d + template + static bool cut(Gecode::FloatVal& d) { + using namespace Gecode; + OptimizeSpace root; + std::unique_ptr> + best(static_cast*>(root.clone())); + rel(*best, best->x, FRT_EQ, 0.5); + if (best->status() == SS_FAILED) + return false; + std::unique_ptr> + s(static_cast*>(root.clone())); + s->constrain(*best); + if ((s->status() == SS_FAILED) || s->x.assigned()) + return false; + d = s->x.domain(); + return true; + } + public: + /// Create and register test + OptimizeCut(void) : Base("Float::Basic::OptimizeCut") {} + /// Perform test + virtual bool run(void) { + using namespace Gecode; + FloatVal min, max; + return cut(min) && cut(max) && + (min.max() < 0.5) && (max.min() > 0.5); + } + }; + + namespace { + OptimizeCut optimize_cut; + } //@} }