OR-Tools  8.2
bop_base.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 <cstdint>
17#include <limits>
18#include <string>
19#include <vector>
20
21#include "absl/synchronization/mutex.h"
23
24namespace operations_research {
25namespace bop {
26
27using ::operations_research::sat::LinearBooleanProblem;
28using ::operations_research::sat::LinearObjective;
29
31 : name_(name), stats_(name) {
33}
34
37}
38
40 switch (status) {
42 return "OPTIMAL_SOLUTION_FOUND";
43 case SOLUTION_FOUND:
44 return "SOLUTION_FOUND";
45 case INFEASIBLE:
46 return "INFEASIBLE";
47 case LIMIT_REACHED:
48 return "LIMIT_REACHED";
50 return "INFORMATION_FOUND";
51 case CONTINUE:
52 return "CONTINUE";
53 case ABORT:
54 return "ABORT";
55 }
56 // Fallback. We don't use "default:" so the compiler will return an error
57 // if we forgot one enum case above.
58 LOG(DFATAL) << "Invalid Status " << static_cast<int>(status);
59 return "UNKNOWN Status";
60}
61
62//------------------------------------------------------------------------------
63// ProblemState
64//------------------------------------------------------------------------------
66
67ProblemState::ProblemState(const LinearBooleanProblem& problem)
68 : original_problem_(problem),
69 parameters_(),
70 update_stamp_(kInitialStampValue + 1),
71 is_fixed_(problem.num_variables(), false),
72 fixed_values_(problem.num_variables(), false),
73 lp_values_(),
74 solution_(problem, "AllZero"),
75 assignment_preference_(),
76 lower_bound_(std::numeric_limits<int64_t>::min()),
77 upper_bound_(std::numeric_limits<int64_t>::max()) {
78 // TODO(user): Extract to a function used by all solvers.
79 // Compute trivial unscaled lower bound.
80 const LinearObjective& objective = problem.objective();
81 lower_bound_ = 0;
82 for (int i = 0; i < objective.coefficients_size(); ++i) {
83 // Fix template version for or-tools.
84 lower_bound_ += std::min<int64_t>(int64_t{0}, objective.coefficients(i));
85 }
86 upper_bound_ = solution_.IsFeasible() ? solution_.GetCost()
88}
89
90// TODO(user): refactor this to not rely on the optimization status.
91// All the information can be encoded in the learned_info bounds.
93 const LearnedInfo& learned_info,
94 BopOptimizerBase::Status optimization_status) {
95 const std::string kIndent(25, ' ');
96
97 bool new_lp_values = false;
98 if (!learned_info.lp_values.empty()) {
99 if (lp_values_ != learned_info.lp_values) {
100 lp_values_ = learned_info.lp_values;
101 new_lp_values = true;
102 VLOG(1) << kIndent + "New LP values.";
103 }
104 }
105
106 bool new_binary_clauses = false;
107 if (!learned_info.binary_clauses.empty()) {
108 const int old_num = binary_clause_manager_.NumClauses();
109 for (sat::BinaryClause c : learned_info.binary_clauses) {
110 const int num_vars = original_problem_.num_variables();
111 if (c.a.Variable() < num_vars && c.b.Variable() < num_vars) {
112 binary_clause_manager_.Add(c);
113 }
114 }
115 if (binary_clause_manager_.NumClauses() > old_num) {
116 new_binary_clauses = true;
117 VLOG(1) << kIndent + "Num binary clauses: "
118 << binary_clause_manager_.NumClauses();
119 }
120 }
121
122 bool new_solution = false;
123 if (learned_info.solution.IsFeasible() &&
124 (!solution_.IsFeasible() ||
125 learned_info.solution.GetCost() < solution_.GetCost())) {
126 solution_ = learned_info.solution;
127 new_solution = true;
128 VLOG(1) << kIndent + "New solution.";
129 }
130
131 bool new_lower_bound = false;
132 if (learned_info.lower_bound > lower_bound()) {
133 lower_bound_ = learned_info.lower_bound;
134 new_lower_bound = true;
135 VLOG(1) << kIndent + "New lower bound.";
136 }
137
138 if (solution_.IsFeasible()) {
139 upper_bound_ = std::min(upper_bound(), solution_.GetCost());
140 if (upper_bound() <= lower_bound() ||
141 (upper_bound() - lower_bound() <=
142 parameters_.relative_gap_limit() *
143 std::max(std::abs(upper_bound()), std::abs(lower_bound())))) {
144 // The lower bound might be greater that the cost of a feasible solution
145 // due to rounding errors in the problem scaling and Glop.
146 // As a feasible solution was found, the solution is proved optimal.
148 }
149 }
150
151 // Merge fixed variables. Note that variables added during search, i.e. not
152 // in the original problem, are ignored.
153 int num_newly_fixed_variables = 0;
154 for (const sat::Literal literal : learned_info.fixed_literals) {
155 const VariableIndex var(literal.Variable().value());
156 if (var >= original_problem_.num_variables()) {
157 continue;
158 }
159 const bool value = literal.IsPositive();
160 if (is_fixed_[var]) {
161 if (fixed_values_[var] != value) {
163 return true;
164 }
165 } else {
166 is_fixed_[var] = true;
167 fixed_values_[var] = value;
168 ++num_newly_fixed_variables;
169 }
170 }
171 if (num_newly_fixed_variables > 0) {
172 int num_fixed_variables = 0;
173 for (const bool is_fixed : is_fixed_) {
174 if (is_fixed) {
175 ++num_fixed_variables;
176 }
177 }
178 VLOG(1) << kIndent << num_newly_fixed_variables
179 << " newly fixed variables (" << num_fixed_variables << " / "
180 << is_fixed_.size() << ").";
181 if (num_fixed_variables == is_fixed_.size()) {
182 // Set the solution to the fixed variables.
183 BopSolution fixed_solution = solution_;
184 for (VariableIndex var(0); var < is_fixed_.size(); ++var) {
185 fixed_solution.SetValue(var, fixed_values_[var]);
186 }
187 if (fixed_solution.IsFeasible()) {
188 solution_ = fixed_solution;
189 }
190 if (solution_.IsFeasible()) {
192 VLOG(1) << kIndent << "Optimal";
193 } else {
195 }
196 }
197 }
198
199 bool known_status = false;
200 if (optimization_status == BopOptimizerBase::OPTIMAL_SOLUTION_FOUND) {
202 known_status = true;
203 } else if (optimization_status == BopOptimizerBase::INFEASIBLE) {
205 known_status = true;
206 }
207
208 const bool updated = new_lp_values || new_binary_clauses || new_solution ||
209 new_lower_bound || num_newly_fixed_variables > 0 ||
210 known_status;
211 if (updated) ++update_stamp_;
212 return updated;
213}
214
216 LearnedInfo learned_info(original_problem_);
217 for (VariableIndex var(0); var < is_fixed_.size(); ++var) {
218 if (is_fixed_[var]) {
219 learned_info.fixed_literals.push_back(
220 sat::Literal(sat::BooleanVariable(var.value()), fixed_values_[var]));
221 }
222 }
223 learned_info.solution = solution_;
224 learned_info.lower_bound = lower_bound();
225 learned_info.lp_values = lp_values_;
227
228 return learned_info;
229}
230
232 CHECK(solution_.IsFeasible());
233 lower_bound_ = upper_bound();
234 ++update_stamp_;
235}
236
238 // Mark as infeasible, i.e. set a lower_bound greater than the upper_bound.
239 CHECK(!solution_.IsFeasible());
241 lower_bound_ = std::numeric_limits<int64_t>::max();
242 upper_bound_ = std::numeric_limits<int64_t>::max() - 1;
243 } else {
244 lower_bound_ = upper_bound_ - 1;
245 }
246 ++update_stamp_;
247}
248
249const std::vector<sat::BinaryClause>& ProblemState::NewlyAddedBinaryClauses()
250 const {
251 return binary_clause_manager_.newly_added();
252}
253
255 binary_clause_manager_.ClearNewlyAdded();
256}
257
258} // namespace bop
259} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define LOG(severity)
Definition: base/logging.h:420
#define VLOG(verboselevel)
Definition: base/logging.h:978
size_type size() const
bool empty() const
std::string StatString() const
Definition: stats.cc:71
static std::string GetStatusString(Status status)
Definition: bop_base.cc:39
BopOptimizerBase(const std::string &name)
Definition: bop_base.cc:30
void SetValue(VariableIndex var, bool value)
Definition: bop_solution.h:39
bool MergeLearnedInfo(const LearnedInfo &learned_info, BopOptimizerBase::Status optimization_status)
Definition: bop_base.cc:92
const std::vector< sat::BinaryClause > & NewlyAddedBinaryClauses() const
Definition: bop_base.cc:249
LearnedInfo GetLearnedInfo() const
Definition: bop_base.cc:215
static const int64_t kInitialStampValue
Definition: bop_base.h:155
const absl::StrongVector< VariableIndex, bool > & is_fixed() const
Definition: bop_base.h:176
ProblemState(const sat::LinearBooleanProblem &problem)
Definition: bop_base.cc:67
const std::vector< BinaryClause > & newly_added() const
Definition: clause.h:403
BooleanVariable Variable() const
Definition: sat_base.h:80
const std::string name
int64 value
IntVar * var
Definition: expr_array.cc:1858
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
STL namespace.
Literal literal
Definition: optimization.cc:84
#define IF_STATS_ENABLED(instructions)
Definition: stats.h:437
#define SCOPED_TIME_STAT(stats)
Definition: stats.h:438
std::vector< sat::Literal > fixed_literals
Definition: bop_base.h:266
std::vector< sat::BinaryClause > binary_clauses
Definition: bop_base.h:281