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 
14 #include "ortools/bop/bop_base.h"
15 
16 #include <cstdint>
17 #include <limits>
18 #include <string>
19 #include <vector>
20 
21 #include "absl/synchronization/mutex.h"
23 
24 namespace operations_research {
25 namespace bop {
26 
27 using ::operations_research::sat::LinearBooleanProblem;
28 using ::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";
49  case INFORMATION_FOUND:
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 //------------------------------------------------------------------------------
65 const int64_t ProblemState::kInitialStampValue(0);
66 
67 ProblemState::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.
147  MarkAsOptimal();
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()) {
191  MarkAsOptimal();
192  VLOG(1) << kIndent << "Optimal";
193  } else {
195  }
196  }
197  }
198 
199  bool known_status = false;
200  if (optimization_status == BopOptimizerBase::OPTIMAL_SOLUTION_FOUND) {
201  MarkAsOptimal();
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_;
226  learned_info.binary_clauses = NewlyAddedBinaryClauses();
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 
249 const 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
ProblemState(const sat::LinearBooleanProblem &problem)
Definition: bop_base.cc:67
const absl::StrongVector< VariableIndex, bool > & is_fixed() const
Definition: bop_base.h:176
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...
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