[CP-SAT] more work on lrat; expose response.solve_log in C#, Java, python

Author: lperron

ortools/java/com/google/ortools/sat/CpSolver.java

@@ -68,40 +68,6 @@ public CpSolverStatus solve(CpModel model, CpSolverSolutionCallback cb) {
     return solveResponse.getStatus();
   }
 
-  /**
-   * Solves the given model, passes each incumber solution to the solution callback if not null, and
-   * returns the solve status.
-   *
-   * @deprecated Use the solve() method with the same signature.
-   */
-  @Deprecated
-  public CpSolverStatus solveWithSolutionCallback(CpModel model, CpSolverSolutionCallback cb) {
-    return solve(model, cb);
-  }
-
-  /**
-   * Searches for all solutions of a satisfiability problem.
-   *
-   * <p>This method searches for all feasible solutions of a given model. Then it feeds the
-   * solutions to the callback.
-   *
-   * <p>Note that the model cannot have an objective.
-   *
-   * @param model the model to solve
-   * @param cb the callback that will be called at each solution
-   * @return the status of the solve (FEASIBLE, INFEASIBLE...)
-   * @deprecated Use the solve() method with the same signature, after setting the
-   *     enumerate_all_solution parameter to true.
-   */
-  @Deprecated
-  public CpSolverStatus searchAllSolutions(CpModel model, CpSolverSolutionCallback cb) {
-    boolean oldValue = solveParameters.getEnumerateAllSolutions();
-    solveParameters.setEnumerateAllSolutions(true);
-    CpSolverStatus status = solve(model, cb);
-    solveParameters.setEnumerateAllSolutions(oldValue);
-    return status;
-  }
-
   private synchronized void createSolveWrapper() {
     solveWrapper = new SolveWrapper();
   }
@@ -213,10 +179,23 @@ public String responseStats() {
    * Returns some information on how the solution was found, or the reason why the model or the
    * parameters are invalid.
    */
+  public String solutionInfo() {
+    return solveResponse.getSolutionInfo();
+  }
+
+  /** Returns the solution info. @Deprecated */
   public String getSolutionInfo() {
     return solveResponse.getSolutionInfo();
   }
 
+  /**
+   * Returns the solve log. You need to set the parameters log_to_response to true to get the solve
+   * log.
+   */
+  public String solveLog() {
+    return solveResponse.getSolveLog();
+  }
+
   private CpSolverResponse solveResponse;
   private final SatParameters.Builder solveParameters;
   private Consumer<String> logCallback;

ortools/sat/BUILD.bazel

@@ -904,23 +904,16 @@ cc_test(
         ":cp_model_cc_proto",
         ":cp_model_checker",
         ":cp_model_solver",
-        ":cp_model_solver_helpers",
         ":cp_model_test_utils",
-        ":cp_model_utils",
-        ":drat_checker",
         ":lp_utils",
         ":model",
-        ":sat_base",
         ":sat_parameters_cc_proto",
-        ":sat_solver",
-        ":synchronization",
         "//ortools/base:gmock_main",
         "//ortools/base:parse_test_proto",
         "//ortools/linear_solver:linear_solver_cc_proto",
         "//ortools/port:os",
         "//ortools/util:logging",
         "@abseil-cpp//absl/container:flat_hash_set",
-        "@abseil-cpp//absl/flags:flag",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/strings",
     ],
@@ -4274,6 +4267,7 @@ cc_library(
         ":model",
         ":sat_base",
         "//ortools/base:file",
+        "@abseil-cpp//absl/flags:flag",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/strings",

ortools/sat/clause.cc

@@ -103,6 +103,8 @@ bool LiteralsAreFixedAtRoot(const Trail& trail,
 ClauseManager::ClauseManager(Model* model)
     : SatPropagator("ClauseManager"),
       clause_id_generator_(model->GetOrCreate<ClauseIdGenerator>()),
+      parameters_(*model->GetOrCreate<SatParameters>()),
+      assignment_(model->GetOrCreate<Trail>()->Assignment()),
       implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
       trail_(model->GetOrCreate<Trail>()),
       num_inspected_clauses_(0),
@@ -327,6 +329,9 @@ SatClause* ClauseManager::AddRemovableClause(ClauseId id,
   }
   if (add_clause_callback_ != nullptr) add_clause_callback_(lbd, literals);
   CHECK(AttachAndPropagate(clause, trail));
+
+  // Create an entry in clauses_info_ to mark that clause as removable.
+  clauses_info_[clause].lbd = lbd;
   return clause;
 }
 
@@ -484,6 +489,35 @@ bool ClauseManager::InprocessingFixLiteral(
   return implication_graph_->Propagate(trail_);
 }
 
+void ClauseManager::ChangeLbdIfBetter(SatClause* clause, int new_lbd) {
+  auto it = clauses_info_.find(clause);
+  if (it == clauses_info_.end()) return;
+
+  // Always take the min.
+  if (new_lbd > it->second.lbd) return;
+
+  ++num_lbd_promotions_;
+  if (new_lbd <= parameters_.clause_cleanup_lbd_bound()) {
+    // We keep the clause forever.
+    clauses_info_.erase(it);
+  } else {
+    it->second.lbd = new_lbd;
+  }
+}
+
+bool ClauseManager::RemoveFixedLiteralsAndTestIfTrue(SatClause* clause) {
+  if (clause->RemoveFixedLiteralsAndTestIfTrue(assignment_)) {
+    // The clause is always true, detach it.
+    LazyDelete(clause, DeletionSourceForStat::FIXED_AT_TRUE);
+    return true;
+  }
+
+  // We should have dealt with unit and unsat clause before this.
+  CHECK_GE(clause->size(), 2);
+  ChangeLbdIfBetter(clause, clause->size());
+  return false;
+}
+
 bool ClauseManager::InprocessingRewriteClause(
     SatClause* clause, absl::Span<const Literal> new_clause,
     absl::Span<const ClauseId> clause_ids) {
@@ -543,6 +577,7 @@ bool ClauseManager::InprocessingRewriteClause(
   }
 
   clause->Rewrite(new_clause);
+  ChangeLbdIfBetter(clause, new_clause.size());
 
   // And we reattach it.
   if (all_clauses_are_attached_) {

ortools/sat/clause.h

@@ -107,14 +107,6 @@ class SatClause {
     return absl::Span<const Literal>(&(literals_[0]), size_);
   }
 
-  // Removes literals that are fixed. This should only be called at level 0
-  // where a literal is fixed iff it is assigned. Aborts and returns true if
-  // they are not all false.
-  //
-  // Note that the removed literal can still be accessed in the portion [size,
-  // old_size) of literals().
-  bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment& assignment);
-
   // Returns true if the clause is satisfied for the given assignment. Note that
   // the assignment may be partial, so false does not mean that the clause can't
   // be satisfied by completing the assignment.
@@ -134,6 +126,14 @@ class SatClause {
   // never be used afterwards.
   void Clear() { size_ = 0; }
 
+  // Removes literals that are fixed. This should only be called at level 0
+  // where a literal is fixed iff it is assigned. Aborts and returns true if
+  // they are not all false.
+  //
+  // Note that the removed literal can still be accessed in the portion [size,
+  // old_size) of literals().
+  bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment& assignment);
+
   // Rewrites a clause with another shorter one. Note that the clause shouldn't
   // be attached when this is called.
   void Rewrite(absl::Span<const Literal> new_clause) {
@@ -154,7 +154,7 @@ class SatClause {
 struct ClauseInfo {
   double activity = 0.0;
   int32_t lbd = 0;
-  bool protected_during_next_cleanup = false;
+  int32_t num_cleanup_rounds_since_last_bumped = 0;
 };
 
 class BinaryImplicationGraph;
@@ -267,6 +267,18 @@ class ClauseManager : public SatPropagator {
     if (it == clauses_info_.end()) return 0;
     return it->second.lbd;
   }
+  void KeepClauseForever(SatClause* const clause) {
+    clauses_info_.erase(clause);
+  }
+  void RescaleClauseActivities(double scaling_factor) {
+    for (auto& entry : clauses_info_) {
+      entry.second.activity *= scaling_factor;
+    }
+  }
+
+  // If the new lbd is better than the stored one, update it.
+  // And return the result of IsRemovable() (this save one hash lookup).
+  void ChangeLbdIfBetter(SatClause* clause, int new_lbd);
 
   // Total number of clauses inspected during calls to Propagate().
   int64_t num_inspected_clauses() const { return num_inspected_clauses_; }
@@ -280,6 +292,10 @@ class ClauseManager : public SatPropagator {
   // Number of clauses currently watched.
   int64_t num_watched_clauses() const { return num_watched_clauses_; }
 
+  // Number of time an existing clause lbd was reduced (due to inprocessing or
+  // recomputation of lbd in different branches).
+  int64_t num_lbd_promotions() const { return num_lbd_promotions_; }
+
   ClauseId GetClauseId(const SatClause* clause) const {
     const auto it = clause_id_.find(clause);
     return it != clause_id_.end() ? it->second : kNoClauseId;
@@ -343,6 +359,8 @@ class ClauseManager : public SatPropagator {
       SatClause* clause, absl::Span<const Literal> new_clause,
       absl::Span<const ClauseId> clause_ids = {});
 
+  bool RemoveFixedLiteralsAndTestIfTrue(SatClause* clause);
+
   // Fix a literal either with an existing LRAT `unit_clause_id`, or with a new
   // inferred unit clause, using `clause_ids` as proof.
   // This do NOT need to be between [Detach/Attach]AllClauses() calls.
@@ -427,14 +445,17 @@ class ClauseManager : public SatPropagator {
   SparseBitset<LiteralIndex> needs_cleaning_;
   bool is_clean_ = true;
 
+  const SatParameters& parameters_;
+  const VariablesAssignment& assignment_;
   BinaryImplicationGraph* implication_graph_;
   Trail* trail_;
 
   // For statistic reporting.
   std::vector<int64_t> deletion_counters_;
-  int64_t num_inspected_clauses_;
-  int64_t num_inspected_clause_literals_;
-  int64_t num_watched_clauses_;
+  int64_t num_inspected_clauses_ = 0;
+  int64_t num_inspected_clause_literals_ = 0;
+  int64_t num_watched_clauses_ = 0;
+  int64_t num_lbd_promotions_ = 0;
   mutable StatsGroup stats_;
 
   // For DetachAllClauses()/AttachAllClauses().

ortools/sat/cp_model_presolve_test.cc

@@ -8155,10 +8155,10 @@ TEST(PresolveCpModelTest, SolveDiophantine) {
 
   SatParameters params;
   params.set_cp_model_presolve(true);
+  params.set_num_workers(1);
   // Should solve in < .01 second. Note that deterministic time is not
   // completely accurate.
   params.set_max_deterministic_time(.001);
-  params.set_num_workers(1);
   const CpSolverResponse response_with =
       SolveWithParameters(model_proto, params);
 

ortools/sat/cp_model_search.cc

@@ -934,6 +934,13 @@ std::vector<SatParameters> GetFullWorkerParameters(
         params.search_branching() == SatParameters::FIXED_SEARCH) {
       continue;
     }
+    // As of November 2025, we don't support any LP reasoning when producing an
+    // UNSAT proof.
+    if ((params.check_lrat_proof() || params.check_drat_proof() ||
+         params.output_drat_proof()) &&
+        params.linearization_level() > 1) {
+      continue;
+    }
 
     // TODO(user): Enable probing_search in deterministic mode.
     // Currently it timeouts on small problems as the deterministic time limit

ortools/sat/cp_model_solver.cc

@@ -49,7 +49,6 @@
 #include "absl/types/span.h"
 #include "google/protobuf/arena.h"
 #include "google/protobuf/text_format.h"
-#include "ortools/base/file.h"
 #include "ortools/base/helpers.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/options.h"
@@ -132,32 +131,6 @@ ABSL_FLAG(bool, cp_model_use_hint_for_debug_only, false,
           "complete, validate that no buggy propagator make it infeasible.");
 ABSL_FLAG(bool, cp_model_fingerprint_model, true, "Fingerprint the model.");
 
-ABSL_FLAG(std::string, cp_model_drat_output, "",
-          "If non-empty, a proof in DRAT format will be written to this file. "
-          "This only works in the same conditions as the --cp_model_lrat_check "
-          "flag, and only for pure SAT models.");
-
-ABSL_FLAG(bool, cp_model_drat_check, false,
-          "If true, a proof in DRAT format will be stored in memory and "
-          "checked if the problem is UNSAT. This only works in the same "
-          "conditions as the --cp_model_lrat_check flag, and only for pure SAT "
-          "models.");
-
-ABSL_FLAG(bool, cp_model_lrat_check, false,
-          "If true, inferred clauses are checked with an LRAT checker as they "
-          "are learned. As of November 2025, this only works with a single "
-          "worker and symmetry level 0 or 1. This also works with presolve, if "
-          "find_clauses_that_are_exactly_one is false and "
-          "merge_at_most_one_work_limit is 0. However, in this case, the "
-          "presolved problem is assumed to be correct, without proof. If the "
-          "model is not pure SAT, the checks are only partial (some clauses "
-          "can be assumed without proof).");
-
-ABSL_FLAG(double, cp_model_max_drat_time_in_seconds,
-          std::numeric_limits<double>::infinity(),
-          "Maximum time in seconds to check the DRAT proof. This will only "
-          "be used is the cp_model_drat_check flag is enabled.");
-
 ABSL_FLAG(bool, cp_model_check_intermediate_solutions, false,
           "When true, all intermediate solutions found by the solver will be "
           "checked. This can be expensive, therefore it is off by default.");
@@ -1035,26 +1008,6 @@ bool SolutionHintIsCompleteAndFeasible(
   }
 }
 
-std::unique_ptr<LratProofHandler> MaybeCreateLratProofHandler(Model* model) {
-  const bool check_lrat = absl::GetFlag(FLAGS_cp_model_lrat_check);
-  const bool check_drat = absl::GetFlag(FLAGS_cp_model_drat_check);
-  File* drat_output = nullptr;
-  if (!absl::GetFlag(FLAGS_cp_model_drat_output).empty()) {
-    CHECK_OK(file::Open(absl::GetFlag(FLAGS_cp_model_drat_output), "w",
-                        &drat_output, file::Defaults()));
-  }
-  if (!check_lrat && !check_drat && drat_output == nullptr) return nullptr;
-
-  // TODO(user): pass the [presolved] model proto to the handler, so that
-  // it can map internal problem clause IDs to constraint indices in the
-  // original model. This will be needed to write the LRAT proof in a file that
-  // can be checked with an external LRAT checker, expecting the standard LRAT
-  // ASCII file format (which requires problem clauses IDs between 1 and n).
-  return std::make_unique<LratProofHandler>(model, check_lrat, check_drat,
-                                            drat_output,
-                                            /*in_binary_drat_format=*/false);
-}
-
 // Encapsulate a full CP-SAT solve without presolve in the SubSolver API.
 class FullProblemSolver : public SubSolver {
  public:
@@ -1082,7 +1035,7 @@ class FullProblemSolver : public SubSolver {
     shared_->RegisterSharedClassesInLocalModel(&local_model_);
 
     std::unique_ptr<LratProofHandler> lrat_proof_handler =
-        MaybeCreateLratProofHandler(&local_model_);
+        LratProofHandler::MaybeCreate(&local_model_);
     if (lrat_proof_handler != nullptr) {
       local_model_.Register<LratProofHandler>(lrat_proof_handler.get());
       local_model_.TakeOwnership(lrat_proof_handler.release());
@@ -1111,8 +1064,7 @@ class FullProblemSolver : public SubSolver {
       WallTimer timer;
       timer.Start();
       const bool valid = local_model_.GetOrCreate<SatSolver>()->ModelIsUnsat()
-                             ? lrat_proof_handler->Check(absl::GetFlag(
-                                   FLAGS_cp_model_max_drat_time_in_seconds))
+                             ? lrat_proof_handler->Check()
                              : lrat_proof_handler->Valid();
       shared_->lrat_proof_status->NewSubsolverProofStatus(
           valid ? DratChecker::Status::VALID : DratChecker::Status::INVALID,
@@ -1801,12 +1753,8 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
   const SatParameters& params = *global_model->GetOrCreate<SatParameters>();
   if (global_model->GetOrCreate<TimeLimit>()->LimitReached()) return;
 
-  if (absl::GetFlag(FLAGS_cp_model_drat_check) ||
-      !absl::GetFlag(FLAGS_cp_model_drat_output).empty()) {
-    LOG(WARNING)
-        << "DRAT check and output are skipped when using several workers";
-    absl::SetFlag(&FLAGS_cp_model_drat_check, false);
-    absl::SetFlag(&FLAGS_cp_model_drat_output, "");
+  if (params.check_drat_proof() || params.output_drat_proof()) {
+    LOG(FATAL) << "DRAT proofs are not supported with several workers";
   }
 
   // If specified by the user, we might disable some parameters based on their

ortools/sat/cp_model_solver.h

@@ -26,9 +26,6 @@
 
 #ifndef SWIG
 OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_dump_response);
-OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_drat_check);
-OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_lrat_check);
-OR_DLL ABSL_DECLARE_FLAG(double, cp_model_max_drat_time_in_seconds);
 #endif
 
 namespace operations_research {