OR-Tools  8.2
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"
25#include "ortools/sat/integer.h"
26#include "ortools/sat/model.h"
28#include "ortools/util/bitset.h"
29
30namespace operations_research {
31namespace 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.
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.
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.
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_
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:813
const std::vector< ImpliedBoundEntry > & GetImpliedBounds(IntegerVariable var)
void NotifyNewIntegerView(Literal literal)
void Add(Literal literal, IntegerLiteral integer_literal)
const std::vector< IntegerVariable > & VariablesWithImpliedBounds() const
void ProcessIntegerTrail(Literal first_decision)
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
const IntegerVariable kNoIntegerVariable(-1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
ImpliedBoundEntry()
bool is_positive
ImpliedBoundEntry(IntegerVariable lit, IntegerValue lb, bool positive)
IntegerValue lower_bound
IntegerVariable literal_view