OR-Tools  8.1
implied_bounds.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 #ifndef OR_TOOLS_SAT_IMPLIED_BOUNDS_H_
15 #define OR_TOOLS_SAT_IMPLIED_BOUNDS_H_
16 
17 #include <algorithm>
18 #include <vector>
19 
20 #include "absl/container/flat_hash_map.h"
21 #include "ortools/base/int_type.h"
23 #include "ortools/base/logging.h"
25 #include "ortools/sat/integer.h"
26 #include "ortools/sat/model.h"
27 #include "ortools/sat/sat_base.h"
28 #include "ortools/util/bitset.h"
29 
30 namespace operations_research {
31 namespace sat {
32 
33 // For each IntegerVariable, the ImpliedBound class allows to list all such
34 // entries.
35 //
36 // This is meant to be used in the cut generation code when it make sense: if we
37 // have BoolVar => X >= bound, we can always lower bound the variable X by
38 // (bound - X_lb) * BoolVar + X_lb, and that can lead to stronger cuts.
40  // An integer variable in [0, 1]. When at 1, then the IntegerVariable
41  // corresponding to this entry must be greater or equal to the given lower
42  // bound.
43  IntegerVariable literal_view = kNoIntegerVariable;
44  IntegerValue lower_bound = IntegerValue(0);
45 
46  // If false, it is when the literal_view is zero that the lower bound is
47  // valid.
48  bool is_positive = true;
49 
50  // These constructors are needed for OR-Tools.
51  ImpliedBoundEntry(IntegerVariable lit, IntegerValue lb, bool positive)
52  : literal_view(lit), lower_bound(lb), is_positive(positive) {}
53 
56 };
57 
58 // Maintains all the implications of the form Literal => IntegerLiteral. We
59 // collect these implication at model loading, during probing and during search.
60 //
61 // TODO(user): This can quickly use up too much memory. Add some limit in place.
62 // In particular, each time we have literal => integer_literal we should avoid
63 // storing the same integer_literal for all other_literal for which
64 // other_literal => literal. For this we need to interact with the
65 // BinaryImplicationGraph.
66 //
67 // TODO(user): This is a bit of a duplicate with the Literal <=> IntegerLiteral
68 // stored in the IntegerEncoder class. However we only need one side here.
69 //
70 // TODO(user): Do like in the DomainDeductions class and allow to process
71 // clauses (or store them) to perform more level zero deductions. Note that this
72 // is again a slight duplicate with what we do there (except that we work at the
73 // Domain level in that presolve class).
74 //
75 // TODO(user): Add an implied bound cut generator to add these simple
76 // constraints to the LP when needed.
78  public:
80  : parameters_(*model->GetOrCreate<SatParameters>()),
81  sat_solver_(model->GetOrCreate<SatSolver>()),
82  integer_trail_(model->GetOrCreate<IntegerTrail>()),
83  integer_encoder_(model->GetOrCreate<IntegerEncoder>()) {}
85 
86  // Adds literal => integer_literal to the repository.
87  //
88  // Not that it checks right aways if there is another bound on the same
89  // variable involving literal.Negated(), in which case we can improve the
90  // level zero lower bound of the variable.
91  void Add(Literal literal, IntegerLiteral integer_literal);
92 
93  // This must be called after first_decision has been enqueued and propagated.
94  // It will inspect the trail and add all new implied bounds.
95  //
96  // Preconditions: The decision level must be one (CHECKed). And the decision
97  // must be equal to first decision (we currently do not CHECK that).
98  void ProcessIntegerTrail(Literal first_decision);
99 
100  // Returns all the implied bounds stored for the given variable.
101  // Note that only literal with an IntegerView are considered here.
102  const std::vector<ImpliedBoundEntry>& GetImpliedBounds(IntegerVariable var);
103 
104  // Returns all the variables for which GetImpliedBounds(var) is not empty. Or
105  // at least that was not empty at some point, because we lazily remove bounds
106  // that become trivial as the search progress.
107  const std::vector<IntegerVariable>& VariablesWithImpliedBounds() const {
108  return has_implied_bounds_.PositionsSetAtLeastOnce();
109  }
110 
111  // Adds to the integer trail all the new level-zero deduction made here.
112  // This can only be called at decision level zero. Returns false iff the model
113  // is infeasible.
114  bool EnqueueNewDeductions();
115 
116  // When a literal does not have an integer view, we do not add any
117  // ImpliedBoundEntry. This allows to create missing entries for a literal for
118  // which a view was just created.
119  //
120  // TODO(user): Implement and call when we create new views in the linear
121  // relaxation.
123 
124  private:
125  const SatParameters& parameters_;
126  SatSolver* sat_solver_;
127  IntegerTrail* integer_trail_;
128  IntegerEncoder* integer_encoder_;
129 
130  // TODO(user): Remove the need for this.
131  std::vector<IntegerLiteral> tmp_integer_literals_;
132 
133  // For each (Literal, IntegerVariable) the best lower bound implied by this
134  // literal. Note that there is no need to store any entries that do not
135  // improve on the level zero lower bound.
136  //
137  // TODO(user): we could lazily remove old entries to save a bit of space if
138  // many deduction where made at level zero.
139  absl::flat_hash_map<std::pair<LiteralIndex, IntegerVariable>, IntegerValue>
140  bounds_;
141 
142  // Note(user): The plan is to use these during cut generation, so only the
143  // Literal with an IntegerView that can be used in the LP relaxation need to
144  // be kept here.
145  //
146  // TODO(user): Use inlined vectors.
147  std::vector<ImpliedBoundEntry> empty_implied_bounds_;
149  var_to_bounds_;
150 
151  // Track the list of variables with some implied bounds.
152  SparseBitset<IntegerVariable> has_implied_bounds_;
153 
154  // TODO(user): Ideally, this should go away if we manage to push level-zero
155  // fact at a positive level directly.
156  absl::StrongVector<IntegerVariable, IntegerValue> level_zero_lower_bounds_;
157  SparseBitset<IntegerVariable> new_level_zero_bounds_;
158 
159  // Stats.
160  int64 num_deductions_ = 0;
161  int64 num_enqueued_in_var_to_bounds_ = 0;
162 };
163 
164 } // namespace sat
165 } // namespace operations_research
166 
167 #endif // OR_TOOLS_SAT_IMPLIED_BOUNDS_H_
var
IntVar * var
Definition: expr_array.cc:1858
integral_types.h
operations_research::sat::IntegerTrail
Definition: integer.h:533
operations_research::sat::ImpliedBoundEntry::ImpliedBoundEntry
ImpliedBoundEntry(IntegerVariable lit, IntegerValue lb, bool positive)
Definition: implied_bounds.h:51
operations_research::sat::kNoIntegerVariable
const IntegerVariable kNoIntegerVariable(-1)
logging.h
operations_research::sat::SatSolver
Definition: sat_solver.h:58
model.h
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
int64
int64_t int64
Definition: integral_types.h:34
sat_base.h
operations_research::sat::ImpliedBounds::ImpliedBounds
ImpliedBounds(Model *model)
Definition: implied_bounds.h:79
operations_research::sat::ImpliedBoundEntry::literal_view
IntegerVariable literal_view
Definition: implied_bounds.h:43
operations_research::SparseBitset< IntegerVariable >
int_type.h
operations_research::SparseBitset::PositionsSetAtLeastOnce
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:815
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::ImpliedBoundEntry::is_positive
bool is_positive
Definition: implied_bounds.h:48
operations_research::sat::IntegerLiteral
Definition: integer.h:153
operations_research::sat::ImpliedBounds
Definition: implied_bounds.h:77
operations_research::sat::ImpliedBounds::NotifyNewIntegerView
void NotifyNewIntegerView(Literal literal)
Definition: implied_bounds.h:122
operations_research::sat::ImpliedBounds::EnqueueNewDeductions
bool EnqueueNewDeductions()
Definition: implied_bounds.cc:180
operations_research::sat::ImpliedBounds::Add
void Add(Literal literal, IntegerLiteral integer_literal)
Definition: implied_bounds.cc:27
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Literal
Definition: sat_base.h:64
operations_research::sat::ImpliedBoundEntry::lower_bound
IntegerValue lower_bound
Definition: implied_bounds.h:44
absl::StrongVector
Definition: strong_vector.h:76
operations_research::sat::ImpliedBounds::VariablesWithImpliedBounds
const std::vector< IntegerVariable > & VariablesWithImpliedBounds() const
Definition: implied_bounds.h:107
operations_research::sat::ImpliedBounds::GetImpliedBounds
const std::vector< ImpliedBoundEntry > & GetImpliedBounds(IntegerVariable var)
Definition: implied_bounds.cc:147
operations_research::sat::ImpliedBounds::~ImpliedBounds
~ImpliedBounds()
Definition: implied_bounds.cc:20
operations_research::sat::ImpliedBoundEntry::ImpliedBoundEntry
ImpliedBoundEntry()
Definition: implied_bounds.h:54
strong_vector.h
literal
Literal literal
Definition: optimization.cc:84
operations_research::sat::ImpliedBounds::ProcessIntegerTrail
void ProcessIntegerTrail(Literal first_decision)
Definition: implied_bounds.cc:169
operations_research::sat::IntegerEncoder
Definition: integer.h:276
integer.h
bitset.h
operations_research::sat::ImpliedBoundEntry
Definition: implied_bounds.h:39