diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 2d201bb642..71fae1e0bb 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -632,21 +632,6 @@ absl::flat_hash_map GetNamedParameters( strategies["fixed"] = new_params; } - // Inprocessing - { - SatParameters new_params = base_params; - new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH); - new_params.set_use_sat_inprocessing(false); - strategies["no_inprocessing"] = new_params; - - new_params.set_use_sat_inprocessing(true); - new_params.set_inprocessing_dtime_ratio(1.0); - strategies["max_inprocessing"] = new_params; - - new_params.set_linearization_level(0); - strategies["max_inprocessing_no_lp"] = new_params; - } - // Quick restart. { // TODO(user): Experiment with search_random_variable_pool_size. diff --git a/ortools/sat/diffn_util.h b/ortools/sat/diffn_util.h index 685cb0ff99..4cd568edab 100644 --- a/ortools/sat/diffn_util.h +++ b/ortools/sat/diffn_util.h @@ -19,6 +19,7 @@ #include #include #include +#include #include #include #include diff --git a/ortools/sat/docs/integer_arithmetic.md b/ortools/sat/docs/integer_arithmetic.md index efdf3884f6..6907e4bb5a 100644 --- a/ortools/sat/docs/integer_arithmetic.md +++ b/ortools/sat/docs/integer_arithmetic.md @@ -1163,7 +1163,7 @@ func stepFunctionSampleSat() error { // expr == 2 on [0, 1] U [3, 4] U [11, 20] b2 := model.NewBoolVar() - d2 := cpmodel.FromIntervals([]cpmodel.ClosedInterval{{0, 1}, {3, 4}, {11, 20}}) + d2 := cpmodel.FromIntervals([]cpmodel.ClosedInterval{{Start: 0, End: 1}, {Start: 3, End: 4}, {Start: 11, End: 20}}) model.AddLinearConstraintForDomain(x, d2).OnlyEnforceIf(b2) model.AddEquality(expr, cpmodel.NewConstant(2)).OnlyEnforceIf(b2) diff --git a/ortools/sat/docs/scheduling.md b/ortools/sat/docs/scheduling.md index 87a186bdad..5aad73d5c2 100644 --- a/ortools/sat/docs/scheduling.md +++ b/ortools/sat/docs/scheduling.md @@ -826,33 +826,37 @@ func main() { } ``` -## Cumulative constraint with varying capacity profile. +## Cumulative constraint with min and max capacity profile. A cumulative constraint takes a list of intervals, and a list of demands, and a capacity. It enforces that at any time point, the sum of demands of tasks active at that time point is less than a given capacity. -Modeling a varying profile can be done using fixed (interval, demand) to occupy -the capacity between the actual profile and it max capacity. +Modeling a non constant max profile can be done using fixed (interval, demand) +to occupy the capacity between the actual profile and it max capacity. + +Modeling a non zero min profile can be done using fixed (interval, demand) +on the complementary cumulative constraint. ### Python code ```python #!/usr/bin/env python3 -"""Solves a simple scheduling problem with a variable work load.""" +"""Solves a scheduling problem with a min and max profile for the work load.""" import io +from absl import app import pandas as pd from ortools.sat.python import cp_model -def create_data_model() -> tuple[pd.DataFrame, pd.DataFrame]: +def create_data_model() -> tuple[pd.DataFrame, pd.DataFrame, pd.DataFrame]: """Creates the two dataframes that describes the model.""" - capacity_str: str = """ - start_hour capacity + max_load_str: str = """ + start_hour max_load 0 0 2 0 4 1 @@ -867,6 +871,22 @@ def create_data_model() -> tuple[pd.DataFrame, pd.DataFrame]: 22 0 """ + min_load_str: str = """ + start_hour min_load + 0 0 + 2 0 + 4 0 + 6 0 + 8 3 + 10 3 + 12 1 + 14 3 + 16 3 + 18 1 + 20 1 + 22 0 + """ + tasks_str: str = """ name duration load priority t1 60 3 2 @@ -901,24 +921,25 @@ def create_data_model() -> tuple[pd.DataFrame, pd.DataFrame]: t30 90 4 2 """ - capacity_df = pd.read_table(io.StringIO(capacity_str), sep=r"\s+") + max_load_df = pd.read_table(io.StringIO(max_load_str), sep=r"\s+") + min_load_df = pd.read_table(io.StringIO(min_load_str), sep=r"\s+") tasks_df = pd.read_table(io.StringIO(tasks_str), index_col=0, sep=r"\s+") - return capacity_df, tasks_df + return max_load_df, min_load_df, tasks_df -def main() -> None: +def main(_) -> None: """Create the model and solves it.""" - capacity_df, tasks_df = create_data_model() + max_load_df, min_load_df, tasks_df = create_data_model() # Create the model. model = cp_model.CpModel() # Get the max capacity from the capacity dataframe. - max_capacity = capacity_df.capacity.max() - print(f"Max capacity = {max_capacity}") + max_load = max_load_df.max_load.max() + print(f"Max capacity = {max_load}") print(f"#tasks = {len(tasks_df)}") - minutes_per_period: int = 120 + minutes_per_hour: int = 60 horizon: int = 24 * 60 # Variables @@ -935,21 +956,67 @@ def main() -> None: are_present=performed, ) - # Set up the profile. We use fixed (intervals, demands) to fill in the space - # between the actual load profile and the max capacity. - time_period_intervals = model.new_fixed_size_interval_var_series( - name="time_period_intervals", - index=capacity_df.index, - starts=capacity_df.start_hour * minutes_per_period, - sizes=minutes_per_period, + # Set up complement intervals (from 0 to start, and from start + size to + # horizon). + prefix_intervals = model.new_optional_interval_var_series( + name="prefix_intervals", + index=tasks_df.index, + starts=0, + sizes=starts, + ends=starts, + are_present=performed, ) - time_period_heights = max_capacity - capacity_df.capacity - # Cumulative constraint. + suffix_intervals = model.new_optional_interval_var_series( + name="suffix_intervals", + index=tasks_df.index, + starts=starts + tasks_df.duration, + sizes=horizon - starts - tasks_df.duration, + ends=horizon, + are_present=performed, + ) + + # Set up the max profile. We use fixed (intervals, demands) to fill in the + # space between the actual max load profile and the max capacity. + time_period_max_intervals = model.new_fixed_size_interval_var_series( + name="time_period_max_intervals", + index=max_load_df.index, + starts=max_load_df.start_hour * minutes_per_hour, + sizes=minutes_per_hour * 2, + ) + time_period_max_heights = max_load - max_load_df.max_load + + # Cumulative constraint for the max profile. model.add_cumulative( - intervals.to_list() + time_period_intervals.to_list(), - tasks_df.load.to_list() + time_period_heights.to_list(), - max_capacity, + intervals.to_list() + time_period_max_intervals.to_list(), + tasks_df.load.to_list() + time_period_max_heights.to_list(), + max_load, + ) + + # Set up the min profile. We use complement intervals to maintain the + # complement of the work load, and fixed intervals to enforce the min + # number of active workers per time period. + time_period_min_intervals = model.new_fixed_size_interval_var_series( + name="time_period_min_intervals", + index=min_load_df.index, + starts=min_load_df.start_hour * minutes_per_hour, + sizes=minutes_per_hour * 2, + ) + time_period_min_heights = min_load_df.min_load + + sum_of_demands = sum(tasks_df.load) + complement_capacity = model.new_int_var(0, sum_of_demands, "complement_capacity") + model.add(complement_capacity == performed.dot(tasks_df.load)) + + # Cumulative constraint for the min profile. + model.add_cumulative( + prefix_intervals.to_list() + + suffix_intervals.to_list() + + time_period_min_intervals.to_list(), + tasks_df.load.to_list() + + tasks_df.load.to_list() + + time_period_min_heights.to_list(), + complement_capacity, ) # Objective: maximize the value of performed intervals. @@ -960,7 +1027,7 @@ def main() -> None: # Create the solver and solve the model. solver = cp_model.CpSolver() solver.parameters.log_search_progress = True - solver.parameters.num_workers = 8 + solver.parameters.num_workers = 16 solver.parameters.max_time_in_seconds = 30.0 status = solver.solve(model) @@ -979,7 +1046,7 @@ def main() -> None: if __name__ == "__main__": - main() + app.run(main) ``` ## Alternative resources for one interval diff --git a/ortools/sat/intervals.cc b/ortools/sat/intervals.cc index b01fff7707..5fef5f10c8 100644 --- a/ortools/sat/intervals.cc +++ b/ortools/sat/intervals.cc @@ -344,6 +344,7 @@ bool SchedulingConstraintHelper::UpdateCachedValues(int t) { // Detect first if we have a conflict using the relation start + size = end. if (dmax < 0) { + ClearReason(); AddSizeMaxReason(t, dmax); return PushTaskAbsence(t); } diff --git a/ortools/sat/restart.h b/ortools/sat/restart.h index 7ec167c476..ea8a9d4c2e 100644 --- a/ortools/sat/restart.h +++ b/ortools/sat/restart.h @@ -57,6 +57,10 @@ class RestartPolicy { // Returns a string with the current restart statistics. std::string InfoString() const; + const RunningAverage& LbdRunningAverage() const { + return lbd_running_average_; + } + private: const SatParameters& parameters_; SatDecisionPolicy* decision_policy_; diff --git a/ortools/sat/samples/cumulative_variable_profile_sample_sat.py b/ortools/sat/samples/cumulative_variable_profile_sample_sat.py index 21736d5991..8e6df0a3b5 100644 --- a/ortools/sat/samples/cumulative_variable_profile_sample_sat.py +++ b/ortools/sat/samples/cumulative_variable_profile_sample_sat.py @@ -12,12 +12,13 @@ # See the License for the specific language governing permissions and # limitations under the License. -"""Solves a simple scheduling problem with a variable work load.""" +"""Solves a scheduling problem with a min and max profile for the work load.""" # [START program] # [START import] import io +from absl import app import pandas as pd from ortools.sat.python import cp_model @@ -26,11 +27,11 @@ from ortools.sat.python import cp_model # [START program_part1] # [START data_model] -def create_data_model() -> tuple[pd.DataFrame, pd.DataFrame]: +def create_data_model() -> tuple[pd.DataFrame, pd.DataFrame, pd.DataFrame]: """Creates the two dataframes that describes the model.""" - capacity_str: str = """ - start_hour capacity + max_load_str: str = """ + start_hour max_load 0 0 2 0 4 1 @@ -45,6 +46,22 @@ def create_data_model() -> tuple[pd.DataFrame, pd.DataFrame]: 22 0 """ + min_load_str: str = """ + start_hour min_load + 0 0 + 2 0 + 4 0 + 6 0 + 8 3 + 10 3 + 12 1 + 14 3 + 16 3 + 18 1 + 20 1 + 22 0 + """ + tasks_str: str = """ name duration load priority t1 60 3 2 @@ -79,16 +96,17 @@ def create_data_model() -> tuple[pd.DataFrame, pd.DataFrame]: t30 90 4 2 """ - capacity_df = pd.read_table(io.StringIO(capacity_str), sep=r"\s+") + max_load_df = pd.read_table(io.StringIO(max_load_str), sep=r"\s+") + min_load_df = pd.read_table(io.StringIO(min_load_str), sep=r"\s+") tasks_df = pd.read_table(io.StringIO(tasks_str), index_col=0, sep=r"\s+") - return capacity_df, tasks_df + return max_load_df, min_load_df, tasks_df # [END data_model] -def main() -> None: +def main(_) -> None: """Create the model and solves it.""" # [START data] - capacity_df, tasks_df = create_data_model() + max_load_df, min_load_df, tasks_df = create_data_model() # [END data] # [END program_part1] @@ -98,11 +116,11 @@ def main() -> None: # [END model] # Get the max capacity from the capacity dataframe. - max_capacity = capacity_df.capacity.max() - print(f"Max capacity = {max_capacity}") + max_load = max_load_df.max_load.max() + print(f"Max capacity = {max_load}") print(f"#tasks = {len(tasks_df)}") - minutes_per_period: int = 120 + minutes_per_hour: int = 60 horizon: int = 24 * 60 # [START program_part2] @@ -120,24 +138,70 @@ def main() -> None: sizes=tasks_df.duration, are_present=performed, ) + + # Set up complement intervals (from 0 to start, and from start + size to + # horizon). + prefix_intervals = model.new_optional_interval_var_series( + name="prefix_intervals", + index=tasks_df.index, + starts=0, + sizes=starts, + ends=starts, + are_present=performed, + ) + + suffix_intervals = model.new_optional_interval_var_series( + name="suffix_intervals", + index=tasks_df.index, + starts=starts + tasks_df.duration, + sizes=horizon - starts - tasks_df.duration, + ends=horizon, + are_present=performed, + ) # [END variables] # [START constraints] - # Set up the profile. We use fixed (intervals, demands) to fill in the space - # between the actual load profile and the max capacity. - time_period_intervals = model.new_fixed_size_interval_var_series( - name="time_period_intervals", - index=capacity_df.index, - starts=capacity_df.start_hour * minutes_per_period, - sizes=minutes_per_period, + # Set up the max profile. We use fixed (intervals, demands) to fill in the + # space between the actual max load profile and the max capacity. + time_period_max_intervals = model.new_fixed_size_interval_var_series( + name="time_period_max_intervals", + index=max_load_df.index, + starts=max_load_df.start_hour * minutes_per_hour, + sizes=minutes_per_hour * 2, ) - time_period_heights = max_capacity - capacity_df.capacity + time_period_max_heights = max_load - max_load_df.max_load - # Cumulative constraint. + # Cumulative constraint for the max profile. model.add_cumulative( - intervals.to_list() + time_period_intervals.to_list(), - tasks_df.load.to_list() + time_period_heights.to_list(), - max_capacity, + intervals.to_list() + time_period_max_intervals.to_list(), + tasks_df.load.to_list() + time_period_max_heights.to_list(), + max_load, + ) + + # Set up the min profile. We use complement intervals to maintain the + # complement of the work load, and fixed intervals to enforce the min + # number of active workers per time period. + time_period_min_intervals = model.new_fixed_size_interval_var_series( + name="time_period_min_intervals", + index=min_load_df.index, + starts=min_load_df.start_hour * minutes_per_hour, + sizes=minutes_per_hour * 2, + ) + time_period_min_heights = min_load_df.min_load + + sum_of_demands = sum(tasks_df.load) + complement_capacity = model.new_int_var(0, sum_of_demands, "complement_capacity") + model.add(complement_capacity == performed.dot(tasks_df.load)) + + # Cumulative constraint for the min profile. + model.add_cumulative( + prefix_intervals.to_list() + + suffix_intervals.to_list() + + time_period_min_intervals.to_list(), + tasks_df.load.to_list() + + tasks_df.load.to_list() + + time_period_min_heights.to_list(), + complement_capacity, ) # [END constraints] @@ -152,7 +216,7 @@ def main() -> None: # Create the solver and solve the model. solver = cp_model.CpSolver() solver.parameters.log_search_progress = True - solver.parameters.num_workers = 8 + solver.parameters.num_workers = 16 solver.parameters.max_time_in_seconds = 30.0 status = solver.solve(model) # [END solve] @@ -174,6 +238,6 @@ def main() -> None: if __name__ == "__main__": - main() + app.run(main) # [END program_part2] # [END program] diff --git a/ortools/sat/samples/step_function_sample_sat.go b/ortools/sat/samples/step_function_sample_sat.go index 3545973734..5fb4e66f9f 100644 --- a/ortools/sat/samples/step_function_sample_sat.go +++ b/ortools/sat/samples/step_function_sample_sat.go @@ -51,7 +51,7 @@ func stepFunctionSampleSat() error { // expr == 2 on [0, 1] U [3, 4] U [11, 20] b2 := model.NewBoolVar() - d2 := cpmodel.FromIntervals([]cpmodel.ClosedInterval{{0, 1}, {3, 4}, {11, 20}}) + d2 := cpmodel.FromIntervals([]cpmodel.ClosedInterval{{Start: 0, End: 1}, {Start: 3, End: 4}, {Start: 11, End: 20}}) model.AddLinearConstraintForDomain(x, d2).OnlyEnforceIf(b2) model.AddEquality(expr, cpmodel.NewConstant(2)).OnlyEnforceIf(b2)