diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 4dfe308875..471dfefca5 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -1092,21 +1092,28 @@ bool SolutionIsFeasible(const CpModelProto& model, default: LOG(FATAL) << "Unuspported constraint: " << ConstraintCaseName(type); } + + // Display a message to help debugging. if (!is_feasible) { VLOG(1) << "Failing constraint #" << c << " : " << ProtobufShortDebugString(model.constraints(c)); if (mapping_proto != nullptr && postsolve_mapping != nullptr) { - std::vector fixed(mapping_proto->variables().size(), false); - for (const int var : *postsolve_mapping) fixed[var] = true; + std::vector reverse_map(mapping_proto->variables().size(), -1); + for (int var = 0; var < postsolve_mapping->size(); ++var) { + reverse_map[(*postsolve_mapping)[var]] = var; + } for (const int var : UsedVariables(model.constraints(c))) { - VLOG(1) << "var: " << var << " value: " << variable_values[var] - << " was_fixed: " << fixed[var] << " initial_domain: " + VLOG(1) << "var: " << var << " mapped_to: " << reverse_map[var] + << " value: " << variable_values[var] << " initial_domain: " << ReadDomainFromProto(model.variables(var)) << " postsolved_domain: " << ReadDomainFromProto(mapping_proto->variables(var)); } + } else { + for (const int var : UsedVariables(model.constraints(c))) { + VLOG(1) << "var: " << var << " value: " << variable_values[var]; + } } - return false; } } diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 7aafdf5cd6..a27f120dc0 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -1054,7 +1054,6 @@ void LoadEquivalenceNeqAC(const std::vector enforcement_literal, void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { auto* mapping = m->GetOrCreate(); - if (ct.linear().vars().empty()) { const Domain rhs = ReadDomainFromProto(ct.linear()); if (rhs.Contains(0)) return; @@ -1171,6 +1170,11 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { } } } else { + // In this case, we can create just one Boolean instead of two since one + // is the negation of the other. + const bool special_case = + ct.enforcement_literal().empty() && ct.linear().domain_size() == 4; + std::vector clause; for (int i = 0; i < ct.linear().domain_size(); i += 2) { int64 lb = ct.linear().domain(i); @@ -1178,8 +1182,11 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { if (min_sum >= lb) lb = kint64min; if (max_sum <= ub) ub = kint64max; - const Literal subdomain_literal(m->Add(NewBooleanVariable()), true); + const Literal subdomain_literal( + special_case && i > 0 ? clause.back().Negated() + : Literal(m->Add(NewBooleanVariable()), true)); clause.push_back(subdomain_literal); + if (lb != kint64min) { m->Add(ConditionalWeightedSumGreaterOrEqual({subdomain_literal}, vars, coeffs, lb)); @@ -1192,10 +1199,7 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { for (const int ref : ct.enforcement_literal()) { clause.push_back(mapping->Literal(ref).Negated()); } - - // TODO(user): In the cases where this clause only contains two literals, - // then we could have only used one literal and its negation above. - m->Add(ClauseConstraint(clause)); + if (!special_case) m->Add(ClauseConstraint(clause)); } } diff --git a/ortools/sat/integer_expr.h b/ortools/sat/integer_expr.h index 9909a94cc9..972771ade0 100644 --- a/ortools/sat/integer_expr.h +++ b/ortools/sat/integer_expr.h @@ -474,19 +474,30 @@ inline std::function ConditionalWeightedSumLowerOrEqual( : integer_trail->UpperBound(vars[i])); } if (expression_min == upper_bound) { + // Tricky: as we create integer literal, we might propagate stuff and + // the bounds might change, so if the expression_min increase with the + // bound we use, then the literal must be false. + IntegerValue non_cached_min; for (int i = 0; i < vars.size(); ++i) { if (coefficients[i] > 0) { - model->Add( - Implication(enforcement_literals, - IntegerLiteral::LowerOrEqual( - vars[i], integer_trail->LowerBound(vars[i])))); + const IntegerValue lb = integer_trail->LowerBound(vars[i]); + non_cached_min += coefficients[i] * lb; + model->Add(Implication(enforcement_literals, + IntegerLiteral::LowerOrEqual(vars[i], lb))); } else if (coefficients[i] < 0) { - model->Add( - Implication(enforcement_literals, - IntegerLiteral::GreaterOrEqual( - vars[i], integer_trail->UpperBound(vars[i])))); + const IntegerValue ub = integer_trail->UpperBound(vars[i]); + non_cached_min += coefficients[i] * ub; + model->Add(Implication(enforcement_literals, + IntegerLiteral::GreaterOrEqual(vars[i], ub))); } } + if (non_cached_min > expression_min) { + std::vector clause; + for (const Literal l : enforcement_literals) { + clause.push_back(l.Negated()); + } + model->Add(ClauseConstraint(clause)); + } } else { IntegerSumLE* constraint = new IntegerSumLE( enforcement_literals, vars, diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index e9e518bc83..2bf6039af5 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -706,7 +706,11 @@ SatSolver::Status SolveIntegerProblem(Model* model) { } // If we pushed root level deductions, we restart to incorporate them. + // Note that in the present of assumptions, it is important to return to + // the level zero first ! otherwise, the new deductions will not be + // incorporated and the solver will loop forever. if (integer_trail->HasPendingRootLevelDeduction()) { + sat_solver->Backtrack(0); if (!sat_solver->RestoreSolverToAssumptionLevel()) { return sat_solver->UnsatStatus(); } diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 0f668254f4..e45c1de78d 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -198,11 +198,10 @@ bool PresolveContext::VariableWasRemoved(int ref) const { if (IsFixed(ref)) return false; if (!removed_variables_.contains(PositiveRef(ref))) return false; if (!var_to_constraints_[PositiveRef(ref)].empty()) { - const AffineRelation::Relation r = GetAffineRelation(PositiveRef(ref)); LOG(INFO) << "Variable " << PositiveRef(ref) << " was removed, yet it appears in some constraints!"; - LOG(INFO) << "affine relation = " << r.coeff << " * X" << r.representative - << " + " << r.offset; + LOG(INFO) << "affine relation: " + << AffineRelationDebugString(PositiveRef(ref)); for (const int c : var_to_constraints_[PositiveRef(ref)]) { LOG(INFO) << "constraint #" << c << " : " << (c >= 0 ? working_model->constraints(c).ShortDebugString() @@ -523,11 +522,7 @@ void PresolveContext::RemoveVariableFromAffineRelation(int var) { } if (VLOG_IS_ON(2)) { - const auto r = GetAffineRelation(var); - LOG(INFO) << "Removing affine relation for " << var << " : " - << DomainOf(var) << " = " << r.coeff << " * " - << DomainOf(r.representative) << " + " << r.offset - << " ( rep : " << rep << ")."; + LOG(INFO) << "Removing affine relation: " << AffineRelationDebugString(var); } } @@ -756,6 +751,17 @@ AffineRelation::Relation PresolveContext::GetAffineRelation(int ref) const { return r; } +std::string PresolveContext::RefDebugString(int ref) const { + return absl::StrCat(RefIsPositive(ref) ? "X" : "-X", PositiveRef(ref), + DomainOf(ref).ToString()); +} + +std::string PresolveContext::AffineRelationDebugString(int ref) const { + const AffineRelation::Relation r = GetAffineRelation(ref); + return absl::StrCat(RefDebugString(ref), " = ", r.coeff, " * ", + RefDebugString(r.representative), " + ", r.offset); +} + // Create the internal structure for any new variables in working_model. void PresolveContext::InitializeNewDomains() { for (int i = domains.size(); i < working_model->variables_size(); ++i) { diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 1e70eca0ee..18b566f1d7 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -214,6 +214,10 @@ class PresolveContext { // representative from the var_equiv_relations. AffineRelation::Relation GetAffineRelation(int ref) const; + // To facilitate debugging. + std::string RefDebugString(int ref) const; + std::string AffineRelationDebugString(int ref) const; + // Makes sure the domain of ref and of its representative are in sync. // Returns false on unsat. bool PropagateAffineRelation(int ref); diff --git a/ortools/sat/timetable.cc b/ortools/sat/timetable.cc index c1012d8f76..de1cf6214c 100644 --- a/ortools/sat/timetable.cc +++ b/ortools/sat/timetable.cc @@ -68,22 +68,25 @@ void TimeTablingPerTask::RegisterWith(GenericLiteralWatcher* watcher) { watcher->RegisterReversibleInt(id, &forward_num_tasks_to_sweep_); watcher->RegisterReversibleInt(id, &backward_num_tasks_to_sweep_); watcher->RegisterReversibleInt(id, &num_profile_tasks_); + + // Changing the times or pushing task absence migth have side effects on the + // other intervals, so we would need to be called again in this case. + watcher->NotifyThatPropagatorMayNotReachFixedPointInOnePass(id); } +// Note that we relly on being called again to reach a fixed point. bool TimeTablingPerTask::Propagate() { - // Repeat until the propagator does not filter anymore. - profile_changed_ = true; - while (profile_changed_) { - profile_changed_ = false; - // This can fail if the profile exceeds the resource capacity. - if (!BuildProfile()) return false; - // Update the minimum start times. - if (!SweepAllTasks(/*is_forward=*/true)) return false; - // We reuse the same profile, but reversed, to update the maximum end times. - ReverseProfile(); - // Update the maximum end times (reversed problem). - if (!SweepAllTasks(/*is_forward=*/false)) return false; - } + // This can fail if the profile exceeds the resource capacity. + if (!BuildProfile()) return false; + + // Update the minimum start times. + if (!SweepAllTasks(/*is_forward=*/true)) return false; + + // We reuse the same profile, but reversed, to update the maximum end times. + ReverseProfile(); + + // Update the maximum end times (reversed problem). + if (!SweepAllTasks(/*is_forward=*/false)) return false; return true; } @@ -307,21 +310,6 @@ bool TimeTablingPerTask::SweepTask(int task_id) { return false; } - // The profile needs to be recomputed if we pushed something (because it can - // have side effects). Note that for the case where the interval is optional - // but not its start, it is possible that UpdateStartingTime() didn't change - // the start, so we need to test this in order to avoid an infinite loop. - // - // TODO(user): find an efficient way to keep the start_max < new_end_min - // condition. The problem is that ReduceProfile() assumes that by_end_min and - // by_start_max are up to date (this is not necessarily the case if we use - // the old condition). A solution is to update those vector before calling - // ReduceProfile() or to ReduceProfile() directly after BuildProfile() in the - // main loop. - if (helper_->StartMin(task_id) != initial_start_min) { - profile_changed_ = true; - } - return true; } diff --git a/ortools/sat/timetable.h b/ortools/sat/timetable.h index 86e12c97c2..514da05eea 100644 --- a/ortools/sat/timetable.h +++ b/ortools/sat/timetable.h @@ -121,10 +121,6 @@ class TimeTablingPerTask : public PropagatorInterface { // height of the leftmost profile rectangle that can be used for propagation. IntegerValue starting_profile_height_; - // True if the last call of the propagator has filtered the domain of a task - // and changed the shape of the profile. - bool profile_changed_; - // Reversible sets of tasks to consider for the forward (resp. backward) // propagation. A task with a fixed start do not need to be considered for the // forward pass, same for task with fixed end for the backward pass. It is why