SLOTY: add config.objective_lower_bound option

slothy/core/config.py

@@ -450,6 +450,11 @@ def objective_precision(self):
         solution is within 5% of the current estimate for the optimal solution."""
         return self._objective_precision
 
+    @property
+    def objective_lower_bound(self):
+        """A lower bound for the objective at which to stop the search."""
+        return self._objective_lower_bound
+
     @property
     def has_objective(self):
         """Indicates whether a different objective than minimization of stalls
@@ -1143,6 +1148,7 @@ def __init__(self, Arch, Target):
         self._retry_timeout = None
         self._ignore_objective = False
         self._objective_precision = 0
+        self._objective_lower_bound = None
 
         # Visualization
         self.indentation = 8
@@ -1280,6 +1286,9 @@ def ignore_objective(self, val):
     @objective_precision.setter
     def objective_precision(self, val):
         self._objective_precision = val
+    @objective_lower_bound.setter
+    def objective_lower_bound(self, val):
+        self._objective_lower_bound = val
     @absorb_spills.setter
     def absorb_spills(self, val):
         self._absorb_spills = val

slothy/core/core.py

@@ -3392,12 +3392,20 @@ def is_good_enough( cur, bound ):
                 if cur - bound <= self.config.constraints.stalls_precision:
                     self.logger.info("Closer than %d stalls to theoretical optimum... stop", prec)
                     return True
+                if self.config.objective_lower_bound is not None and \
+                   cur <= self.config.objective_lower_bound:
+                    self.logger.info("Reached user-defined objective_lower_bound ... stop", prec)
+                    return True
             elif self._model.objective_name != "no objective":
                 prec = self.config.objective_precision
                 if bound > 0 and abs(1 - (cur / bound)) < prec:
                     self.logger.info("Closer than %d%% to theoretical optimum... stop",
                                         int(prec*100))
                     return True
+                if self.config.objective_lower_bound is not None and \
+                   cur <= self.config.objective_lower_bound:
+                    self.logger.info("Reached user-defined objective_lower_bound ... stop", prec)
+                    return True
             return False
 
         solution_cb = SlothyBase.CpSatSolutionCb(self.logger,self._model.objective_name,