OR-Tools  8.2
sat_proto_solver.cc
Go to the documentation of this file.
1 // Copyright 2010-2018 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 // http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13 
15 
16 #include <vector>
17 
18 #include "absl/status/statusor.h"
19 #include "ortools/linear_solver/linear_solver.pb.h"
23 #include "ortools/sat/cp_model.pb.h"
25 #include "ortools/sat/lp_utils.h"
26 #include "ortools/sat/sat_parameters.pb.h"
28 
29 namespace operations_research {
30 
31 namespace {
32 
33 #if defined(PROTOBUF_INTERNAL_IMPL)
34 using google::protobuf::Message;
35 #else
36 using google::protobuf::Message;
37 #endif
38 
39 // Proto-lite disables some features of protos (see
40 // go/abp-libraries/proto2-lite) and messages inherit from MessageLite directly
41 // instead of inheriting from Message (which is itself a specialization of
42 // MessageLite).
43 constexpr bool kProtoLiteSatParameters =
45 
46 MPSolverResponseStatus ToMPSolverResponseStatus(sat::CpSolverStatus status,
47  bool has_objective) {
48  switch (status) {
49  case sat::CpSolverStatus::UNKNOWN:
50  return MPSOLVER_NOT_SOLVED;
51  case sat::CpSolverStatus::MODEL_INVALID:
52  return MPSOLVER_MODEL_INVALID;
53  case sat::CpSolverStatus::FEASIBLE:
54  return has_objective ? MPSOLVER_FEASIBLE : MPSOLVER_OPTIMAL;
55  case sat::CpSolverStatus::INFEASIBLE:
56  return MPSOLVER_INFEASIBLE;
57  case sat::CpSolverStatus::OPTIMAL:
58  return MPSOLVER_OPTIMAL;
59  default: {
60  }
61  }
62  return MPSOLVER_ABNORMAL;
63 }
64 } // namespace
65 
66 absl::StatusOr<MPSolutionResponse> SatSolveProto(
67  MPModelRequest request, std::atomic<bool>* interrupt_solve) {
68  // By default, we use 8 threads as it allows to try a good set of orthogonal
69  // parameters. This can be overridden by the user.
70  sat::SatParameters params;
71  params.set_num_search_workers(8);
72  params.set_log_search_progress(request.enable_internal_solver_output());
73  if (request.has_solver_specific_parameters()) {
74  // See EncodeSatParametersAsString() documentation.
75  if (kProtoLiteSatParameters) {
76  if (!params.MergeFromString(request.solver_specific_parameters())) {
77  return absl::InvalidArgumentError(
78  "solver_specific_parameters is not a valid binary stream of the "
79  "SatParameters proto");
80  }
81  } else {
83  request.solver_specific_parameters(), &params)) {
84  return absl::InvalidArgumentError(
85  "solver_specific_parameters is not a valid textual representation "
86  "of the SatParameters proto");
87  }
88  }
89  }
90  if (request.has_solver_time_limit_seconds()) {
91  params.set_max_time_in_seconds(
92  static_cast<double>(request.solver_time_limit_seconds()) / 1000.0);
93  }
94 
95  MPSolutionResponse response;
97  &response)) {
98  if (params.log_search_progress()) {
99  // This is needed for our benchmark scripts.
100  sat::CpSolverResponse cp_response;
101  cp_response.set_status(sat::CpSolverStatus::MODEL_INVALID);
102  LOG(INFO) << CpSolverResponseStats(cp_response);
103  }
104  return response;
105  }
106 
107  // Note(user): the LP presolvers API is a bit weird and keep a reference to
108  // the given GlopParameters, so we need to make sure it outlive them.
109  const glop::GlopParameters glop_params;
110  MPModelProto* const mp_model = request.mutable_model();
111  std::vector<std::unique_ptr<glop::Preprocessor>> for_postsolve;
112  const bool log_info = VLOG_IS_ON(1) || params.log_search_progress();
113  const auto status =
114  ApplyMipPresolveSteps(log_info, glop_params, mp_model, &for_postsolve);
115  if (status == MPSolverResponseStatus::MPSOLVER_INFEASIBLE) {
116  if (params.log_search_progress()) {
117  // This is needed for our benchmark scripts.
118  sat::CpSolverResponse cp_response;
119  cp_response.set_status(sat::CpSolverStatus::INFEASIBLE);
120  LOG(INFO) << CpSolverResponseStats(cp_response);
121  }
122  response.set_status(MPSolverResponseStatus::MPSOLVER_INFEASIBLE);
123  response.set_status_str("Problem proven infeasible during MIP presolve");
124  return response;
125  }
126 
127  // We need to do that before the automatic detection of integers.
128  RemoveNearZeroTerms(params, mp_model);
129 
130  const int num_variables = mp_model->variable_size();
131  std::vector<double> var_scaling(num_variables, 1.0);
132  if (params.mip_automatically_scale_variables()) {
133  var_scaling = sat::DetectImpliedIntegers(log_info, mp_model);
134  }
135  if (params.mip_var_scaling() != 1.0) {
136  const std::vector<double> other_scaling = sat::ScaleContinuousVariables(
137  params.mip_var_scaling(), params.mip_max_bound(), mp_model);
138  for (int i = 0; i < var_scaling.size(); ++i) {
139  var_scaling[i] *= other_scaling[i];
140  }
141  }
142 
143  sat::CpModelProto cp_model;
144  if (!ConvertMPModelProtoToCpModelProto(params, *mp_model, &cp_model)) {
145  if (params.log_search_progress()) {
146  // This is needed for our benchmark scripts.
147  sat::CpSolverResponse cp_response;
148  cp_response.set_status(sat::CpSolverStatus::MODEL_INVALID);
149  LOG(INFO) << CpSolverResponseStats(cp_response);
150  }
151  response.set_status(MPSOLVER_MODEL_INVALID);
152  response.set_status_str("Failed to convert model into CP-SAT model");
153  return response;
154  }
155  DCHECK_EQ(cp_model.variables().size(), var_scaling.size());
156  DCHECK_EQ(cp_model.variables().size(), mp_model->variable().size());
157 
158  // Copy and scale the hint if there is one.
159  if (request.model().has_solution_hint()) {
160  auto* cp_model_hint = cp_model.mutable_solution_hint();
161  const int size = request.model().solution_hint().var_index().size();
162  for (int i = 0; i < size; ++i) {
163  const int var = request.model().solution_hint().var_index(i);
164  if (var >= var_scaling.size()) continue;
165 
166  // To handle weird hint input values, we cap any large value to +/-
167  // mip_max_bound() which is also the min/max value of any variable once
168  // scaled.
169  double value =
170  request.model().solution_hint().var_value(i) * var_scaling[var];
171  if (std::abs(value) > params.mip_max_bound()) {
172  value = value > 0 ? params.mip_max_bound() : -params.mip_max_bound();
173  }
174 
175  cp_model_hint->add_vars(var);
176  cp_model_hint->add_values(static_cast<int64>(std::round(value)));
177  }
178  }
179 
180  // We no longer need the request. Reclaim its memory.
181  const int old_num_variables = mp_model->variable().size();
182  const int old_num_constraints = mp_model->constraint().size();
183  request.Clear();
184 
185  // Solve.
186  sat::Model sat_model;
187  sat_model.Add(NewSatParameters(params));
188  if (interrupt_solve != nullptr) {
189  sat_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
190  interrupt_solve);
191  }
192  const sat::CpSolverResponse cp_response =
193  sat::SolveCpModel(cp_model, &sat_model);
194 
195  // Convert the response.
196  //
197  // TODO(user): Implement the row and column status.
198  response.set_status(
199  ToMPSolverResponseStatus(cp_response.status(), cp_model.has_objective()));
200  if (response.status() == MPSOLVER_FEASIBLE ||
201  response.status() == MPSOLVER_OPTIMAL) {
202  response.set_objective_value(cp_response.objective_value());
203  response.set_best_objective_bound(cp_response.best_objective_bound());
204 
205  // Postsolve the bound shift and scaling.
206  glop::ProblemSolution solution((glop::RowIndex(old_num_constraints)),
207  (glop::ColIndex(old_num_variables)));
208  for (int v = 0; v < solution.primal_values.size(); ++v) {
209  solution.primal_values[glop::ColIndex(v)] =
210  static_cast<double>(cp_response.solution(v)) / var_scaling[v];
211  }
212  for (int i = for_postsolve.size(); --i >= 0;) {
213  for_postsolve[i]->RecoverSolution(&solution);
214  }
215  for (int v = 0; v < solution.primal_values.size(); ++v) {
216  response.add_variable_value(solution.primal_values[glop::ColIndex(v)]);
217  }
218  }
219 
220  return response;
221 }
222 
223 std::string EncodeSatParametersAsString(const sat::SatParameters& parameters) {
224  if (kProtoLiteSatParameters) {
225  // Here we use SerializeToString() instead of SerializeAsString() since the
226  // later ignores errors and returns an empty string instead (which can be a
227  // valid value when no fields are set).
228  std::string bytes;
229  CHECK(parameters.SerializeToString(&bytes));
230  return bytes;
231  }
232 
233  return parameters.ShortDebugString();
234 }
235 
236 } // namespace operations_research
#define CHECK(condition)
Definition: base/logging.h:495
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
T Add(std::function< T(Model *)> f)
This makes it possible to have a nicer API on the client side, and it allows both of these forms:
Definition: sat/model.h:81
T * GetOrCreate()
Returns an object of type T that is unique to this model (like a "local" singleton).
Definition: sat/model.h:106
SatParameters parameters
SharedResponseManager * response
int64 value
IntVar * var
Definition: expr_array.cc:1858
int64_t int64
const int INFO
Definition: log_severity.h:31
void RemoveNearZeroTerms(const SatParameters &params, MPModelProto *mp_model)
std::function< SatParameters(Model *)> NewSatParameters(const std::string &params)
Creates parameters for the solver, which you can add to the model with.
std::string CpSolverResponseStats(const CpSolverResponse &response, bool has_objective)
Returns a string with some statistics on the solver response.
std::vector< double > DetectImpliedIntegers(bool log_info, MPModelProto *mp_model)
CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)
Solves the given CpModelProto.
std::vector< double > ScaleContinuousVariables(double scaling, double max_bound, MPModelProto *mp_model)
Definition: sat/lp_utils.cc:99
bool ConvertMPModelProtoToCpModelProto(const SatParameters &params, const MPModelProto &mp_model, CpModelProto *cp_model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
bool ExtractValidMPModelInPlaceOrPopulateResponseStatus(MPModelRequest *request, MPSolutionResponse *response)
Like ExtractValidMPModelOrPopulateResponseStatus(), but works in-place: if the MPModel needed extract...
MPSolverResponseStatus ApplyMipPresolveSteps(bool log_info, const glop::GlopParameters &glop_params, MPModelProto *model, std::vector< std::unique_ptr< glop::Preprocessor >> *for_postsolve)
bool ProtobufTextFormatMergeFromString(const std::string &proto_text_string, ProtoType *proto)
std::string EncodeSatParametersAsString(const sat::SatParameters &parameters)
absl::StatusOr< MPSolutionResponse > SatSolveProto(MPModelRequest request, std::atomic< bool > *interrupt_solve)
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41