forked from google/or-tools
-
Notifications
You must be signed in to change notification settings - Fork 0
/
implied_bounds.h
157 lines (135 loc) · 6.2 KB
/
implied_bounds.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#ifndef OR_TOOLS_SAT_IMPLIED_BOUNDS_H_
#define OR_TOOLS_SAT_IMPLIED_BOUNDS_H_
#include <algorithm>
#include <vector>
#include "absl/container/flat_hash_map.h"
#include "ortools/base/int_type.h"
#include "ortools/base/int_type_indexed_vector.h"
#include "ortools/base/integral_types.h"
#include "ortools/base/logging.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
#include "ortools/util/bitset.h"
namespace operations_research {
namespace sat {
// For each IntegerVariable, the ImpliedBound class allows to list all such
// entries.
//
// This is meant to be used in the cut generation code when it make sense: if we
// have BoolVar => X >= bound, we can always lower bound the variable X by
// (bound - X_lb) * BoolVar + X_lb, and that can lead to stronger cuts.
struct ImpliedBoundEntry {
// An integer variable in [0, 1]. When at 1, then the IntegerVariable
// corresponding to this entry must be greater or equal to the given lower
// bound.
IntegerVariable literal_view = kNoIntegerVariable;
IntegerValue lower_bound = IntegerValue(0);
// If false, it is when the literal_view is zero that the lower bound is
// valid.
bool is_positive = true;
// These constructors are needed for OR-Tools.
ImpliedBoundEntry(IntegerVariable lit, IntegerValue lb, bool positive)
: literal_view(lit), lower_bound(lb), is_positive(positive) {}
ImpliedBoundEntry()
: literal_view(kNoIntegerVariable), lower_bound(0), is_positive(true) {}
};
// Maintains all the implications of the form Literal => IntegerLiteral. We
// collect these implication at model loading, during probing and during search.
//
// TODO(user): This can quickly use up too much memory. Add some limit in place.
// In particular, each time we have literal => integer_literal we should avoid
// storing the same integer_literal for all other_literal for which
// other_literal => literal. For this we need to interact with the
// BinaryImplicationGraph.
//
// TODO(user): This is a bit of a duplicate with the Literal <=> IntegerLiteral
// stored in the IntegerEncoder class. However we only need one side here.
//
// TODO(user): Do like in the DomainDeductions class and allow to process
// clauses (or store them) to perform more level zero deductions. Note that this
// is again a slight duplicate with what we do there (except that we work at the
// Domain level in that presolve class).
//
// TODO(user): Add an implied bound cut generator to add these simple
// constraints to the LP when needed.
class ImpliedBounds {
public:
explicit ImpliedBounds(Model* model)
: parameters_(*model->GetOrCreate<SatParameters>()),
sat_solver_(model->GetOrCreate<SatSolver>()),
integer_trail_(model->GetOrCreate<IntegerTrail>()),
integer_encoder_(model->GetOrCreate<IntegerEncoder>()) {}
~ImpliedBounds();
// Adds literal => integer_literal to the repository.
//
// Not that it checks right aways if there is another bound on the same
// variable involving literal.Negated(), in which case we can improve the
// level zero lower bound of the variable.
void Add(Literal literal, IntegerLiteral integer_literal);
// This must be called after first_decision has been enqueued and propagated.
// It will inspect the trail and add all new implied bounds.
//
// Preconditions: The decision level must be one (CHECKed). And the decision
// must be equal to first decision (we currently do not CHECK that).
void ProcessIntegerTrail(Literal first_decision);
// Returns all the implied bounds stored for the given variable.
// Note that only literal with an IntegerView are considered here.
const std::vector<ImpliedBoundEntry>& GetImpliedBounds(IntegerVariable var);
// Adds to the integer trail all the new level-zero deduction made here.
// This can only be called at decision level zero. Returns false iff the model
// is infeasible.
bool EnqueueNewDeductions();
// When a literal does not have an integer view, we do not add any
// ImpliedBoundEntry. This allows to create missing entries for a literal for
// which a view was just created.
//
// TODO(user): Implement and call when we create new views in the linear
// relaxation.
void NotifyNewIntegerView(Literal literal) {}
private:
const SatParameters& parameters_;
SatSolver* sat_solver_;
IntegerTrail* integer_trail_;
IntegerEncoder* integer_encoder_;
// TODO(user): Remove the need for this.
std::vector<IntegerLiteral> tmp_integer_literals_;
// For each (Literal, IntegerVariable) the best lower bound implied by this
// literal. Note that there is no need to store any entries that do not
// improve on the level zero lower bound.
//
// TODO(user): we could lazily remove old entries to save a bit of space if
// many deduction where made at level zero.
absl::flat_hash_map<std::pair<LiteralIndex, IntegerVariable>, IntegerValue>
bounds_;
// Note(user): The plan is to use these during cut generation, so only the
// Literal with an IntegerView that can be used in the LP relaxation need to
// be kept here.
//
// TODO(user): Use inlined vectors.
std::vector<ImpliedBoundEntry> empty_implied_bounds_;
gtl::ITIVector<IntegerVariable, std::vector<ImpliedBoundEntry>>
var_to_bounds_;
// TODO(user): Ideally, this should go away if we manage to push level-zero
// fact at a positive level directly.
gtl::ITIVector<IntegerVariable, IntegerValue> level_zero_lower_bounds_;
SparseBitset<IntegerVariable> new_level_zero_bounds_;
// Stats.
int64 num_deductions_ = 0;
int64 num_enqueued_in_var_to_bounds_ = 0;
};
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_IMPLIED_BOUNDS_H_