27 #include "ortools/sat/sat_parameters.pb.h"
36 const std::vector<IntervalVariable>& vars,
40 if (vars.empty())
return;
51 for (
int i = 0; i < demands.size(); ++i) {
52 if (intervals->MaxSize(vars[i]) == 0)
continue;
55 builder.
AddTerm(demands[i], IntegerValue(1));
59 std::vector<Literal> enforcement_literals;
60 if (intervals->IsOptional(vars[i])) {
61 enforcement_literals.push_back(intervals->PresenceLiteral(vars[i]));
67 if (intervals->MinSize(vars[i]) == 0) {
68 enforcement_literals.push_back(encoder->GetOrCreateAssociatedLiteral(
69 intervals->Size(vars[i]).GreaterOrEqual(IntegerValue(1))));
72 if (enforcement_literals.empty()) {
79 if (vars.size() == 1)
return;
81 const SatParameters&
parameters = *(
model->GetOrCreate<SatParameters>());
85 if (
parameters.use_disjunctive_constraint_in_cumulative_constraint()) {
93 std::vector<IntervalVariable> in_disjunction;
94 for (
int i = 0; i < vars.size(); ++i) {
95 if (intervals->MinSize(vars[i]) > 0 &&
96 2 * integer_trail->LowerBound(demands[i]) >
97 integer_trail->UpperBound(
capacity)) {
98 in_disjunction.push_back(vars[i]);
119 if (in_disjunction.size() == vars.size())
return;
122 if (helper ==
nullptr) {
124 model->TakeOwnership(helper);
133 model->TakeOwnership(time_tabling);
137 if (
parameters.use_overload_checker_in_cumulative_constraint()) {
144 if (
parameters.use_timetable_edge_finding_in_cumulative_constraint()) {
148 model->TakeOwnership(time_table_edge_finding);
154 const std::vector<IntervalVariable>& vars,
158 if (vars.empty())
return;
162 const Coefficient fixed_capacity(
165 const int num_tasks = vars.size();
170 std::vector<IntegerVariable> start_vars;
171 std::vector<IntegerVariable> end_vars;
172 std::vector<IntegerValue> fixed_demands;
174 for (
int t = 0; t < num_tasks; ++t) {
175 start_vars.push_back(intervals->StartVar(vars[t]));
176 end_vars.push_back(intervals->EndVar(vars[t]));
178 fixed_demands.push_back(integer_trail->
LowerBound(demands[t]));
184 for (
int t = 0; t < num_tasks; ++t) {
189 for (IntegerValue
time = min_start;
time < max_end; ++
time) {
190 std::vector<LiteralWithCoeff> literals_with_coeff;
191 for (
int t = 0; t < num_tasks; ++t) {
200 std::vector<Literal> consume_condition;
204 if (intervals->IsOptional(vars[t])) {
205 consume_condition.push_back(intervals->PresenceLiteral(vars[t]));
209 consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral(
211 consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral(
213 IntegerValue(
time + 1))));
221 literals_with_coeff.push_back(
226 fixed_capacity, &literals_with_coeff);
235 const std::vector<IntervalVariable>& vars,
239 if (vars.empty())
return;
246 const IntegerValue fixed_capacity(
247 integer_trail->UpperBound(
capacity).value());
249 std::vector<AffineExpression> times;
250 std::vector<IntegerValue> deltas;
251 std::vector<Literal> presences;
253 const int num_tasks = vars.size();
254 for (
int t = 0; t < num_tasks; ++t) {
255 CHECK(integer_trail->IsFixed(demands[t]));
256 times.push_back(intervals->StartVar(vars[t]));
257 deltas.push_back(integer_trail->LowerBound(demands[t]));
258 times.push_back(intervals->EndVar(vars[t]));
259 deltas.push_back(-integer_trail->LowerBound(demands[t]));
260 if (intervals->IsOptional(vars[t])) {
261 presences.push_back(intervals->PresenceLiteral(vars[t]));
262 presences.push_back(intervals->PresenceLiteral(vars[t]));
264 presences.push_back(encoder->GetTrueLiteral());
265 presences.push_back(encoder->GetTrueLiteral());
bool IsFixed(IntegerVariable i) const
IntegerValue UpperBound(IntegerVariable i) const
IntegerValue LowerBound(IntegerVariable i) const
void AddTerm(IntegerVariable var, IntegerValue coeff)
Class that owns everything related to a particular optimization model.
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
bool IsModelUnsat() const
void RegisterWith(GenericLiteralWatcher *watcher)
void RegisterWith(GenericLiteralWatcher *watcher)
void AddCumulativeOverloadChecker(const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper, Model *model)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
std::function< void(Model *)> Cumulative(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
void AddReservoirConstraint(std::vector< AffineExpression > times, std::vector< IntegerValue > deltas, std::vector< Literal > presences, int64 min_level, int64 max_level, Model *model)
std::function< void(Model *)> Disjunctive(const std::vector< IntervalVariable > &vars)
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
std::function< void(Model *)> CumulativeTimeDecomposition(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
std::function< void(Model *)> CumulativeUsingReservoir(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)