[CP-SAT] Work on linear1 encodings; more work on lrat; cleanup linear2 code; work on probing

Author: lperron

ortools/linear_solver/proto_solver/sat_proto_solver.cc

@@ -160,7 +160,8 @@ MPSolutionResponse TimeLimitResponse(SolverLogger& logger) {
 MPSolutionResponse SatSolveProto(
     LazyMutableCopy<MPModelRequest> request, std::atomic<bool>* interrupt_solve,
     std::function<void(const std::string&)> logging_callback,
-    std::function<void(const MPSolution&)> solution_callback) {
+    std::function<void(const MPSolution&)> solution_callback,
+    std::function<void(const double)> best_bound_callback) {
   sat::SatParameters params;
   params.set_log_search_progress(request->enable_internal_solver_output());
 
@@ -431,6 +432,9 @@ MPSolutionResponse SatSolveProto(
           solution_callback(post_solve(cp_response));
         }));
   }
+  if (best_bound_callback != nullptr) {
+    sat_model.Add(sat::NewBestBoundCallback(best_bound_callback));
+  }
 
   // Solve.
   const sat::CpSolverResponse cp_response =

ortools/linear_solver/proto_solver/sat_proto_solver.h

@@ -49,11 +49,18 @@ namespace operations_research {
 // found by the solver. The solver may call solution_callback from multiple
 // threads, but it will ensure that at most one thread executes
 // solution_callback at a time.
+//
+// The optional best_bound_callback will be called each time the best bound is
+// improved. The solver may call solution_callback from multiple
+// threads, but it will ensure that at most one thread executes
+// solution_callback at a time. It is guaranteed that the best bound is strictly
+// improving.
 MPSolutionResponse SatSolveProto(
     LazyMutableCopy<MPModelRequest> request,
     std::atomic<bool>* interrupt_solve = nullptr,
     std::function<void(const std::string&)> logging_callback = nullptr,
-    std::function<void(const MPSolution&)> solution_callback = nullptr);
+    std::function<void(const MPSolution&)> solution_callback = nullptr,
+    std::function<void(const double)> best_bound_callback = nullptr);
 
 // Returns a string that describes the version of the CP-SAT solver.
 std::string SatSolverVersion();

ortools/sat/BUILD.bazel

@@ -1470,11 +1470,11 @@ cc_library(
         "//ortools/util:stats",
         "//ortools/util:strong_integers",
         "//ortools/util:time_limit",
-        "@abseil-cpp//absl/algorithm:container",
         "@abseil-cpp//absl/base:core_headers",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
+        "@abseil-cpp//absl/functional:function_ref",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/log:vlog_is_on",
@@ -1524,6 +1524,7 @@ cc_library(
         ":implied_bounds",
         ":integer",
         ":integer_base",
+        ":lrat_proof_handler",
         ":model",
         ":sat_base",
         ":sat_parameters_cc_proto",

ortools/sat/clause.cc

@@ -366,8 +366,7 @@ void ClauseManager::InternalDetach(SatClause* clause) {
   }
   if (lrat_proof_handler_ != nullptr) {
     const auto it = clause_id_.find(clause);
-    // TODO(user): why is it necessary to keep binary clauses?
-    if (it != clause_id_.end() && size != 2) {
+    if (it != clause_id_.end()) {
       lrat_proof_handler_->DeleteClauses({it->second});
       clause_id_.erase(it);
     }

ortools/sat/clause.h

@@ -797,15 +797,6 @@ class BinaryImplicationGraph : public SatPropagator {
 
   void SetDratProofHandler(DratProofHandler* drat_proof_handler);
 
-  // Changes the reason of the variable at trail index to a binary reason.
-  // Note that the implication "new_reason => trail_[trail_index]" should be
-  // part of the implication graph.
-  void ChangeReason(int trail_index, Literal new_reason) {
-    CHECK(trail_->Assignment().LiteralIsTrue(new_reason));
-    reasons_[trail_index] = new_reason.Negated();
-    trail_->ChangeReason(trail_index, propagator_id_);
-  }
-
   // The literals that are "directly" implied when literal is set to true. This
   // is not a full "reachability". It includes at most ones propagation. The set
   // of all direct implications is enough to describe the implications graph