diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 16b5eec38d..ba5a24833f 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1838,6 +1838,26 @@ void TryToAddCutGenerators(const CpModelProto& model_proto, num_nodes - ignore_zero_offset, tails, heads, vars); cut_generators->push_back(std::move(generator)); } + if (ct.constraint_case() == ConstraintProto::ConstraintCase::kRoutes) { + LpCutGenerators generator; + std::vector tails; + std::vector heads; + std::vector vars; + int num_nodes = 0; + for (int i = 0; i < ct.routes().tails_size(); ++i) { + const int ref = ct.routes().literals(i); + if (!m->IsInteger(ref)) return; + generator.refs.push_back(ref); + tails.push_back(ct.routes().tails(i)); + heads.push_back(ct.routes().heads(i)); + vars.push_back(m->Integer(ref)); + num_nodes = std::max(num_nodes, 1 + ct.routes().tails(i)); + num_nodes = std::max(num_nodes, 1 + ct.routes().heads(i)); + } + generator.cut_generator = + CreateStronglyConnectedGraphCutGenerator(num_nodes, tails, heads, vars); + cut_generators->push_back(std::move(generator)); + } } } // namespace diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 7deaefc093..3106784399 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -33,12 +33,13 @@ namespace sat { const double LinearProgrammingConstraint::kEpsilon = 1e-6; LinearProgrammingConstraint::LinearProgrammingConstraint(Model* model) - : integer_trail_(model->GetOrCreate()), + : sat_parameters_(model->GetOrCreate()->parameters()), + integer_trail_(model->GetOrCreate()), + trail_(model->GetOrCreate()), dispatcher_(model->GetOrCreate()) { // TODO(user): Find a way to make GetOrCreate() construct it by // default. time_limit_ = model->Mutable(); - max_num_cuts_ = model->GetOrCreate()->parameters().max_num_cuts(); if (time_limit_ == nullptr) { model->SetSingleton(TimeLimit::Infinite()); time_limit_ = model->Mutable(); @@ -197,10 +198,11 @@ bool LinearProgrammingConstraint::Propagate() { << status.error_message(); // Add cuts and resolve. - if (!cut_generators_.empty() && + if (!cut_generators_.empty() && num_cuts_ < sat_parameters_.max_num_cuts() && + (trail_->CurrentDecisionLevel() == 0 || + !sat_parameters_.only_add_cuts_at_level_zero()) && (simplex_.GetProblemStatus() == glop::ProblemStatus::OPTIMAL || - simplex_.GetProblemStatus() == glop::ProblemStatus::DUAL_FEASIBLE) && - num_cuts_ < max_num_cuts_) { + simplex_.GetProblemStatus() == glop::ProblemStatus::DUAL_FEASIBLE)) { int num_new_cuts = 0; for (const CutGenerator& generator : cut_generators_) { std::vector local_solution; @@ -396,6 +398,11 @@ CutGenerator CreateStronglyConnectedGraphCutGenerator( int num_arcs_in_lp_solution = 0; std::vector> graph(num_nodes); for (int i = 0; i < lp_solution.size(); ++i) { + // TODO(user): a more advanced algorithm consist of adding the arcs + // in the decreasing order of their lp_solution, and for each strongly + // connected components S along the way, try to add the corresponding + // cuts. We can stop as soon as there is only two components left, after + // adding the corresponding cut. if (lp_solution[i] > 1e-6) { ++num_arcs_in_lp_solution; graph[tails[i]].push_back(heads[i]); @@ -435,8 +442,8 @@ CutGenerator CreateStronglyConnectedGraphCutGenerator( incoming.coeffs.push_back(1.0); } } - if (sum_incoming < 1.0) cuts.push_back(std::move(incoming)); - if (sum_outgoing < 1.0) cuts.push_back(std::move(outgoing)); + if (sum_incoming < 1.0 - 1e-6) cuts.push_back(std::move(incoming)); + if (sum_outgoing < 1.0 - 1e-6) cuts.push_back(std::move(outgoing)); // In this case, the cuts for each component are the same. if (components.size() == 2) break; diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h index 8efa57be73..ef8b2fbe88 100644 --- a/ortools/sat/linear_programming_constraint.h +++ b/ortools/sat/linear_programming_constraint.h @@ -165,7 +165,9 @@ class LinearProgrammingConstraint : public PropagatorInterface { std::vector> objective_lp_; // Structures for propagators. + const SatParameters sat_parameters_; IntegerTrail* integer_trail_; + Trail* trail_; std::vector integer_reason_; std::vector deductions_; @@ -186,7 +188,6 @@ class LinearProgrammingConstraint : public PropagatorInterface { LinearProgrammingDispatcher* dispatcher_; int num_cuts_ = 0; - int max_num_cuts_; // const after construction. std::vector cut_generators_; }; diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 54655e223e..b6f355c836 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -18,7 +18,7 @@ package operations_research.sat; // Contains the definitions for all the sat algorithm parameters and their // default values. // -// NEXT TAG: 92 +// NEXT TAG: 93 message SatParameters { // ========================================================================== // Branching and polarity @@ -495,7 +495,8 @@ message SatParameters { // For now, we don't have any manager for the LP cuts, so we just add any // generated cuts until this limit is reached. - optional int32 max_num_cuts = 91 [default = 500]; + optional int32 max_num_cuts = 91 [default = 1000]; + optional bool only_add_cuts_at_level_zero = 92 [default = false]; // If true then all decisions taken by the solver are made using a fixed order // as specified in the API or in the cp_model.proto search_order field. diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index f154ccbc34..e57819bb8d 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -928,7 +928,6 @@ SatSolver::Status SatSolver::StatusWithLog(Status status) { } void SatSolver::SetAssumptionLevel(int assumption_level) { - DCHECK(!is_model_unsat_); CHECK_GE(assumption_level, 0); CHECK_LE(assumption_level, CurrentDecisionLevel()); assumption_level_ = assumption_level;