OR-Tools  8.2
sat_interface.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
14#include <atomic>
15#include <string>
16#include <vector>
17
18#include "absl/status/status.h"
19#include "absl/status/statusor.h"
20#include "ortools/base/hash.h"
24#include "ortools/linear_solver/linear_solver.pb.h"
27#include "ortools/sat/cp_model.pb.h"
30#include "ortools/sat/model.h"
32
33namespace operations_research {
34
35#if defined(PROTOBUF_INTERNAL_IMPL)
36using google::protobuf::Message;
37#else
38using google::protobuf::Message;
39#endif
40
42 public:
43 explicit SatInterface(MPSolver* const solver);
44 ~SatInterface() override;
45
46 // ----- Solve -----
47 MPSolver::ResultStatus Solve(const MPSolverParameters& param) override;
48 bool InterruptSolve() override;
49
50 // ----- Model modifications and extraction -----
51 void Reset() override;
52 void SetOptimizationDirection(bool maximize) override;
53 void SetVariableBounds(int index, double lb, double ub) override;
54 void SetVariableInteger(int index, bool integer) override;
55 void SetConstraintBounds(int index, double lb, double ub) override;
56 void AddRowConstraint(MPConstraint* const ct) override;
57 void AddVariable(MPVariable* const var) override;
58 void SetCoefficient(MPConstraint* const constraint,
59 const MPVariable* const variable, double new_value,
60 double old_value) override;
61 void ClearConstraint(MPConstraint* const constraint) override;
62 void SetObjectiveCoefficient(const MPVariable* const variable,
63 double coefficient) override;
64 void SetObjectiveOffset(double value) override;
65 void ClearObjective() override;
66
67 bool AddIndicatorConstraint(MPConstraint* const ct) override { return true; }
68
69 // ------ Query statistics on the solution and the solve ------
70 int64 iterations() const override;
71 int64 nodes() const override;
72 MPSolver::BasisStatus row_status(int constraint_index) const override;
73 MPSolver::BasisStatus column_status(int variable_index) const override;
74
75 // ----- Misc -----
76 bool IsContinuous() const override;
77 bool IsLP() const override;
78 bool IsMIP() const override;
79
80 std::string SolverVersion() const override;
81 void* underlying_solver() override;
82
83 void ExtractNewVariables() override;
84 void ExtractNewConstraints() override;
85 void ExtractObjective() override;
86
87 void SetParameters(const MPSolverParameters& param) override;
88 void SetRelativeMipGap(double value) override;
89 void SetPrimalTolerance(double value) override;
90 void SetDualTolerance(double value) override;
91 void SetPresolveMode(int value) override;
92 void SetScalingMode(int value) override;
93 void SetLpAlgorithm(int value) override;
95 const std::string& parameters) override;
96 absl::Status SetNumThreads(int num_threads) override;
97
98 private:
99 void NonIncrementalChange();
100
101 std::atomic<bool> interrupt_solve_;
102 sat::SatParameters parameters_;
103 int num_threads_ = 8;
104};
105
107 : MPSolverInterface(solver), interrupt_solve_(false) {}
108
110
112 interrupt_solve_ = false;
113
114 // Reset extraction as this interface is not incremental yet.
115 Reset();
116 ExtractModel();
117
118 SetParameters(param);
120 solver_->solver_specific_parameter_string_);
121
122 // Time limit.
123 if (solver_->time_limit()) {
124 VLOG(1) << "Setting time limit = " << solver_->time_limit() << " ms.";
125 parameters_.set_max_time_in_seconds(
126 static_cast<double>(solver_->time_limit()) / 1000.0);
127 }
128
129 // Mark variables and constraints as extracted.
130 for (int i = 0; i < solver_->variables_.size(); ++i) {
132 }
133 for (int i = 0; i < solver_->constraints_.size(); ++i) {
135 }
136
137 MPModelRequest request;
138 solver_->ExportModelToProto(request.mutable_model());
139 request.set_solver_specific_parameters(
140 EncodeSatParametersAsString(parameters_));
141 request.set_enable_internal_solver_output(!quiet_);
142 const absl::StatusOr<MPSolutionResponse> status_or =
143 SatSolveProto(std::move(request), &interrupt_solve_);
144
145 if (!status_or.ok()) return MPSolver::ABNORMAL;
146 const MPSolutionResponse& response = status_or.value();
147
148 // The solution must be marked as synchronized even when no solution exists.
150 switch (response.status()) {
151 case MPSOLVER_OPTIMAL:
153 break;
154 case MPSOLVER_FEASIBLE:
156 break;
157 case MPSOLVER_INFEASIBLE:
159 break;
160 case MPSOLVER_MODEL_INVALID:
162 break;
163 default:
165 break;
166 }
167
168 // TODO(user): Just use LoadSolutionFromProto(), but fix that function first
169 // to load everything and not just the solution.
170 if (response.status() == MPSOLVER_FEASIBLE ||
171 response.status() == MPSOLVER_OPTIMAL) {
172 objective_value_ = response.objective_value();
173 best_objective_bound_ = response.best_objective_bound();
174 const size_t num_vars = solver_->variables_.size();
175 for (int var_id = 0; var_id < num_vars; ++var_id) {
176 MPVariable* const var = solver_->variables_[var_id];
177 var->set_solution_value(response.variable_value(var_id));
178 }
179 }
180
181 return result_status_;
182}
183
185 interrupt_solve_ = true;
186 return true;
187}
188
190
192 NonIncrementalChange();
193}
194
195void SatInterface::SetVariableBounds(int index, double lb, double ub) {
196 NonIncrementalChange();
197}
198
200 NonIncrementalChange();
201}
202
203void SatInterface::SetConstraintBounds(int index, double lb, double ub) {
204 NonIncrementalChange();
205}
206
208 NonIncrementalChange();
209}
210
212 NonIncrementalChange();
213}
214
216 const MPVariable* const variable,
217 double new_value, double old_value) {
218 NonIncrementalChange();
219}
220
222 NonIncrementalChange();
223}
224
226 double coefficient) {
227 NonIncrementalChange();
228}
229
230void SatInterface::SetObjectiveOffset(double value) { NonIncrementalChange(); }
231
232void SatInterface::ClearObjective() { NonIncrementalChange(); }
233
235 return 0; // FIXME
236}
237
238int64 SatInterface::nodes() const { return 0; }
239
241 return MPSolver::BasisStatus::FREE; // FIXME
242}
243
245 return MPSolver::BasisStatus::FREE; // FIXME
246}
247
248bool SatInterface::IsContinuous() const { return false; }
249bool SatInterface::IsLP() const { return false; }
250bool SatInterface::IsMIP() const { return true; }
251
252std::string SatInterface::SolverVersion() const {
253 return "SAT Based MIP Solver";
254}
255
256void* SatInterface::underlying_solver() { return nullptr; }
257
258void SatInterface::ExtractNewVariables() { NonIncrementalChange(); }
259
260void SatInterface::ExtractNewConstraints() { NonIncrementalChange(); }
261
262void SatInterface::ExtractObjective() { NonIncrementalChange(); }
263
265 // By default, we use 8 threads as it allows to try a good set of orthogonal
266 // parameters. This can be overridden by the user.
267 parameters_.set_num_search_workers(num_threads_);
268 parameters_.set_log_search_progress(!quiet_);
269 SetCommonParameters(param);
270}
271
272absl::Status SatInterface::SetNumThreads(int num_threads) {
273 num_threads_ = num_threads;
274 return absl::OkStatus();
275}
276
277// All these have no effect.
283
284// TODO(user): Implement me.
286
288 const std::string& parameters) {
289 return ProtobufTextFormatMergeFromString(parameters, &parameters_);
290}
291
292void SatInterface::NonIncrementalChange() {
293 // The current implementation is not incremental.
295}
296
297// Register Sat in the global linear solver factory.
299 return new SatInterface(solver);
300}
301
302} // namespace operations_research
#define VLOG(verboselevel)
Definition: base/logging.h:978
The class for constraints of a Mathematical Programming (MP) model.
This mathematical programming (MP) solver class is the main class though which users build and solve ...
ResultStatus
The status of solving the problem.
@ FEASIBLE
feasible, or stopped by limit.
@ NOT_SOLVED
not been solved yet.
@ INFEASIBLE
proven infeasible.
@ ABNORMAL
abnormal, i.e., error of some kind.
@ MODEL_INVALID
the model is trivially invalid (NaN coefficients, etc).
bool SetSolverSpecificParametersAsString(const std::string &parameters)
Advanced usage: pass solver specific parameters in text format.
void ExportModelToProto(MPModelProto *output_model) const
Exports model to protocol buffer.
BasisStatus
Advanced usage: possible basis status values for a variable and the slack variable of a linear constr...
void set_constraint_as_extracted(int ct_index, bool extracted)
void set_variable_as_extracted(int var_index, bool extracted)
void SetCommonParameters(const MPSolverParameters &param)
This class stores parameter settings for LP and MIP solvers.
The class for variables of a Mathematical Programming (MP) model.
void SetScalingMode(int value) override
void SetDualTolerance(double value) override
void AddRowConstraint(MPConstraint *const ct) override
void SetLpAlgorithm(int value) override
SatInterface(MPSolver *const solver)
int64 nodes() const override
bool IsContinuous() const override
MPSolver::ResultStatus Solve(const MPSolverParameters &param) override
void SetPrimalTolerance(double value) override
void ClearConstraint(MPConstraint *const constraint) override
bool SetSolverSpecificParametersAsString(const std::string &parameters) override
void SetObjectiveCoefficient(const MPVariable *const variable, double coefficient) override
void SetCoefficient(MPConstraint *const constraint, const MPVariable *const variable, double new_value, double old_value) override
MPSolver::BasisStatus row_status(int constraint_index) const override
void SetObjectiveOffset(double value) override
void SetVariableInteger(int index, bool integer) override
void SetParameters(const MPSolverParameters &param) override
std::string SolverVersion() const override
void SetRelativeMipGap(double value) override
void SetConstraintBounds(int index, double lb, double ub) override
absl::Status SetNumThreads(int num_threads) override
void SetPresolveMode(int value) override
void SetVariableBounds(int index, double lb, double ub) override
void AddVariable(MPVariable *const var) override
bool AddIndicatorConstraint(MPConstraint *const ct) override
void SetOptimizationDirection(bool maximize) override
MPSolver::BasisStatus column_status(int variable_index) const override
int64 iterations() const override
SatParameters parameters
SharedResponseManager * response
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
int64_t int64
A C++ wrapper that provides a simple and unified interface to several linear programming and mixed in...
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
bool ProtobufTextFormatMergeFromString(const std::string &proto_text_string, ProtoType *proto)
std::string EncodeSatParametersAsString(const sat::SatParameters &parameters)
MPSolverInterface * BuildSatInterface(MPSolver *const solver)
absl::StatusOr< MPSolutionResponse > SatSolveProto(MPModelRequest request, std::atomic< bool > *interrupt_solve)
int index
Definition: pack.cc:508
int64 coefficient