OR-Tools  8.2
restart.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_RESTART_H_
15#define OR_TOOLS_SAT_RESTART_H_
16
17#include <vector>
18
19#include "ortools/sat/model.h"
21#include "ortools/sat/sat_parameters.pb.h"
22#include "ortools/util/bitset.h"
24
25namespace operations_research {
26namespace sat {
27
28// Contain the logic to decide when to restart a SAT tree search.
30 public:
32 : parameters_(*(model->GetOrCreate<SatParameters>())),
33 decision_policy_(model->GetOrCreate<SatDecisionPolicy>()) {
34 Reset();
35 }
36
37 // Resets the policy using the current model parameters.
38 void Reset();
39
40 // Returns true if the solver should be restarted before the next decision is
41 // taken. Note that this will return true just once and then assumes that
42 // the search was restarted and starts worrying about the next restart.
43 bool ShouldRestart();
44
45 // This will be called by the solver engine after each conflict. The arguments
46 // reflect the state of the solver when the conflict was detected and before
47 // the backjump.
48 void OnConflict(int conflict_trail_index, int conflict_decision_level,
49 int conflict_lbd);
50
51 // Returns the number of restarts since the last Reset().
52 int NumRestarts() const { return num_restarts_; }
53
54 // Returns a string with the current restart statistics.
55 std::string InfoString() const;
56
57 private:
58 const SatParameters& parameters_;
59 SatDecisionPolicy* decision_policy_;
60
61 int num_restarts_;
62 int conflicts_until_next_strategy_change_;
63 int strategy_change_conflicts_;
64
65 int strategy_counter_;
66 std::vector<SatParameters::RestartAlgorithm> strategies_;
67
68 int luby_count_;
69 int conflicts_until_next_restart_;
70
71 RunningAverage dl_running_average_;
72 RunningAverage lbd_running_average_;
73 RunningAverage trail_size_running_average_;
74};
75
76// Returns the ith element of the strategy S^univ proposed by M. Luby et al. in
77// Optimal Speedup of Las Vegas Algorithms, Information Processing Letters 1993.
78// This is used to decide the number of conflicts allowed before the next
79// restart. This method, used by most SAT solvers, is usually referenced as
80// Luby.
81// Returns 2^{k-1} when i == 2^k - 1
82// and SUniv(i - 2^{k-1} + 1) when 2^{k-1} <= i < 2^k - 1.
83// The sequence is defined for i > 0 and starts with:
84// {1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, ...}
85inline int SUniv(int i) {
86 DCHECK_GT(i, 0);
87 while (i > 2) {
88 const int most_significant_bit_position =
90 if ((1 << most_significant_bit_position) == i + 1) {
91 return 1 << (most_significant_bit_position - 1);
92 }
93 i -= (1 << most_significant_bit_position) - 1;
94 }
95 return 1;
96}
97
98} // namespace sat
99} // namespace operations_research
100
101#endif // OR_TOOLS_SAT_RESTART_H_
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
void OnConflict(int conflict_trail_index, int conflict_decision_level, int conflict_lbd)
Definition: restart.cc:144
GRBmodel * model
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int MostSignificantBitPosition64(uint64 n)
Definition: bitset.h:231