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
"
22
#include "
ortools/base/integral_types.h
"
23
#include "
ortools/base/logging.h
"
24
#include "
ortools/base/strong_vector.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.
39
struct
ImpliedBoundEntry
{
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
54
ImpliedBoundEntry
()
55
:
literal_view
(
kNoIntegerVariable
),
lower_bound
(0),
is_positive
(true) {}
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.
77
class
ImpliedBounds
{
78
public
:
79
explicit
ImpliedBounds
(
Model
*
model
)
80
: parameters_(*
model
->GetOrCreate<SatParameters>()),
81
sat_solver_(
model
->GetOrCreate<
SatSolver
>()),
82
integer_trail_(
model
->GetOrCreate<
IntegerTrail
>()),
83
integer_encoder_(
model
->GetOrCreate<
IntegerEncoder
>()) {}
84
~ImpliedBounds
();
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.
122
void
NotifyNewIntegerView
(
Literal
literal
) {}
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_;
148
absl::StrongVector<IntegerVariable, std::vector<ImpliedBoundEntry>
>
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
ortools
sat
implied_bounds.h
Generated by
1.8.20