add no cycle cuts to the lp relaxation in the vrp tour constraint inside the sat solver

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<int> tails;
+    std::vector<int> heads;
+    std::vector<IntegerVariable> 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

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<IntegerTrail>()),
+    : sat_parameters_(model->GetOrCreate<SatSolver>()->parameters()),
+      integer_trail_(model->GetOrCreate<IntegerTrail>()),
+      trail_(model->GetOrCreate<Trail>()),
       dispatcher_(model->GetOrCreate<LinearProgrammingDispatcher>()) {
   // TODO(user): Find a way to make GetOrCreate<TimeLimit>() construct it by
   // default.
   time_limit_ = model->Mutable<TimeLimit>();
-  max_num_cuts_ = model->GetOrCreate<SatSolver>()->parameters().max_num_cuts();
   if (time_limit_ == nullptr) {
     model->SetSingleton(TimeLimit::Infinite());
     time_limit_ = model->Mutable<TimeLimit>();
@@ -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<double> local_solution;
@@ -396,6 +398,11 @@ CutGenerator CreateStronglyConnectedGraphCutGenerator(
     int num_arcs_in_lp_solution = 0;
     std::vector<std::vector<int>> 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;

ortools/sat/linear_programming_constraint.h

@@ -165,7 +165,9 @@ class LinearProgrammingConstraint : public PropagatorInterface {
   std::vector<std::pair<glop::ColIndex, double>> objective_lp_;
 
   // Structures for propagators.
+  const SatParameters sat_parameters_;
   IntegerTrail* integer_trail_;
+  Trail* trail_;
   std::vector<IntegerLiteral> integer_reason_;
   std::vector<IntegerLiteral> deductions_;
 
@@ -186,7 +188,6 @@ class LinearProgrammingConstraint : public PropagatorInterface {
   LinearProgrammingDispatcher* dispatcher_;
 
   int num_cuts_ = 0;
-  int max_num_cuts_;  // const after construction.
   std::vector<CutGenerator> cut_generators_;
 };
 

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.

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;