[CP-SAT] fix more fuzzer bugs; fix #4324

google · Dec 19, 2024 · f152e3a · f152e3a
1 parent fc422b4
commit f152e3a
Show file tree

Hide file tree

Showing 6 changed files with 60 additions and 7 deletions.
diff --git a/ortools/sat/cp_model_lns.h b/ortools/sat/cp_model_lns.h
@@ -17,6 +17,7 @@
 #include <cmath>
 #include <cstdint>
 #include <functional>
+#include <memory>
 #include <string>
 #include <tuple>
 #include <utility>

diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
@@ -13822,7 +13822,11 @@ CpSolverStatus CpModelPresolver::Presolve() {
       }
     }
 
+    if (!context_->HintIsLoaded()) {
+      context_->LoadSolutionHint();
+    }
     ExpandCpModelAndCanonicalizeConstraints();
+    UpdateHintInProto(context_);
     if (context_->ModelIsUnsat()) return InfeasibleStatus();
 
     // We still write back the canonical objective has we don't deal well
@@ -14046,6 +14050,11 @@ CpSolverStatus CpModelPresolver::Presolve() {
   if (context_->working_model->has_objective()) {
     if (!context_->params().keep_symmetry_in_presolve()) {
       ExpandObjective();
+      if (!context_->modified_domains.PositionsSetAtLeastOnce().empty()) {
+        // If we have fixed variables or created new affine relations, there
+        // might be more things to presolve.
+        PresolveToFixPoint();
+      }
       if (context_->ModelIsUnsat()) return InfeasibleStatus();
       ShiftObjectiveWithExactlyOnes();
       if (context_->ModelIsUnsat()) return InfeasibleStatus();

diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
@@ -868,7 +868,27 @@ bool SolutionHintIsCompleteAndFeasible(
     solution[var] = hinted_value;
   }
 
-  if (SolutionIsFeasible(model_proto, solution)) {
+  const bool is_feasible = SolutionIsFeasible(model_proto, solution);
+  bool breaks_assumptions = false;
+  if (is_feasible) {
+    for (const int literal_ref : model_proto.assumptions()) {
+      if (solution[PositiveRef(literal_ref)] !=
+          (RefIsPositive(literal_ref) ? 1 : 0)) {
+        breaks_assumptions = true;
+        break;
+      }
+    }
+  }
+  if (is_feasible && breaks_assumptions) {
+    if (logger != nullptr) {
+      SOLVER_LOG(
+          logger,
+          "The solution hint is complete and feasible, but it breaks the "
+          "assumptions of the model.");
+    }
+    return false;
+  }
+  if (is_feasible) {
     if (manager != nullptr) {
       // Add it to the pool right away! Note that we already have a log in this
       // case, so we don't log anything more.

diff --git a/ortools/sat/cp_model_solver_fuzz.cc b/ortools/sat/cp_model_solver_fuzz.cc
@@ -31,14 +31,32 @@ std::string GetTestDataDir() {
 }
 
 void Solve(const CpModelProto& proto) {
+  SatParameters params;
+  params.set_max_time_in_seconds(4.0);
+  params.set_debug_crash_if_presolve_breaks_hint(true);
+
+  // Enable all fancy heuristics.
+  params.set_linearization_level(2);
+  params.set_use_try_edge_reasoning_in_no_overlap_2d(true);
+  params.set_exploit_all_precedences(true);
+  params.set_use_hard_precedences_in_cumulative(true);
+  params.set_max_num_intervals_for_timetable_edge_finding(1000);
+  params.set_use_overload_checker_in_cumulative(true);
+  params.set_use_strong_propagation_in_disjunctive(true);
+  params.set_use_timetable_edge_finding_in_cumulative(true);
+  params.set_max_pairs_pairwise_reasoning_in_no_overlap_2d(50000);
+  params.set_use_timetabling_in_no_overlap_2d(true);
+  params.set_use_energetic_reasoning_in_no_overlap_2d(true);
+  params.set_use_area_energetic_reasoning_in_no_overlap_2d(true);
+  params.set_use_conservative_scale_overload_checker(true);
+  params.set_use_dual_scheduling_heuristics(true);
+
   const CpSolverResponse response =
-      operations_research::sat::SolveWithParameters(
-          proto,
-          "max_time_in_seconds: 4.0,debug_crash_if_presolve_breaks_hint:true");
+      operations_research::sat::SolveWithParameters(proto, params);
 
+  params.set_cp_model_presolve(false);
   const CpSolverResponse response_no_presolve =
-      operations_research::sat::SolveWithParameters(
-          proto, "max_time_in_seconds:4.0,cp_model_presolve:false");
+      operations_research::sat::SolveWithParameters(proto, params);
 
   CHECK_EQ(response.status() == CpSolverStatus::MODEL_INVALID,
            response_no_presolve.status() == CpSolverStatus::MODEL_INVALID)

diff --git a/ortools/sat/diffn_util_test.cc b/ortools/sat/diffn_util_test.cc
@@ -21,6 +21,7 @@
 #include <optional>
 #include <sstream>
 #include <string>
+#include <tuple>
 #include <utility>
 #include <vector>
 

diff --git a/ortools/sat/var_domination.cc b/ortools/sat/var_domination.cc
@@ -992,7 +992,11 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) {
             context->UpdateConstraintVariableUsage(ct_index);
             processed[PositiveRef(ref)] = true;
             processed[PositiveRef(var)] = true;
-            processed[PositiveRef(encoding_lit)] = true;
+            // `encoding_lit` was maybe a new variable added during this loop,
+            // so make sure we cannot go out-of-bound.
+            if (PositiveRef(encoding_lit) < processed.size()) {
+              processed[PositiveRef(encoding_lit)] = true;
+            }
             continue;
           }