OR-Tools  8.2
complete_optimizer.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
20
21namespace operations_research {
22namespace bop {
23
26 state_update_stamp_(ProblemState::kInitialStampValue),
27 initialized_(false),
28 assumptions_already_added_(false) {
29 // This is in term of number of variables not at their minimal value.
30 lower_bound_ = sat::Coefficient(0);
31 upper_bound_ = sat::kCoefficientMax;
32}
33
35
36BopOptimizerBase::Status SatCoreBasedOptimizer::SynchronizeIfNeeded(
37 const ProblemState& problem_state) {
38 if (state_update_stamp_ == problem_state.update_stamp()) {
40 }
41 state_update_stamp_ = problem_state.update_stamp();
42
43 // Note that if the solver is not empty, this only load the newly learned
44 // information.
45 const BopOptimizerBase::Status status =
46 LoadStateProblemToSatSolver(problem_state, &solver_);
47 if (status != BopOptimizerBase::CONTINUE) return status;
48
49 if (!initialized_) {
50 // Initialize the algorithm.
52 problem_state.original_problem().objective(), &offset_, &repository_);
53 initialized_ = true;
54
55 // This is used by the "stratified" approach.
56 stratified_lower_bound_ = sat::Coefficient(0);
57 for (sat::EncodingNode* n : nodes_) {
58 stratified_lower_bound_ = std::max(stratified_lower_bound_, n->weight());
59 }
60 }
61
62 // Extract the new upper bound.
63 if (problem_state.solution().IsFeasible()) {
64 upper_bound_ = problem_state.solution().GetCost() + offset_;
65 }
67}
68
69sat::SatSolver::Status SatCoreBasedOptimizer::SolveWithAssumptions() {
70 const std::vector<sat::Literal> assumptions =
72 stratified_lower_bound_,
73 &lower_bound_, &nodes_, &solver_);
74 return solver_.ResetAndSolveWithGivenAssumptions(assumptions);
75}
76
77// Only run this if there is an objective.
79 const ProblemState& problem_state) const {
80 return problem_state.original_problem().objective().literals_size() > 0;
81}
82
84 const BopParameters& parameters, const ProblemState& problem_state,
85 LearnedInfo* learned_info, TimeLimit* time_limit) {
87 CHECK(learned_info != nullptr);
88 CHECK(time_limit != nullptr);
89 learned_info->Clear();
90
91 const BopOptimizerBase::Status sync_status =
92 SynchronizeIfNeeded(problem_state);
93 if (sync_status != BopOptimizerBase::CONTINUE) {
94 return sync_status;
95 }
96
97 int64_t conflict_limit = parameters.max_number_of_conflicts_in_random_lns();
98 double deterministic_time_at_last_sync = solver_.deterministic_time();
99 while (!time_limit->LimitReached()) {
100 sat::SatParameters sat_params = solver_.parameters();
101 sat_params.set_max_time_in_seconds(time_limit->GetTimeLeft());
102 sat_params.set_max_deterministic_time(
103 time_limit->GetDeterministicTimeLeft());
104 sat_params.set_random_seed(parameters.random_seed());
105 sat_params.set_max_number_of_conflicts(conflict_limit);
106 solver_.SetParameters(sat_params);
107
108 const int64_t old_num_conflicts = solver_.num_failures();
109 const sat::SatSolver::Status sat_status =
110 assumptions_already_added_ ? solver_.Solve() : SolveWithAssumptions();
111 time_limit->AdvanceDeterministicTime(solver_.deterministic_time() -
112 deterministic_time_at_last_sync);
113 deterministic_time_at_last_sync = solver_.deterministic_time();
114
115 assumptions_already_added_ = true;
116 conflict_limit -= solver_.num_failures() - old_num_conflicts;
117 learned_info->lower_bound = lower_bound_.value() - offset_.value();
118
119 // This is possible because we over-constrain the objective.
120 if (sat_status == sat::SatSolver::INFEASIBLE) {
121 return problem_state.solution().IsFeasible()
124 }
125
126 ExtractLearnedInfoFromSatSolver(&solver_, learned_info);
127 if (sat_status == sat::SatSolver::LIMIT_REACHED || conflict_limit < 0) {
129 }
130 if (sat_status == sat::SatSolver::FEASIBLE) {
131 stratified_lower_bound_ =
132 MaxNodeWeightSmallerThan(nodes_, stratified_lower_bound_);
133
134 // We found a better solution!
135 SatAssignmentToBopSolution(solver_.Assignment(), &learned_info->solution);
136 if (stratified_lower_bound_ > 0) {
137 assumptions_already_added_ = false;
139 }
141 }
142
143 // The interesting case: we have a core.
144 // TODO(user): Check that this cannot fail because of the conflict limit.
145 std::vector<sat::Literal> core = solver_.GetLastIncompatibleDecisions();
146 sat::MinimizeCore(&solver_, &core);
147
148 const sat::Coefficient min_weight = sat::ComputeCoreMinWeight(nodes_, core);
149 sat::ProcessCore(core, min_weight, &repository_, &nodes_, &solver_);
150 assumptions_already_added_ = false;
151 }
153}
154
155} // namespace bop
156} // namespace operations_research
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
const BopSolution & solution() const
Definition: bop_base.h:196
const sat::LinearBooleanProblem & original_problem() const
Definition: bop_base.h:201
bool ShouldBeRun(const ProblemState &problem_state) const override
Status Optimize(const BopParameters &parameters, const ProblemState &problem_state, LearnedInfo *learned_info, TimeLimit *time_limit) override
const SatParameters & parameters() const
Definition: sat_solver.cc:110
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions)
Definition: sat_solver.cc:947
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
void SetParameters(const SatParameters &parameters)
Definition: sat_solver.cc:115
std::vector< Literal > GetLastIncompatibleDecisions()
Definition: sat_solver.cc:1272
SatParameters parameters
SharedTimeLimit * time_limit
const std::string name
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
Coefficient ComputeCoreMinWeight(const std::vector< EncodingNode * > &nodes, const std::vector< Literal > &core)
Definition: encoding.cc:418
std::vector< Literal > ReduceNodesAndExtractAssumptions(Coefficient upper_bound, Coefficient stratified_lower_bound, Coefficient *lower_bound, std::vector< EncodingNode * > *nodes, SatSolver *solver)
Definition: encoding.cc:366
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
Definition: sat_solver.cc:2547
void ProcessCore(const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver)
Definition: encoding.cc:445
const Coefficient kCoefficientMax(std::numeric_limits< Coefficient::ValueType >::max())
Coefficient MaxNodeWeightSmallerThan(const std::vector< EncodingNode * > &nodes, Coefficient upper_bound)
Definition: encoding.cc:433
std::vector< EncodingNode * > CreateInitialEncodingNodes(const std::vector< Literal > &literals, const std::vector< Coefficient > &coeffs, Coefficient *offset, std::deque< EncodingNode > *repository)
Definition: encoding.cc:302
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
#define SCOPED_TIME_STAT(stats)
Definition: stats.h:438