OR-Tools  8.2
sat/util.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_UTIL_H_
15 #define OR_TOOLS_SAT_UTIL_H_
16 
17 #include <deque>
18 
19 #include "absl/random/bit_gen_ref.h"
20 #include "absl/random/random.h"
21 #include "ortools/sat/model.h"
22 #include "ortools/sat/sat_base.h"
23 #include "ortools/sat/sat_parameters.pb.h"
25 
26 #if !defined(__PORTABLE_PLATFORM__)
27 #include "google/protobuf/descriptor.h"
28 #endif // __PORTABLE_PLATFORM__
29 
30 namespace operations_research {
31 namespace sat {
32 
33 // The model "singleton" random engine used in the solver.
34 //
35 // In test, we usually set use_absl_random() so that the sequence is changed at
36 // each invocation. This way, clients do not relly on the wrong assumption that
37 // a particular optimal solution will be returned if they are many equivalent
38 // ones.
39 class ModelRandomGenerator : public absl::BitGenRef {
40  public:
41  // We seed the strategy at creation only. This should be enough for our use
42  // case since the SatParameters is set first before the solver is created. We
43  // also never really need to change the seed afterwards, it is just used to
44  // diversify solves with identical parameters on different Model objects.
46  : absl::BitGenRef(deterministic_random_) {
47  const auto& params = *model->GetOrCreate<SatParameters>();
48  deterministic_random_.seed(params.random_seed());
49  if (params.use_absl_random()) {
50  absl_random_ = absl::BitGen(absl::SeedSeq({params.random_seed()}));
51  absl::BitGenRef::operator=(absl::BitGenRef(absl_random_));
52  }
53  }
54 
55  // This is just used to display ABSL_RANDOM_SALT_OVERRIDE in the log so that
56  // it is possible to reproduce a failure more easily while looking at a solver
57  // log.
58  //
59  // TODO(user): I didn't find a cleaner way to log this.
60  void LogSalt() const {}
61 
62  private:
63  random_engine_t deterministic_random_;
64  absl::BitGen absl_random_;
65 };
66 
67 // Randomizes the decision heuristic of the given SatParameters.
68 template <typename URBG>
69 void RandomizeDecisionHeuristic(URBG* random, SatParameters* parameters);
70 
71 // Context: this function is not really generic, but required to be unit-tested.
72 // It is used in a clause minimization algorithm when we try to detect if any of
73 // the clause literals can be propagated by a subset of the other literal being
74 // false. For that, we want to enqueue in the solver all the subset of size n-1.
75 //
76 // This moves one of the unprocessed literal from literals to the last position.
77 // The function tries to do that while preserving the longest possible prefix of
78 // literals "amortized" through the calls assuming that we want to move each
79 // literal to the last position once.
80 //
81 // For a vector of size n, if we want to call this n times so that each literal
82 // is last at least once, the sum of the size of the changed suffixes will be
83 // O(n log n). If we were to use a simpler algorithm (like moving the last
84 // unprocessed literal to the last position), this sum would be O(n^2).
85 //
86 // Returns the size of the common prefix of literals before and after the move,
87 // or -1 if all the literals are already processed. The argument
88 // relevant_prefix_size is used as a hint when keeping more that this prefix
89 // size do not matter. The returned value will always be lower or equal to
90 // relevant_prefix_size.
91 int MoveOneUnprocessedLiteralLast(const std::set<LiteralIndex>& processed,
92  int relevant_prefix_size,
93  std::vector<Literal>* literals);
94 
95 // ============================================================================
96 // Implementation.
97 // ============================================================================
98 
99 template <typename URBG>
100 inline void RandomizeDecisionHeuristic(URBG* random,
101  SatParameters* parameters) {
102 #if !defined(__PORTABLE_PLATFORM__)
103  // Random preferred variable order.
104  const google::protobuf::EnumDescriptor* order_d =
105  SatParameters::VariableOrder_descriptor();
106  parameters->set_preferred_variable_order(
107  static_cast<SatParameters::VariableOrder>(
108  order_d->value(absl::Uniform(*random, 0, order_d->value_count()))
109  ->number()));
110 
111  // Random polarity initial value.
112  const google::protobuf::EnumDescriptor* polarity_d =
113  SatParameters::Polarity_descriptor();
114  parameters->set_initial_polarity(static_cast<SatParameters::Polarity>(
115  polarity_d->value(absl::Uniform(*random, 0, polarity_d->value_count()))
116  ->number()));
117 #endif // __PORTABLE_PLATFORM__
118  // Other random parameters.
119  parameters->set_use_phase_saving(absl::Bernoulli(*random, 0.5));
120  parameters->set_random_polarity_ratio(absl::Bernoulli(*random, 0.5) ? 0.01
121  : 0.0);
122  parameters->set_random_branches_ratio(absl::Bernoulli(*random, 0.5) ? 0.01
123  : 0.0);
124 }
125 
126 // Manages incremental averages.
128  public:
129  // Initializes the average with 'initial_average' and number of records to 0.
130  explicit IncrementalAverage(double initial_average)
131  : average_(initial_average) {}
133 
134  // Sets the number of records to 0 and average to 'reset_value'.
135  void Reset(double reset_value);
136 
137  double CurrentAverage() const { return average_; }
138  int64 NumRecords() const { return num_records_; }
139 
140  void AddData(double new_record);
141 
142  private:
143  double average_ = 0.0;
144  int64 num_records_ = 0;
145 };
146 
147 // Manages exponential moving averages defined as
148 // new_average = decaying_factor * old_average
149 // + (1 - decaying_factor) * new_record.
150 // where 0 < decaying_factor < 1.
152  public:
153  explicit ExponentialMovingAverage(double decaying_factor)
154  : decaying_factor_(decaying_factor) {
155  DCHECK_GE(decaying_factor, 0.0);
156  DCHECK_LE(decaying_factor, 1.0);
157  }
158 
159  // Returns exponential moving average for all the added data so far.
160  double CurrentAverage() const { return average_; }
161 
162  // Returns the total number of added records so far.
163  int64 NumRecords() const { return num_records_; }
164 
165  void AddData(double new_record);
166 
167  private:
168  double average_ = 0.0;
169  int64 num_records_ = 0;
170  const double decaying_factor_;
171 };
172 
173 // Utility to calculate percentile (First variant) for limited number of
174 // records. Reference: https://en.wikipedia.org/wiki/Percentile
175 //
176 // After the vector is sorted, we assume that the element with index i
177 // correspond to the percentile 100*(i+0.5)/size. For percentiles before the
178 // first element (resp. after the last one) we return the first element (resp.
179 // the last). And otherwise we do a linear interpolation between the two element
180 // around the asked percentile.
181 class Percentile {
182  public:
183  explicit Percentile(int record_limit) : record_limit_(record_limit) {}
184 
185  void AddRecord(double record);
186 
187  // Returns number of stored records.
188  int64 NumRecords() const { return records_.size(); }
189 
190  // Note that this is not fast and runs in O(n log n) for n records.
191  double GetPercentile(double percent);
192 
193  private:
194  std::deque<double> records_;
195  const int record_limit_;
196 };
197 
198 // This method tries to compress a list of tuples by merging complementary
199 // tuples, that is a set of tuples that only differ on one variable, and that
200 // cover the domain of the variable. In that case, it will keep only one tuple,
201 // and replace the value for variable by any_value, the equivalent of '*' in
202 // regexps.
203 //
204 // This method is exposed for testing purposes.
205 void CompressTuples(absl::Span<const int64> domain_sizes, int64 any_value,
206  std::vector<std::vector<int64>>* tuples);
207 
208 } // namespace sat
209 } // namespace operations_research
210 
211 #endif // OR_TOOLS_SAT_UTIL_H_
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
ExponentialMovingAverage(double decaying_factor)
Definition: sat/util.h:153
IncrementalAverage(double initial_average)
Definition: sat/util.h:130
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
double GetPercentile(double percent)
Definition: sat/util.cc:87
void AddRecord(double record)
Definition: sat/util.cc:80
SatParameters parameters
GRBmodel * model
int64_t int64
Definition: cleanup.h:22
int MoveOneUnprocessedLiteralLast(const std::set< LiteralIndex > &processed, int relevant_prefix_size, std::vector< Literal > *literals)
Definition: sat/util.cc:24
void RandomizeDecisionHeuristic(URBG *random, SatParameters *parameters)
Definition: sat/util.h:100
void CompressTuples(absl::Span< const int64 > domain_sizes, int64 any_value, std::vector< std::vector< int64 >> *tuples)
Definition: sat/util.cc:112
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::mt19937 random_engine_t
Definition: random_engine.h:23