OR-Tools  8.2
complete_optimizer.h
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 // This file contains some BopOptimizerBase implementations that are "complete"
15 // solvers. That is, they work on the full problem, and can solve the problem
16 // (and prove optimality) by themselves. Moreover, they can be run for short
17 // period of time and resumed later from the state they where left off.
18 //
19 // The idea is that it is worthwhile spending some time in these algorithms,
20 // because in some situation they can improve the current upper/lower bound or
21 // even solve the problem to optimality.
22 //
23 // Note(user): The GuidedSatFirstSolutionGenerator can also be used as a
24 // complete SAT solver provided that we keep running it after it has found a
25 // first solution. This is the default behavior of the kNotGuided policy.
26 
27 #ifndef OR_TOOLS_BOP_COMPLETE_OPTIMIZER_H_
28 #define OR_TOOLS_BOP_COMPLETE_OPTIMIZER_H_
29 
30 #include <cstdint>
31 #include <deque>
32 
33 #include "ortools/bop/bop_base.h"
35 #include "ortools/bop/bop_types.h"
36 #include "ortools/sat/boolean_problem.pb.h"
37 #include "ortools/sat/encoding.h"
38 #include "ortools/sat/sat_solver.h"
39 
40 namespace operations_research {
41 namespace bop {
42 
43 // TODO(user): Merge this with the code in sat/optimization.cc
45  public:
46  explicit SatCoreBasedOptimizer(const std::string& name);
47  ~SatCoreBasedOptimizer() override;
48 
49  protected:
50  bool ShouldBeRun(const ProblemState& problem_state) const override;
51  Status Optimize(const BopParameters& parameters,
52  const ProblemState& problem_state, LearnedInfo* learned_info,
53  TimeLimit* time_limit) override;
54 
55  private:
56  BopOptimizerBase::Status SynchronizeIfNeeded(
57  const ProblemState& problem_state);
58  sat::SatSolver::Status SolveWithAssumptions();
59 
60  int64_t state_update_stamp_;
61  bool initialized_;
62  bool assumptions_already_added_;
63  sat::SatSolver solver_;
64  sat::Coefficient offset_;
65  sat::Coefficient lower_bound_;
66  sat::Coefficient upper_bound_;
67  sat::Coefficient stratified_lower_bound_;
68  std::deque<sat::EncodingNode> repository_;
69  std::vector<sat::EncodingNode*> nodes_;
70 };
71 
72 } // namespace bop
73 } // namespace operations_research
74 
75 #endif // OR_TOOLS_BOP_COMPLETE_OPTIMIZER_H_
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 std::string & name() const
Definition: bop_base.h:49
bool ShouldBeRun(const ProblemState &problem_state) const override
Status Optimize(const BopParameters &parameters, const ProblemState &problem_state, LearnedInfo *learned_info, TimeLimit *time_limit) override
SatParameters parameters
SharedTimeLimit * time_limit
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...