OR-Tools  8.2
bop_util.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_util.h"
15 
16 #include <limits>
17 #include <vector>
18 
21 #include "ortools/bop/bop_base.h"
24 #include "ortools/sat/sat_solver.h"
25 
26 namespace operations_research {
27 namespace bop {
28 namespace {
29 static const int kMaxLubyIndex = 30;
30 static const int kMaxBoost = 30;
31 
32 // Loads the problem state into the SAT solver. If the problem has already been
33 // loaded in the sat_solver, fixed variables and objective bounds are updated.
34 // Returns false when the problem is proved UNSAT.
35 bool InternalLoadStateProblemToSatSolver(const ProblemState& problem_state,
36  sat::SatSolver* sat_solver) {
37  const bool first_time = (sat_solver->NumVariables() == 0);
38  if (first_time) {
39  sat_solver->SetNumVariables(
40  problem_state.original_problem().num_variables());
41  } else {
42  // Backtrack the solver to be able to add new constraints.
43  sat_solver->Backtrack(0);
44  }
45 
46  // Set the fixed variables first so that loading the problem will be faster.
47  for (VariableIndex var(0); var < problem_state.is_fixed().size(); ++var) {
48  if (problem_state.is_fixed()[var]) {
49  if (!sat_solver->AddUnitClause(
50  sat::Literal(sat::BooleanVariable(var.value()),
51  problem_state.fixed_values()[var]))) {
52  return false;
53  }
54  }
55  }
56 
57  // Load the problem if not done yet.
58  if (first_time &&
59  !LoadBooleanProblem(problem_state.original_problem(), sat_solver)) {
60  return false;
61  }
62 
63  // Constrain the objective cost to be greater or equal to the lower bound,
64  // and to be smaller than the upper bound. If enforcing the strictier upper
65  // bound constraint leads to an UNSAT problem, it means the current solution
66  // is proved optimal (if the solution is feasible, else the problem is proved
67  // infeasible).
69  problem_state.original_problem(),
70  problem_state.lower_bound() != std::numeric_limits<int64_t>::min(),
71  sat::Coefficient(problem_state.lower_bound()),
72  problem_state.upper_bound() != std::numeric_limits<int64_t>::max(),
73  sat::Coefficient(problem_state.upper_bound() - 1), sat_solver)) {
74  return false;
75  }
76 
77  // Adds the new binary clauses.
78  sat_solver->TrackBinaryClauses(true);
79  if (!sat_solver->AddBinaryClauses(problem_state.NewlyAddedBinaryClauses())) {
80  return false;
81  }
82  sat_solver->ClearNewlyAddedBinaryClauses();
83 
84  return true;
85 }
86 } // anonymous namespace
87 
89  const ProblemState& problem_state, sat::SatSolver* sat_solver) {
90  if (InternalLoadStateProblemToSatSolver(problem_state, sat_solver)) {
92  }
93 
94  return problem_state.solution().IsFeasible()
97 }
98 
100  LearnedInfo* info) {
101  CHECK(nullptr != solver);
102  CHECK(nullptr != info);
103 
104  // This should never be called if the problem is UNSAT.
105  CHECK(!solver->IsModelUnsat());
106 
107  // Fixed variables.
108  info->fixed_literals.clear();
109  const sat::Trail& propagation_trail = solver->LiteralTrail();
110  const int root_size = solver->CurrentDecisionLevel() == 0
111  ? propagation_trail.Index()
112  : solver->Decisions().front().trail_index;
113  for (int trail_index = 0; trail_index < root_size; ++trail_index) {
114  info->fixed_literals.push_back(propagation_trail[trail_index]);
115  }
116 
117  // Binary clauses.
118  info->binary_clauses = solver->NewlyAddedBinaryClauses();
120 }
121 
123  BopSolution* solution) {
124  CHECK(solution != nullptr);
125 
126  // Only extract the variables of the initial problem.
127  CHECK_LE(solution->Size(), assignment.NumberOfVariables());
128  for (sat::BooleanVariable var(0); var < solution->Size(); ++var) {
129  CHECK(assignment.VariableIsAssigned(var));
130  const bool value = assignment.LiteralIsTrue(sat::Literal(var, true));
131  const VariableIndex bop_var_id(var.value());
132  solution->SetValue(bop_var_id, value);
133  }
134 }
135 
136 //------------------------------------------------------------------------------
137 // AdaptiveParameterValue
138 //------------------------------------------------------------------------------
140  : value_(initial_value), num_changes_(0) {}
141 
142 void AdaptiveParameterValue::Reset() { num_changes_ = 0; }
143 
145  ++num_changes_;
146  const double factor = 1.0 + 1.0 / (num_changes_ / 2.0 + 1);
147  value_ = std::min(1.0 - (1.0 - value_) / factor, value_ * factor);
148 }
149 
151  ++num_changes_;
152  const double factor = 1.0 + 1.0 / (num_changes_ / 2.0 + 1);
153  value_ = std::max(value_ / factor, 1.0 - (1.0 - value_) * factor);
154 }
155 
156 //------------------------------------------------------------------------------
157 // LubyAdaptiveParameterValue
158 //------------------------------------------------------------------------------
160  : luby_id_(0),
161  luby_boost_(0),
162  luby_value_(0),
163  difficulties_(kMaxLubyIndex, AdaptiveParameterValue(initial_value)) {
164  Reset();
165 }
166 
168  luby_id_ = 0;
169  luby_boost_ = 0;
170  luby_value_ = 0;
171  for (int i = 0; i < difficulties_.size(); ++i) {
172  difficulties_[i].Reset();
173  }
174 }
175 
177  const int luby_msb = MostSignificantBitPosition64(luby_value_);
178  difficulties_[luby_msb].Increase();
179 }
180 
182  const int luby_msb = MostSignificantBitPosition64(luby_value_);
183  difficulties_[luby_msb].Decrease();
184 }
185 
187  const int luby_msb = MostSignificantBitPosition64(luby_value_);
188  return difficulties_[luby_msb].value();
189 }
190 
192  ++luby_boost_;
193  return luby_boost_ >= kMaxBoost;
194 }
195 
197  ++luby_id_;
198  luby_value_ = sat::SUniv(luby_id_) << luby_boost_;
199 }
200 } // namespace bop
201 } // 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 CHECK_LE(val1, val2)
Definition: base/logging.h:699
void SetValue(VariableIndex var, bool value)
Definition: bop_solution.h:39
const BopSolution & solution() const
Definition: bop_base.h:196
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
const std::vector< BinaryClause > & NewlyAddedBinaryClauses()
Definition: sat_solver.cc:932
const std::vector< Decision > & Decisions() const
Definition: sat_solver.h:359
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
int64 value
IntVar * var
Definition: expr_array.cc:1858
BopOptimizerBase::Status LoadStateProblemToSatSolver(const ProblemState &problem_state, sat::SatSolver *sat_solver)
Definition: bop_util.cc:88
void SatAssignmentToBopSolution(const sat::VariablesAssignment &assignment, BopSolution *solution)
Definition: bop_util.cc:122
void ExtractLearnedInfoFromSatSolver(sat::SatSolver *solver, LearnedInfo *info)
Definition: bop_util.cc:99
bool AddObjectiveConstraint(const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver *solver)
bool LoadBooleanProblem(const LinearBooleanProblem &problem, SatSolver *solver)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int MostSignificantBitPosition64(uint64 n)
Definition: bitset.h:231
std::vector< sat::Literal > fixed_literals
Definition: bop_base.h:266
std::vector< sat::BinaryClause > binary_clauses
Definition: bop_base.h:281