always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] fix bug with negative sized intervals; improve cumulative variable profile

Browse Source
This commit is contained in:
Laurent Perron
2024-04-02 16:17:01 +02:00
committed by Corentin Le Molgat
parent 0ec48be40c
commit 3a08e10bcf
8 changed files with 192 additions and 70 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
ortools/sat/cp_model_search.cc
View File

@@ -632,21 +632,6 @@ absl::flat_hash_map<std::string, SatParameters> 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.

1
ortools/sat/diffn_util.h
View File

@@ -19,6 +19,7 @@
#include <limits>
#include <optional>
#include <ostream>
#include <string>
#include <tuple>
#include <utility>
#include <vector>

2
ortools/sat/docs/integer_arithmetic.md
View File

@@ -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)

123
ortools/sat/docs/scheduling.md
View File

@@ -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

1
ortools/sat/intervals.cc
View File

@@ -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);
}

4
ortools/sat/restart.h
View File

@@ -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_;

114
ortools/sat/samples/cumulative_variable_profile_sample_sat.py
View File

@@ -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]

2
ortools/sat/samples/step_function_sample_sat.go
View File

@@ -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)