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
15
16#include <limits>
17#include <vector>
18
25
26namespace operations_research {
27namespace bop {
28namespace {
29static const int kMaxLubyIndex = 30;
30static 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.
35bool 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
142void 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 std::vector< BinaryClause > & NewlyAddedBinaryClauses()
Definition: sat_solver.cc:932
const std::vector< Decision > & Decisions() const
Definition: sat_solver.h:359
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
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