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 
18 #include "ortools/bop/bop_util.h"
20 
21 namespace operations_research {
22 namespace 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 
36 BopOptimizerBase::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 
69 sat::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 sat::LinearBooleanProblem & original_problem() const
Definition: bop_base.h:201
const BopSolution & solution() const
Definition: bop_base.h:196
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
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
const Coefficient kCoefficientMax(std::numeric_limits< Coefficient::ValueType >::max())
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