[CP-SAT] simplify lns model when possible; reimplement max_hs

Author: lperron

ortools/sat/BUILD.bazel

@@ -215,6 +215,7 @@ cc_library(
         ":sat_parameters_cc_proto",
         "//ortools/base:protobuf_util",
         "//ortools/base/macros:os_support",
+        "//ortools/util:saturated_arithmetic",
         "//ortools/util:sorted_interval_list",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
@@ -238,7 +239,6 @@ cc_test(
         ":sat_parameters_cc_proto",
         "//ortools/base:gmock_main",
         "//ortools/base:parse_test_proto",
-        "//ortools/base:protobuf_util",
         "//ortools/linear_solver:linear_solver_cc_proto",
     ],
 )
@@ -567,13 +567,15 @@ cc_library(
         ":cp_model_utils",
         ":integer_base",
         ":model",
+        ":sat_base",
         ":sat_parameters_cc_proto",
         ":symmetry_util",
         ":util",
         "//ortools/algorithms:sparse_permutation",
         "//ortools/base:file",
         "//ortools/base:log_severity",
         "//ortools/base:stl_util",
+        "//ortools/base:strong_vector",
         "//ortools/base:timer",
         "//ortools/base/macros:os_support",
         "//ortools/util:bitset",
@@ -607,6 +609,7 @@ cc_test(
     srcs = ["synchronization_test.cc"],
     deps = [
         ":cp_model_cc_proto",
+        ":cp_model_utils",
         ":integer_base",
         ":model",
         ":synchronization",
@@ -1631,6 +1634,7 @@ cc_library(
         "@abseil-cpp//absl/base:core_headers",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
+        "@abseil-cpp//absl/strings",
         "@abseil-cpp//absl/strings:str_format",
         "@abseil-cpp//absl/types:span",
     ],
@@ -3154,6 +3158,7 @@ cc_library(
         "//ortools/util:saturated_arithmetic",
         "//ortools/util:strong_integers",
         "//ortools/util:time_limit",
+        "@abseil-cpp//absl/algorithm:container",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/log",
@@ -3515,6 +3520,7 @@ cc_library(
     deps = [
         ":cp_model_cc_proto",
         ":cp_model_mapping",
+        ":cp_model_utils",
         ":integer",
         ":integer_base",
         ":integer_search",
@@ -3533,6 +3539,7 @@ cc_library(
         "//ortools/util:time_limit",
         "@abseil-cpp//absl/cleanup",
         "@abseil-cpp//absl/container:flat_hash_map",
+        "@abseil-cpp//absl/container:flat_hash_set",
         "@abseil-cpp//absl/flags:flag",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
@@ -4331,7 +4338,6 @@ cc_library(
         "//ortools/base:timer",
         "//ortools/base/macros:os_support",
         "//ortools/util:stats",
-        "@abseil-cpp//absl/flags:flag",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/log:vlog_is_on",

ortools/sat/CMakeLists.txt

@@ -18,7 +18,6 @@ list(REMOVE_ITEM _SRCS
   ${CMAKE_CURRENT_SOURCE_DIR}/opb_reader.h
   ${CMAKE_CURRENT_SOURCE_DIR}/sat_cnf_reader.h
   ${CMAKE_CURRENT_SOURCE_DIR}/sat_runner.cc
-  ${CMAKE_CURRENT_SOURCE_DIR}/lrat_checker_main.cc
 )
 set(NAME ${PROJECT_NAME}_sat)