forked from google/or-tools
-
Notifications
You must be signed in to change notification settings - Fork 3
/
sat_interface.cc
302 lines (244 loc) · 9.73 KB
/
sat_interface.cc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#include <atomic>
#include <string>
#include <vector>
#include "absl/status/status.h"
#include "absl/status/statusor.h"
#include "ortools/base/hash.h"
#include "ortools/base/integral_types.h"
#include "ortools/base/logging.h"
#include "ortools/linear_solver/linear_solver.h"
#include "ortools/linear_solver/linear_solver.pb.h"
#include "ortools/linear_solver/sat_proto_solver.h"
#include "ortools/port/proto_utils.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/lp_utils.h"
#include "ortools/sat/model.h"
#include "ortools/util/time_limit.h"
namespace operations_research {
#if defined(PROTOBUF_INTERNAL_IMPL)
using google::protobuf::Message;
#else
using google::protobuf::Message;
#endif
class SatInterface : public MPSolverInterface {
public:
explicit SatInterface(MPSolver* const solver);
~SatInterface() override;
// ----- Solve -----
MPSolver::ResultStatus Solve(const MPSolverParameters& param) override;
bool InterruptSolve() override;
// ----- Model modifications and extraction -----
void Reset() override;
void SetOptimizationDirection(bool maximize) override;
void SetVariableBounds(int index, double lb, double ub) override;
void SetVariableInteger(int index, bool integer) override;
void SetConstraintBounds(int index, double lb, double ub) override;
void AddRowConstraint(MPConstraint* const ct) override;
void AddVariable(MPVariable* const var) override;
void SetCoefficient(MPConstraint* const constraint,
const MPVariable* const variable, double new_value,
double old_value) override;
void ClearConstraint(MPConstraint* const constraint) override;
void SetObjectiveCoefficient(const MPVariable* const variable,
double coefficient) override;
void SetObjectiveOffset(double value) override;
void ClearObjective() override;
bool AddIndicatorConstraint(MPConstraint* const ct) override { return true; }
// ------ Query statistics on the solution and the solve ------
int64 iterations() const override;
int64 nodes() const override;
MPSolver::BasisStatus row_status(int constraint_index) const override;
MPSolver::BasisStatus column_status(int variable_index) const override;
// ----- Misc -----
bool IsContinuous() const override;
bool IsLP() const override;
bool IsMIP() const override;
std::string SolverVersion() const override;
void* underlying_solver() override;
void ExtractNewVariables() override;
void ExtractNewConstraints() override;
void ExtractObjective() override;
void SetParameters(const MPSolverParameters& param) override;
void SetRelativeMipGap(double value) override;
void SetPrimalTolerance(double value) override;
void SetDualTolerance(double value) override;
void SetPresolveMode(int value) override;
void SetScalingMode(int value) override;
void SetLpAlgorithm(int value) override;
bool SetSolverSpecificParametersAsString(
const std::string& parameters) override;
absl::Status SetNumThreads(int num_threads) override;
private:
void NonIncrementalChange();
std::atomic<bool> interrupt_solve_;
sat::SatParameters parameters_;
int num_threads_ = 8;
};
SatInterface::SatInterface(MPSolver* const solver)
: MPSolverInterface(solver), interrupt_solve_(false) {}
SatInterface::~SatInterface() {}
MPSolver::ResultStatus SatInterface::Solve(const MPSolverParameters& param) {
interrupt_solve_ = false;
// Reset extraction as this interface is not incremental yet.
Reset();
ExtractModel();
SetParameters(param);
solver_->SetSolverSpecificParametersAsString(
solver_->solver_specific_parameter_string_);
// Time limit.
if (solver_->time_limit()) {
VLOG(1) << "Setting time limit = " << solver_->time_limit() << " ms.";
parameters_.set_max_time_in_seconds(
static_cast<double>(solver_->time_limit()) / 1000.0);
}
// Mark variables and constraints as extracted.
for (int i = 0; i < solver_->variables_.size(); ++i) {
set_variable_as_extracted(i, true);
}
for (int i = 0; i < solver_->constraints_.size(); ++i) {
set_constraint_as_extracted(i, true);
}
MPModelRequest request;
solver_->ExportModelToProto(request.mutable_model());
request.set_solver_specific_parameters(
EncodeSatParametersAsString(parameters_));
request.set_enable_internal_solver_output(!quiet_);
const absl::StatusOr<MPSolutionResponse> status_or =
SatSolveProto(std::move(request), &interrupt_solve_);
if (!status_or.ok()) return MPSolver::ABNORMAL;
const MPSolutionResponse& response = status_or.value();
// The solution must be marked as synchronized even when no solution exists.
sync_status_ = SOLUTION_SYNCHRONIZED;
switch (response.status()) {
case MPSOLVER_OPTIMAL:
result_status_ = MPSolver::OPTIMAL;
break;
case MPSOLVER_FEASIBLE:
result_status_ = MPSolver::FEASIBLE;
break;
case MPSOLVER_INFEASIBLE:
result_status_ = MPSolver::INFEASIBLE;
break;
case MPSOLVER_MODEL_INVALID:
result_status_ = MPSolver::MODEL_INVALID;
break;
default:
result_status_ = MPSolver::NOT_SOLVED;
break;
}
// TODO(user): Just use LoadSolutionFromProto(), but fix that function first
// to load everything and not just the solution.
if (response.status() == MPSOLVER_FEASIBLE ||
response.status() == MPSOLVER_OPTIMAL) {
objective_value_ = response.objective_value();
best_objective_bound_ = response.best_objective_bound();
const size_t num_vars = solver_->variables_.size();
for (int var_id = 0; var_id < num_vars; ++var_id) {
MPVariable* const var = solver_->variables_[var_id];
var->set_solution_value(response.variable_value(var_id));
}
}
return result_status_;
}
bool SatInterface::InterruptSolve() {
interrupt_solve_ = true;
return true;
}
void SatInterface::Reset() { ResetExtractionInformation(); }
void SatInterface::SetOptimizationDirection(bool maximize) {
NonIncrementalChange();
}
void SatInterface::SetVariableBounds(int index, double lb, double ub) {
NonIncrementalChange();
}
void SatInterface::SetVariableInteger(int index, bool integer) {
NonIncrementalChange();
}
void SatInterface::SetConstraintBounds(int index, double lb, double ub) {
NonIncrementalChange();
}
void SatInterface::AddRowConstraint(MPConstraint* const ct) {
NonIncrementalChange();
}
void SatInterface::AddVariable(MPVariable* const var) {
NonIncrementalChange();
}
void SatInterface::SetCoefficient(MPConstraint* const constraint,
const MPVariable* const variable,
double new_value, double old_value) {
NonIncrementalChange();
}
void SatInterface::ClearConstraint(MPConstraint* const constraint) {
NonIncrementalChange();
}
void SatInterface::SetObjectiveCoefficient(const MPVariable* const variable,
double coefficient) {
NonIncrementalChange();
}
void SatInterface::SetObjectiveOffset(double value) { NonIncrementalChange(); }
void SatInterface::ClearObjective() { NonIncrementalChange(); }
int64 SatInterface::iterations() const {
return 0; // FIXME
}
int64 SatInterface::nodes() const { return 0; }
MPSolver::BasisStatus SatInterface::row_status(int constraint_index) const {
return MPSolver::BasisStatus::FREE; // FIXME
}
MPSolver::BasisStatus SatInterface::column_status(int variable_index) const {
return MPSolver::BasisStatus::FREE; // FIXME
}
bool SatInterface::IsContinuous() const { return false; }
bool SatInterface::IsLP() const { return false; }
bool SatInterface::IsMIP() const { return true; }
std::string SatInterface::SolverVersion() const {
return "SAT Based MIP Solver";
}
void* SatInterface::underlying_solver() { return nullptr; }
void SatInterface::ExtractNewVariables() { NonIncrementalChange(); }
void SatInterface::ExtractNewConstraints() { NonIncrementalChange(); }
void SatInterface::ExtractObjective() { NonIncrementalChange(); }
void SatInterface::SetParameters(const MPSolverParameters& param) {
// By default, we use 8 threads as it allows to try a good set of orthogonal
// parameters. This can be overridden by the user.
parameters_.set_num_search_workers(num_threads_);
parameters_.set_log_search_progress(!quiet_);
SetCommonParameters(param);
}
absl::Status SatInterface::SetNumThreads(int num_threads) {
num_threads_ = num_threads;
return absl::OkStatus();
}
// All these have no effect.
void SatInterface::SetPrimalTolerance(double value) {}
void SatInterface::SetDualTolerance(double value) {}
void SatInterface::SetScalingMode(int value) {}
void SatInterface::SetLpAlgorithm(int value) {}
void SatInterface::SetRelativeMipGap(double value) {}
// TODO(user): Implement me.
void SatInterface::SetPresolveMode(int value) {}
bool SatInterface::SetSolverSpecificParametersAsString(
const std::string& parameters) {
return ProtobufTextFormatMergeFromString(parameters, ¶meters_);
}
void SatInterface::NonIncrementalChange() {
// The current implementation is not incremental.
sync_status_ = MUST_RELOAD;
}
// Register Sat in the global linear solver factory.
MPSolverInterface* BuildSatInterface(MPSolver* const solver) {
return new SatInterface(solver);
}
} // namespace operations_research