BUILD.bazel

# 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.

# Home of CP/SAT solver (which includes SAT, max-SAT and PB problems).

load("@rules_proto//proto:defs.bzl", "proto_library")
load("@rules_java//java:defs.bzl", "java_proto_library")
load("@rules_cc//cc:defs.bzl", "cc_library", "cc_proto_library")
load("@rules_python//python:proto.bzl", "py_proto_library")

package(default_visibility = ["//visibility:public"])

cc_library(
    name = "cp_model",
    srcs = ["cp_model.cc"],
    hdrs = ["cp_model.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_solver",
        ":cp_model_utils",
        ":model",
        ":sat_parameters_cc_proto",
        "//ortools/util:sorted_interval_list",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "model",
    hdrs = ["model.h"],
    deps = [
        "//ortools/base",
        "//ortools/base:typeid",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
    ],
)

proto_library(
    name = "sat_parameters_proto",
    srcs = ["sat_parameters.proto"],
)

cc_proto_library(
    name = "sat_parameters_cc_proto",
    deps = [":sat_parameters_proto"],
)

py_proto_library(
    name = "sat_parameters_py_pb2",
    deps = [":sat_parameters_proto"],
)

java_proto_library(
    name = "sat_parameters_java_proto",
    deps = [":sat_parameters_proto"],
)

proto_library(
    name = "cp_model_proto",
    srcs = ["cp_model.proto"],
)

cc_proto_library(
    name = "cp_model_cc_proto",
    deps = [":cp_model_proto"],
)

py_proto_library(
    name = "cp_model_py_pb2",
    deps = [":cp_model_proto"],
)

java_proto_library(
    name = "cp_model_java_proto",
    deps = [":cp_model_proto"],
)

cc_library(
    name = "cp_model_utils",
    srcs = ["cp_model_utils.cc"],
    hdrs = ["cp_model_utils.h"],
    deps = [
        ":cp_model_cc_proto",
        ":sat_base",
        "//ortools/base:file",
        "//ortools/base:hash",
        "//ortools/base:stl_util",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "synchronization",
    srcs = ["synchronization.cc"],
    hdrs = ["synchronization.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_utils",
        ":integer",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":util",
        "//ortools/base",
        "//ortools/base:status_macros",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/base:timer",
        "//ortools/util:bitset",
        "//ortools/util:logging",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/algorithm:container",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/synchronization",
        "@com_google_absl//absl/time",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "cp_model_checker",
    srcs = ["cp_model_checker.cc"],
    hdrs = ["cp_model_checker.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_utils",
        ":sat_parameters_cc_proto",
        "//ortools/base",
        "//ortools/base:types",
        "//ortools/port:proto_utils",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "constraint_violation",
    srcs = ["constraint_violation.cc"],
    hdrs = ["constraint_violation.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_utils",
        ":sat_parameters_cc_proto",
        ":util",
        "//ortools/base:stl_util",
        "//ortools/graph:strongly_connected_components",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "@com_google_absl//absl/algorithm:container",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "feasibility_jump",
    srcs = ["feasibility_jump.cc"],
    hdrs = ["feasibility_jump.h"],
    deps = [
        ":constraint_violation",
        ":cp_model_cc_proto",
        ":cp_model_checker",
        ":cp_model_utils",
        ":integer",
        ":linear_model",
        ":restart",
        ":sat_parameters_cc_proto",
        ":stat_tables",
        ":subsolver",
        ":synchronization",
        ":util",
        "//ortools/algorithms:binary_search",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/functional:any_invocable",
        "@com_google_absl//absl/functional:bind_front",
        "@com_google_absl//absl/functional:function_ref",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "linear_model",
    srcs = ["linear_model.cc"],
    hdrs = ["linear_model.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_utils",
        "//ortools/util:sorted_interval_list",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
    ],
)

cc_library(
    name = "parameters_validation",
    srcs = ["parameters_validation.cc"],
    hdrs = ["parameters_validation.h"],
    deps = [
        ":cp_model_search",
        ":sat_parameters_cc_proto",
        "@com_google_absl//absl/strings",
    ],
)

cc_library(
    name = "cp_model_search",
    srcs = ["cp_model_search.cc"],
    hdrs = ["cp_model_search.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_mapping",
        ":cp_model_utils",
        ":integer",
        ":integer_search",
        ":linear_propagation",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":util",
        "//ortools/base",
        "//ortools/base:types",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings",
    ],
)

cc_library(
    name = "cp_model_solver",
    srcs = ["cp_model_solver.cc"],
    hdrs = ["cp_model_solver.h"],
    deps = [
        ":circuit",
        ":clause",
        ":cp_model_cc_proto",
        ":cp_model_checker",
        ":cp_model_lns",
        ":cp_model_loader",
        ":cp_model_mapping",
        ":cp_model_postsolve",
        ":cp_model_presolve",
        ":cp_model_search",
        ":cp_model_symmetries",
        ":cp_model_utils",
        ":cuts",
        ":feasibility_jump",
        ":feasibility_pump",
        ":implied_bounds",
        ":integer",
        ":integer_expr",
        ":integer_search",
        ":intervals",
        ":lb_tree_search",
        ":linear_constraint",
        ":linear_model",
        ":linear_programming_constraint",
        ":linear_relaxation",
        ":lp_utils",
        ":max_hs",
        ":model",
        ":optimization",
        ":parameters_validation",
        ":precedences",
        ":presolve_context",
        ":probing",
        ":rins",
        ":sat_base",
        ":sat_inprocessing",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":simplification",
        ":stat_tables",
        ":subsolver",
        ":synchronization",
        ":util",
        ":work_assignment",
        "//ortools/base",
        "//ortools/base:status_macros",
        "//ortools/base:strong_vector",
        "//ortools/base:threadpool",
        "//ortools/base:timer",
        "//ortools/base:types",
        "//ortools/graph:connected_components",
        "//ortools/linear_solver:linear_solver_cc_proto",
        "//ortools/port:proto_utils",
        "//ortools/util:logging",
        "//ortools/util:random_engine",
        "//ortools/util:sigint",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/cleanup",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/synchronization",
        "@com_google_absl//absl/types:span",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "cp_model_mapping",
    hdrs = ["cp_model_mapping.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_utils",
        ":integer",
        ":intervals",
        ":linear_constraint",
        ":model",
        ":sat_base",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/base:types",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
    ],
)

cc_library(
    name = "cp_model_loader",
    srcs = ["cp_model_loader.cc"],
    hdrs = ["cp_model_loader.h"],
    deps = [
        ":all_different",
        ":circuit",
        ":cp_constraints",
        ":cp_model_cc_proto",
        ":cp_model_mapping",
        ":cp_model_utils",
        ":cumulative",
        ":diffn",
        ":disjunctive",
        ":implied_bounds",
        ":integer",
        ":integer_expr",
        ":intervals",
        ":linear_constraint",
        ":linear_relaxation",
        ":model",
        ":pb_constraint",
        ":precedences",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":symmetry",
        ":table",
        ":timetable",
        ":util",
        "//ortools/algorithms:sparse_permutation",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/base:types",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

proto_library(
    name = "boolean_problem_proto",
    srcs = ["boolean_problem.proto"],
)

cc_proto_library(
    name = "boolean_problem_cc_proto",
    deps = [":boolean_problem_proto"],
)

cc_library(
    name = "presolve_util",
    srcs = ["presolve_util.cc"],
    hdrs = ["presolve_util.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_utils",
        ":util",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/base:types",
        "//ortools/util:bitset",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/random",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "presolve_context",
    srcs = ["presolve_context.cc"],
    hdrs = ["presolve_context.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_checker",
        ":cp_model_loader",
        ":cp_model_mapping",
        ":cp_model_utils",
        ":integer",
        ":lp_utils",
        ":model",
        ":presolve_util",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":util",
        "//ortools/base",
        "//ortools/base:mathutil",
        "//ortools/port:proto_utils",
        "//ortools/util:affine_relation",
        "//ortools/util:bitset",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "cp_model_presolve",
    srcs = [
        "cp_model_presolve.cc",
    ],
    hdrs = ["cp_model_presolve.h"],
    deps = [
        ":circuit",
        ":clause",
        ":cp_model_cc_proto",
        ":cp_model_checker",
        ":cp_model_expand",
        ":cp_model_mapping",
        ":cp_model_symmetries",
        ":cp_model_utils",
        ":diffn_util",
        ":diophantine",
        ":inclusion",
        ":integer",
        ":model",
        ":presolve_context",
        ":presolve_util",
        ":probing",
        ":sat_base",
        ":sat_inprocessing",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":simplification",
        ":util",
        ":var_domination",
        "//ortools/base",
        "//ortools/base:mathutil",
        "//ortools/base:protobuf_util",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/base:timer",
        "//ortools/graph:strongly_connected_components",
        "//ortools/graph:topologicalsorter",
        "//ortools/port:proto_utils",
        "//ortools/util:affine_relation",
        "//ortools/util:bitset",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/algorithm:container",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/hash",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "cp_model_postsolve",
    srcs = [
        "cp_model_postsolve.cc",
    ],
    hdrs = ["cp_model_postsolve.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_utils",
        "//ortools/base",
        "//ortools/base:types",
        "//ortools/port:proto_utils",
        "//ortools/util:sorted_interval_list",
        "@com_google_absl//absl/log:check",
    ],
)

cc_library(
    name = "cp_model_expand",
    srcs = ["cp_model_expand.cc"],
    hdrs = ["cp_model_expand.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_checker",
        ":cp_model_utils",
        ":presolve_context",
        ":sat_parameters_cc_proto",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:types",
        "//ortools/port:proto_utils",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "sat_base",
    hdrs = ["sat_base.h"],
    deps = [
        ":model",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/base:types",
        "//ortools/util:bitset",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

# Enable a warning to check for floating point to integer conversions.
# In GCC-4.8, this was "-Wreal-conversion", but was removed in 4.9
# In Clang, this warning is "-Wfloat-conversion"
W_FLOAT_CONVERSION = "-Wfloat-conversion"

cc_library(
    name = "sat_solver",
    srcs = [
        "sat_solver.cc",
    ],
    hdrs = ["sat_solver.h"],
    deps = [
        ":clause",
        ":drat_proof_handler",
        ":model",
        ":pb_constraint",
        ":restart",
        ":sat_base",
        ":sat_decision",
        ":sat_parameters_cc_proto",
        ":util",
        "//ortools/base",
        "//ortools/base:hash",
        "//ortools/base:stl_util",
        "//ortools/base:timer",
        "//ortools/base:types",
        "//ortools/port:proto_utils",
        "//ortools/port:sysinfo",
        "//ortools/util:bitset",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:stats",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "restart",
    srcs = ["restart.cc"],
    hdrs = ["restart.h"],
    deps = [
        ":model",
        ":sat_decision",
        ":sat_parameters_cc_proto",
        "//ortools/base",
        "//ortools/port:proto_utils",
        "//ortools/util:bitset",
        "//ortools/util:running_stat",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
    ],
)

cc_library(
    name = "probing",
    srcs = ["probing.cc"],
    hdrs = ["probing.h"],
    deps = [
        ":clause",
        ":implied_bounds",
        ":integer",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":util",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/base:timer",
        "//ortools/util:bitset",
        "//ortools/util:logging",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "sat_inprocessing",
    srcs = ["sat_inprocessing.cc"],
    hdrs = ["sat_inprocessing.h"],
    deps = [
        ":clause",
        ":drat_checker",
        ":linear_programming_constraint",
        ":model",
        ":probing",
        ":sat_base",
        ":sat_decision",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/base:timer",
        "//ortools/util:bitset",
        "//ortools/util:integer_pq",
        "//ortools/util:logging",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/cleanup",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "sat_decision",
    srcs = ["sat_decision.cc"],
    hdrs = ["sat_decision.h"],
    deps = [
        ":model",
        ":pb_constraint",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":util",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/base:types",
        "//ortools/util:bitset",
        "//ortools/util:integer_pq",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
    ],
)

cc_library(
    name = "clause",
    srcs = ["clause.cc"],
    hdrs = ["clause.h"],
    deps = [
        ":drat_proof_handler",
        ":inclusion",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/base:timer",
        "//ortools/graph:strongly_connected_components",
        "//ortools/util:bitset",
        "//ortools/util:stats",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "simplification",
    srcs = ["simplification.cc"],
    hdrs = ["simplification.h"],
    deps = [
        ":drat_proof_handler",
        ":model",
        ":probing",
        ":sat_base",
        ":sat_inprocessing",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        "//ortools/algorithms:dynamic_partition",
        "//ortools/base",
        "//ortools/base:adjustable_priority_queue",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/base:timer",
        "//ortools/base:types",
        "//ortools/graph:strongly_connected_components",
        "//ortools/util:logging",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "pb_constraint",
    srcs = ["pb_constraint.cc"],
    hdrs = ["pb_constraint.h"],
    deps = [
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/base:types",
        "//ortools/util:bitset",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:stats",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/hash",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "symmetry",
    srcs = ["symmetry.cc"],
    hdrs = ["symmetry.h"],
    deps = [
        ":sat_base",
        "//ortools/algorithms:sparse_permutation",
        "//ortools/base:strong_vector",
        "//ortools/util:stats",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "symmetry_util",
    srcs = ["symmetry_util.cc"],
    hdrs = ["symmetry_util.h"],
    deps = [
        "//ortools/algorithms:dynamic_partition",
        "//ortools/algorithms:sparse_permutation",
        "//ortools/base",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "var_domination",
    srcs = ["var_domination.cc"],
    hdrs = ["var_domination.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_utils",
        ":integer",
        ":presolve_context",
        ":presolve_util",
        ":util",
        "//ortools/algorithms:dynamic_partition",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/util:affine_relation",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "integer",
    srcs = ["integer.cc"],
    hdrs = ["integer.h"],
    deps = [
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/util:bitset",
        "//ortools/util:rev",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/cleanup",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "integer_search",
    srcs = ["integer_search.cc"],
    hdrs = ["integer_search.h"],
    deps = [
        ":clause",
        ":cp_model_cc_proto",
        ":cp_model_mapping",
        ":implied_bounds",
        ":integer",
        ":intervals",
        ":linear_constraint_manager",
        ":linear_programming_constraint",
        ":model",
        ":probing",
        ":pseudo_costs",
        ":restart",
        ":rins",
        ":sat_base",
        ":sat_decision",
        ":sat_inprocessing",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":synchronization",
        ":util",
        "//ortools/base",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "lb_tree_search",
    srcs = ["lb_tree_search.cc"],
    hdrs = ["lb_tree_search.h"],
    deps = [
        ":cp_model_mapping",
        ":integer",
        ":integer_expr",
        ":integer_search",
        ":linear_programming_constraint",
        ":model",
        ":sat_base",
        ":sat_decision",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":synchronization",
        ":util",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/time",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "pseudo_costs",
    srcs = ["pseudo_costs.cc"],
    hdrs = ["pseudo_costs.h"],
    deps = [
        ":integer",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":util",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
    ],
)

cc_library(
    name = "intervals",
    srcs = ["intervals.cc"],
    hdrs = ["intervals.h"],
    deps = [
        ":cp_constraints",
        ":implied_bounds",
        ":integer",
        ":integer_expr",
        ":linear_constraint",
        ":model",
        ":pb_constraint",
        ":precedences",
        ":sat_base",
        ":sat_solver",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/util:rev",
        "//ortools/util:sort",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "precedences",
    srcs = ["precedences.cc"],
    hdrs = ["precedences.h"],
    deps = [
        ":clause",
        ":cp_constraints",
        ":integer",
        ":model",
        ":sat_base",
        ":sat_solver",
        ":synchronization",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/base:types",
        "//ortools/graph",
        "//ortools/graph:topologicalsorter",
        "//ortools/util:bitset",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/cleanup",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "integer_expr",
    srcs = ["integer_expr.cc"],
    hdrs = ["integer_expr.h"],
    deps = [
        ":integer",
        ":linear_constraint",
        ":linear_propagation",
        ":model",
        ":precedences",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":util",
        "//ortools/base",
        "//ortools/base:mathutil",
        "//ortools/base:stl_util",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "linear_propagation",
    srcs = ["linear_propagation.cc"],
    hdrs = ["linear_propagation.h"],
    deps = [
        ":integer",
        ":model",
        ":sat_base",
        ":sat_solver",
        ":synchronization",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/util:bitset",
        "//ortools/util:rev",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "all_different",
    srcs = ["all_different.cc"],
    hdrs = ["all_different.h"],
    deps = [
        ":integer",
        ":model",
        ":sat_base",
        ":sat_solver",
        "//ortools/base",
        "//ortools/base:types",
        "//ortools/graph:strongly_connected_components",
        "//ortools/util:sort",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "theta_tree",
    srcs = ["theta_tree.cc"],
    hdrs = ["theta_tree.h"],
    deps = [
        ":integer",
        "//ortools/base",
        "@com_google_absl//absl/log:check",
    ],
)

cc_library(
    name = "disjunctive",
    srcs = ["disjunctive.cc"],
    hdrs = ["disjunctive.h"],
    deps = [
        ":all_different",
        ":integer",
        ":integer_expr",
        ":intervals",
        ":model",
        ":precedences",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":theta_tree",
        ":timetable",
        "//ortools/base",
        "//ortools/util:sort",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/algorithm:container",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "timetable",
    srcs = ["timetable.cc"],
    hdrs = ["timetable.h"],
    deps = [
        ":integer",
        ":intervals",
        ":model",
        ":sat_base",
        "//ortools/util:rev",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "timetable_edgefinding",
    srcs = ["timetable_edgefinding.cc"],
    hdrs = ["timetable_edgefinding.h"],
    deps = [
        ":integer",
        ":intervals",
        ":model",
        ":sat_base",
        "//ortools/base:iterator_adaptors",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
    ],
)

cc_library(
    name = "cumulative",
    srcs = ["cumulative.cc"],
    hdrs = ["cumulative.h"],
    deps = [
        ":cumulative_energy",
        ":disjunctive",
        ":integer",
        ":integer_expr",
        ":intervals",
        ":linear_constraint",
        ":model",
        ":pb_constraint",
        ":precedences",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":timetable",
        ":timetable_edgefinding",
        "//ortools/base",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
    ],
)

cc_library(
    name = "cumulative_energy",
    srcs = ["cumulative_energy.cc"],
    hdrs = ["cumulative_energy.h"],
    deps = [
        ":integer",
        ":intervals",
        ":model",
        ":theta_tree",
        ":util",
        "//ortools/base",
        "//ortools/base:iterator_adaptors",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
    ],
)

cc_library(
    name = "boolean_problem",
    srcs = ["boolean_problem.cc"],
    hdrs = ["boolean_problem.h"],
    deps = [
        ":boolean_problem_cc_proto",
        ":cp_model_cc_proto",
        ":pb_constraint",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":simplification",
        "//ortools/algorithms:find_graph_symmetries",
        "//ortools/algorithms:sparse_permutation",
        "//ortools/base",
        "//ortools/base:hash",
        "//ortools/base:status_macros",
        "//ortools/base:strong_vector",
        "//ortools/graph",
        "//ortools/graph:io",
        "//ortools/graph:util",
        "//ortools/port:proto_utils",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
    ],
)

cc_library(
    name = "linear_relaxation",
    srcs = ["linear_relaxation.cc"],
    hdrs = ["linear_relaxation.h"],
    deps = [
        ":circuit",
        ":clause",
        ":cp_model_cc_proto",
        ":cp_model_mapping",
        ":cp_model_utils",
        ":cuts",
        ":diffn_cuts",
        ":implied_bounds",
        ":integer",
        ":integer_expr",
        ":intervals",
        ":linear_constraint",
        ":model",
        ":precedences",
        ":presolve_util",
        ":routing_cuts",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":scheduling_cuts",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/types:span",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "linear_constraint",
    srcs = ["linear_constraint.cc"],
    hdrs = ["linear_constraint.h"],
    deps = [
        ":integer",
        ":model",
        ":sat_base",
        "//ortools/base:mathutil",
        "//ortools/base:strong_vector",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "linear_programming_constraint",
    srcs = ["linear_programming_constraint.cc"],
    hdrs = ["linear_programming_constraint.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_mapping",
        ":cuts",
        ":implied_bounds",
        ":integer",
        ":integer_expr",
        ":linear_constraint",
        ":linear_constraint_manager",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":synchronization",
        ":util",
        ":zero_half_cuts",
        "//ortools/algorithms:binary_search",
        "//ortools/base",
        "//ortools/base:mathutil",
        "//ortools/base:strong_vector",
        "//ortools/glop:parameters_cc_proto",
        "//ortools/glop:revised_simplex",
        "//ortools/glop:status",
        "//ortools/glop:variables_info",
        "//ortools/lp_data",
        "//ortools/lp_data:base",
        "//ortools/lp_data:lp_data_utils",
        "//ortools/lp_data:scattered_vector",
        "//ortools/lp_data:sparse_column",
        "//ortools/util:bitset",
        "//ortools/util:rev",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "linear_constraint_manager",
    srcs = ["linear_constraint_manager.cc"],
    hdrs = ["linear_constraint_manager.h"],
    deps = [
        ":integer",
        ":linear_constraint",
        ":model",
        ":sat_parameters_cc_proto",
        ":synchronization",
        ":util",
        "//ortools/base",
        "//ortools/base:hash",
        "//ortools/base:strong_vector",
        "//ortools/glop:revised_simplex",
        "//ortools/glop:variables_info",
        "//ortools/lp_data:base",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
    ],
)

cc_library(
    name = "cuts",
    srcs = ["cuts.cc"],
    hdrs = ["cuts.h"],
    deps = [
        ":clause",
        ":implied_bounds",
        ":integer",
        ":linear_constraint",
        ":linear_constraint_manager",
        ":model",
        ":sat_base",
        ":synchronization",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/lp_data:base",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "routing_cuts",
    srcs = ["routing_cuts.cc"],
    hdrs = ["routing_cuts.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cuts",
        ":integer",
        ":linear_constraint",
        ":linear_constraint_manager",
        ":model",
        ":sat_base",
        ":util",
        "//ortools/base",
        "//ortools/base:mathutil",
        "//ortools/base:strong_vector",
        "//ortools/graph",
        "//ortools/graph:max_flow",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/cleanup",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "scheduling_cuts",
    srcs = ["scheduling_cuts.cc"],
    hdrs = ["scheduling_cuts.h"],
    deps = [
        ":cuts",
        ":implied_bounds",
        ":integer",
        ":intervals",
        ":linear_constraint",
        ":linear_constraint_manager",
        ":model",
        ":sat_base",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "diffn_cuts",
    srcs = ["diffn_cuts.cc"],
    hdrs = ["diffn_cuts.h"],
    deps = [
        ":cuts",
        ":diffn_util",
        ":implied_bounds",
        ":integer",
        ":intervals",
        ":linear_constraint",
        ":linear_constraint_manager",
        ":model",
        ":sat_base",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "zero_half_cuts",
    srcs = ["zero_half_cuts.cc"],
    hdrs = ["zero_half_cuts.h"],
    deps = [
        ":integer",
        ":util",
        "//ortools/base",
        "//ortools/lp_data:base",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "lp_utils",
    srcs = ["lp_utils.cc"],
    hdrs = ["lp_utils.h"],
    deps = [
        ":boolean_problem",
        ":boolean_problem_cc_proto",
        ":cp_model_cc_proto",
        ":cp_model_utils",
        ":integer",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/glop:lp_solver",
        "//ortools/glop:parameters_cc_proto",
        "//ortools/linear_solver:linear_solver_cc_proto",
        "//ortools/lp_data",
        "//ortools/lp_data:base",
        "//ortools/port:proto_utils",
        "//ortools/util:fp_utils",
        "//ortools/util:logging",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "optimization",
    srcs = ["optimization.cc"],
    hdrs = ["optimization.h"],
    deps = [
        ":boolean_problem",
        ":boolean_problem_cc_proto",
        ":clause",
        ":cp_model_mapping",
        ":encoding",
        ":integer",
        ":integer_expr",
        ":integer_search",
        ":model",
        ":pb_constraint",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":synchronization",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/port:proto_utils",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/cleanup",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "max_hs",
    srcs = ["max_hs.cc"],
    hdrs = ["max_hs.h"],
    deps = [
        ":boolean_problem",
        ":cp_model_cc_proto",
        ":cp_model_mapping",
        ":cp_model_utils",
        ":encoding",
        ":integer",
        ":integer_expr",
        ":integer_search",
        ":linear_constraint",
        ":linear_relaxation",
        ":model",
        ":optimization",
        ":pb_constraint",
        ":presolve_util",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":synchronization",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:strong_vector",
        "//ortools/base:timer",
        "//ortools/linear_solver:linear_solver_cc_proto",
        "//ortools/port:proto_utils",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/cleanup",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/random",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "util",
    srcs = ["util.cc"],
    hdrs = ["util.h"],
    deps = [
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        "//ortools/base",
        "//ortools/base:mathutil",
        "//ortools/base:stl_util",
        "//ortools/util:random_engine",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/log:log_streamer",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/random",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "stat_tables",
    srcs = ["stat_tables.cc"],
    hdrs = ["stat_tables.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_lns",
        ":linear_programming_constraint",
        ":model",
        ":sat_solver",
        ":subsolver",
        ":synchronization",
        ":util",
        "//ortools/lp_data:base",
        "//ortools/util:logging",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/synchronization",
    ],
)

cc_library(
    name = "table",
    srcs = ["table.cc"],
    hdrs = ["table.h"],
    deps = [
        ":integer",
        ":model",
        ":sat_base",
        ":sat_solver",
        "//ortools/base:types",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "cp_constraints",
    srcs = ["cp_constraints.cc"],
    hdrs = ["cp_constraints.h"],
    deps = [
        ":integer",
        ":model",
        ":sat_base",
        "//ortools/base",
        "//ortools/base:types",
        "//ortools/util:rev",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "diffn_util",
    srcs = ["diffn_util.cc"],
    hdrs = ["diffn_util.h"],
    deps = [
        ":integer",
        ":intervals",
        ":util",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/util:integer_pq",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "2d_orthogonal_packing",
    srcs = ["2d_orthogonal_packing.cc"],
    hdrs = ["2d_orthogonal_packing.h"],
    deps = [
        ":integer",
        ":synchronization",
        ":util",
        "//ortools/util:bitset",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/numeric:bits",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "2d_orthogonal_packing_testing",
    testonly = 1,
    srcs = ["2d_orthogonal_packing_testing.cc"],
    hdrs = ["2d_orthogonal_packing_testing.h"],
    deps = [
        ":diffn_util",
        ":integer",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
    ],
)

cc_library(
    name = "diffn",
    srcs = ["diffn.cc"],
    hdrs = ["diffn.h"],
    deps = [
        ":2d_orthogonal_packing",
        ":cumulative_energy",
        ":diffn_util",
        ":disjunctive",
        ":integer",
        ":integer_expr",
        ":intervals",
        ":linear_constraint",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":synchronization",
        ":timetable",
        ":util",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/container:inlined_vector",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "circuit",
    srcs = ["circuit.cc"],
    hdrs = ["circuit.h"],
    deps = [
        ":integer",
        ":model",
        ":sat_base",
        ":sat_solver",
        "//ortools/base",
        "//ortools/base:types",
        "//ortools/graph:strongly_connected_components",
        "//ortools/util:rev",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
    ],
)

cc_library(
    name = "encoding",
    srcs = ["encoding.cc"],
    hdrs = ["encoding.h"],
    deps = [
        ":boolean_problem_cc_proto",
        ":pb_constraint",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        "//ortools/base",
        "//ortools/base:stl_util",
        "//ortools/base:types",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "cp_model_lns",
    srcs = ["cp_model_lns.cc"],
    hdrs = ["cp_model_lns.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_mapping",
        ":cp_model_presolve",
        ":cp_model_utils",
        ":integer",
        ":linear_constraint_manager",
        ":linear_programming_constraint",
        ":model",
        ":presolve_context",
        ":rins",
        ":sat_parameters_cc_proto",
        ":subsolver",
        ":synchronization",
        ":util",
        "//ortools/base:stl_util",
        "//ortools/graph:connected_components",
        "//ortools/util:adaptative_parameter_value",
        "//ortools/util:integer_pq",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/algorithm:container",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/synchronization",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "feasibility_pump",
    srcs = ["feasibility_pump.cc"],
    hdrs = ["feasibility_pump.h"],
    deps = [
        ":cp_model_mapping",
        ":integer",
        ":linear_constraint",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":synchronization",
        ":util",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/glop:parameters_cc_proto",
        "//ortools/glop:revised_simplex",
        "//ortools/glop:status",
        "//ortools/lp_data",
        "//ortools/lp_data:base",
        "//ortools/lp_data:lp_data_utils",
        "//ortools/lp_data:sparse_column",
        "//ortools/util:saturated_arithmetic",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
    ],
)

cc_library(
    name = "rins",
    srcs = ["rins.cc"],
    hdrs = ["rins.h"],
    deps = [
        ":cp_model_mapping",
        ":integer",
        ":linear_programming_constraint",
        ":model",
        ":synchronization",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random:bit_gen_ref",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "subsolver",
    srcs = ["subsolver.cc"],
    hdrs = ["subsolver.h"],
    deps = [
        "//ortools/base",
        "//ortools/base:threadpool",
        "//ortools/base:timer",
        "//ortools/base:types",
        "//ortools/util:stats",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/synchronization",
        "@com_google_absl//absl/time",
    ],
)

cc_library(
    name = "drat_proof_handler",
    srcs = ["drat_proof_handler.cc"],
    hdrs = ["drat_proof_handler.h"],
    deps = [
        ":drat_checker",
        ":drat_writer",
        ":sat_base",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "drat_checker",
    srcs = ["drat_checker.cc"],
    hdrs = ["drat_checker.h"],
    deps = [
        ":sat_base",
        "//ortools/base",
        "//ortools/base:hash",
        "//ortools/base:strong_vector",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/time",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "drat_writer",
    srcs = ["drat_writer.cc"],
    hdrs = ["drat_writer.h"],
    deps = [
        ":sat_base",
        "//ortools/base",
        "//ortools/base:file",
        "//ortools/base:status_macros",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:span",
    ],
)

cc_binary(
    name = "sat_runner",
    srcs = [
        "opb_reader.h",
        "sat_runner.cc",
    ],
    deps = [
        ":boolean_problem",
        ":boolean_problem_cc_proto",
        ":cp_model_cc_proto",
        ":cp_model_solver",
        ":cp_model_utils",
        ":model",
        ":sat_cnf_reader",
        ":sat_parameters_cc_proto",
        "//ortools/base",
        "//ortools/base:file",
        "//ortools/base:path",
        "//ortools/util:file_util",
        "//ortools/util:filelineiter",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/log:flags",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "sat_cnf_reader",
    hdrs = ["sat_cnf_reader.h"],
    deps = [
        ":boolean_problem_cc_proto",
        ":cp_model_cc_proto",
        "//ortools/base",
        "//ortools/util:filelineiter",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "cp_model_symmetries",
    srcs = ["cp_model_symmetries.cc"],
    hdrs = ["cp_model_symmetries.h"],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_mapping",
        ":cp_model_utils",
        ":model",
        ":presolve_context",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":symmetry_util",
        ":util",
        "//ortools/algorithms:find_graph_symmetries",
        "//ortools/algorithms:sparse_permutation",
        "//ortools/base",
        "//ortools/base:hash",
        "//ortools/graph",
        "//ortools/util:affine_relation",
        "//ortools/util:logging",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "swig_helper",
    srcs = ["swig_helper.cc"],
    hdrs = ["swig_helper.h"],
    visibility = [
        "//ortools/sat/java:__pkg__",
        "//ortools/sat/python:__pkg__",
    ],
    deps = [
        ":cp_model_cc_proto",
        ":cp_model_checker",
        ":cp_model_solver",
        ":cp_model_utils",
        ":model",
        ":sat_parameters_cc_proto",
        "//ortools/util:logging",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:time_limit",
    ],
)

cc_library(
    name = "implied_bounds",
    srcs = ["implied_bounds.cc"],
    hdrs = ["implied_bounds.h"],
    deps = [
        "linear_constraint",
        ":clause",
        ":integer",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":synchronization",
        "//ortools/base",
        "//ortools/base:strong_vector",
        "//ortools/base:types",
        "//ortools/lp_data:base",
        "//ortools/util:bitset",
        "//ortools/util:sorted_interval_list",
        "//ortools/util:strong_integers",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/container:flat_hash_set",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/meta:type_traits",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "inclusion",
    hdrs = ["inclusion.h"],
    deps = [
        "//ortools/base",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "diophantine",
    srcs = ["diophantine.cc"],
    hdrs = ["diophantine.h"],
    deps = [
        ":util",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/types:span",
    ],
)

cc_library(
    name = "work_assignment",
    srcs = ["work_assignment.cc"],
    hdrs = ["work_assignment.h"],
    deps = [
        ":cp_model_mapping",
        ":cp_model_utils",
        ":integer",
        ":integer_search",
        ":model",
        ":sat_base",
        ":sat_parameters_cc_proto",
        ":sat_solver",
        ":synchronization",
        ":util",
        "//ortools/util:strong_integers",
        "//ortools/util:time_limit",
        "@com_google_absl//absl/base:core_headers",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/log:check",
        "@com_google_absl//absl/random:distributions",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/synchronization",
        "@com_google_absl//absl/types:span",
    ],
)