[CP-SAT] lots of fuzzer bugs fixed

Author: lperron

ortools/sat/2d_rectangle_presolve.cc

@@ -31,7 +31,7 @@
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/stl_util.h"
-#include "ortools/graph/max_flow.h"
+#include "ortools/graph/minimum_vertex_cover.h"
 #include "ortools/graph/strongly_connected_components.h"
 #include "ortools/sat/diffn_util.h"
 #include "ortools/sat/integer_base.h"

ortools/sat/BUILD.bazel

@@ -523,6 +523,7 @@ cc_library(
     deps = [
         ":circuit",
         ":clause",
+        ":combine_solutions",
         ":cp_model_cc_proto",
         ":cp_model_checker",
         ":cp_model_lns",
@@ -3009,7 +3010,7 @@ cc_library(
         ":diffn_util",
         ":integer_base",
         "//ortools/base:stl_util",
-        "//ortools/graph:max_flow",
+        "//ortools/graph:minimum_vertex_cover",
         "//ortools/graph:strongly_connected_components",
         "@com_google_absl//absl/algorithm:container",
         "@com_google_absl//absl/container:btree",
@@ -3701,6 +3702,32 @@ cc_library(
     ],
 )
 
+cc_library(
+    name = "combine_solutions",
+    srcs = ["combine_solutions.cc"],
+    hdrs = ["combine_solutions.h"],
+    deps = [
+        ":cp_model_cc_proto",
+        ":cp_model_checker",
+        ":synchronization",
+        "@com_google_absl//absl/log:check",
+        "@com_google_absl//absl/strings",
+        "@com_google_absl//absl/types:span",
+    ],
+)
+
+cc_test(
+    name = "combine_solutions_test",
+    srcs = ["combine_solutions_test.cc"],
+    deps = [
+        ":combine_solutions",
+        ":model",
+        ":synchronization",
+        "//ortools/base:gmock_main",
+        "//ortools/base:parse_test_proto",
+    ],
+)
+
 cc_library(
     name = "work_assignment",
     srcs = ["work_assignment.cc"],

ortools/sat/combine_solutions.cc

@@ -0,0 +1,79 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#include "ortools/sat/combine_solutions.h"
+
+#include <cstdint>
+#include <memory>
+#include <optional>
+#include <string>
+#include <string_view>
+#include <vector>
+
+#include "absl/log/check.h"
+#include "absl/strings/str_cat.h"
+#include "absl/types/span.h"
+#include "ortools/sat/cp_model_checker.h"
+#include "ortools/sat/synchronization.h"
+
+namespace operations_research {
+namespace sat {
+
+bool TrySolution(const CpModelProto& model, absl::Span<const int64_t> solution,
+                 absl::Span<const int64_t> new_solution,
+                 absl::Span<const int64_t> base_solution,
+                 std::vector<int64_t>* new_combined_solution) {
+  new_combined_solution->resize(new_solution.size());
+  for (int i = 0; i < new_solution.size(); ++i) {
+    if (new_solution[i] != base_solution[i]) {
+      // A value that changed that we patch.
+      (*new_combined_solution)[i] = new_solution[i];
+    } else {
+      (*new_combined_solution)[i] = solution[i];
+    }
+  }
+  return SolutionIsFeasible(model, *new_combined_solution);
+}
+
+std::optional<std::vector<int64_t>> FindCombinedSolution(
+    const CpModelProto& model, absl::Span<const int64_t> new_solution,
+    absl::Span<const int64_t> base_solution,
+    const SharedResponseManager* response_manager, std::string* solution_info) {
+  CHECK_EQ(new_solution.size(), base_solution.size());
+  const std::vector<
+      std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>>
+      solutions = response_manager->SolutionsRepository().GetBestNSolutions(10);
+
+  for (int sol_idx = 0; sol_idx < solutions.size(); ++sol_idx) {
+    std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution> s =
+        solutions[sol_idx];
+    DCHECK_EQ(s->variable_values.size(), new_solution.size());
+
+    if (s->variable_values == new_solution ||
+        s->variable_values == base_solution) {
+      continue;
+    }
+    std::vector<int64_t> new_combined_solution;
+    if (TrySolution(model, s->variable_values, new_solution, base_solution,
+                    &new_combined_solution)) {
+      absl::StrAppend(solution_info, " [combined with: ",
+                      std::string_view(solutions[sol_idx]->info).substr(0, 20),
+                      "...]");
+      return new_combined_solution;
+    }
+  }
+  return std::nullopt;
+}
+
+}  // namespace sat
+}  // namespace operations_research

ortools/sat/combine_solutions.h

@@ -0,0 +1,40 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#ifndef OR_TOOLS_SAT_COMBINE_SOLUTIONS_H_
+#define OR_TOOLS_SAT_COMBINE_SOLUTIONS_H_
+
+#include <cstdint>
+#include <optional>
+#include <string>
+#include <vector>
+
+#include "absl/types/span.h"
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/synchronization.h"
+
+namespace operations_research {
+namespace sat {
+
+// Given a `new_solution` that was created by changing a bit a `base_solution`,
+// try to apply the same changes to the other solutions stored in the
+// `response_manager` and return any such generated solution that is valid.
+std::optional<std::vector<int64_t>> FindCombinedSolution(
+    const CpModelProto& model, absl::Span<const int64_t> new_solution,
+    absl::Span<const int64_t> base_solution,
+    const SharedResponseManager* response_manager, std::string* solution_info);
+
+}  // namespace sat
+}  // namespace operations_research
+
+#endif  // OR_TOOLS_SAT_COMBINE_SOLUTIONS_H_

ortools/sat/combine_solutions_test.cc

@@ -0,0 +1,61 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#include "ortools/sat/combine_solutions.h"
+
+#include <cstdint>
+#include <string>
+#include <vector>
+
+#include "gtest/gtest.h"
+#include "ortools/base/gmock.h"
+#include "ortools/base/parse_test_proto.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/synchronization.h"
+
+namespace operations_research {
+namespace sat {
+namespace {
+
+using ::google::protobuf::contrib::parse_proto::ParseTestProto;
+using ::testing::ElementsAre;
+using ::testing::Optional;
+
+TEST(CombineSolutionsTest, BasicTest) {
+  const CpModelProto model = ParseTestProto(R"pb(
+    variables { domain: [ 0, 1 ] }
+    variables { domain: [ 0, 1 ] }
+    variables { domain: [ 0, 1 ] }
+    variables { domain: [ 0, 1 ] }
+    objective {
+      vars: [ 0, 1, 2, 3 ]
+      coeffs: [ 1, 1, 1, 1 ]
+    }
+  )pb");
+  const std::vector<int64_t> existing_solution = {1, 0, 0, 0};
+  const std::vector<int64_t> base_solution = {0, 1, 0, 0};
+  const std::vector<int64_t> new_solution = {0, 1, 1, 0};
+  Model m;
+  SharedResponseManager response_manager(&m);
+  response_manager.NewSolution(existing_solution, "existing", nullptr);
+  response_manager.NewSolution(base_solution, "base", nullptr);
+  response_manager.NewSolution(new_solution, "new", nullptr);
+  std::string solution_info;
+  const auto combined_solution = FindCombinedSolution(
+      model, new_solution, base_solution, &response_manager, &solution_info);
+  EXPECT_THAT(combined_solution, Optional(ElementsAre(1, 0, 1, 0)));
+}
+
+}  // namespace
+}  // namespace sat
+}  // namespace operations_research

ortools/sat/cp_model_checker.cc

@@ -105,13 +105,13 @@ std::string ValidateIntegerVariable(const CpModelProto& model, int v) {
 
   // Internally, we often take the negation of a domain, and we also want to
   // have sentinel values greater than the min/max of a variable domain, so
-  // the domain must fall in [kint64min + 2, kint64max - 1].
+  // the domain must fall in [-kint64max / 2, kint64max / 2].
   const int64_t lb = proto.domain(0);
   const int64_t ub = proto.domain(proto.domain_size() - 1);
-  if (lb < std::numeric_limits<int64_t>::min() + 2 ||
-      ub > std::numeric_limits<int64_t>::max() - 1) {
+  if (lb < -std::numeric_limits<int64_t>::max() / 2 ||
+      ub > std::numeric_limits<int64_t>::max() / 2) {
     return absl::StrCat(
-        "var #", v, " domain do not fall in [kint64min + 2, kint64max - 1]. ",
+        "var #", v, " domain do not fall in [-kint64max / 2, kint64max / 2]. ",
         ProtobufShortDebugString(proto));
   }
 
@@ -361,8 +361,14 @@ std::string ValidateIntProdConstraint(const CpModelProto& model,
   // Detect potential overflow.
   Domain product_domain(1);
   for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
-    product_domain = product_domain.ContinuousMultiplicationBy(
-        {MinOfExpression(model, expr), MaxOfExpression(model, expr)});
+    const int64_t min_expr = MinOfExpression(model, expr);
+    const int64_t max_expr = MaxOfExpression(model, expr);
+    if (min_expr == 0 && max_expr == 0) {
+      // An overflow multiplied by zero is still invalid.
+      continue;
+    }
+    product_domain =
+        product_domain.ContinuousMultiplicationBy({min_expr, max_expr});
   }
 
   if (product_domain.Max() <= -std ::numeric_limits<int64_t>::max() ||
@@ -918,11 +924,6 @@ std::string ValidateSearchStrategies(const CpModelProto& model) {
                             " has a domain too large to be used in a"
                             " SELECT_MEDIAN_VALUE value selection strategy");
       }
-      if (PossibleIntegerOverflow(model, {ref}, {1})) {
-        // This will become an overflow if translated to an expr.
-        return absl::StrCat("Possible integer overflow in strategy: ",
-                            ProtobufShortDebugString(strategy));
-      }
     }
     for (const LinearExpressionProto& expr : strategy.exprs()) {
       for (const int var : expr.vars()) {
@@ -1025,9 +1026,6 @@ bool PossibleIntegerOverflow(const CpModelProto& model,
 }
 
 std::string ValidateCpModel(const CpModelProto& model, bool after_presolve) {
-  if (!after_presolve && model.has_symmetry()) {
-    return "The symmetry field should be empty and reserved for internal use.";
-  }
   int64_t int128_overflow = 0;
   for (int v = 0; v < model.variables_size(); ++v) {
     RETURN_IF_NOT_EMPTY(ValidateIntegerVariable(model, v));
@@ -1637,26 +1635,51 @@ class ConstraintChecker {
     const int num_arcs = ct.routes().tails_size();
     int num_used_arcs = 0;
     int num_self_arcs = 0;
+
+    // Compute the number of nodes.
     int num_nodes = 0;
-    std::vector<int> tail_to_head;
+    for (int i = 0; i < num_arcs; ++i) {
+      num_nodes = std::max(num_nodes, 1 + ct.routes().tails(i));
+      num_nodes = std::max(num_nodes, 1 + ct.routes().heads(i));
+    }
+
+    std::vector<int> tail_to_head(num_nodes, -1);
+    std::vector<bool> has_incoming_arc(num_nodes, false);
+    std::vector<int> has_outgoing_arc(num_nodes, false);
     std::vector<int> depot_nexts;
     for (int i = 0; i < num_arcs; ++i) {
       const int tail = ct.routes().tails(i);
       const int head = ct.routes().heads(i);
-      num_nodes = std::max(num_nodes, 1 + tail);
-      num_nodes = std::max(num_nodes, 1 + head);
-      tail_to_head.resize(num_nodes, -1);
       if (LiteralIsTrue(ct.routes().literals(i))) {
+        // Check for loops.
+        if (tail != 0) {
+          if (has_outgoing_arc[tail]) {
+            VLOG(1) << "routes: node " << tail << "has two outgoing arcs";
+            return false;
+          }
+          has_outgoing_arc[tail] = true;
+        }
+        if (head != 0) {
+          if (has_incoming_arc[head]) {
+            VLOG(1) << "routes: node " << head << "has two incoming arcs";
+            return false;
+          }
+          has_incoming_arc[head] = true;
+        }
+
         if (tail == head) {
-          if (tail == 0) return false;
+          if (tail == 0) {
+            VLOG(1) << "Self loop on node 0 are forbidden.";
+            return false;
+          }
           ++num_self_arcs;
           continue;
         }
         ++num_used_arcs;
         if (tail == 0) {
           depot_nexts.push_back(head);
         } else {
-          if (tail_to_head[tail] != -1) return false;
+          DCHECK_EQ(tail_to_head[tail], -1);
           tail_to_head[tail] = head;
         }
       }
@@ -1769,9 +1792,9 @@ class ConstraintChecker {
             // This indicates that such a constraint was not added to the model.
             // It should probably be a validation error, but it is hard to
             // detect beforehand.
-            LOG(ERROR) << "Warning, an interval constraint was likely used "
-                          "without a corresponding linear constraint linking "
-                          "its start, size and end.";
+            VLOG(1) << "Warning, an interval constraint was likely used "
+                       "without a corresponding linear constraint linking "
+                       "its start, size and end.";
           }
           return false;
         }