Register CP-SAT decision strategy to stabilize solve times; Switch to ortools 9.15

pyproject.toml

@@ -44,12 +44,7 @@ classifiers = [
 ]
 requires-python = ">=3.10"
 dependencies = [
-    "ortools==9.7.2996; python_version < '3.12'",
-    # ortools depends on pandas, but 9.7 does not specify it as dependency
-    "pandas>=2.0.3; python_version < '3.12'",
-    # ortools 9.7 requires protobuf<=6.31.1
-    "protobuf<=6.31.1; python_version < '3.12'",
-    "ortools==9.15.6755; python_version >= '3.12'",
+    "ortools==9.15.6755",
     "sympy==1.14.0",
     "unicorn==2.1.4",
 ]

requirements.txt

@@ -1,9 +1,4 @@
-ortools==9.7.2996 ; python_version < "3.12"
-ortools==9.15.6755 ; python_version >= "3.12"
-# ortools 9.7 requires protobuf<=6.31.1
-protobuf<=6.31.1 ; python_version < "3.12"
-# ortools depends on pandas, but 9.7 does not specify it as dependency
-pandas>=2.3.3 ; python_version < "3.12"
+ortools==9.15.6755
 sympy==1.14.0
 unicorn==2.1.4
 black==26.5.1

slothy/core/config.py

@@ -333,6 +333,29 @@ def variable_size(self):
         """
         return self._variable_size
 
+    @property
+    def solver_search_strategy(self):
+        """Decision strategy to register with the CP-SAT solver.
+
+        CP-SAT's "fixed" subsolver follows decision strategies registered in the
+        model. Guiding it explicitly makes solve times reproducible and fast for
+        SLOTHY's scheduling models; without a strategy, OR-Tools >= 9.8 relies on
+        its internal scheduling heuristic, whose randomized tie-breaking makes
+        solve times on large models highly variable, frequently exceeding
+        timeouts.
+
+        Valid values:
+
+        - "lowest_min" (default): branch on the instruction with the earliest
+          possible position, trying the earliest position first. This mimics a
+          greedy earliest-first scheduling pass.
+        - "program_order": branch on instruction positions in original program
+          order, trying the earliest position first.
+        - "auto": do not register a strategy; leave the search entirely to the
+          solver's internal heuristics (previous behavior).
+        """
+        return self._solver_search_strategy
+
     @property
     def keep_tags(self):
         """Indicates whether tags in the input source should be kept or removed.
@@ -1460,6 +1483,7 @@ def __init__(self, Arch, Target, logger):
         self.mirror_char = "~"
 
         self.solver_random_seed = 42
+        self._solver_search_strategy = "lowest_min"
 
         self._log_dir = "."
         self._log_model = None
@@ -1524,6 +1548,15 @@ def reserved_regs_are_locked(self, val):
     def variable_size(self, val):
         self._variable_size = val
 
+    @solver_search_strategy.setter
+    def solver_search_strategy(self, val):
+        if val not in ["program_order", "lowest_min", "auto"]:
+            raise InvalidConfig(
+                "Invalid solver_search_strategy: "
+                f"{val} (expected 'program_order', 'lowest_min', or 'auto')"
+            )
+        self._solver_search_strategy = val
+
     @selftest.setter
     def selftest(self, val):
         self._selftest = val

slothy/core/core.py

@@ -1730,6 +1730,8 @@ def optimize(self, source, prefix_len=0, suffix_len=0, log_model=None, retry=Fal
 
         # - Objective
         self._add_objective()
+        # - Search strategy
+        self._add_search_strategy()
         self._result = Result(self.config)
 
         # Do the actual work
@@ -3990,6 +3992,22 @@ def _add_objective(self, force_objective=False):
             self.logger.info("Objective: None (any satisfying solution is fine)")
             self._model.objective_name = "no objective"
 
+    def _add_search_strategy(self):
+        # See Config.solver_search_strategy for the rationale.
+        strategy = self.config.solver_search_strategy
+        if strategy == "auto":
+            return
+        var_strategy = {
+            "program_order": cp_model.CHOOSE_FIRST,
+            "lowest_min": cp_model.CHOOSE_LOWEST_MIN,
+        }[strategy]
+        position_vars = [t.program_start_var for t in self._get_nodes()]
+        if len(position_vars) == 0:
+            return
+        self._AddDecisionStrategy(
+            position_vars, var_strategy, cp_model.SELECT_MIN_VALUE
+        )
+
     #
     # Dummy wrappers around CP-SAT
     #
@@ -4005,7 +4023,7 @@ def _describe_solver(self):
     def _init_external_model_and_solver(self):
         self._model.cp_model = cp_model.CpModel()
         self._model.cp_solver = cp_model.CpSolver()
-        self._model.cp_solver.random_seed = self.config.solver_random_seed
+        self._model.cp_solver.parameters.random_seed = self.config.solver_random_seed
 
     def _NewIntVar(self, minval, maxval, name=""):
         r = self._model.cp_model.NewIntVar(minval, maxval, name)
@@ -4057,6 +4075,11 @@ def _AddHint(self, var, val):
     def _AddMaxEquality(self, varlist, var):
         return self._model.cp_model.AddMaxEquality(varlist, var)
 
+    def _AddDecisionStrategy(self, varlist, var_strategy, value_strategy):
+        return self._model.cp_model.AddDecisionStrategy(
+            varlist, var_strategy, value_strategy
+        )
+
     def _export_model(self):
         if self.config.log_model is None:
             return