Merge pull request #7 from google/master

Fast forward to upstream
2017-07-03 15:43:25 +05:30
parent 31863e4dda 4033496f0e
commit 883f404873
33 changed files with 735 additions and 2201 deletions
--- a/examples/cpp/BUILD
+++ b/examples/cpp/BUILD
@@ -12,9 +12,9 @@ cc_binary(
    name = "cryptarithm",
    srcs = ["cryptarithm.cc"],
    deps = [
-        "@com_google_protobuf_cc//:protobuf",
        "//ortools/base",
        "//ortools/constraint_solver:cp",
+        "@com_google_protobuf_cc//:protobuf",
    ],
 )

@@ -230,7 +230,7 @@ cc_binary(
    srcs = ["integer_programming.cc"],
    deps = [
        "//ortools/base",
-        "//ortools/linear_solver:linear_solver",
+        "//ortools/linear_solver",
    ],
 )

@@ -309,7 +309,7 @@ cc_binary(
    copts = ["-DUSE_GLOP"],
    deps = [
        "//ortools/base",
-        "//ortools/linear_solver:linear_solver",
+        "//ortools/linear_solver",
        "//ortools/linear_solver:linear_solver_cc_proto",
    ],
 )
@@ -319,7 +319,7 @@ cc_binary(
    srcs = ["linear_solver_protocol_buffers.cc"],
    deps = [
        "//ortools/base",
-        "//ortools/linear_solver:linear_solver",
+        "//ortools/linear_solver",
        "//ortools/linear_solver:linear_solver_cc_proto",
    ],
 )
@@ -415,28 +415,28 @@ cc_binary(
        "sat_runner.cc",
    ],
    deps = [
-        "@com_google_protobuf_cc//:protobuf",
+        "//ortools/algorithms:sparse_permutation",
+        "//ortools/base",
+        "//ortools/base:file",
+        "//ortools/base:random",
+        "//ortools/base:status",
+        "//ortools/base:strings",
+        "//ortools/base:threadpool",
+        "//ortools/lp_data:mps_reader",
+        "//ortools/lp_data:proto_utils",
        "//ortools/sat:boolean_problem",
        "//ortools/sat:boolean_problem_cc_proto",
-        #        "//ortools/sat:cp_model_proto",
-        #        "//ortools/sat:cp_model_solver",
+        "//ortools/sat:cp_model_cc_proto",
+        "//ortools/sat:cp_model_solver",
        "//ortools/sat:drat",
        "//ortools/sat:lp_utils",
        "//ortools/sat:optimization",
        "//ortools/sat:sat_solver",
        "//ortools/sat:simplification",
        "//ortools/sat:symmetry",
-        "//ortools/base",
-        "//ortools/base:file",
-        "//ortools/base:strings",
-        "//ortools/base:status",
-        "//ortools/base:random",
-        "//ortools/base:threadpool",
-        "//ortools/algorithms:sparse_permutation",
-        "//ortools/lp_data:mps_reader",
-        "//ortools/lp_data:proto_utils",
        "//ortools/util:filelineiter",
        "//ortools/util:time_limit",
+        "@com_google_protobuf_cc//:protobuf",
    ],
 )

@@ -470,7 +470,7 @@ cc_binary(
    ],
    deps = [
        "//ortools/base",
-        "//ortools/linear_solver:linear_solver",
+        "//ortools/linear_solver",
        "//ortools/linear_solver:linear_solver_cc_proto",
        "//ortools/lp_data:mps_reader",
    ],
@@ -491,7 +491,7 @@ cc_binary(
    copts = ["-DUSE_GLOP"],
    deps = [
        "//ortools/base",
-        "//ortools/linear_solver:linear_solver",
+        "//ortools/linear_solver",
    ],
 )

@@ -499,11 +499,11 @@ cc_binary(
    name = "tsp",
    srcs = ["tsp.cc"],
    deps = [
-        "@com_google_protobuf_cc//:protobuf",
        "//ortools/base",
        "//ortools/constraint_solver:cp",
        "//ortools/constraint_solver:routing",
        "//ortools/constraint_solver:routing_flags",
+        "@com_google_protobuf_cc//:protobuf",
    ],
 )

@@ -513,7 +513,6 @@ cc_binary(
        "weighted_tardiness_sat.cc",
    ],
    deps = [
-        "@com_google_protobuf_cc//:protobuf",
        "//ortools/base",
        "//ortools/base:file",
        "//ortools/base:strings",
@@ -526,5 +525,6 @@ cc_binary(
        "//ortools/sat:precedences",
        "//ortools/sat:sat_solver",
        "//ortools/util:filelineiter",
+        "@com_google_protobuf_cc//:protobuf",
    ],
 )
--- a/examples/cpp/sat_cnf_reader.h
+++ b/examples/cpp/sat_cnf_reader.h
@@ -103,11 +103,11 @@ class SatCnfReader {
    return problem_name;
  }

-  int64 StringViewAtoi(const string_view& input) {
+  int64 StringPieceAtoi(string_view input) {
    // Hack: data() is not null terminated, but we do know that it points
    // inside a std::string where numbers are separated by " " and since atoi64 will
    // stop at the first invalid char, this works.
-    return atoi64(input.data());
+    return atoi64(input.data());  // NOLINT
  }

  void ProcessNewLine(const std::string& line, LinearBooleanProblem* problem) {
@@ -123,11 +123,11 @@ class SatCnfReader {

    if (words_[0] == "p") {
      if (words_[1] == "cnf" || words_[1] == "wcnf") {
-        num_variables_ = StringViewAtoi(words_[2]);
-        num_clauses_ = StringViewAtoi(words_[3]);
+        num_variables_ = StringPieceAtoi(words_[2]);
+        num_clauses_ = StringPieceAtoi(words_[3]);
        if (words_[1] == "wcnf") {
          is_wcnf_ = true;
-          hard_weight_ = (words_.size() > 4) ? StringViewAtoi(words_[4]) : 0;
+          hard_weight_ = (words_.size() > 4) ? StringPieceAtoi(words_[4]) : 0;
        }
      } else {
        // TODO(user): The ToString() is only required for the open source. Fix.
@@ -148,7 +148,7 @@ class SatCnfReader {
      int64 weight =
          (!is_wcnf_ && interpret_cnf_as_max_sat_) ? 1 : hard_weight_;
      for (int i = 0; i < size; ++i) {
-        const int64 signed_value = StringViewAtoi(words_[i]);
+        const int64 signed_value = StringPieceAtoi(words_[i]);
        if (i == 0 && is_wcnf_) {
          // Mathematically, a soft clause of weight 0 can be removed.
          if (signed_value == 0) {
--- a/examples/cpp/sat_runner.cc
+++ b/examples/cpp/sat_runner.cc
@@ -30,6 +30,8 @@
 #include "ortools/base/threadpool.h"
 #include "ortools/algorithms/sparse_permutation.h"
 #include "ortools/sat/boolean_problem.h"
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
 #include "ortools/sat/drat.h"
 #include "examples/cpp/opb_reader.h"
 #include "ortools/sat/optimization.h"
@@ -38,6 +40,7 @@
 #include "ortools/sat/sat_solver.h"
 #include "ortools/sat/simplification.h"
 #include "ortools/sat/symmetry.h"
+#include "ortools/util/file_util.h"
 #include "ortools/util/time_limit.h"
 #include "ortools/base/random.h"
 #include "ortools/base/status.h"
@@ -106,11 +109,19 @@ DEFINE_bool(presolve, true,
 DEFINE_bool(probing, false, "If true, presolve the problem using probing.");


+DEFINE_bool(use_cp_model, true,
+            "Whether to interpret a linear program input as a CpModelProto or "
+            "to read by default a CpModelProto.");
+
 DEFINE_bool(reduce_memory_usage, false,
            "If true, do not keep a copy of the original problem in memory."
            "This reduce the memory usage, but disable the solution cheking at "
            "the end.");

+DEFINE_string(
+    drat_output, "",
+    "If non-empty, a proof in DRAT format will be written to this file.");
+
 namespace operations_research {
 namespace sat {
 namespace {
@@ -126,7 +137,8 @@ double GetScaledTrivialBestBound(const LinearBooleanProblem& problem) {
  return AddOffsetAndScaleObjectiveValue(problem, best_bound);
 }

-void LoadBooleanProblem(std::string filename, LinearBooleanProblem* problem) {
+void LoadBooleanProblem(const std::string& filename, LinearBooleanProblem* problem,
+                        CpModelProto* cp_model) {
  if (strings::EndsWith(filename, ".opb") ||
      strings::EndsWith(filename, ".opb.bz2")) {
    OpbReader reader;
@@ -145,8 +157,12 @@ void LoadBooleanProblem(std::string filename, LinearBooleanProblem* problem) {
    if (!reader.Load(filename, problem)) {
      LOG(FATAL) << "Cannot load file '" << filename << "'.";
    }
+  } else if (FLAGS_use_cp_model) {
+    LOG(INFO) << "Reading a CpModelProto.";
+    *cp_model = ReadFileToProtoOrDie<CpModelProto>(filename);
  } else {
-    file::ReadFileToProtoOrDie(filename, problem);
+    LOG(INFO) << "Reading a LinearBooleanProblem.";
+    *problem = ReadFileToProtoOrDie<LinearBooleanProblem>(filename);
  }
 }

@@ -178,14 +194,20 @@ int Run() {
        << FLAGS_params;
  }

-  Model model;
-  DratWriter* drat_writer = model.GetOrCreate<DratWriter>();

  // Initialize the solver.
  std::unique_ptr<SatSolver> solver(new SatSolver());
-  solver->SetDratWriter(drat_writer);
  solver->SetParameters(parameters);

+  // Create a DratWriter?
+  std::unique_ptr<DratWriter> drat_writer;
+  if (!FLAGS_drat_output.empty()) {
+    File* output;
+    CHECK_OK(file::Open(FLAGS_drat_output, "w", &output, file::Defaults()));
+    drat_writer.reset(new DratWriter(/*in_binary_format=*/false, output));
+    solver->SetDratWriter(drat_writer.get());
+  }
+
  // The global time limit.
  std::unique_ptr<TimeLimit> time_limit(TimeLimit::FromParameters(parameters));

@@ -195,7 +217,21 @@ int Run() {

  // Read the problem.
  LinearBooleanProblem problem;
-  LoadBooleanProblem(FLAGS_input, &problem);
+  CpModelProto cp_model;
+  LoadBooleanProblem(FLAGS_input, &problem, &cp_model);
+
+  // TODO(user): clean this hack. Ideally LinearBooleanProblem should be
+  // completely replaced by the more general CpModelProto.
+  if (cp_model.variables_size() != 0) {
+    Model model;
+    model.GetOrCreate<SatSolver>()->SetParameters(parameters);
+    model.SetSingleton(std::move(time_limit));
+    LOG(INFO) << CpModelStats(cp_model);
+    const CpSolverResponse response = SolveCpModel(cp_model, &model);
+    LOG(INFO) << CpSolverResponseStats(response);
+    exit(EXIT_SUCCESS);
+  }
+
  if (FLAGS_strict_validity) {
    const util::Status status = ValidateBooleanProblem(problem);
    if (!status.ok()) {
@@ -255,7 +291,8 @@ int Run() {
    for (int i = 0; i < generators.size(); ++i) {
      propagator->AddSymmetry(std::move(generators[i]));
    }
-    solver->AddPropagator(std::move(propagator));
+    solver->AddPropagator(propagator.get());
+    solver->TakePropagatorOwnership(std::move(propagator));
  }

  // Optimize?
@@ -292,7 +329,7 @@ int Run() {
    parameters.set_log_search_progress(true);
    solver->SetParameters(parameters);
    if (FLAGS_presolve) {
-      result = SolveWithPresolve(&solver, &solution, drat_writer);
+      result = SolveWithPresolve(&solver, &solution, drat_writer.get());
      if (result == SatSolver::MODEL_SAT) {
        CHECK(IsAssignmentValid(problem, solution));
      }
--- a/examples/cpp/solve.cc
+++ b/examples/cpp/solve.cc
@@ -45,8 +45,8 @@ DEFINE_string(params_file, "",
              "If this flag is set, the --params flag is ignored.");
 DEFINE_string(params, "", "Solver specific parameters");
 DEFINE_int64(time_limit_ms, 0,
-             "If stricitly positive, specifies a limit in ms on the solving"
-             " time.");
+             "If strictly positive, specifies a limit in ms on the solving "
+             "time. Otherwise, no time limit will be imposed.");
 DEFINE_string(forced_mps_format, "",
              "Set to force the mps format to use: free, fixed");

--- a/makefiles/Makefile.archive.mk
+++ b/makefiles/Makefile.archive.mk
@@ -35,6 +35,7 @@ create_dirs:
 	$(MKDIR) temp$S$(INSTALL_DIR)$Sinclude$Sortools$Sgoogle
 	$(MKDIR) temp$S$(INSTALL_DIR)$Sinclude$Sortools$Sgraph
 	$(MKDIR) temp$S$(INSTALL_DIR)$Sinclude$Sortools$Slinear_solver
+	$(MKDIR) temp$S$(INSTALL_DIR)$Sinclude$Sortools$Slp_data
 	$(MKDIR) temp$S$(INSTALL_DIR)$Sinclude$Sortools$Ssat
 	$(MKDIR) temp$S$(INSTALL_DIR)$Sinclude$Sortools$Sutil
 	$(MKDIR) temp$S$(INSTALL_DIR)$Sexamples
@@ -84,6 +85,7 @@ cc_archive: cc
 	$(COPY) ortools$Sgraph$S*.h temp$S$(INSTALL_DIR)$Sinclude$Sortools$Sgraph
 	$(COPY) ortools$Sgen$Sortools$Sgraph$S*.h temp$S$(INSTALL_DIR)$Sinclude$Sortools$Sgraph
 	$(COPY) ortools$Slinear_solver$S*.h temp$S$(INSTALL_DIR)$Sinclude$Sortools$Slinear_solver
+	$(COPY) ortools$Slp_data$S*.h temp$S$(INSTALL_DIR)$Sinclude$Sortools$Slp_data
 	$(COPY) ortools$Sgen$Sortools$Slinear_solver$S*.pb.h temp$S$(INSTALL_DIR)$Sinclude$Sortools$Slinear_solver
 	$(COPY) ortools$Ssat$S*.h temp$S$(INSTALL_DIR)$Sinclude$Sortools$Ssat
 	$(COPY) ortools$Sgen$Sortools$Ssat$S*.pb.h temp$S$(INSTALL_DIR)$Sinclude$Sortools$Ssat
--- a/makefiles/Makefile.cpp.mk
+++ b/makefiles/Makefile.cpp.mk
@@ -102,7 +102,6 @@ FLATZINC_DEPS = \
 	$(SRC_DIR)/ortools/flatzinc/presolve.h \
 	$(SRC_DIR)/ortools/flatzinc/reporting.h \
 	$(SRC_DIR)/ortools/flatzinc/sat_constraint.h \
-	$(SRC_DIR)/ortools/flatzinc/sat_fz_solver.h \
 	$(SRC_DIR)/ortools/flatzinc/solver_data.h \
 	$(SRC_DIR)/ortools/flatzinc/solver.h \
 	$(SRC_DIR)/ortools/flatzinc/solver_util.h \
@@ -206,7 +205,6 @@ FLATZINC_OBJS=\
 	$(OBJ_DIR)/flatzinc/presolve.$O \
 	$(OBJ_DIR)/flatzinc/reporting.$O \
 	$(OBJ_DIR)/flatzinc/sat_constraint.$O \
-	$(OBJ_DIR)/flatzinc/sat_fz_solver.$O \
 	$(OBJ_DIR)/flatzinc/solver.$O \
 	$(OBJ_DIR)/flatzinc/solver_data.$O \
 	$(OBJ_DIR)/flatzinc/solver_util.$O
@@ -251,9 +249,6 @@ $(OBJ_DIR)/flatzinc/reporting.$O: $(SRC_DIR)/ortools/flatzinc/reporting.cc $(FLA
 $(OBJ_DIR)/flatzinc/sat_constraint.$O: $(SRC_DIR)/ortools/flatzinc/sat_constraint.cc $(FLATZINC_DEPS)
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sflatzinc$Ssat_constraint.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Ssat_constraint.$O

-$(OBJ_DIR)/flatzinc/sat_fz_solver.$O: $(SRC_DIR)/ortools/flatzinc/sat_fz_solver.cc $(FLATZINC_DEPS)
-	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sflatzinc$Ssat_fz_solver.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Ssat_fz_solver.$O
-
 $(OBJ_DIR)/flatzinc/solver.$O: $(SRC_DIR)/ortools/flatzinc/solver.cc $(FLATZINC_DEPS)
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sflatzinc$Ssolver.cc $(OBJ_OUT)$(OBJ_DIR)$Sflatzinc$Ssolver.$O

--- a/ortools/bop/bop_fs.cc
+++ b/ortools/bop/bop_fs.cc
@@ -105,7 +105,8 @@ BopOptimizerBase::Status GuidedSatFirstSolutionGenerator::SynchronizeIfNeeded(
      for (int i = 0; i < generators.size(); ++i) {
        propagator->AddSymmetry(std::move(generators[i]));
      }
-      sat_solver_->AddPropagator(std::move(propagator));
+      sat_solver_->AddPropagator(propagator.get());
+      sat_solver_->TakePropagatorOwnership(std::move(propagator));
    }
  }

--- a/ortools/bop/bop_portfolio.cc
+++ b/ortools/bop/bop_portfolio.cc
@@ -307,7 +307,8 @@ void PortfolioOptimizer::CreateOptimizers(
    for (int i = 0; i < generators.size(); ++i) {
      propagator->AddSymmetry(std::move(generators[i]));
    }
-    sat_propagator_.AddPropagator(std::move(propagator));
+    sat_propagator_.AddPropagator(propagator.get());
+    sat_propagator_.TakePropagatorOwnership(std::move(propagator));
  }

  const int max_num_optimizers =
--- a/ortools/flatzinc/BUILD
+++ b/ortools/flatzinc/BUILD
@@ -259,33 +259,6 @@ cc_library(
    ],
 )

-cc_library(
-    name = "sat_fz_solver",
-    srcs = ["sat_fz_solver.cc"],
-    hdrs = ["sat_fz_solver.h"],
-    deps = [
-        ":checker",
-        ":logging",
-        ":model",
-        ":solver",
-        "//ortools/base",
-        "//ortools/base:map_util",
-        "//ortools/sat:cp_constraints",
-        "//ortools/sat:cumulative",
-        "//ortools/sat:disjunctive",
-        "//ortools/sat:flow_costs",
-        "//ortools/sat:integer",
-        "//ortools/sat:integer_expr",
-        "//ortools/sat:intervals",
-        "//ortools/sat:linear_programming_constraint",
-        "//ortools/sat:model",
-        "//ortools/sat:optimization",
-        "//ortools/sat:sat_solver",
-        "//ortools/sat:table",
-        "//ortools/util:sorted_interval_list",
-    ],
-)
-
 cc_library(
    name = "cp_model_fz_solver",
    srcs = ["cp_model_fz_solver.cc"],
@@ -323,7 +296,6 @@ cc_binary(
        ":parser_lib",
        ":presolve",
        ":reporting",
-        ":sat_fz_solver",
        ":solver",
        ":solver_util",
        "//ortools/base",
--- a/ortools/flatzinc/cp_model_fz_solver.cc
+++ b/ortools/flatzinc/cp_model_fz_solver.cc
@@ -34,7 +34,7 @@
 #include "ortools/sat/sat_solver.h"
 #include "ortools/sat/table.h"

-DEFINE_string(cp_model_solver_params, "", "SatParameters as a text proto.");
+DEFINE_string(cp_sat_params, "", "SatParameters as a text proto.");

 namespace operations_research {
 namespace sat {
@@ -748,13 +748,14 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,

  // Fill the objective.
  if (fz_model.objective() != nullptr) {
-    CpObjectiveProto* objective = m.proto.add_objectives();
+    CpObjectiveProto* objective = m.proto.mutable_objective();
+    objective->add_coeffs(1);
    if (fz_model.maximize()) {
-      objective->set_objective_var(
-          NegatedCpModelVariable(m.fz_var_to_index[fz_model.objective()]));
      objective->set_scaling_factor(-1);
+      objective->add_vars(
+          NegatedCpModelVariable(m.fz_var_to_index[fz_model.objective()]));
    } else {
-      objective->set_objective_var(m.fz_var_to_index[fz_model.objective()]);
+      objective->add_vars(m.fz_var_to_index[fz_model.objective()]);
    }
  }

@@ -766,9 +767,9 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
  // The order is important, we want the flag parameters to overwrite anything
  // set in m.parameters.
  sat::SatParameters flag_parameters;
-  CHECK(google::protobuf::TextFormat::ParseFromString(FLAGS_cp_model_solver_params,
+  CHECK(google::protobuf::TextFormat::ParseFromString(FLAGS_cp_sat_params,
                                            &flag_parameters))
-      << FLAGS_cp_model_solver_params;
+      << FLAGS_cp_sat_params;
  m.parameters.MergeFrom(flag_parameters);
  sat_model.GetOrCreate<SatSolver>()->SetParameters(m.parameters);

--- a/ortools/flatzinc/fz.cc
+++ b/ortools/flatzinc/fz.cc
@@ -36,7 +36,6 @@
 #include "ortools/flatzinc/parser.h"
 #include "ortools/flatzinc/presolve.h"
 #include "ortools/flatzinc/reporting.h"
-#include "ortools/flatzinc/sat_fz_solver.h"
 #include "ortools/flatzinc/solver.h"
 #include "ortools/flatzinc/solver_util.h"

@@ -66,15 +65,13 @@ DEFINE_bool(
    verbose_impact, false,
    "Increase verbosity of the impact based search when used in free search.");
 DEFINE_bool(verbose_mt, false, "Verbose Multi-Thread.");
-DEFINE_bool(use_fz_sat, false, "Use the SAT/CP solver.");
-DEFINE_bool(use_cp_model, false, "Use the SAT/CP solver through CpModel.");
+DEFINE_bool(use_cp_sat, false, "Use the CP/SAT solver.");
 DEFINE_string(fz_model_name, "stdin",
              "Define problem name when reading from stdin.");

 // TODO(user): Remove when using ABCL in open-source.
 DECLARE_bool(log_prefix);
 DECLARE_bool(fz_use_sat);
-DECLARE_bool(vmodule);

 using operations_research::ThreadPool;

@@ -328,17 +325,11 @@ int main(int argc, char** argv) {
      operations_research::fz::ParseFlatzincModel(input,
                                                  !FLAGS_read_from_stdin);

-  if (FLAGS_use_fz_sat || FLAGS_use_cp_model) {
+  if (FLAGS_use_cp_sat) {
    bool interrupt_solve = false;
-    if (FLAGS_use_fz_sat) {
-      operations_research::sat::SolveWithSat(
-          model, operations_research::fz::SingleThreadParameters(),
-          &interrupt_solve);
-    } else {
-      operations_research::sat::SolveFzWithCpModelProto(
-          model, operations_research::fz::SingleThreadParameters(),
-          &interrupt_solve);
-    }
+    operations_research::sat::SolveFzWithCpModelProto(
+        model, operations_research::fz::SingleThreadParameters(),
+        &interrupt_solve);
  } else {
    operations_research::fz::Solve(model);
  }
--- a/ortools/flatzinc/sat_fz_solver.cc
+++ b/ortools/flatzinc/sat_fz_solver.cc
--- a/ortools/flatzinc/sat_fz_solver.h
+++ b/ortools/flatzinc/sat_fz_solver.h
@@ -1,29 +0,0 @@
-// Copyright 2010-2014 Google
-// 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_FLATZINC_SAT_FZ_SOLVER_H_
-#define OR_TOOLS_FLATZINC_SAT_FZ_SOLVER_H_
-
-#include "ortools/flatzinc/model.h"
-#include "ortools/flatzinc/solver.h"
-
-namespace operations_research {
-namespace sat {
-
-void SolveWithSat(const fz::Model& model, const fz::FlatzincParameters& p,
-                  bool* interup_solve);
-
-}  // namespace sat
-}  // namespace operations_research
-
-#endif  // OR_TOOLS_FLATZINC_SAT_FZ_SOLVER_H_
--- a/ortools/lp_data/lp_data.h
+++ b/ortools/lp_data/lp_data.h
@@ -455,8 +455,9 @@ class LinearProgram {
  // Scales the problem using the given scaler.
  void Scale(SparseMatrixScaler* scaler);

-  // Scales the costs to always have a maximum cost magnitude of 1.0 and returns
-  // the used cost scaling factor.
+  // Scales the costs to always have a maximum cost magnitude of 1.0. The old
+  // cost of each variable can be retrieved by multiplying the new one with the
+  // returned factor. This also updates objective_scaling_factor().
  Fractional ScaleObjective();

  // Removes the given row indices from the LinearProgram.
--- a/ortools/sat/cp_model.proto
+++ b/ortools/sat/cp_model.proto
@@ -226,14 +226,14 @@ message ConstraintProto {
 //
 // This is in a message because decision problems don't have any objective.
 message CpObjectiveProto {
-  // Index of the variable to minimize.
-  //
-  // For a maximization problem, one can refer to the negation of the real
+  // The linear terms of the objective to minimize.
+  // For a maximization problem, one can negate all coefficients in the
  // objective and set a scaling_factor to -1.
-  int32 objective_var = 1;
+  repeated int32 vars = 1;
+  repeated int64 coeffs = 4;

  // The displayed objective is always:
-  //   scaling_factor * (Value(objective_var) + offset).
+  //   scaling_factor * (sum(coefficients[i] * objective_vars[i]) + offset).
  // This is needed to have a consistent objective after presolve or when
  // scaling a double problem to express it with integers.
  //
@@ -264,7 +264,7 @@ message DecisionStrategyProto {
  }
  VariableSelectionStrategy variable_selection_strategy = 2;

-  // Once a variable has been choosen, this enum describe what decision is taken
+  // Once a variable has been chosen, this enum describe what decision is taken
  // on its domain.
  //
  // TODO(user): extend as needed.
@@ -298,10 +298,7 @@ message CpModelProto {
  repeated ConstraintProto constraints = 3;

  // The objective to minimize. Can be empty for pure decision problems.
-  // Note that we can have more than one objective for the cases where we want
-  // to optimize them in lexicographic order, or if we want to list the Pareto
-  // optimal solutions.
-  repeated CpObjectiveProto objectives = 4;
+  CpObjectiveProto objective = 4;

  // Defines the strategy that the solver should follow when the "fixed_search"
  // parameters is set to true. Note that this strategy is also used as an
@@ -347,7 +344,7 @@ message CpSolverResponse {
  CpSolverStatus status = 1;

  // A feasible solution to the given problem. Depending on the returned status
-  // it may be optimal or just feasible. This is in one-to-one correspondance
+  // it may be optimal or just feasible. This is in one-to-one correspondence
  // with a CpModelProto::variables repeated field and list the values of all
  // the variables.
  repeated int64 solution = 2;
--- a/ortools/sat/cp_model_checker.cc
+++ b/ortools/sat/cp_model_checker.cc
@@ -149,6 +149,38 @@ std::string ValidateLinearConstraint(const CpModelProto& model,
  return "";
 }

+std::string ValidateObjective(const CpModelProto& model,
+                         const CpObjectiveProto& obj) {
+  // TODO(user): share the code with ValidateLinearConstraint().
+  if (obj.vars_size() == 1 && obj.coeffs(0) == 1) return "";
+  int64 sum_min = 0;
+  int64 sum_max = 0;
+  for (int i = 0; i < obj.vars_size(); ++i) {
+    const int ref = obj.vars(i);
+    const auto& var_proto = model.variables(PositiveRef(ref));
+    const int64 min_domain = var_proto.domain(0);
+    const int64 max_domain = var_proto.domain(var_proto.domain_size() - 1);
+    const int64 coeff = RefIsPositive(ref) ? obj.coeffs(i) : -obj.coeffs(i);
+    const int64 prod1 = CapProd(min_domain, coeff);
+    const int64 prod2 = CapProd(max_domain, coeff);
+
+    // Note that we use min/max with zero to disallow "alternative" terms and
+    // be sure that we cannot have an overflow if we do the computation in a
+    // different order.
+    sum_min = CapAdd(sum_min, std::min(0ll, std::min(prod1, prod2)));
+    sum_max = CapAdd(sum_max, std::max(0ll, std::max(prod1, prod2)));
+    for (const int64 v : {prod1, prod2, sum_min, sum_max}) {
+      // When introducing the objective variable, we use a [...] domain so we
+      // need to be more defensive here to make sure no overflow can happen in
+      // linear constraint propagator.
+      if (v == kint64max / 2 || v == kint64min / 2) {
+        return "Possible integer overflow in objective: " + obj.DebugString();
+      }
+    }
+  }
+  return "";
+}
+
 }  // namespace

 std::string ValidateCpModel(const CpModelProto& model) {
@@ -186,12 +218,14 @@ std::string ValidateCpModel(const CpModelProto& model) {
        break;
    }
  }
-  for (const CpObjectiveProto& objective : model.objectives()) {
-    const int v = objective.objective_var();
-    if (!VariableReferenceIsValid(model, v)) {
-      return StrCat("Out of bound objective variable ", v, " : ",
-                    objective.ShortDebugString());
+  if (model.has_objective()) {
+    for (const int v : model.objective().vars()) {
+      if (!VariableReferenceIsValid(model, v)) {
+        return StrCat("Out of bound objective variable ", v, " : ",
+                      model.objective().ShortDebugString());
+      }
    }
+    RETURN_IF_NOT_EMPTY(ValidateObjective(model, model.objective()));
  }

  return "";
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -167,6 +167,11 @@ struct PresolveContext {
                              : -domains[PositiveRef(ref)].Min();
  }

+  bool IsUniqueOrFixed(int ref) {
+    return var_to_constraints[PositiveRef(ref)].size() == 1 ||
+           domains[PositiveRef(ref)].IsFixed();
+  }
+
  // Regroups fixed variables with the same value.
  // TODO(user): Also regroup cte and -cte?
  void ExploitFixedDomain(int var) {
@@ -993,16 +998,18 @@ bool PresolveInterval(ConstraintProto* ct, PresolveContext* context) {

 bool PresolveElement(ConstraintProto* ct, PresolveContext* context) {
  const int index_ref = ct->element().index();
-  if (context->var_to_constraints[PositiveRef(index_ref)].size() == 1) {
-    context->UpdateRuleStats("TODO element: index not used elsewhere");
-  }
  const int target_ref = ct->element().target();
-  if (context->var_to_constraints[PositiveRef(target_ref)].size() == 1) {
-    context->UpdateRuleStats("TODO element: target not used elsewhere");
-  }
+  const bool unique_index = context->IsUniqueOrFixed(index_ref);
+  const bool unique_target = context->IsUniqueOrFixed(target_ref);

+  // TODO(user): think about this once we do have such constraint.
  if (HasEnforcementLiteral(*ct)) return false;

+  int num_vars = 0;
+  bool all_constants = true;
+  std::unordered_set<int64> constant_set;
+
+  bool all_included_in_target_domain = true;
  bool reduced_index_domain = false;
  std::vector<ClosedInterval> infered_domain;
  const std::vector<ClosedInterval> target_dom =
@@ -1018,6 +1025,17 @@ bool PresolveElement(ConstraintProto* ct, PresolveContext* context) {
            RefIsPositive(index_ref) ? i : -i);
        reduced_index_domain = true;
      } else {
+        ++num_vars;
+        if (domain.front().start == domain.back().end) {
+          constant_set.insert(domain.front().start);
+        } else {
+          all_constants = false;
+        }
+        if (IntersectionOfSortedDisjointIntervals(
+                target_dom, ComplementOfSortedDisjointIntervals(domain))
+                .empty()) {
+          all_included_in_target_domain = false;
+        }
        infered_domain = UnionOfSortedDisjointIntervals(infered_domain, domain);
      }
    }
@@ -1031,6 +1049,33 @@ bool PresolveElement(ConstraintProto* ct, PresolveContext* context) {
  if (context->domains[PositiveRef(target_ref)].IntersectWith(infered_domain)) {
    context->UpdateRuleStats("element: reduced target domain");
  }
+  if (all_constants && unique_index) {
+    // This constraint is just here to reduce the domain of the target! We can
+    // add it to the mapping_model to reconstruct the index value during
+    // postsolve and get rid of it now.
+    context->UpdateRuleStats("element: trivial target domain reduction");
+    *(context->mapping_model->add_constraints()) = *ct;
+    return RemoveConstraint(ct, context);
+  }
+  if (all_included_in_target_domain && unique_target) {
+    context->UpdateRuleStats("element: trivial index domain reduction");
+    *(context->mapping_model->add_constraints()) = *ct;
+    return RemoveConstraint(ct, context);
+  }
+
+  if (all_constants && num_vars == constant_set.size()) {
+    // TODO(user): We should be able to do something for simple mapping.
+    context->UpdateRuleStats("TODO element: one to one mapping");
+  }
+  if (unique_target) {
+    context->UpdateRuleStats("TODO element: target not used elsewhere");
+  }
+  if (context->domains[PositiveRef(index_ref)].IsFixed()) {
+    context->UpdateRuleStats("TODO element: fixed index.");
+  } else if (unique_index) {
+    context->UpdateRuleStats("TODO element: index not used elsewhere");
+  }
+
  return false;
 }

@@ -1291,8 +1336,10 @@ void PresolveCpModel(const CpModelProto& initial_model,

  // Hack for the objective so that it is never considered to appear in only one
  // constraint.
-  for (const CpObjectiveProto& obj : initial_model.objectives()) {
-    context.var_to_constraints[PositiveRef(obj.objective_var())].insert(-1);
+  if (initial_model.has_objective()) {
+    for (const int obj_var : initial_model.objective().vars()) {
+      context.var_to_constraints[PositiveRef(obj_var)].insert(-1);
+    }
  }

  while (!queue.empty() && !context.is_unsat) {
@@ -1421,6 +1468,88 @@ void PresolveCpModel(const CpModelProto& initial_model,
    return;
  }

+  // If the objective is a single variable, try to find a linear equation that
+  // "defines" it and expand the objective into its longer linear
+  // representation.
+  // TODO(user): Insert in main loop.
+  if (context.working_model->has_objective() &&
+      context.working_model->objective().vars_size() == 1) {
+    CpObjectiveProto* const mutable_objective =
+        context.working_model->mutable_objective();
+    const int initial_obj_var = mutable_objective->vars(0);
+    const int64 initial_coeff = mutable_objective->coeffs(0);
+    const double initial_offset = mutable_objective->offset();
+    // TODO(user): Expand the linear equation recursively in order to have
+    // as much term as possible? This would also enable expanding an objective
+    // with multiple terms.
+    int expanded_linear_index = -1;
+    for (int ct_index = 0; ct_index < context.working_model->constraints_size();
+         ++ct_index) {
+      const ConstraintProto& ct = context.working_model->constraints(ct_index);
+      // Skip everything that is not a linear equality constraint.
+      if (!ct.enforcement_literal().empty()) continue;
+      if (ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
+        continue;
+      }
+      if (ct.linear().domain().size() != 2) continue;
+      if (ct.linear().domain(0) != ct.linear().domain(1)) continue;
+
+      // Find out if initial_obj_var appear in this constraint.
+      bool present = false;
+      int64 objective_coeff;
+      const int num_terms = ct.linear().vars_size();
+      for (int i = 0; i < num_terms; ++i) {
+        const int ref = ct.linear().vars(i);
+        const int64 coeff = ct.linear().coeffs(i);
+        if (PositiveRef(ref) == PositiveRef(initial_obj_var)) {
+          CHECK(!present) << "Duplicate variables not supported";
+          present = true;
+          objective_coeff = ref == initial_obj_var ? coeff : -coeff;
+        }
+      }
+
+      // We use the longest equality we can find.
+      // TODO(user): Deal with objective_coeff with a magnitude greater than 1?
+      //             Accept when initial_coeff divides objective_coeff.
+      if (present && std::abs(objective_coeff) == 1 &&
+          num_terms > mutable_objective->vars_size() + 1) {
+        expanded_linear_index = ct_index;
+        mutable_objective->clear_coeffs();
+        mutable_objective->clear_vars();
+        const int64 rhs = ct.linear().domain(0);
+        if (rhs != 0) {
+          mutable_objective->set_offset(rhs * initial_coeff * objective_coeff +
+                                        initial_offset);
+        }
+        for (int i = 0; i < num_terms; ++i) {
+          const int ref = ct.linear().vars(i);
+          if (PositiveRef(ref) != PositiveRef(initial_obj_var)) {
+            mutable_objective->add_vars(ref);
+            mutable_objective->add_coeffs(
+                -1 * initial_coeff * ct.linear().coeffs(i) * objective_coeff);
+          }
+        }
+      }
+    }
+
+    if (expanded_linear_index != -1) {
+      context.UpdateRuleStats("objective: expanded single objective");
+      ConstraintProto* const ct =
+          context.working_model->mutable_constraints(expanded_linear_index);
+      // Remove the objective variable special case and make sure the new
+      // objective variables cannot be removed:
+      for (int ref : ct->linear().vars()) {
+        context.var_to_constraints[PositiveRef(ref)].insert(-1);
+      }
+      context.var_to_constraints[PositiveRef(initial_obj_var)].erase(-1);
+
+      // This function will detect that the old objective is not used
+      // elsewhere and remove it from the equation.
+      PresolveLinear(ct, &context);
+      context.UpdateConstraintVariableUsage(expanded_linear_index);
+    }
+  }
+
  // Remove all empty or affine constraints (they will be re-added later if
  // needed) in the presolved model. Note that we need to remap the interval
  // references.
@@ -1607,12 +1736,13 @@ void ApplyVariableMapping(const std::vector<int>& mapping,
    ApplyToAllLiteralIndices(f, &ct_ref);
  }

-  // Remap the objectives.
-  for (CpObjectiveProto& objective : *proto->mutable_objectives()) {
-    const int ref = objective.objective_var();
-    const int image = mapping[PositiveRef(ref)];
-    CHECK_GE(image, 0);
-    objective.set_objective_var(ref >= 0 ? image : NegatedRef(image));
+  // Remap the objective variables.
+  if (proto->has_objective()) {
+    for (int& mutable_var : *proto->mutable_objective()->mutable_vars()) {
+      const int image = mapping[PositiveRef(mutable_var)];
+      CHECK_GE(image, 0);
+      mutable_var = (mutable_var >= 0 ? image : NegatedRef(image));
+    }
  }

  // Remap the search decision heuristic.
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -70,8 +70,10 @@ VariableUsage ComputeVariableUsage(const CpModelProto& model_proto) {

  // Add the objectives and search heuristics variables that needs to be
  // referenceable as integer even if they are only used as Booleans.
-  for (const CpObjectiveProto& objective : model_proto.objectives()) {
-    references.variables.insert(objective.objective_var());
+  if (model_proto.has_objective()) {
+    for (const int obj_var : model_proto.objective().vars()) {
+      references.variables.insert(obj_var);
+    }
  }
  for (const DecisionStrategyProto& strategy : model_proto.search_strategy()) {
    for (const int var : strategy.variables()) {
@@ -124,6 +126,16 @@ class ModelWithMapping {
    return integers_[PositiveRef(i)] != kNoIntegerVariable;
  }

+  // TODO(user): This does not returns true for [0,1] Integer variable that
+  // never appear as a literal elsewhere. This is not ideal because in
+  // LoadLinearConstraint() we probably still want to create the associated
+  // Boolean and maybe not even create the [0,1] integer variable if it is not
+  // used.
+  bool IsBoolean(int i) const {
+    CHECK_LT(PositiveRef(i), booleans_.size());
+    return booleans_[PositiveRef(i)] != kNoBooleanVariable;
+  }
+
  IntegerVariable Integer(int i) const {
    CHECK_LT(PositiveRef(i), integers_.size());
    const IntegerVariable var = integers_[PositiveRef(i)];
@@ -146,7 +158,7 @@ class ModelWithMapping {
  }

  sat::Literal Literal(int i) const {
-    CHECK_LT(PositiveRef(i), integers_.size());
+    CHECK_LT(PositiveRef(i), booleans_.size());
    return sat::Literal(booleans_[PositiveRef(i)], RefIsPositive(i));
  }

@@ -215,6 +227,8 @@ class ModelWithMapping {
    return ContainsKey(ct_to_ignore_, ct);
  }

+  Model* model() const { return model_; }
+
 private:
  void ExtractEncoding(const CpModelProto& model_proto);

@@ -741,8 +755,29 @@ void LoadLinearConstraint(const ConstraintProto& ct, ModelWithMapping* m) {
    const int64 lb = ct.linear().domain(0);
    const int64 ub = ct.linear().domain(1);
    if (!HasEnforcementLiteral(ct)) {
-      if (lb != kint64min) m->Add(WeightedSumGreaterOrEqual(vars, coeffs, lb));
-      if (ub != kint64max) m->Add(WeightedSumLowerOrEqual(vars, coeffs, ub));
+      // Detect if there is only Booleans in order to use a more efficient
+      // propagator. TODO(user): we should probably also implement an
+      // half-reified version of this constraint.
+      bool all_booleans = true;
+      std::vector<LiteralWithCoeff> cst;
+      for (int i = 0; i < vars.size(); ++i) {
+        const int ref = ct.linear().vars(i);
+        if (!m->IsBoolean(ref)) {
+          all_booleans = false;
+          continue;
+        }
+        cst.push_back({m->Literal(ref), coeffs[i]});
+      }
+      if (all_booleans) {
+        m->Add(BooleanLinearConstraint(lb, ub, &cst));
+      } else {
+        if (lb != kint64min) {
+          m->Add(WeightedSumGreaterOrEqual(vars, coeffs, lb));
+        }
+        if (ub != kint64max) {
+          m->Add(WeightedSumLowerOrEqual(vars, coeffs, ub));
+        }
+      }
    } else {
      const Literal is_true = m->Literal(ct.enforcement_literal(0));
      if (lb != kint64min) {
@@ -859,8 +894,59 @@ void LoadCumulativeConstraint(const ConstraintProto& ct, ModelWithMapping* m) {
  m->Add(Cumulative(intervals, demands, capacity));
 }

+// If a variable is constant and its value appear in no other variable domains,
+// then the literal encoding the index and the one encoding the target at this
+// value are equivalent.
+void DetectEquivalencesInElementConstraint(const ConstraintProto& ct,
+                                           ModelWithMapping* m) {
+  IntegerEncoder* encoder = m->GetOrCreate<IntegerEncoder>();
+  IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
+
+  const IntegerVariable index = m->Integer(ct.element().index());
+  const IntegerVariable target = m->Integer(ct.element().target());
+  const std::vector<IntegerVariable> vars = m->Integers(ct.element().vars());
+
+  if (m->Get(IsFixed(index))) return;
+
+  std::vector<ClosedInterval> union_of_non_constant_domains;
+  std::map<IntegerValue, int> constant_to_num;
+  for (const auto literal_value : m->Add(FullyEncodeVariable(index))) {
+    const int i = literal_value.value.value();
+    if (m->Get(IsFixed(vars[i]))) {
+      const IntegerValue value(m->Get(Value(vars[i])));
+      constant_to_num[value]++;
+    } else {
+      union_of_non_constant_domains = UnionOfSortedDisjointIntervals(
+          union_of_non_constant_domains,
+          integer_trail->InitialVariableDomain(vars[i]));
+    }
+  }
+
+  // Bump the number if the constant appear in union_of_non_constant_domains.
+  for (const auto entry : constant_to_num) {
+    if (SortedDisjointIntervalsContain(union_of_non_constant_domains,
+                                       entry.first.value())) {
+      constant_to_num[entry.first]++;
+    }
+  }
+
+  // Use the literal from the index encoding to encode the target at the
+  // "unique" values.
+  for (const auto literal_value : m->Add(FullyEncodeVariable(index))) {
+    const int i = literal_value.value.value();
+    if (!m->Get(IsFixed(vars[i]))) continue;
+
+    const IntegerValue value(m->Get(Value(vars[i])));
+    if (constant_to_num[value] == 1) {
+      const Literal r = literal_value.literal;
+      encoder->AssociateToIntegerEqualValue(r, target, value);
+    }
+  }
+}
+
 // TODO(user): Be more efficient when the element().vars() are constants.
-// Ideally we should avoid creating them as integer variable...
+// Ideally we should avoid creating them as integer variable since we don't
+// use them.
 void LoadElementConstraintBounds(const ConstraintProto& ct,
                                 ModelWithMapping* m) {
  const IntegerVariable index = m->Integer(ct.element().index());
@@ -886,11 +972,17 @@ void LoadElementConstraintBounds(const ConstraintProto& ct,
    selectors.push_back(literal_value.literal);
    const Literal r = literal_value.literal;

-    // TODO(user): Be more efficient if one of the two is a constant. Or handle
-    // that directly in the model function.
    if (vars[i] == target) continue;
-    m->Add(ConditionalLowerOrEqualWithOffset(vars[i], target, 0, r));
-    m->Add(ConditionalLowerOrEqualWithOffset(target, vars[i], 0, r));
+    if (m->Get(IsFixed(target))) {
+      const int64 value = m->Get(Value(target));
+      m->Add(ImpliesInInterval(r, vars[i], value, value));
+    } else if (m->Get(IsFixed(vars[i]))) {
+      const int64 value = m->Get(Value(vars[i]));
+      m->Add(ImpliesInInterval(r, target, value, value));
+    } else {
+      m->Add(ConditionalLowerOrEqualWithOffset(vars[i], target, 0, r));
+      m->Add(ConditionalLowerOrEqualWithOffset(target, vars[i], 0, r));
+    }
  }
  m->Add(PartialIsOneOfVar(target, possible_vars, selectors));
 }
@@ -997,6 +1089,8 @@ void LoadElementConstraint(const ConstraintProto& ct, ModelWithMapping* m) {
        m->Get(IsFixed(variable)) || encoder->VariableIsFullyEncoded(variable);
    if (is_full) num_AC_variables++;
  }
+
+  DetectEquivalencesInElementConstraint(ct, m);
  if (target_is_AC || num_AC_variables >= num_vars - 1) {
    LoadElementConstraintAC(ct, m);
  } else {
@@ -1403,8 +1497,49 @@ void FillSolutionInResponse(const CpModelProto& model_proto,
  }
 }

+namespace {
+IntegerVariable GetOrCreateVariableEqualToSumOf(
+    Model* model, const std::vector<std::pair<IntegerVariable, int64>>& terms) {
+  if (terms.empty()) return model->Add(ConstantIntegerVariable(0));
+  if (terms.size() == 1 && terms.front().second == 1) {
+    return terms.front().first;
+  }
+  if (terms.size() == 1 && terms.front().second == -1) {
+    return NegationOf(terms.front().first);
+  }
+
+  // Create a new variable equal to the sum, with a tight domain.
+  int64 sum_min = 0;
+  int64 sum_max = 0;
+
+  for (const std::pair<IntegerVariable, int64> var_coeff : terms) {
+    const int64 min_domain = model->Get(LowerBound(var_coeff.first));
+    const int64 max_domain = model->Get(UpperBound(var_coeff.first));
+    const int64 coeff = var_coeff.second;
+    const int64 prod1 = min_domain * coeff;
+    const int64 prod2 = max_domain * coeff;
+    sum_min += std::min(prod1, prod2);
+    sum_max += std::max(prod1, prod2);
+  }
+  IntegerVariable new_var = model->Add(NewIntegerVariable(sum_min, sum_max));
+
+  // Link new variables with the linear terms.
+  std::vector<IntegerVariable> vars;
+  std::vector<int64> coeffs;
+  for (const auto& term : terms) {
+    vars.push_back(term.first);
+    coeffs.push_back(term.second);
+  }
+  vars.push_back(new_var);
+  coeffs.push_back(-1);
+  model->Add(FixedWeightedSum(vars, coeffs, 0));
+  return new_var;
+}
+}  // namespace
+
 // Adds one LinearProgrammingConstraint per connected component of the model.
-void AddLPConstraints(const CpModelProto& model_proto, ModelWithMapping* m) {
+IntegerVariable AddLPConstraints(const CpModelProto& model_proto,
+                                 ModelWithMapping* m) {
  const int num_constraints = model_proto.constraints().size();
  const int num_variables = model_proto.variables().size();

@@ -1457,15 +1592,17 @@ void AddLPConstraints(const CpModelProto& model_proto, ModelWithMapping* m) {

  // Dispatch every constraint to its LinearProgrammingConstraint.
  std::unordered_map<int, LinearProgrammingConstraint*> representative_to_lp_constraint;
+  std::unordered_map<int, std::vector<std::pair<IntegerVariable, int64>>>
+      representative_to_cp_terms;
+  std::vector<std::pair<IntegerVariable, int64>> top_level_cp_terms;
  std::vector<LinearProgrammingConstraint*> lp_constraints;
-  IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
  for (int i = 0; i < num_constraints; i++) {
    if (constraint_has_lp_representation[i]) {
      const auto& ct = model_proto.constraints(i);
      const int id = components.GetClassRepresentative(i);
      if (components_to_size[id] <= 1) continue;
      if (!ContainsKey(representative_to_lp_constraint, id)) {
-        auto* lp = new LinearProgrammingConstraint(integer_trail);
+        auto* lp = m->model()->Create<LinearProgrammingConstraint>();
        representative_to_lp_constraint[id] = lp;
        lp_constraints.push_back(lp);
      }
@@ -1474,25 +1611,56 @@ void AddLPConstraints(const CpModelProto& model_proto, ModelWithMapping* m) {
  }

  // Add the objective.
-  if (model_proto.objectives_size() != 0) {
-    const int var = model_proto.objectives(0).objective_var();
-    const int id = components.GetClassRepresentative(get_var_index(var));
-    if (ContainsKey(representative_to_lp_constraint, id)) {
-      representative_to_lp_constraint[id]->SetObjective(m->Integer(var), true);
+  int num_components_containing_objective = 0;
+  if (model_proto.has_objective()) {
+    // First pass: set objective coefficients on the lp constraints, and store
+    // the cp terms in one vector per component.
+    for (int i = 0; i < model_proto.objective().coeffs_size(); ++i) {
+      const int var = model_proto.objective().vars(i);
+      const IntegerVariable cp_var = m->Integer(var);
+      const int64 coeff = model_proto.objective().coeffs(i);
+      const int id = components.GetClassRepresentative(get_var_index(var));
+      if (ContainsKey(representative_to_lp_constraint, id)) {
+        representative_to_lp_constraint[id]->SetObjectiveCoefficient(cp_var,
+                                                                     coeff);
+        representative_to_cp_terms[id].push_back(std::make_pair(cp_var, coeff));
+      } else {
+        // Component is too small. We still need to store the objective term.
+        top_level_cp_terms.push_back(std::make_pair(cp_var, coeff));
+      }
+    }
+    // Second pass: Build the cp sub-objectives per component.
+    for (const auto& it : representative_to_cp_terms) {
+      const int id = it.first;
+      LinearProgrammingConstraint* lp =
+          FindOrDie(representative_to_lp_constraint, id);
+      const std::vector<std::pair<IntegerVariable, int64>>& terms = it.second;
+      const IntegerVariable sub_obj_var =
+          GetOrCreateVariableEqualToSumOf(m->model(), terms);
+      top_level_cp_terms.push_back(std::make_pair(sub_obj_var, 1));
+      lp->SetMainObjectiveVariable(sub_obj_var);
+      num_components_containing_objective++;
    }
  }

-  // Register LP constraints and transfer their ownership to the CP model.
+  const IntegerVariable main_objective_var =
+      GetOrCreateVariableEqualToSumOf(m->model(), top_level_cp_terms);
+
+  // Register LP constraints. Note that this needs to be done after all the
+  // constraints have been added.
  for (auto* lp_constraint : lp_constraints) {
-    m->TakeOwnership(lp_constraint);
    lp_constraint->RegisterWith(m->GetOrCreate<GenericLiteralWatcher>());
  }

  VLOG_IF(1, !lp_constraints.empty())
      << "Added " << lp_constraints.size() << " LP constraints.";
+  VLOG_IF(1, num_components_containing_objective > 1)
+      << "Objective split into " << num_components_containing_objective
+      << " components";
+  return main_objective_var;
 }

-// The function responsible for implementing the choosen search strategy.
+// The function responsible for implementing the chosen search strategy.
 //
 // TODO(user): expose and unit-test, it seems easy to get the order wrong, and
 // that would not change the correctness.
@@ -1590,69 +1758,22 @@ const std::function<LiteralIndex()> ConstructSearchStrategy(
  };
 }

-// TODO(user): Also consider linear inequality where the objective is minimized
-// in the good direction.
 void ExtractLinearObjective(const CpModelProto& model_proto,
                            ModelWithMapping* m,
                            std::vector<IntegerVariable>* linear_vars,
                            std::vector<IntegerValue>* linear_coeffs) {
-  CHECK(!model_proto.objectives().empty());
-  const CpObjectiveProto obj = model_proto.objectives(0);
-  const IntegerVariable objective_var = m->Integer(obj.objective_var());
-
-  // Default linear objective if we don't find any linear equality defining it.
-  *linear_vars = {objective_var};
-  *linear_coeffs = {IntegerValue(1)};
-
-  // TODO(user): Expand the linear equation recursively in order to have
-  // as much term as possible?
-  for (const ConstraintProto& ct : model_proto.constraints()) {
-    // Skip everything that is not a linear equality constraint.
-    if (!ct.enforcement_literal().empty()) continue;
-    if (ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
-      continue;
-    }
-    if (ct.linear().domain().size() != 2) continue;
-    if (ct.linear().domain(0) != ct.linear().domain(1)) continue;
-
-    // Find out if objective_var appear in this constraint.
-    bool present = false;
-    int64 objective_coeff;
-    const int num_terms = ct.linear().vars_size();
-    for (int i = 0; i < num_terms; ++i) {
-      const int ref = ct.linear().vars(i);
-      const int64 coeff = ct.linear().coeffs(i);
-      if (PositiveRef(ref) == PositiveRef(obj.objective_var())) {
-        CHECK(!present) << "Duplicate variables not supported";
-        present = true;
-        objective_coeff = (ref == obj.objective_var()) ? coeff : -coeff;
-      }
-    }
-
-    // We use the longest equality we can find.
-    // TODO(user): Deal with objective_coeff with a magnitude greater than 1?
-    if (present && std::abs(objective_coeff) == 1 &&
-        num_terms > linear_vars->size() + 1) {
-      linear_vars->clear();
-      linear_coeffs->clear();
-      const int64 rhs = ct.linear().domain(0);
-      if (rhs != 0) {
-        linear_vars->push_back(m->Add(NewIntegerVariable(rhs, rhs)));
-        linear_coeffs->push_back(IntegerValue(objective_coeff == 1 ? 1 : -1));
-      }
-      for (int i = 0; i < num_terms; ++i) {
-        const int ref = ct.linear().vars(i);
-        if (PositiveRef(ref) != PositiveRef(obj.objective_var())) {
-          linear_vars->push_back(m->Integer(ref));
-          const IntegerValue coeff(ct.linear().coeffs(i));
-          linear_coeffs->push_back(objective_coeff == 1 ? -coeff : coeff);
-        }
-      }
-    }
+  CHECK(model_proto.has_objective());
+  const CpObjectiveProto& obj = model_proto.objective();
+  linear_vars->reserve(obj.vars_size());
+  linear_coeffs->reserve(obj.vars_size());
+  for (int i = 0; i < obj.vars_size(); ++i) {
+    linear_vars->push_back(m->Integer(obj.vars(i)));
+    linear_coeffs->push_back(IntegerValue(obj.coeffs(i)));
  }
 }

 CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
+                                      bool display_fixing_constraints,
                                      Model* model) {
  // Timing.
  WallTimer wall_timer;
@@ -1667,7 +1788,7 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
  // We will add them all at once after model_proto is loaded.
  model->GetOrCreate<IntegerEncoder>()->DisableImplicationBetweenLiteral();

-  // Instanciate all the needed variables.
+  // Instantiate all the needed variables.
  const VariableUsage usage = ComputeVariableUsage(model_proto);
  ModelWithMapping m(model_proto, usage, model);

@@ -1698,10 +1819,10 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
    }

    // We propagate after each new Boolean constraint but not the integer
-    // ones. So we call Propagate() manually here. TODO(user): Do that
-    // automatically?
+    // ones. So we call Propagate() manually here.
+    // TODO(user): Do that automatically?
    model->GetOrCreate<SatSolver>()->Propagate();
-    if (trail->Index() > old_num_fixed) {
+    if (display_fixing_constraints && trail->Index() > old_num_fixed) {
      VLOG(1) << "Constraint fixed " << trail->Index() - old_num_fixed
              << " Boolean variable(s): " << ct.DebugString();
    }
@@ -1723,9 +1844,21 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
    return response;
  }

-  // Linearize some part of the problem and register LP constraint(s).
+  // Create an objective variable and its associated linear constraint if
+  // needed.
+  IntegerVariable objective_var = kNoIntegerVariable;
+
  if (parameters.use_global_lp_constraint()) {
-    AddLPConstraints(model_proto, &m);
+    // Linearize some part of the problem and register LP constraint(s).
+    objective_var = AddLPConstraints(model_proto, &m);
+  } else if (model_proto.has_objective()) {
+    const CpObjectiveProto& obj = model_proto.objective();
+    std::vector<std::pair<IntegerVariable, int64>> terms;
+    terms.reserve(obj.vars_size());
+    for (int i = 0; i < obj.vars_size(); ++i) {
+      terms.push_back(std::make_pair(m.Integer(obj.vars(i)), obj.coeffs(i)));
+    }
+    objective_var = GetOrCreateVariableEqualToSumOf(m.model(), terms);
  }

  model->GetOrCreate<IntegerEncoder>()
@@ -1736,11 +1869,10 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
  if (model_proto.search_strategy().empty()) {
    std::vector<IntegerVariable> decisions;
    for (const int i : usage.integers) {
-      if (!model_proto.objectives().empty()) {
+      if (model_proto.has_objective()) {
        // Make sure we try to fix the objective to its lowest value first.
-        const int obj = model_proto.objectives(0).objective_var();
-        if (PositiveRef(i) == PositiveRef(obj)) {
-          decisions.push_back(m.Integer(obj));
+        if (m.Integer(i) == NegationOf(objective_var)) {
+          decisions.push_back(objective_var);
          continue;
        }
      }
@@ -1773,7 +1905,7 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
  // Solve.
  int num_solutions = 0;
  SatSolver::Status status;
-  if (model_proto.objectives_size() == 0) {
+  if (!model_proto.has_objective()) {
    status = SolveIntegerProblemWithLazyEncoding(
        /*assumptions=*/{}, next_decision, model);
    if (status == SatSolver::MODEL_SAT) {
@@ -1781,9 +1913,7 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
    }
  } else {
    // Optimization problem.
-    CHECK_EQ(model_proto.objectives_size(), 1);
-    const CpObjectiveProto obj = model_proto.objectives(0);
-    const IntegerVariable objective_var = m.Integer(obj.objective_var());
+    const CpObjectiveProto& obj = model_proto.objective();
    const auto solution_observer =
        [&model_proto, &response, &num_solutions, &obj, &m,
         objective_var](const Model& sat_model) {
@@ -1800,15 +1930,19 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
      std::vector<IntegerVariable> linear_vars;
      std::vector<IntegerValue> linear_coeffs;
      ExtractLinearObjective(model_proto, &m, &linear_vars, &linear_coeffs);
+#if defined(USE_CBC) || defined(USE_SCIPe)
      if (parameters.optimize_with_max_hs()) {
        status = MinimizeWithHittingSetAndLazyEncoding(
            VLOG_IS_ON(1), objective_var, linear_vars, linear_coeffs,
            next_decision, solution_observer, model);
      } else {
+#endif  //  defined(USE_CBC) || defined(USE_SCIPe)
        status = MinimizeWithCoreAndLazyEncoding(
            VLOG_IS_ON(1), objective_var, linear_vars, linear_coeffs,
            next_decision, solution_observer, model);
+#if defined(USE_CBC) || defined(USE_SCIPe)
      }
+#endif  //  defined(USE_CBC) || defined(USE_SCIPe)
    } else {
      status = MinimizeIntegerVariableWithLinearScanAndLazyEncoding(
          /*log_info=*/false, objective_var, next_decision, solution_observer,
@@ -1837,7 +1971,7 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto,
      break;
    }
    case SatSolver::MODEL_SAT: {
-      response.set_status(model_proto.objectives_size() != 0
+      response.set_status(model_proto.has_objective()
                              ? CpSolverStatus::OPTIMAL
                              : CpSolverStatus::MODEL_SAT);
      break;
@@ -1880,7 +2014,7 @@ CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto,
      return response;
    }
  }
-  return SolveCpModelInternal(model_proto, model);
+  return SolveCpModelInternal(model_proto, true, model);
 }

 CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
@@ -1905,7 +2039,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
  VLOG(1) << CpModelStats(presolved_proto);

  CpSolverResponse response =
-      SolveCpModelWithoutPresolve(presolved_proto, model);
+      SolveCpModelInternal(presolved_proto, true, model);
  if (response.status() != CpSolverStatus::MODEL_SAT &&
      response.status() != CpSolverStatus::OPTIMAL) {
    return response;
@@ -1937,7 +2071,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
    postsolve_model.Add(operations_research::sat::NewSatParameters(params));
  }
  const CpSolverResponse postsolve_response =
-      SolveCpModelInternal(mapping_proto, &postsolve_model);
+      SolveCpModelInternal(mapping_proto, false, &postsolve_model);
  CHECK_EQ(postsolve_response.status(), CpSolverStatus::MODEL_SAT);
  response.clear_solution();
  response.clear_solution_lower_bounds();
--- a/ortools/sat/drat.cc
+++ b/ortools/sat/drat.cc
@@ -13,13 +13,8 @@

 #include "ortools/sat/drat.h"

-#include "ortools/base/commandlineflags.h"
 #include "ortools/base/stringprintf.h"

-DEFINE_string(
-    drat_output, "",
-    "If non-empty, a proof in DRAT format will be written to this file.");
-
 namespace operations_research {
 namespace sat {

@@ -30,16 +25,6 @@ DratWriter::~DratWriter() {
  }
 }

-// static
-DratWriter* DratWriter::CreateInModel(Model* model) {
-  if (FLAGS_drat_output.empty()) return nullptr;
-  File* output;
-  CHECK_OK(file::Open(FLAGS_drat_output, "w", &output, file::Defaults()));
-  DratWriter* drat_writer = new DratWriter(/*in_binary_format=*/false, output);
-  model->TakeOwnership(drat_writer);
-  return drat_writer;
-}
-
 void DratWriter::ApplyMapping(
    const ITIVector<BooleanVariable, BooleanVariable>& mapping) {
  ITIVector<BooleanVariable, BooleanVariable> new_mapping;
--- a/ortools/sat/drat.h
+++ b/ortools/sat/drat.h
@@ -35,10 +35,6 @@ class DratWriter {
        output_(output) {}
  ~DratWriter();

-  // This tries to open the FLAGS_drat_file file and if it succeed it will
-  // return a non-nullptr DratWriter class.
-  static DratWriter* CreateInModel(Model* model);
-
  // During the presolve step, variable get deleted and the set of non-deleted
  // variable is remaped in a dense set. This allows to keep track of that and
  // always output the DRAT clauses in term of the original variables.
--- a/ortools/sat/integer.cc
+++ b/ortools/sat/integer.cc
@@ -41,14 +41,10 @@ void IntegerEncoder::FullyEncodeVariable(IntegerVariable var) {
    }
  }

-  // TODO(user): This case is annoying, so for now we want the caller to deal
-  // with it, hence the CHECK. We do not want to create a fixed Boolean
-  // variable, but we also do not want to complexify the API of
-  // FullDomainEncoding().
-  CHECK_NE(values.size(), 1);
-
  std::vector<Literal> literals;
-  if (values.size() == 2) {
+  if (values.size() == 1) {
+    literals.push_back(GetLiteralTrue());
+  } else if (values.size() == 2) {
    literals.push_back(GetOrCreateAssociatedLiteral(
        IntegerLiteral::LowerOrEqual(var, values[0])));
    literals.push_back(literals.back().Negated());
@@ -70,7 +66,12 @@ void IntegerEncoder::FullyEncodeVariableUsingGivenLiterals(
    const std::vector<IntegerValue>& values) {
  CHECK(!VariableIsFullyEncoded(var));
  CHECK(!literals.empty());
-  CHECK_NE(literals.size(), 1);
+
+  if (literals.size() == 1) {
+    full_encoding_index_[var] = full_encoding_.size();
+    full_encoding_.push_back({ValueLiteralPair(values[0], literals[0])});
+    return;
+  }

  // Sort the literals by values.
  std::vector<ValueLiteralPair> encoding;
@@ -1031,11 +1032,22 @@ void IntegerTrail::EnqueueLiteral(
  trail_->Enqueue(literal, propagator_id_);
 }

-GenericLiteralWatcher::GenericLiteralWatcher(
-    IntegerTrail* integer_trail, RevRepository<int>* rev_int_repository)
+GenericLiteralWatcher::GenericLiteralWatcher(Model* model)
    : SatPropagator("GenericLiteralWatcher"),
-      integer_trail_(integer_trail),
-      rev_int_repository_(rev_int_repository) {
+      integer_trail_(model->GetOrCreate<IntegerTrail>()) {
+  // TODO(user): Have a general mecanism to register "global" reversible
+  // classes and keep them synchronized with the search.
+  std::unique_ptr<RevRepository<int>> rev_int_repository(
+      new RevRepository<int>());
+  rev_int_repository_ = rev_int_repository.get();
+  model->SetSingleton(std::move(rev_int_repository));
+
+  // TODO(user): This propagator currently needs to be last because it is the
+  // only one enforcing that a fix-point is reached on the integer variables.
+  // Figure out a better interaction between the sat propagation loop and
+  // this one.
+  model->GetOrCreate<SatSolver>()->AddLastPropagator(this);
+
  integer_trail_->RegisterWatcher(&modified_vars_);
  queue_by_priority_.resize(2);  // Because default priority is 1.
 }
--- a/ortools/sat/integer.h
+++ b/ortools/sat/integer.h
@@ -157,11 +157,7 @@ using InlinedIntegerLiteralVector = gtl::InlinedVector<IntegerLiteral, 2>;
 struct IntegerDomains
    : public ITIVector<IntegerVariable,
                       gtl::InlinedVector<ClosedInterval, 1>> {
-  static IntegerDomains* CreateInModel(Model* model) {
-    IntegerDomains* domains = new IntegerDomains();
-    model->TakeOwnership(domains);
-    return domains;
-  }
+  explicit IntegerDomains(Model* model) {}
 };

 // Each integer variable x will be associated with a set of literals encoding
@@ -184,20 +180,15 @@ struct IntegerDomains
 // though.
 class IntegerEncoder {
 public:
-  IntegerEncoder(SatSolver* sat_solver, IntegerDomains* domains)
-      : sat_solver_(sat_solver), domains_(domains), num_created_variables_(0) {}
+  explicit IntegerEncoder(Model* model)
+      : sat_solver_(model->GetOrCreate<SatSolver>()),
+        domains_(model->GetOrCreate<IntegerDomains>()),
+        num_created_variables_(0) {}

  ~IntegerEncoder() {
    VLOG(1) << "#variables created = " << num_created_variables_;
  }

-  static IntegerEncoder* CreateInModel(Model* model) {
-    IntegerEncoder* encoder = new IntegerEncoder(
-        model->GetOrCreate<SatSolver>(), model->GetOrCreate<IntegerDomains>());
-    model->TakeOwnership(encoder);
-    return encoder;
-  }
-
  // Fully encode a variable using its current initial domain.
  // This can be called only once.
  //
@@ -332,6 +323,18 @@ class IntegerEncoder {
  // Adds the implications: Literal(before) <= associated_lit <= Literal(after).
  void AddImplications(IntegerLiteral i, Literal associated_lit);

+  // Get the literal always set to true, make it if it does not exist.
+  Literal GetLiteralTrue() {
+    DCHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
+    if (literal_index_true_ == kNoLiteralIndex) {
+      const Literal literal_true =
+          Literal(sat_solver_->NewBooleanVariable(), true);
+      literal_index_true_ = literal_true.Index();
+      sat_solver_->AddUnitClause(literal_true);
+    }
+    return Literal(literal_index_true_);
+  }
+
  SatSolver* sat_solver_;
  IntegerDomains* domains_;

@@ -359,6 +362,10 @@ class IntegerEncoder {
  std::unordered_map<IntegerVariable, int> full_encoding_index_;
  std::vector<std::vector<ValueLiteralPair>> full_encoding_;

+  // A literal that is always true, convenient to encode trivial domains.
+  // This will be lazily created when needed.
+  LiteralIndex literal_index_true_ = kNoLiteralIndex;
+
  DISALLOW_COPY_AND_ASSIGN(IntegerEncoder);
 };

@@ -367,23 +374,15 @@ class IntegerEncoder {
 // to maintain the reason for each propagation.
 class IntegerTrail : public SatPropagator {
 public:
-  IntegerTrail(IntegerDomains* domains, IntegerEncoder* encoder, Trail* trail)
+  explicit IntegerTrail(Model* model)
      : SatPropagator("IntegerTrail"),
        num_enqueues_(0),
-        domains_(domains),
-        encoder_(encoder),
-        trail_(trail) {}
-  ~IntegerTrail() final {}
-
-  static IntegerTrail* CreateInModel(Model* model) {
-    IntegerDomains* domains = model->GetOrCreate<IntegerDomains>();
-    IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
-    Trail* trail = model->GetOrCreate<Trail>();
-    IntegerTrail* integer_trail = new IntegerTrail(domains, encoder, trail);
-    model->GetOrCreate<SatSolver>()->AddPropagator(
-        std::unique_ptr<IntegerTrail>(integer_trail));
-    return integer_trail;
+        domains_(model->GetOrCreate<IntegerDomains>()),
+        encoder_(model->GetOrCreate<IntegerEncoder>()),
+        trail_(model->GetOrCreate<Trail>()) {
+    model->GetOrCreate<SatSolver>()->AddPropagator(this);
  }
+  ~IntegerTrail() final {}

  // SatPropagator interface. These functions make sure the current bounds
  // information is in sync with the current solver literal trail. Any
@@ -709,28 +708,9 @@ class PropagatorInterface {
 // TODO(user): Move this to its own file. Add unit tests!
 class GenericLiteralWatcher : public SatPropagator {
 public:
-  explicit GenericLiteralWatcher(IntegerTrail* trail,
-                                 RevRepository<int>* rev_int_repository);
+  explicit GenericLiteralWatcher(Model* model);
  ~GenericLiteralWatcher() final {}

-  static GenericLiteralWatcher* CreateInModel(Model* model) {
-    // TODO(user): Have a general mecanism to register "global" reversible
-    // classes and keep them synchronized with the search.
-    std::unique_ptr<RevRepository<int>> rev_int_repository(
-        new RevRepository<int>());
-    GenericLiteralWatcher* watcher = new GenericLiteralWatcher(
-        model->GetOrCreate<IntegerTrail>(), rev_int_repository.get());
-    model->SetSingleton(std::move(rev_int_repository));
-
-    // TODO(user): This propagator currently needs to be last because it is the
-    // only one enforcing that a fix-point is reached on the integer variables.
-    // Figure out a better interaction between the sat propagation loop and
-    // this one.
-    model->GetOrCreate<SatSolver>()->AddLastPropagator(
-        std::unique_ptr<GenericLiteralWatcher>(watcher));
-    return watcher;
-  }
-
  // On propagate, the registered propagators will be called if they need to
  // until a fixed point is reached. Propagators with low ids will tend to be
  // called first, but it ultimately depends on their "waking" order.
@@ -955,12 +935,6 @@ class LiteralViews {
 public:
  explicit LiteralViews(Model* model) : model_(model) {}

-  static LiteralViews* CreateInModel(Model* model) {
-    LiteralViews* const views = new LiteralViews(model);
-    model->TakeOwnership(views);
-    return views;
-  }
-
  IntegerVariable GetIntegerView(const Literal lit) {
    const LiteralIndex index = lit.Index();

@@ -1054,13 +1028,6 @@ inline std::function<void(Model*)> Equality(IntegerVariable v, int64 value) {
  };
 }

-// Associate the given literal to the given integer inequality.
-inline std::function<void(Model*)> Equality(IntegerLiteral i, Literal l) {
-  return [=](Model* model) {
-    model->GetOrCreate<IntegerEncoder>()->AssociateToIntegerLiteral(l, i);
-  };
-}
-
 // TODO(user): This is one of the rare case where it is better to use Equality()
 // rather than two Implications(). Maybe we should modify our internal
 // implementation to use half-reified encoding? that is do not propagate the
@@ -1077,7 +1044,7 @@ inline std::function<void(Model*)> Implication(Literal l, IntegerLiteral i) {
      model->Add(ClauseConstraint({l.Negated()}));
    } else {
      // TODO(user): Double check what happen when we associate a trivially
-      // true or false literal. This applies to Equality() too.
+      // true or false literal.
      IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
      const Literal current = encoder->GetOrCreateAssociatedLiteral(i);
      model->Add(Implication(l, current));
@@ -1085,27 +1052,15 @@ inline std::function<void(Model*)> Implication(Literal l, IntegerLiteral i) {
  };
 }

-// in_interval <=> v in [lb, ub].
-inline std::function<void(Model*)> ReifiedInInterval(IntegerVariable v,
-                                                     int64 lb, int64 ub,
-                                                     Literal in_interval) {
+// in_interval => v in [lb, ub].
+inline std::function<void(Model*)> ImpliesInInterval(Literal in_interval,
+                                                     IntegerVariable v,
+                                                     int64 lb, int64 ub) {
  return [=](Model* model) {
-    IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
-    const auto lb_lit = IntegerLiteral::GreaterOrEqual(v, IntegerValue(lb));
-    const auto ub_lit = IntegerLiteral::LowerOrEqual(v, IntegerValue(ub));
-    if (lb <= model->Get(LowerBound(v))) {
-      if (ub >= model->Get(UpperBound(v))) {
-        model->GetOrCreate<SatSolver>()->AddUnitClause(in_interval);
-      } else {
-        model->Add(Equality(ub_lit, in_interval));
-      }
-    } else if (ub >= model->Get(UpperBound(v))) {
-      model->Add(Equality(lb_lit, in_interval));
-    } else {
-      const Literal is_ge_lb = encoder->GetOrCreateAssociatedLiteral(lb_lit);
-      const Literal is_le_ub = encoder->GetOrCreateAssociatedLiteral(ub_lit);
-      model->Add(ReifiedBoolAnd({is_ge_lb, is_le_ub}, in_interval));
-    }
+    model->Add(Implication(
+        in_interval, IntegerLiteral::GreaterOrEqual(v, IntegerValue(lb))));
+    model->Add(Implication(in_interval,
+                           IntegerLiteral::LowerOrEqual(v, IntegerValue(ub))));
  };
 }

--- a/ortools/sat/intervals.h
+++ b/ortools/sat/intervals.h
@@ -34,17 +34,9 @@ const IntervalVariable kNoIntervalVariable(-1);
 // provides many helper functions to add precedences relation between intervals.
 class IntervalsRepository {
 public:
-  IntervalsRepository(IntegerTrail* integer_trail,
-                      PrecedencesPropagator* precedences)
-      : integer_trail_(integer_trail), precedences_(precedences) {}
-
-  static IntervalsRepository* CreateInModel(Model* model) {
-    IntervalsRepository* intervals =
-        new IntervalsRepository(model->GetOrCreate<IntegerTrail>(),
-                                model->GetOrCreate<PrecedencesPropagator>());
-    model->TakeOwnership(intervals);
-    return intervals;
-  }
+  explicit IntervalsRepository(Model* model)
+      : integer_trail_(model->GetOrCreate<IntegerTrail>()),
+        precedences_(model->GetOrCreate<PrecedencesPropagator>()) {}

  // Returns the current number of intervals in the repository.
  // The interval will always be identified by an integer in [0, num_intervals).
--- a/ortools/sat/linear_programming_constraint.cc
+++ b/ortools/sat/linear_programming_constraint.cc
@@ -27,9 +27,16 @@ namespace sat {

 const double LinearProgrammingConstraint::kEpsilon = 1e-6;

-LinearProgrammingConstraint::LinearProgrammingConstraint(
-    IntegerTrail* integer_trail)
-    : integer_trail_(integer_trail) {
+LinearProgrammingConstraint::LinearProgrammingConstraint(Model* model)
+    : integer_trail_(model->GetOrCreate<IntegerTrail>()) {
+  // TODO(user): Find a way to make GetOrCreate<TimeLimit>() construct it by
+  // default.
+  time_limit_ = model->Mutable<TimeLimit>();
+  if (time_limit_ == nullptr) {
+    model->SetSingleton(TimeLimit::Infinite());
+    time_limit_ = model->Mutable<TimeLimit>();
+  }
+
  if (!FLAGS_lp_constraint_use_dual_ray) {
    // The violation_sum_ variable will be the sum of constraints' violation.
    violation_sum_constraint_ = lp_data_.CreateNewConstraint();
@@ -74,27 +81,27 @@ void LinearProgrammingConstraint::SetCoefficient(ConstraintIndex ct,
  lp_data_.SetCoefficient(ct, cvar, coefficient);
 }

-void LinearProgrammingConstraint::SetObjective(IntegerVariable ivar,
-                                               bool is_minimization) {
+void LinearProgrammingConstraint::SetObjectiveCoefficient(IntegerVariable ivar,
+                                                          double coeff) {
  CHECK(!lp_constraint_is_registered_);
-  CHECK(!objective_is_defined_) << "Objective was set more than once.";
  objective_is_defined_ = true;
-  objective_cp_ = ivar;
-  objective_lp_ = GetOrCreateMirrorVariable(ivar);
-  objective_is_minimization_ = is_minimization;
+  objective_lp_.push_back(
+      std::make_pair(GetOrCreateMirrorVariable(ivar), coeff));
 }

 void LinearProgrammingConstraint::RegisterWith(GenericLiteralWatcher* watcher) {
  DCHECK(!lp_constraint_is_registered_);
  lp_constraint_is_registered_ = true;

-  lp_data_.Scale(&scaler_);
-
-  // Note that we set the objective AFTER the scaling.
+  // Note that the order is important so that the lp objective is exactly
+  // lp_to_cp_objective_scale_ times the cp one.
  if (objective_is_defined_) {
-    lp_data_.SetObjectiveCoefficient(objective_lp_, 1.0);
-    lp_data_.SetMaximizationProblem(!objective_is_minimization_);
+    for (const auto& var_coeff : objective_lp_) {
+      lp_data_.SetObjectiveCoefficient(var_coeff.first, var_coeff.second);
+    }
  }
+  lp_data_.Scale(&scaler_);
+  lp_to_cp_objective_scale_ = lp_data_.ScaleObjective();

  if (!FLAGS_lp_constraint_use_dual_ray) {
    // Add all the individual violation variables. Note that it is important
@@ -175,15 +182,17 @@ bool LinearProgrammingConstraint::Propagate() {

  if (!FLAGS_lp_constraint_use_dual_ray) {
    if (objective_is_defined_) {
-      lp_data_.SetObjectiveCoefficient(objective_lp_, 0.0);
+      for (auto& var_coeff : objective_lp_) {
+        lp_data_.SetObjectiveCoefficient(var_coeff.first, 0.0);
+      }
    }
    lp_data_.SetObjectiveCoefficient(violation_sum_, 1.0);
+    lp_data_.SetObjectiveScalingFactor(1.0);
    lp_data_.SetVariableBounds(violation_sum_, 0.0,
                               std::numeric_limits<double>::infinity());
-    lp_data_.SetMaximizationProblem(false);

    // Feasibility deductions.
-    const auto status = simplex_.Solve(lp_data_, TimeLimit::Infinite().get());
+    const auto status = simplex_.Solve(lp_data_, time_limit_);
    CHECK(status.ok()) << "LinearProgrammingConstraint encountered an error: "
                       << status.error_message();
    CHECK_EQ(simplex_.GetProblemStatus(), glop::ProblemStatus::OPTIMAL)
@@ -191,14 +200,14 @@ bool LinearProgrammingConstraint::Propagate() {
        << simplex_.GetProblemStatus();

    if (simplex_.GetVariableValue(violation_sum_) > kEpsilon) {  // infeasible.
-      FillIntegerReason(1.0);
+      FillReducedCostsReason();
      return integer_trail_->ReportConflict(integer_reason_);
    }

    // Reduced cost strengthening for feasibility.
-    ReducedCostStrengtheningDeductions(1.0, 0.0);
+    ReducedCostStrengtheningDeductions(0.0);
    if (!deductions_.empty()) {
-      FillIntegerReason(1.0);
+      FillReducedCostsReason();
      for (const IntegerLiteral deduction : deductions_) {
        if (!integer_trail_->Enqueue(deduction, {}, integer_reason_)) {
          return false;
@@ -210,8 +219,12 @@ bool LinearProgrammingConstraint::Propagate() {
    lp_data_.SetVariableBounds(violation_sum_, 0.0, 0.0);
    lp_data_.SetObjectiveCoefficient(violation_sum_, 0.0);
    if (objective_is_defined_) {
-      lp_data_.SetObjectiveCoefficient(objective_lp_, 1.0);
-      lp_data_.SetMaximizationProblem(!objective_is_minimization_);
+      for (auto& var_coeff : objective_lp_) {
+        const glop::ColIndex col = var_coeff.first;
+        lp_data_.SetObjectiveCoefficient(
+            col, var_coeff.second * scaler_.col_scale(col));
+      }
+      lp_to_cp_objective_scale_ = lp_data_.ScaleObjective();
    }
    for (int i = 0; i < num_vars; i++) {
      lp_solution_[i] = GetVariableValueAtCpScale(mirror_lp_variables_[i]);
@@ -222,7 +235,7 @@ bool LinearProgrammingConstraint::Propagate() {
    return true;
  }

-  const auto status = simplex_.Solve(lp_data_, TimeLimit::Infinite().get());
+  const auto status = simplex_.Solve(lp_data_, time_limit_);
  CHECK(status.ok()) << "LinearProgrammingConstraint encountered an error: "
                     << status.error_message();

@@ -235,56 +248,31 @@ bool LinearProgrammingConstraint::Propagate() {
  // Optimality deductions if problem has an objective.
  if (objective_is_defined_ &&
      simplex_.GetProblemStatus() == glop::ProblemStatus::OPTIMAL) {
-    const double objective_cp_lb =
-        static_cast<double>(integer_trail_->LowerBound(objective_cp_).value());
-    const double objective_cp_ub =
-        static_cast<double>(integer_trail_->UpperBound(objective_cp_).value());
-
-    // Try to filter optimal objective value.
-    const double objective_value = GetVariableValueAtCpScale(objective_lp_);
-    if (objective_is_minimization_) {
-      const double new_lb = std::ceil(objective_value - kEpsilon);
-      if (objective_cp_lb < new_lb) {
-        const IntegerValue new_int_lb(static_cast<IntegerValue>(new_lb));
-        FillIntegerReason(1.0);
-        const IntegerLiteral deduction =
-            IntegerLiteral::GreaterOrEqual(objective_cp_, new_int_lb);
-        if (!integer_trail_->Enqueue(deduction, {}, integer_reason_)) {
-          return false;
-        }
-      }
-    } else {
-      const double new_ub = std::floor(objective_value + kEpsilon);
-      if (objective_cp_ub > new_ub) {
-        const IntegerValue new_int_ub(static_cast<IntegerValue>(new_ub));
-        FillIntegerReason(-1.0);
-        const IntegerLiteral deduction =
-            IntegerLiteral::LowerOrEqual(objective_cp_, new_int_ub);
-        if (!integer_trail_->Enqueue(deduction, {}, integer_reason_)) {
-          return false;
-        }
+    // Try to filter optimal objective value. Note that GetObjectiveValue()
+    // already take care of the scaling so that it returns an objective in the
+    // CP world.
+    const double relaxed_optimal_objective = simplex_.GetObjectiveValue();
+    const IntegerValue old_lb = integer_trail_->LowerBound(objective_cp_);
+    const IntegerValue new_lb(
+        static_cast<int64>(std::ceil(relaxed_optimal_objective - kEpsilon)));
+    if (old_lb < new_lb) {
+      FillReducedCostsReason();
+      const IntegerLiteral deduction =
+          IntegerLiteral::GreaterOrEqual(objective_cp_, new_lb);
+      if (!integer_trail_->Enqueue(deduction, {}, integer_reason_)) {
+        return false;
      }
    }

    // Reduced cost strengthening.
-    const double objective_slack = objective_is_minimization_
-                                       ? objective_cp_ub - objective_value
-                                       : objective_value - objective_cp_lb;
-    const double objective_direction = objective_is_minimization_ ? 1.0 : -1.0;
-    ReducedCostStrengtheningDeductions(
-        objective_direction,
-        objective_slack * scaler_.col_scale(objective_lp_));
-
+    const double objective_cp_ub =
+        static_cast<double>(integer_trail_->UpperBound(objective_cp_).value());
+    ReducedCostStrengtheningDeductions(objective_cp_ub -
+                                       relaxed_optimal_objective);
    if (!deductions_.empty()) {
-      FillIntegerReason(objective_direction);
-
-      // Add the opposite bound of the variable used for strengthening.
-      const IntegerLiteral opposite_bound =
-          objective_is_minimization_
-              ? integer_trail_->UpperBoundAsLiteral(objective_cp_)
-              : integer_trail_->LowerBoundAsLiteral(objective_cp_);
-      integer_reason_.push_back(opposite_bound);
-
+      FillReducedCostsReason();
+      integer_reason_.push_back(
+          integer_trail_->UpperBoundAsLiteral(objective_cp_));
      for (const IntegerLiteral deduction : deductions_) {
        if (!integer_trail_->Enqueue(deduction, {}, integer_reason_)) {
          return false;
@@ -301,9 +289,8 @@ bool LinearProgrammingConstraint::Propagate() {
  return true;
 }

-void LinearProgrammingConstraint::FillIntegerReason(double direction) {
+void LinearProgrammingConstraint::FillReducedCostsReason() {
  integer_reason_.clear();
-
  const int num_vars = integer_variables_.size();
  for (int i = 0; i < num_vars; i++) {
    // TODO(user): try to extend the bounds that are put in the
@@ -312,8 +299,7 @@ void LinearProgrammingConstraint::FillIntegerReason(double direction) {
    // feasible? If the violation minimum is 10 and a variable has rc 1,
    // then decreasing it by 9 would still leave the problem infeasible.
    // Using this could allow to generalize some explanations.
-    const double rc =
-        simplex_.GetReducedCost(mirror_lp_variables_[i]) * direction;
+    const double rc = simplex_.GetReducedCost(mirror_lp_variables_[i]);
    if (rc > kEpsilon) {
      integer_reason_.push_back(
          integer_trail_->LowerBoundAsLiteral(integer_variables_[i]));
@@ -326,10 +312,9 @@ void LinearProgrammingConstraint::FillIntegerReason(double direction) {

 void LinearProgrammingConstraint::FillDualRayReason() {
  integer_reason_.clear();
-
  const int num_vars = integer_variables_.size();
  for (int i = 0; i < num_vars; i++) {
-    // TODO(user): Like for FillIntegerReason(), the bounds could be
+    // TODO(user): Like for FillReducedCostsReason(), the bounds could be
    // extended here. Actually, the "dual ray cost updates" is the reduced cost
    // of an optimal solution if we were optimizing one direction of one basic
    // variable. The simplex_ interface would need to be slightly extended to
@@ -347,14 +332,19 @@ void LinearProgrammingConstraint::FillDualRayReason() {
 }

 void LinearProgrammingConstraint::ReducedCostStrengtheningDeductions(
-    double direction, double lp_objective_delta) {
+    double cp_objective_delta) {
  deductions_.clear();

+  // TRICKY: while simplex_.GetObjectiveValue() use the objective scaling factor
+  // stored in the lp_data_, all the other functions like GetReducedCost() or
+  // GetVariableValue() do not.
+  const double lp_objective_delta =
+      cp_objective_delta / lp_to_cp_objective_scale_;
  const int num_vars = integer_variables_.size();
  for (int i = 0; i < num_vars; i++) {
    const IntegerVariable cp_var = integer_variables_[i];
    const glop::ColIndex lp_var = mirror_lp_variables_[i];
-    const double rc = simplex_.GetReducedCost(lp_var) * direction;
+    const double rc = simplex_.GetReducedCost(lp_var);
    const double value = simplex_.GetVariableValue(lp_var);
    const double lp_other_bound = value + lp_objective_delta / rc;
    const double cp_other_bound = lp_other_bound / scaler_.col_scale(lp_var);
--- a/ortools/sat/linear_programming_constraint.h
+++ b/ortools/sat/linear_programming_constraint.h
@@ -22,6 +22,7 @@
 #include "ortools/sat/integer.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
+#include "ortools/util/time_limit.h"

 namespace operations_research {
 namespace sat {
@@ -62,34 +63,25 @@ class LinearProgrammingConstraint : public PropagatorInterface {
 public:
  typedef glop::RowIndex ConstraintIndex;

-  explicit LinearProgrammingConstraint(IntegerTrail* integer_trail);
-
-  // Creates a LinearProgrammingConstraint for templated GetOrCreate idiom.
-  static LinearProgrammingConstraint* CreateInModel(Model* model) {
-    IntegerTrail* trail = model->GetOrCreate<IntegerTrail>();
-    LinearProgrammingConstraint* constraint =
-        new LinearProgrammingConstraint(trail);
-    model->TakeOwnership(constraint);
-    return constraint;
-  }
+  explicit LinearProgrammingConstraint(Model* model);

  // User API, see header description.
  ConstraintIndex CreateNewConstraint(double lb, double ub);

-  void SetCoefficient(ConstraintIndex ct, IntegerVariable ivar,
-                      double coefficient);
-
  // TODO(user): Allow Literals to appear in linear constraints.
  // TODO(user): Calling SetCoefficient() twice on the same
  // (constraint, variable) pair will overwrite coefficients where accumulating
  // them might be desired, this is a common mistake, change API.
+  void SetCoefficient(ConstraintIndex ct, IntegerVariable ivar,
+                      double coefficient);

-  // Objective may or may not be defined. It can be defined only once,
-  // must be exactly one IntegerVariable, and can be either
-  // minimized (is_minimization = true) or maximized (is_minimization = false).
-  // TODO(user): change API for always minimization, so that
-  // maximization(var) = minimization(Negation(var)).
-  void SetObjective(IntegerVariable ivar, bool is_minimization);
+  // Set the coefficient of the variable in the objective. Calling it twice will
+  // overwrite the previous value.
+  void SetObjectiveCoefficient(IntegerVariable ivar, double coeff);
+
+  // The main objective variable should be equal to the linear sum of
+  // the arguments passed to SetObjectiveCoefficient().
+  void SetMainObjectiveVariable(IntegerVariable ivar) { objective_cp_ = ivar; }

  // PropagatorInterface API.
  bool Propagate() override;
@@ -101,22 +93,18 @@ class LinearProgrammingConstraint : public PropagatorInterface {
 private:
  // Generates a set of IntegerLiterals explaining why the best solution can not
  // be improved using reduced costs. This is used to generate explanations for
-  // both infeasibility and bounds deductions. The direction variable should be
-  // 1.0 if the last Solve() was a minimization, -1.0 if it was a maximization.
-  void FillIntegerReason(double direction);
+  // both infeasibility and bounds deductions.
+  void FillReducedCostsReason();

-  // Same as FillIntegerReason() but for the case of a DUAL_UNBOUNDED problem.
-  // This exploit the dual ray as a reason for the primal infeasiblity.
+  // Same as FillReducedCostReason() but for the case of a DUAL_UNBOUNDED
+  // problem. This exploit the dual ray as a reason for the primal infeasiblity.
  void FillDualRayReason();

  // Fills the deductions vector with reduced cost deductions that can be made
-  // from the current state of the LP solver. This should be called after
-  // Solve(): if the optimization was a minimization, the direction variable
-  // should be 1.0 and lp_objective_delta the objective's upper bound minus the
-  // optimal; if the optimization was a maximization, direction should be -1.0
-  // and lp_objective_delta the optimal minus the objective's lower bound.
-  void ReducedCostStrengtheningDeductions(double direction,
-                                          double lp_objective_delta);
+  // from the current state of the LP solver. The given delta should be the
+  // difference between the cp objective upper bound and lower bound given by
+  // the lp.
+  void ReducedCostStrengtheningDeductions(double cp_objective_delta);

  // Gets or creates an LP variable that mirrors a CP variable.
  // TODO(user): only accept positive variables to prevent having different
@@ -135,6 +123,7 @@ class LinearProgrammingConstraint : public PropagatorInterface {

  // For the scaling.
  glop::SparseMatrixScaler scaler_;
+  glop::Fractional lp_to_cp_objective_scale_;

  // violation_sum_ is used to simulate phase I of the simplex and be able to
  // do reduced cost strengthening on problem feasibility by using the sum of
@@ -155,8 +144,7 @@ class LinearProgrammingConstraint : public PropagatorInterface {
  // then we will switch the objective between feasibility and optimization.
  bool objective_is_defined_ = false;
  IntegerVariable objective_cp_;
-  glop::ColIndex objective_lp_;
-  bool objective_is_minimization_;
+  std::vector<std::pair<glop::ColIndex, double>> objective_lp_;

  // Structures for propagators.
  IntegerTrail* integer_trail_;
@@ -170,6 +158,9 @@ class LinearProgrammingConstraint : public PropagatorInterface {

  // Linear constraints cannot be created or modified after this is registered.
  bool lp_constraint_is_registered_ = false;
+
+  // Time limit (shared with, owned by the sat solver).
+  TimeLimit* time_limit_;
 };

 }  // namespace sat
--- a/ortools/sat/lp_utils.cc
+++ b/ortools/sat/lp_utils.cc
@@ -205,44 +205,21 @@ bool ConvertMPModelProtoToCpModelProto(const MPModelProto& mp_model,
    // Note that here we set the scaling factor for the inverse operation of
    // getting the "true" objective value from the scaled one. Hence the
    // inverse.
-    auto* objective = cp_model->add_objectives();
-    objective->set_offset(mp_model.objective_offset() * scaling_factor / gcd);
-    objective->set_scaling_factor(1.0 / scaling_factor * gcd);
-    objective->set_objective_var(cp_model->variables_size());
-    {
-      auto* objective_var = cp_model->add_variables();
-      objective_var->set_name("objective");
-      objective_var->add_domain(-kMaxObjective);
-      objective_var->add_domain(kMaxObjective);
-    }
-
-    // Link the objective variable with a linear constraint.
-    {
-      auto* objective_constraint = cp_model->add_constraints();
-      auto* objective_arg = objective_constraint->mutable_linear();
-      objective_constraint->set_name("objective");
-      objective_arg->add_domain(0);
-      objective_arg->add_domain(0);
-      for (int i = 0; i < num_variables; ++i) {
-        const MPVariableProto& mp_var = mp_model.variable(i);
-        const int64 value =
-            static_cast<int64>(
-                std::round(mp_var.objective_coefficient() * scaling_factor)) /
-            gcd;
-        if (value != 0) {
-          objective_arg->add_vars(i);
-          objective_arg->add_coeffs(value);
-        }
+    auto* objective = cp_model->mutable_objective();
+    const int mult = mp_model.maximize() ? -1 : 1;
+    objective->set_offset(mp_model.objective_offset() * scaling_factor / gcd *
+                          mult);
+    objective->set_scaling_factor(1.0 / scaling_factor * gcd * mult);
+    for (int i = 0; i < num_variables; ++i) {
+      const MPVariableProto& mp_var = mp_model.variable(i);
+      const int64 value =
+          static_cast<int64>(
+              std::round(mp_var.objective_coefficient() * scaling_factor)) /
+          gcd;
+      if (value != 0) {
+        objective->add_vars(i);
+        objective->add_coeffs(value * mult);
      }
-      objective_arg->add_vars(objective->objective_var());
-      objective_arg->add_coeffs(-1);
-    }
-
-    // If the problem was a maximization one, we need to modify the objective.
-    if (mp_model.maximize()) {
-      objective->set_objective_var(-objective->objective_var() - 1);
-      objective->set_scaling_factor(-objective->scaling_factor());
-      objective->set_offset(-objective->offset());
    }
  }

--- a/ortools/sat/model.h
+++ b/ortools/sat/model.h
@@ -64,8 +64,7 @@ class Model {

  // Returns an object of type T that is unique to this model (this is a bit
  // like a "local" singleton). This returns an already created instance or
-  // create a new one if needed using the T::CreateInModel(Model* model)
-  // function of the class T.
+  // create a new one if needed using the T(Model* model) constructor.
  //
  // This works a bit like in a dependency injection framework and allows to
  // really easily wire all the classes that make up a solver together. For
@@ -73,25 +72,31 @@ class Model {
  // or both, it can depend on a Watcher class to register itself in order to
  // be called when needed and so on.
  //
-  // IMPORTANT: the CreateInModel() functiond shouldn't form a cycle between
+  // IMPORTANT: the Model* constructors function shouldn't form a cycle between
  // each other, otherwise this will crash the program.
+  //
+  // TODO(user): Rename to GetOrCreateSingleton().
  template <typename T>
  T* GetOrCreate() {
    const size_t type_id = FastTypeId<T>();
    if (!ContainsKey(singletons_, type_id)) {
-      // Note that it is up to CreateInModel() to call model->TakeOwnership()
-      // of the returned pointer.
-      //
-      // TODO(user): Always take ownership of the pointer instead. That would
-      // requires some cleanup, but it is probably a safer solution and would
-      // allow SetSingleton() to change an instance dynamically.
-      T* new_t = T::CreateInModel(this);
+      // TODO(user): directly store std::unique_ptr<> in singletons_?
+      T* new_t = new T(this);
      singletons_[type_id] = new_t;
+      TakeOwnership(new_t);
      return new_t;
    }
    return static_cast<T*>(FindOrDie(singletons_, type_id));
  }

+  // This returns a non-singleton object owned by the model.
+  template <typename T>
+  T* Create() {
+    T* new_t = new T(this);
+    TakeOwnership(new_t);
+    return new_t;
+  }
+
  // Registers a given instance of type T as a "local singleton" for this type.
  // For now this CHECKs that the object was not yet created.
  template <typename T>
--- a/ortools/sat/no_cycle.h
+++ b/ortools/sat/no_cycle.h
@@ -16,7 +16,6 @@

 #include <vector>

-#include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_solver.h"

@@ -39,13 +38,6 @@ class NoCyclePropagator : public SatPropagator {
        include_propagated_arcs_in_graph_(true) {}
  ~NoCyclePropagator() final {}

-  static NoCyclePropagator* CreateInModel(Model* model) {
-    NoCyclePropagator* no_cycle = new NoCyclePropagator();
-    model->GetOrCreate<SatSolver>()->AddPropagator(
-        std::unique_ptr<NoCyclePropagator>(no_cycle));
-    return no_cycle;
-  }
-
  bool Propagate(Trail* trail) final;
  void Untrail(const Trail& trail, int trail_index) final;
  gtl::Span<Literal> Reason(const Trail& trail,
--- a/ortools/sat/precedences.h
+++ b/ortools/sat/precedences.h
@@ -39,27 +39,15 @@ namespace sat {
 // Another word is "separation logic".
 class PrecedencesPropagator : public SatPropagator, PropagatorInterface {
 public:
-  PrecedencesPropagator(Trail* trail, IntegerTrail* integer_trail,
-                        GenericLiteralWatcher* watcher)
+  explicit PrecedencesPropagator(Model* model)
      : SatPropagator("PrecedencesPropagator"),
-        trail_(trail),
-        integer_trail_(integer_trail),
-        watcher_(watcher),
-        watcher_id_(watcher->Register(this)) {
+        trail_(model->GetOrCreate<Trail>()),
+        integer_trail_(model->GetOrCreate<IntegerTrail>()),
+        watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
+        watcher_id_(watcher_->Register(this)) {
+    model->GetOrCreate<SatSolver>()->AddPropagator(this);
    integer_trail_->RegisterWatcher(&modified_vars_);
-    watcher->SetPropagatorPriority(watcher_id_, 0);
-  }
-
-  static PrecedencesPropagator* CreateInModel(Model* model) {
-    PrecedencesPropagator* precedences = new PrecedencesPropagator(
-        model->GetOrCreate<Trail>(), model->GetOrCreate<IntegerTrail>(),
-        model->GetOrCreate<GenericLiteralWatcher>());
-
-    // TODO(user): Find a way to have more control on the order in which
-    // the propagators are added.
-    model->GetOrCreate<SatSolver>()->AddPropagator(
-        std::unique_ptr<PrecedencesPropagator>(precedences));
-    return precedences;
+    watcher_->SetPropagatorPriority(watcher_id_, 0);
  }

  bool Propagate() final;
--- a/ortools/sat/sat_base.h
+++ b/ortools/sat/sat_base.h
@@ -224,17 +224,13 @@ struct AssignmentType {
 // and the information of each assignment.
 class Trail {
 public:
+  explicit Trail(Model* model) : Trail() {}
+
  Trail() : num_enqueues_(0) {
    current_info_.trail_index = 0;
    current_info_.level = 0;
  }

-  static Trail* CreateInModel(Model* model) {
-    Trail* trail = new Trail();
-    model->TakeOwnership(trail);
-    return trail;
-  }
-
  void Resize(int num_variables);

  // Registers a propagator. This assigns a unique id to this propagator and
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -31,13 +31,14 @@
 namespace operations_research {
 namespace sat {

-SatSolver::SatSolver() : SatSolver(new Trail()) { owned_trail_.reset(trail_); }
+SatSolver::SatSolver() : SatSolver(new Model()) { owned_model_.reset(model_); }

-SatSolver::SatSolver(Trail* trail)
-    : num_variables_(0),
+SatSolver::SatSolver(Model* model)
+    : model_(model),
+      num_variables_(0),
      pb_constraints_(),
      track_binary_clauses_(false),
-      trail_(trail),
+      trail_(model->GetOrCreate<Trail>()),
      current_decision_level_(0),
      last_decision_or_backtrack_trail_index_(0),
      assumption_level_(0),
@@ -397,20 +398,20 @@ void SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
  }
 }

-void SatSolver::AddPropagator(std::unique_ptr<SatPropagator> propagator) {
+void SatSolver::AddPropagator(SatPropagator* propagator) {
  CHECK_EQ(CurrentDecisionLevel(), 0);
  problem_is_pure_sat_ = false;
-  trail_->RegisterPropagator(propagator.get());
-  external_propagators_.push_back(std::move(propagator));
+  trail_->RegisterPropagator(propagator);
+  external_propagators_.push_back(propagator);
  InitializePropagators();
 }

-void SatSolver::AddLastPropagator(std::unique_ptr<SatPropagator> propagator) {
+void SatSolver::AddLastPropagator(SatPropagator* propagator) {
  CHECK_EQ(CurrentDecisionLevel(), 0);
  CHECK(last_propagator_ == nullptr);
  problem_is_pure_sat_ = false;
-  trail_->RegisterPropagator(propagator.get());
-  last_propagator_ = std::move(propagator);
+  trail_->RegisterPropagator(propagator);
+  last_propagator_ = propagator;
  InitializePropagators();
 }

@@ -1538,10 +1539,10 @@ void SatSolver::InitializePropagators() {
    propagators_.push_back(&pb_constraints_);
  }
  for (int i = 0; i < external_propagators_.size(); ++i) {
-    propagators_.push_back(external_propagators_[i].get());
+    propagators_.push_back(external_propagators_[i]);
  }
  if (last_propagator_ != nullptr) {
-    propagators_.push_back(last_propagator_.get());
+    propagators_.push_back(last_propagator_);
  }
 }

--- a/ortools/sat/sat_solver.h
+++ b/ortools/sat/sat_solver.h
@@ -57,16 +57,9 @@ const int kUnsatTrailIndex = -1;
 class SatSolver {
 public:
  SatSolver();
-  explicit SatSolver(Trail* trail);
+  explicit SatSolver(Model* model);
  ~SatSolver();

-  static SatSolver* CreateInModel(Model* model) {
-    Trail* trail = model->GetOrCreate<Trail>();
-    SatSolver* solver = new SatSolver(trail);
-    model->TakeOwnership(solver);
-    return solver;
-  }
-
  // Parameters management. Note that calling SetParameters() will reset the
  // value of many heuristics. For instance:
  // - The restart strategy will be reinitialized.
@@ -136,8 +129,11 @@ class SatSolver {

  // Adds and registers the given propagator with the sat solver. Note that
  // during propagation, they will be called in the order they where added.
-  void AddPropagator(std::unique_ptr<SatPropagator> propagator);
-  void AddLastPropagator(std::unique_ptr<SatPropagator> propagator);
+  void AddPropagator(SatPropagator* propagator);
+  void AddLastPropagator(SatPropagator* propagator);
+  void TakePropagatorOwnership(std::unique_ptr<SatPropagator> propagator) {
+    owned_propagators_.push_back(std::move(propagator));
+  }

  // Gives a hint so the solver tries to find a solution with the given literal
  // set to true. Currently this take precedence over the phase saving heuristic
@@ -655,6 +651,10 @@ class SatSolver {
  std::string StatusString(Status status) const;
  std::string RunningStatisticsString() const;

+  // This is used by the old non-model constructor.
+  Model* model_;
+  std::unique_ptr<Model> owned_model_;
+
  BooleanVariable num_variables_;

  // All the clauses managed by the solver (initial and learned). This vector
@@ -686,8 +686,11 @@ class SatSolver {
  std::vector<SatPropagator*> propagators_;

  // Ordered list of propagators added with AddPropagator().
-  std::vector<std::unique_ptr<SatPropagator>> external_propagators_;
-  std::unique_ptr<SatPropagator> last_propagator_;
+  std::vector<SatPropagator*> external_propagators_;
+  SatPropagator* last_propagator_ = nullptr;
+
+  // For the old, non-model interface.
+  std::vector<std::unique_ptr<SatPropagator>> owned_propagators_;

  // Keep track of all binary clauses so they can be exported.
  bool track_binary_clauses_;
@@ -696,9 +699,6 @@ class SatSolver {
  // The solver trail.
  Trail* trail_;

-  // This is used by the non-model constructor to properly cleanup trail_.
-  std::unique_ptr<Trail> owned_trail_;
-
  // Used for debugging only. See SaveDebugAssignment().
  VariablesAssignment debug_assignment_;

--- a/tools/generate_deps.sh
+++ b/tools/generate_deps.sh
@@ -1,7 +1,7 @@
 main_dir=$2

 # List all files on ortools/$main_dir
-all_cc=`ls ortools/$main_dir/*.cc`
+all_cc=`ls ortools/$main_dir/*.cc | grep -v test.cc`
 all_h=`ls ortools/$main_dir/*.h`
 if ls ortools/$main_dir/*proto 1> /dev/null 2>&1; then
    all_proto=`ls ortools/$main_dir/*.proto`