OR-Tools  8.2
sat_decision.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_SAT_DECISION_H_
15#define OR_TOOLS_SAT_SAT_DECISION_H_
16
17#include <vector>
18
21#include "ortools/sat/model.h"
24#include "ortools/sat/sat_parameters.pb.h"
25#include "ortools/sat/util.h"
26#include "ortools/util/bitset.h"
28
29namespace operations_research {
30namespace sat {
31
32// Implement the SAT branching policy responsible for deciding the next Boolean
33// variable to branch on, and its polarity (true or false).
35 public:
36 explicit SatDecisionPolicy(Model* model);
37
38 // Notifies that more variables are now present. Note that currently this may
39 // change the current variable order because the priority queue need to be
40 // reconstructed.
41 void IncreaseNumVariables(int num_variables);
42
43 // Reinitializes the decision heuristics (which variables to choose with which
44 // polarity) according to the current parameters. Note that this also resets
45 // the activity of the variables to 0. Note that this function is lazy, and
46 // the work will only happen on the first NextBranch() to cover the cases when
47 // this policy is not used at all.
49
50 // Returns next decision to branch upon. This shouldn't be called if all the
51 // variables are assigned.
53
54 // Updates statistics about literal occurences in constraints.
55 // Input is a canonical linear constraint of the form (terms <= rhs).
56 void UpdateWeightedSign(const std::vector<LiteralWithCoeff>& terms,
57 Coefficient rhs);
58
59 // Bumps the activity of all variables appearing in the conflict. All literals
60 // must be currently assigned. See VSIDS decision heuristic: Chaff:
61 // Engineering an Efficient SAT Solver. M.W. Moskewicz et al. ANNUAL ACM IEEE
62 // DESIGN AUTOMATION CONFERENCE 2001.
63 void BumpVariableActivities(const std::vector<Literal>& literals);
64
65 // Updates the increment used for activity bumps. This is basically the same
66 // as decaying all the variable activities, but it is a lot more efficient.
68
69 // Called on Untrail() so that we can update the set of possible decisions.
70 void Untrail(int target_trail_index);
71
72 // Called on a new conflict before Untrail(). The trail before the given index
73 // is used in the phase saving heuristic as a partial assignment.
74 void BeforeConflict(int trail_index);
75
76 // By default, we alternate between a stable phase (better suited for finding
77 // SAT solution) and a more restart heavy phase more suited for proving UNSAT.
78 // This changes a bit the polarity heuristics and is controlled from within
79 // SatRestartPolicy.
80 void SetStablePhase(bool is_stable) { in_stable_phase_ = is_stable; }
81 bool InStablePhase() const { return in_stable_phase_; }
82
83 // This is used to temporarily disable phase_saving when we do some probing
84 // during search for instance.
85 void MaybeEnablePhaseSaving(bool save_phase) {
86 maybe_enable_phase_saving_ = save_phase;
87 }
88
89 // Gives a hint so the solver tries to find a solution with the given literal
90 // set to true. Currently this take precedence over the phase saving heuristic
91 // and a variable with a preference will always be branched on according to
92 // this preference.
93 //
94 // The weight is used as a tie-breaker between variable with the same
95 // activities. Larger weight will be selected first. A weight of zero is the
96 // default value for the other variables.
97 //
98 // Note(user): Having a lot of different weights may slow down the priority
99 // queue operations if there is millions of variables.
101
102 // Returns the vector of the current assignment preferences.
103 std::vector<std::pair<Literal, double>> AllPreferences() const;
104
105 private:
106 // Computes an initial variable ordering.
107 void InitializeVariableOrdering();
108
109 // Rescales activity value of all variables when one of them reached the max.
110 void RescaleVariableActivities(double scaling_factor);
111
112 // Reinitializes the inital polarity of all the variables with an index
113 // greater than or equal to the given one.
114 void ResetInitialPolarity(int from, bool inverted = false);
115
116 // Code used for resetting the initial polarity at the beginning of each
117 // phase.
118 void RephaseIfNeeded();
119 void UseLongestAssignmentAsInitialPolarity();
120 void FlipCurrentPolarity();
121 void RandomizeCurrentPolarity();
122
123 // Adds the given variable to var_ordering_ or updates its priority if it is
124 // already present.
125 void PqInsertOrUpdate(BooleanVariable var);
126
127 // Singleton model objects.
128 const SatParameters& parameters_;
129 const Trail& trail_;
130 ModelRandomGenerator* random_;
131
132 // Variable ordering (priority will be adjusted dynamically). queue_elements_
133 // holds the elements used by var_ordering_ (it uses pointers).
134 //
135 // Note that we recover the variable that a WeightedVarQueueElement refers to
136 // by its position in the queue_elements_ vector, and we can recover the later
137 // using (pointer - &queue_elements_[0]).
138 struct WeightedVarQueueElement {
139 // Interface for the IntegerPriorityQueue.
140 int Index() const { return var.value(); }
141
142 // Priority order. The IntegerPriorityQueue returns the largest element
143 // first.
144 //
145 // Note(user): We used to also break ties using the variable index, however
146 // this has two drawbacks:
147 // - On problem with many variables, this slow down quite a lot the priority
148 // queue operations (which do as little work as possible and hence benefit
149 // from having the majority of elements with a priority of 0).
150 // - It seems to be a bad heuristics. One reason could be that the priority
151 // queue will automatically diversify the choice of the top variables
152 // amongst the ones with the same priority.
153 //
154 // Note(user): For the same reason as explained above, it is probably a good
155 // idea not to have too many different values for the tie_breaker field. I
156 // am not even sure we should have such a field...
157 bool operator<(const WeightedVarQueueElement& other) const {
158 return weight < other.weight ||
159 (weight == other.weight && (tie_breaker < other.tie_breaker));
160 }
161
162 BooleanVariable var;
163 float tie_breaker;
164
165 // TODO(user): Experiment with float. In the rest of the code, we use
166 // double, but maybe we don't need that much precision. Using float here may
167 // save memory and make the PQ operations faster.
168 double weight;
169 };
170 static_assert(sizeof(WeightedVarQueueElement) == 16,
171 "ERROR_WeightedVarQueueElement_is_not_well_compacted");
172
173 bool var_ordering_is_initialized_ = false;
174 IntegerPriorityQueue<WeightedVarQueueElement> var_ordering_;
175
176 // This is used for the branching heuristic described in "Learning Rate Based
177 // Branching Heuristic for SAT solvers", J.H.Liang, V. Ganesh, P. Poupart,
178 // K.Czarnecki, SAT 2016.
179 //
180 // The entries are sorted by trail index, and one can get the number of
181 // conflicts during which a variable at a given trail index i was assigned by
182 // summing the entry.count for all entries with a trail index greater than i.
183 struct NumConflictsStackEntry {
184 int trail_index;
185 int64 count;
186 };
187 int64 num_conflicts_ = 0;
188 std::vector<NumConflictsStackEntry> num_conflicts_stack_;
189
190 // Whether the priority of the given variable needs to be updated in
191 // var_ordering_. Note that this is only accessed for assigned variables and
192 // that for efficiency it is indexed by trail indices. If
193 // pq_need_update_for_var_at_trail_index_[trail_->Info(var).trail_index] is
194 // true when we untrail var, then either var need to be inserted in the queue,
195 // or we need to notify that its priority has changed.
196 BitQueue64 pq_need_update_for_var_at_trail_index_;
197
198 // Increment used to bump the variable activities.
199 double variable_activity_increment_ = 1.0;
200
201 // Stores variable activity and the number of time each variable was "bumped".
202 // The later is only used with the ERWA heuristic.
206
207 // If the polarity if forced (externally) we alway use this first.
210
211 // If we are in a stable phase, we follow the current target.
212 bool in_stable_phase_ = false;
213 int target_length_ = 0;
216
217 // Otherwise we follow var_polarity_ which is reset at the beginning of
218 // each new polarity phase. This is also overwritten by phase saving.
219 // Each phase last for an arithmetically increasing number of conflicts.
221 bool maybe_enable_phase_saving_ = true;
222 int64 polarity_phase_ = 0;
223 int64 num_conflicts_until_rephase_ = 1000;
224
225 // The longest partial assignment since the last reset.
226 std::vector<Literal> best_partial_assignment_;
227
228 // Used in initial polarity computation.
230
231 // Used in InitializeVariableOrdering().
232 std::vector<BooleanVariable> tmp_variables_;
233};
234
235} // namespace sat
236} // namespace operations_research
237
238#endif // OR_TOOLS_SAT_SAT_DECISION_H_
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
std::vector< std::pair< Literal, double > > AllPreferences() const
void IncreaseNumVariables(int num_variables)
Definition: sat_decision.cc:26
void SetAssignmentPreference(Literal literal, double weight)
void MaybeEnablePhaseSaving(bool save_phase)
Definition: sat_decision.h:85
void Untrail(int target_trail_index)
void BumpVariableActivities(const std::vector< Literal > &literals)
void UpdateWeightedSign(const std::vector< LiteralWithCoeff > &terms, Coefficient rhs)
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int64 weight
Definition: pack.cc:509