OR-Tools  8.1
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 
20 #include "ortools/sat/model.h"
22 #include "ortools/sat/sat_base.h"
24 #include "ortools/sat/util.h"
25 #include "ortools/util/bitset.h"
28 
29 namespace operations_research {
30 namespace 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.
208  absl::StrongVector<BooleanVariable, bool> has_forced_polarity_;
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;
214  absl::StrongVector<BooleanVariable, bool> has_target_polarity_;
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 
232 } // namespace sat
233 } // namespace operations_research
234 
235 #endif // OR_TOOLS_SAT_SAT_DECISION_H_
var
IntVar * var
Definition: expr_array.cc:1858
integral_types.h
operations_research::sat::SatDecisionPolicy::SetStablePhase
void SetStablePhase(bool is_stable)
Definition: sat_decision.h:80
operations_research::sat::SatDecisionPolicy::Untrail
void Untrail(int target_trail_index)
Definition: sat_decision.cc:395
operations_research::sat::SatDecisionPolicy::NextBranch
Literal NextBranch()
Definition: sat_decision.cc:336
operations_research::sat::SatDecisionPolicy::IncreaseNumVariables
void IncreaseNumVariables(int num_variables)
Definition: sat_decision.cc:26
integer_pq.h
operations_research::sat::ModelRandomGenerator
Definition: sat/util.h:33
operations_research::sat::SatDecisionPolicy::AllPreferences
std::vector< std::pair< Literal, double > > AllPreferences() const
Definition: sat_decision.cc:263
weight
int64 weight
Definition: pack.cc:509
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
operations_research::sat::SatDecisionPolicy::SetAssignmentPreference
void SetAssignmentPreference(Literal literal, double weight)
Definition: sat_decision.cc:248
int64
int64_t int64
Definition: integral_types.h:34
random_engine.h
sat_base.h
pb_constraint.h
operations_research::sat::SatDecisionPolicy::MaybeEnablePhaseSaving
void MaybeEnablePhaseSaving(bool save_phase)
Definition: sat_decision.h:85
operations_research::sat::SatDecisionPolicy::ResetDecisionHeuristic
void ResetDecisionHeuristic()
Definition: sat_decision.cc:126
sat_parameters.pb.h
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::SatDecisionPolicy
Definition: sat_decision.h:34
operations_research::sat::SatDecisionPolicy::SatDecisionPolicy
SatDecisionPolicy(Model *model)
Definition: sat_decision.cc:21
operations_research::sat::SatDecisionPolicy::UpdateWeightedSign
void UpdateWeightedSign(const std::vector< LiteralWithCoeff > &terms, Coefficient rhs)
Definition: sat_decision.cc:277
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Literal
Definition: sat_base.h:64
absl::StrongVector< BooleanVariable, double >
util.h
operations_research::sat::SatDecisionPolicy::InStablePhase
bool InStablePhase() const
Definition: sat_decision.h:81
operations_research::sat::SatDecisionPolicy::BumpVariableActivities
void BumpVariableActivities(const std::vector< Literal > &literals)
Definition: sat_decision.cc:287
operations_research::glop::Index
int32 Index
Definition: lp_types.h:37
literal
Literal literal
Definition: optimization.cc:84
operations_research::sat::SatDecisionPolicy::BeforeConflict
void BeforeConflict(int trail_index)
Definition: sat_decision.cc:55
operations_research::sat::Trail
Definition: sat_base.h:233
bitset.h
operations_research::sat::SatDecisionPolicy::UpdateVariableActivityIncrement
void UpdateVariableActivityIncrement()
Definition: sat_decision.cc:332