OR-Tools  8.0
bop_ls.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 // This file defines the needed classes to efficiently perform Local Search in
15 // Bop.
16 // Local Search is a technique used to locally improve an existing solution by
17 // flipping a limited number of variables. To be successful the produced
18 // solution has to satisfy all constraints of the problem and improve the
19 // objective cost.
20 //
21 // The class BopLocalSearchOptimizer is the only public interface for Local
22 // Search in Bop. For unit-testing purposes this file also contains the four
23 // internal classes AssignmentAndConstraintFeasibilityMaintainer,
24 // OneFlipConstraintRepairer, SatWrapper and LocalSearchAssignmentIterator.
25 // They are implementation details and should not be used outside of bop_ls.
26 
27 #ifndef OR_TOOLS_BOP_BOP_LS_H_
28 #define OR_TOOLS_BOP_BOP_LS_H_
29 
30 #include <array>
31 
32 #include "absl/container/flat_hash_map.h"
33 #include "absl/container/flat_hash_set.h"
34 #include "absl/random/random.h"
35 #include "ortools/base/hash.h"
36 #include "ortools/base/random.h"
37 #include "ortools/bop/bop_base.h"
39 #include "ortools/bop/bop_types.h"
41 #include "ortools/sat/sat_solver.h"
42 
43 namespace operations_research {
44 namespace bop {
45 
46 // This class is used to ease the connection with the SAT solver.
47 //
48 // TODO(user): remove? the meat of the logic is used in just one place, so I am
49 // not sure having this extra layer improve the readability.
50 class SatWrapper {
51  public:
52  explicit SatWrapper(sat::SatSolver* sat_solver);
53 
54  // Returns the current state of the solver propagation trail.
55  std::vector<sat::Literal> FullSatTrail() const;
56 
57  // Returns true if the problem is UNSAT.
58  // Note that an UNSAT problem might not be marked as UNSAT at first because
59  // the SAT solver is not able to prove it; After some decisions / learned
60  // conflicts, the SAT solver might be able to prove UNSAT and so this will
61  // return true.
62  bool IsModelUnsat() const { return sat_solver_->IsModelUnsat(); }
63 
64  // Return the current solver VariablesAssignment.
66  return sat_solver_->Assignment();
67  }
68 
69  // Applies the decision that makes the given literal true and returns the
70  // number of decisions to backtrack due to conflicts if any.
71  // Two cases:
72  // - No conflicts: Returns 0 and fills the propagated_literals with the
73  // literals that have been propagated due to the decision including the
74  // the decision itself.
75  // - Conflicts: Returns the number of decisions to backtrack (the current
76  // decision included, i.e. returned value > 0) and fills the
77  // propagated_literals with the literals that the conflicts propagated.
78  // Note that the decision variable should not be already assigned in SAT.
79  int ApplyDecision(sat::Literal decision_literal,
80  std::vector<sat::Literal>* propagated_literals);
81 
82  // Backtracks the last decision if any.
83  void BacktrackOneLevel();
84 
85  // Bactracks all the decisions.
86  void BacktrackAll();
87 
88  // Extracts any new information learned during the search.
89  void ExtractLearnedInfo(LearnedInfo* info);
90 
91  // Returns a deterministic number that should be correlated with the time
92  // spent in the SAT wrapper. The order of magnitude should be close to the
93  // time in seconds.
94  double deterministic_time() const;
95 
96  private:
97  sat::SatSolver* sat_solver_;
98  DISALLOW_COPY_AND_ASSIGN(SatWrapper);
99 };
100 
101 // Forward declaration.
102 class LocalSearchAssignmentIterator;
103 
104 // This class defines a Local Search optimizer. The goal is to find a new
105 // solution with a better cost than the given solution by iterating on all
106 // assignments that can be reached in max_num_decisions decisions or less.
107 // The bop parameter max_number_of_explored_assignments_per_try_in_ls can be
108 // used to specify the number of new assignments to iterate on each time the
109 // method Optimize() is called. Limiting that parameter allows to reduce the
110 // time spent in the Optimize() method at once, and still explore all the
111 // reachable assignments (if Optimize() is called enough times).
112 // Note that due to propagation, the number of variables with a different value
113 // in the new solution can be greater than max_num_decisions.
115  public:
116  LocalSearchOptimizer(const std::string& name, int max_num_decisions,
117  sat::SatSolver* sat_propagator);
118  ~LocalSearchOptimizer() override;
119 
120  private:
121  bool ShouldBeRun(const ProblemState& problem_state) const override;
122  Status Optimize(const BopParameters& parameters,
123  const ProblemState& problem_state, LearnedInfo* learned_info,
124  TimeLimit* time_limit) override;
125 
126  int64 state_update_stamp_;
127 
128  // Maximum number of decisions the Local Search can take.
129  // Note that there is no limit on the number of changed variables due to
130  // propagation.
131  const int max_num_decisions_;
132 
133  // A wrapper around the given sat_propagator.
134  SatWrapper sat_wrapper_;
135 
136  // Iterator on all reachable assignments.
137  // Note that this iterator is only reset when Synchronize() is called, i.e.
138  // the iterator continues its iteration of the next assignments each time
139  // Optimize() is called until everything is explored or a solution is found.
140  std::unique_ptr<LocalSearchAssignmentIterator> assignment_iterator_;
141 };
142 
143 //------------------------------------------------------------------------------
144 // Implementation details. The declarations of those utility classes are in
145 // the .h for testing reasons.
146 //------------------------------------------------------------------------------
147 
148 // Maintains some information on a sparse set of integers in [0, n). More
149 // specifically this class:
150 // - Allows to dynamically add/remove element from the set.
151 // - Has a backtracking support.
152 // - Maintains the number of elements in the set.
153 // - Maintains a superset of the elements of the set that contains all the
154 // modified elements.
155 template <typename IntType>
157  public:
159 
160  // Prepares the class for integers in [0, n) and initializes the set to the
161  // empty one. Note that this run in O(n). Once resized, it is better to call
162  // BacktrackAll() instead of this to clear the set.
163  void ClearAndResize(IntType n);
164 
165  // Changes the state of the given integer i to be either inside or outside the
166  // set. Important: this should only be called with the opposite state of the
167  // current one, otherwise size() will not be correct.
168  void ChangeState(IntType i, bool should_be_inside);
169 
170  // Returns the current number of elements in the set.
171  // Note that this is not its maximum size n.
172  int size() const { return size_; }
173 
174  // Returns a superset of the current set of integers.
175  const std::vector<IntType>& Superset() const { return stack_; }
176 
177  // BacktrackOneLevel() backtracks to the state the class was in when the
178  // last AddBacktrackingLevel() was called. BacktrackAll() just restore the
179  // class to its state just after the last ClearAndResize().
180  void AddBacktrackingLevel();
181  void BacktrackOneLevel();
182  void BacktrackAll();
183 
184  private:
185  int size_;
186 
187  // Contains the elements whose status has been changed at least once.
188  std::vector<IntType> stack_;
189  std::vector<bool> in_stack_;
190 
191  // Used for backtracking. Contains the size_ and the stack_.size() at the time
192  // of each call to AddBacktrackingLevel() that is not yet backtracked over.
193  std::vector<int> saved_sizes_;
194  std::vector<int> saved_stack_sizes_;
195 };
196 
197 // A simple and efficient class to hash a given set of integers in [0, n).
198 // It uses O(n) memory and produces a good hash (random linear function).
199 template <typename IntType>
201  public:
202  NonOrderedSetHasher() : random_("Random seed") {}
203 
204  // Initializes the NonOrderedSetHasher to hash sets of integer in [0, n).
205  void Initialize(int size) {
206  hashes_.resize(size);
207  for (IntType i(0); i < size; ++i) {
208  hashes_[i] = random_.Rand64();
209  }
210  }
211 
212  // Ignores the given set element in all subsequent hash computation. Note that
213  // this will be reset by the next call to Initialize().
214  void IgnoreElement(IntType e) { hashes_[e] = 0; }
215 
216  // Returns the hash of the given set. The hash is independent of the set
217  // order, but there must be no duplicate element in the set. This uses a
218  // simple random linear function which has really good hashing properties.
219  uint64 Hash(const std::vector<IntType>& set) const {
220  uint64 hash = 0;
221  for (const IntType i : set) hash ^= hashes_[i];
222  return hash;
223  }
224 
225  // The hash of a set is simply the XOR of all its elements. This allows
226  // to compute an hash incrementally or without the need of a vector<>.
227  uint64 Hash(IntType e) const { return hashes_[e]; }
228 
229  // Returns true if Initialize() has been called with a non-zero size.
230  bool IsInitialized() const { return !hashes_.empty(); }
231 
232  private:
233  MTRandom random_;
235 };
236 
237 // This class is used to incrementally maintain an assignment and the
238 // feasibility of the constraints of a given LinearBooleanProblem.
239 //
240 // The current assignment is initialized using a feasible reference solution,
241 // i.e. the reference solution satisfies all the constraints of the problem.
242 // The current assignment is updated using the Assign() method.
243 //
244 // Note that the current assignment is not a solution in the sense that it
245 // might not be feasible, ie. violates some constraints.
246 //
247 // The assignment can be accessed at any time using Assignment().
248 // The set of infeasible constraints can be accessed at any time using
249 // PossiblyInfeasibleConstraints().
250 //
251 // Note that this class is reversible, i.e. it is possible to backtrack to
252 // previously added backtracking levels.
253 // levels. Consider for instance variable a, b, c, and d.
254 // Method called Assigned after method call
255 // 1- Assign({a, b}) a b
256 // 2- AddBacktrackingLevel() a b |
257 // 3- Assign({c}) a b | c
258 // 4- Assign({d}) a b | c d
259 // 5- BacktrackOneLevel() a b
260 // 6- Assign({c}) a b c
261 // 7- BacktrackOneLevel()
263  public:
264  // Note that the constraint indices used in this class are not the same as
265  // the one used in the given LinearBooleanProblem here.
267  const sat::LinearBooleanProblem& problem);
268 
269  // When we construct the problem, we treat the objective as one constraint.
270  // This is the index of this special "objective" constraint.
271  static const ConstraintIndex kObjectiveConstraint;
272 
273  // Sets a new reference solution and reverts all internal structures to their
274  // initial state. Note that the reference solution has to be feasible.
275  void SetReferenceSolution(const BopSolution& reference_solution);
276 
277  // Behaves exactly like SetReferenceSolution() where the passed reference
278  // is the current assignment held by this class. Note that the current
279  // assignment must be feasible (i.e. IsFeasible() is true).
281 
282  // Assigns all literals. That updates the assignment, the constraint values,
283  // and the infeasible constraints.
284  // Note that the assignment of those literals can be reverted thanks to
285  // AddBacktrackingLevel() and BacktrackOneLevel().
286  // Note that a variable can't be assigned twice, even for the same literal.
287  void Assign(const std::vector<sat::Literal>& literals);
288 
289  // Adds a new backtracking level to specify the state that will be restored
290  // by BacktrackOneLevel().
291  // See the example in the class comment.
292  void AddBacktrackingLevel();
293 
294  // Backtracks internal structures to the previous level defined by
295  // AddBacktrackingLevel(). As a consequence the state will be exactly as
296  // before the previous call to AddBacktrackingLevel().
297  // Note that backtracking the initial state has no effect.
298  void BacktrackOneLevel();
299  void BacktrackAll();
300 
301  // This returns the list of literal that appear in exactly all the current
302  // infeasible constraints (ignoring the objective) and correspond to a flip in
303  // a good direction for all the infeasible constraint. Performing this flip
304  // may repair the problem without any propagations.
305  //
306  // Important: The returned reference is only valid until the next
307  // PotentialOneFlipRepairs() call.
308  const std::vector<sat::Literal>& PotentialOneFlipRepairs();
309 
310  // Returns true if there is no infeasible constraint in the current state.
311  bool IsFeasible() const { return infeasible_constraint_set_.size() == 0; }
312 
313  // Returns the *exact* number of infeasible constraints.
314  // Note that PossiblyInfeasibleConstraints() will potentially return a larger
315  // number of constraints.
317  return infeasible_constraint_set_.size();
318  }
319 
320  // Returns a superset of all the infeasible constraints in the current state.
321  const std::vector<ConstraintIndex>& PossiblyInfeasibleConstraints() const {
322  return infeasible_constraint_set_.Superset();
323  }
324 
325  // Returns the number of constraints of the problem, objective included,
326  // i.e. the number of constraint in the problem + 1.
327  size_t NumConstraints() const { return constraint_lower_bounds_.size(); }
328 
329  // Returns the value of the var in the assignment.
330  // As the assignment is initialized with the reference solution, if the
331  // variable has not been assigned through Assign(), the returned value is
332  // the value of the variable in the reference solution.
333  bool Assignment(VariableIndex var) const { return assignment_.Value(var); }
334 
335  // Returns the current assignment.
336  const BopSolution& reference() const { return reference_; }
337 
338  // Returns the lower bound of the constraint.
339  int64 ConstraintLowerBound(ConstraintIndex constraint) const {
340  return constraint_lower_bounds_[constraint];
341  }
342 
343  // Returns the upper bound of the constraint.
344  int64 ConstraintUpperBound(ConstraintIndex constraint) const {
345  return constraint_upper_bounds_[constraint];
346  }
347 
348  // Returns the value of the constraint. The value is computed using the
349  // variable values in the assignment. Note that a constraint is feasible iff
350  // its value is between its two bounds (inclusive).
351  int64 ConstraintValue(ConstraintIndex constraint) const {
352  return constraint_values_[constraint];
353  }
354 
355  // Returns true if the given constraint is currently feasible.
356  bool ConstraintIsFeasible(ConstraintIndex constraint) const {
357  const int64 value = ConstraintValue(constraint);
358  return value >= ConstraintLowerBound(constraint) &&
359  value <= ConstraintUpperBound(constraint);
360  }
361 
362  std::string DebugString() const;
363 
364  private:
365  // This is lazily called by PotentialOneFlipRepairs() once.
366  void InitializeConstraintSetHasher();
367 
368  // This is used by PotentialOneFlipRepairs(). It encodes a ConstraintIndex
369  // together with a "repair" direction depending on the bound that make a
370  // constraint infeasible. An "up" direction means that the constraint activity
371  // is lower than the lower bound and we need to make the activity move up to
372  // fix the infeasibility.
373  DEFINE_INT_TYPE(ConstraintIndexWithDirection, int32);
374  ConstraintIndexWithDirection FromConstraintIndex(ConstraintIndex index,
375  bool up) const {
376  return ConstraintIndexWithDirection(2 * index.value() + (up ? 1 : 0));
377  }
378 
379  // Over constrains the objective cost by the given delta. This should only be
380  // called on a feasible reference solution and a fully backtracked state.
381  void MakeObjectiveConstraintInfeasible(int delta);
382 
383  // Local structure to represent the sparse matrix by variable used for fast
384  // update of the contraint values.
385  struct ConstraintEntry {
386  ConstraintEntry(ConstraintIndex c, int64 w) : constraint(c), weight(w) {}
387  ConstraintIndex constraint;
388  int64 weight;
389  };
390 
392  by_variable_matrix_;
393  gtl::ITIVector<ConstraintIndex, int64> constraint_lower_bounds_;
394  gtl::ITIVector<ConstraintIndex, int64> constraint_upper_bounds_;
395 
396  BopSolution assignment_;
397  BopSolution reference_;
398 
399  gtl::ITIVector<ConstraintIndex, int64> constraint_values_;
400  BacktrackableIntegerSet<ConstraintIndex> infeasible_constraint_set_;
401 
402  // This contains the list of variable flipped in assignment_.
403  // flipped_var_trail_backtrack_levels_[i-1] is the index in flipped_var_trail_
404  // of the first variable flipped after the i-th AddBacktrackingLevel() call.
405  std::vector<int> flipped_var_trail_backtrack_levels_;
406  std::vector<VariableIndex> flipped_var_trail_;
407 
408  // Members used by PotentialOneFlipRepairs().
409  std::vector<sat::Literal> tmp_potential_repairs_;
410  NonOrderedSetHasher<ConstraintIndexWithDirection> constraint_set_hasher_;
411  absl::flat_hash_map<uint64, std::vector<sat::Literal>>
412  hash_to_potential_repairs_;
413 
414  DISALLOW_COPY_AND_ASSIGN(AssignmentAndConstraintFeasibilityMaintainer);
415 };
416 
417 // This class is an utility class used to select which infeasible constraint to
418 // repair and identify one variable to flip to actually repair the constraint.
419 // A constraint 'lb <= sum_i(w_i * x_i) <= ub', with 'lb' the lower bound,
420 // 'ub' the upper bound, 'w_i' the weight of the i-th term and 'x_i' the
421 // boolean variable appearing in the i-th term, is infeasible for a given
422 // assignment iff its value 'sum_i(w_i * x_i)' is outside of the bounds.
423 // Repairing-a-constraint-in-one-flip means making the constraint feasible by
424 // just flipping the value of one unassigned variable of the current assignment
425 // from the AssignmentAndConstraintFeasibilityMaintainer.
426 // For performance reasons, the pairs weight / variable (w_i, x_i) are stored
427 // in a sparse manner as a vector of terms (w_i, x_i). In the following the
428 // TermIndex term_index refers to the position of the term in the vector.
430  public:
431  // Note that the constraint indices used in this class follow the same
432  // convention as the one used in the
433  // AssignmentAndConstraintFeasibilityMaintainer.
434  //
435  // TODO(user): maybe merge the two classes? maintaining this implicit indices
436  // convention between the two classes sounds like a bad idea.
438  const sat::LinearBooleanProblem& problem,
440  const sat::VariablesAssignment& sat_assignment);
441 
442  static const ConstraintIndex kInvalidConstraint;
443  static const TermIndex kInitTerm;
444  static const TermIndex kInvalidTerm;
445 
446  // Returns the index of a constraint to repair. This will always return the
447  // index of a constraint that can be repaired in one flip if there is one.
448  // Note however that if there is only one possible candidate, it will be
449  // returned without checking that it can indeed be repaired in one flip.
450  // This is because the later check can be expensive, and is not needed in our
451  // context.
452  ConstraintIndex ConstraintToRepair() const;
453 
454  // Returns the index of the next term which repairs the constraint when the
455  // value of its variable is flipped. This method explores terms with an
456  // index strictly greater than start_term_index and then terms with an index
457  // smaller than or equal to init_term_index if any.
458  // Returns kInvalidTerm when no reparing terms are found.
459  //
460  // Note that if init_term_index == start_term_index, then all the terms will
461  // be explored. Both TermIndex arguments can take values in [-1, constraint
462  // size).
463  TermIndex NextRepairingTerm(ConstraintIndex ct_index,
464  TermIndex init_term_index,
465  TermIndex start_term_index) const;
466 
467  // Returns true if the constraint is infeasible and if flipping the variable
468  // at the given index will repair it.
469  bool RepairIsValid(ConstraintIndex ct_index, TermIndex term_index) const;
470 
471  // Returns the literal formed by the variable at the given constraint term and
472  // assigned to the opposite value of this variable in the current assignment.
473  sat::Literal GetFlip(ConstraintIndex ct_index, TermIndex term_index) const;
474 
475  // Local structure to represent the sparse matrix by constraint used for fast
476  // lookups.
477  struct ConstraintTerm {
478  ConstraintTerm(VariableIndex v, int64 w) : var(v), weight(w) {}
479  VariableIndex var;
481  };
482 
483  private:
484  // Sorts the terms of each constraints in the by_constraint_matrix_ to iterate
485  // on most promising variables first.
486  void SortTermsOfEachConstraints(int num_variables);
487 
489  by_constraint_matrix_;
491  const sat::VariablesAssignment& sat_assignment_;
492 
493  DISALLOW_COPY_AND_ASSIGN(OneFlipConstraintRepairer);
494 };
495 
496 // This class is used to iterate on all assignments that can be obtained by
497 // deliberately flipping 'n' variables from the reference solution, 'n' being
498 // smaller than or equal to max_num_decisions.
499 // Note that one deliberate variable flip may lead to many other flips due to
500 // constraint propagation, those additional flips are not counted in 'n'.
502  public:
503  LocalSearchAssignmentIterator(const ProblemState& problem_state,
504  int max_num_decisions,
505  int max_num_broken_constraints,
506  SatWrapper* sat_wrapper);
508 
509  // Parameters of the LS algorithm.
510  void UseTranspositionTable(bool v) { use_transposition_table_ = v; }
512  use_potential_one_flip_repairs_ = v;
513  }
514 
515  // Synchronizes the iterator with the problem state, e.g. set fixed variables,
516  // set the reference solution. Call this only when a new solution has been
517  // found. This will restart the LS.
518  void Synchronize(const ProblemState& problem_state);
519 
520  // Synchronize the SatWrapper with our current search state. This needs to be
521  // called before calls to NextAssignment() if the underlying SatWrapper was
522  // used by someone else than this class.
523  void SynchronizeSatWrapper();
524 
525  // Move to the next assignment. Returns false when the search is finished.
526  bool NextAssignment();
527 
528  // Returns the last feasible assignment.
530  return maintainer_.reference();
531  }
532 
533  // Returns true if the current assignment has a better solution than the one
534  // passed to the last Synchronize() call.
536  return better_solution_has_been_found_;
537  }
538 
539  // Returns a deterministic number that should be correlated with the time
540  // spent in the iterator. The order of magnitude should be close to the time
541  // in seconds.
542  double deterministic_time() const;
543 
544  std::string DebugString() const;
545 
546  private:
547  // This is called when a better solution has been found to restore the search
548  // to the new "root" node.
549  void UseCurrentStateAsReference();
550 
551  // See transposition_table_ below.
552  static constexpr size_t kStoredMaxDecisions = 4;
553 
554  // Internal structure used to represent a node of the search tree during local
555  // search.
556  struct SearchNode {
557  SearchNode()
558  : constraint(OneFlipConstraintRepairer::kInvalidConstraint),
559  term_index(OneFlipConstraintRepairer::kInvalidTerm) {}
560  SearchNode(ConstraintIndex c, TermIndex t) : constraint(c), term_index(t) {}
561  ConstraintIndex constraint;
562  TermIndex term_index;
563  };
564 
565  // Applies the decision. Automatically backtracks when SAT detects conflicts.
566  void ApplyDecision(sat::Literal literal);
567 
568  // Adds one more decision to repair infeasible constraints.
569  // Returns true in case of success.
570  bool GoDeeper();
571 
572  // Backtracks and moves to the next decision in the search tree.
573  void Backtrack();
574 
575  // Looks if the current decisions (in search_nodes_) plus the new one (given
576  // by l) lead to a position already present in transposition_table_.
577  bool NewStateIsInTranspositionTable(sat::Literal l);
578 
579  // Inserts the current set of decisions in transposition_table_.
580  void InsertInTranspositionTable();
581 
582  // Initializes the given array with the current decisions in search_nodes_ and
583  // by filling the other positions with 0.
584  void InitializeTranspositionTableKey(
585  std::array<int32, kStoredMaxDecisions>* a);
586 
587  // Looks for the next repairing term in the given constraints while skipping
588  // the position already present in transposition_table_. A given TermIndex of
589  // -1 means that this is the first time we explore this constraint.
590  bool EnqueueNextRepairingTermIfAny(ConstraintIndex ct_to_repair,
591  TermIndex index);
592 
593  const int max_num_decisions_;
594  const int max_num_broken_constraints_;
595  bool better_solution_has_been_found_;
596  AssignmentAndConstraintFeasibilityMaintainer maintainer_;
597  SatWrapper* const sat_wrapper_;
598  OneFlipConstraintRepairer repairer_;
599  std::vector<SearchNode> search_nodes_;
600  gtl::ITIVector<ConstraintIndex, TermIndex> initial_term_index_;
601 
602  // Temporary vector used by ApplyDecision().
603  std::vector<sat::Literal> tmp_propagated_literals_;
604 
605  // For each set of explored decisions, we store it in this table so that we
606  // don't explore decisions (a, b) and later (b, a) for instance. The decisions
607  // are converted to int32, sorted and padded with 0 before beeing inserted
608  // here.
609  //
610  // TODO(user): We may still miss some equivalent states because it is possible
611  // that completely differents decisions lead to exactly the same state.
612  // However this is more time consuming to detect because we must apply the
613  // last decision first before trying to compare the states.
614  //
615  // TODO(user): Currently, we only store kStoredMaxDecisions or less decisions.
616  // Ideally, this should be related to the maximum number of decision in the
617  // LS, but that requires templating the whole LS optimizer.
618  bool use_transposition_table_;
619  absl::flat_hash_set<std::array<int32, kStoredMaxDecisions>>
620  transposition_table_;
621 
622  bool use_potential_one_flip_repairs_;
623 
624  // The number of explored nodes.
625  int64 num_nodes_;
626 
627  // The number of skipped nodes thanks to the transposition table.
628  int64 num_skipped_nodes_;
629 
630  // The overall number of better solution found. And the ones found by the
631  // use_potential_one_flip_repairs_ heuristic.
632  int64 num_improvements_;
633  int64 num_improvements_by_one_flip_repairs_;
634  int64 num_inspected_one_flip_repairs_;
635 
636  DISALLOW_COPY_AND_ASSIGN(LocalSearchAssignmentIterator);
637 };
638 
639 } // namespace bop
640 } // namespace operations_research
641 #endif // OR_TOOLS_BOP_BOP_LS_H_
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::AssignmentAndConstraintFeasibilityMaintainer
AssignmentAndConstraintFeasibilityMaintainer(const sat::LinearBooleanProblem &problem)
Definition: bop_ls.cc:179
var
IntVar * var
Definition: expr_array.cc:1858
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::SetReferenceSolution
void SetReferenceSolution(const BopSolution &reference_solution)
Definition: bop_ls.cc:242
operations_research::bop::LocalSearchAssignmentIterator::BetterSolutionHasBeenFound
bool BetterSolutionHasBeenFound() const
Definition: bop_ls.h:535
operations_research::bop::SatWrapper::BacktrackOneLevel
void BacktrackOneLevel()
Definition: bop_ls.cc:654
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::UseCurrentStateAsReference
void UseCurrentStateAsReference()
Definition: bop_ls.cc:267
operations_research::bop::LocalSearchAssignmentIterator::UsePotentialOneFlipRepairs
void UsePotentialOneFlipRepairs(bool v)
Definition: bop_ls.h:511
operations_research::bop::BacktrackableIntegerSet::BacktrackAll
void BacktrackAll()
Definition: bop_ls.cc:160
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::BacktrackOneLevel
void BacktrackOneLevel()
Definition: bop_ls.cc:321
operations_research::bop::LocalSearchAssignmentIterator::Synchronize
void Synchronize(const ProblemState &problem_state)
Definition: bop_ls.cc:703
operations_research::bop::OneFlipConstraintRepairer::ConstraintTerm::var
VariableIndex var
Definition: bop_ls.h:479
operations_research::bop::BacktrackableIntegerSet::size
int size() const
Definition: bop_ls.h:172
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::NumInfeasibleConstraints
int NumInfeasibleConstraints() const
Definition: bop_ls.h:316
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::NumConstraints
size_t NumConstraints() const
Definition: bop_ls.h:327
operations_research::bop::BopSolution::Value
bool Value(VariableIndex var) const
Definition: bop_solution.h:42
operations_research::bop::LocalSearchAssignmentIterator::UseTranspositionTable
void UseTranspositionTable(bool v)
Definition: bop_ls.h:510
operations_research::MTRandom
Definition: random.h:55
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::ConstraintLowerBound
int64 ConstraintLowerBound(ConstraintIndex constraint) const
Definition: bop_ls.h:339
operations_research::bop::ProblemState
Definition: bop_base.h:111
operations_research::bop::BacktrackableIntegerSet::ClearAndResize
void ClearAndResize(IntType n)
Definition: bop_ls.cc:120
operations_research::bop::LocalSearchOptimizer::LocalSearchOptimizer
LocalSearchOptimizer(const std::string &name, int max_num_decisions, sat::SatSolver *sat_propagator)
Definition: bop_ls.cc:32
operations_research::sat::VariablesAssignment
Definition: sat_base.h:122
operations_research::bop::NonOrderedSetHasher::Hash
uint64 Hash(IntType e) const
Definition: bop_ls.h:227
operations_research::bop::NonOrderedSetHasher::Initialize
void Initialize(int size)
Definition: bop_ls.h:205
hash
int64 hash
Definition: matrix_utils.cc:60
value
int64 value
Definition: demon_profiler.cc:43
weight
int64 weight
Definition: pack.cc:509
operations_research::bop::SatWrapper::SatWrapper
SatWrapper(sat::SatSolver *sat_solver)
Definition: bop_ls.cc:615
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::reference
const BopSolution & reference() const
Definition: bop_ls.h:336
operations_research::bop::SatWrapper::FullSatTrail
std::vector< sat::Literal > FullSatTrail() const
Definition: bop_ls.cc:619
gtl::ITIVector::resize
void resize(size_type new_size)
Definition: int_type_indexed_vector.h:149
operations_research::bop::OneFlipConstraintRepairer
Definition: bop_ls.h:429
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
bop_solution.h
operations_research::bop::BacktrackableIntegerSet
Definition: bop_ls.h:156
int64
int64_t int64
Definition: integral_types.h:34
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::ConstraintUpperBound
int64 ConstraintUpperBound(ConstraintIndex constraint) const
Definition: bop_ls.h:344
gtl::ITIVector::size
size_type size() const
Definition: int_type_indexed_vector.h:146
sat_solver.h
gtl::ITIVector::empty
bool empty() const
Definition: int_type_indexed_vector.h:155
operations_research::bop::LearnedInfo
Definition: bop_base.h:245
operations_research::bop::NonOrderedSetHasher::NonOrderedSetHasher
NonOrderedSetHasher()
Definition: bop_ls.h:202
operations_research::bop::BacktrackableIntegerSet::ChangeState
void ChangeState(IntType i, bool should_be_inside)
Definition: bop_ls.cc:129
operations_research::bop::BacktrackableIntegerSet::Superset
const std::vector< IntType > & Superset() const
Definition: bop_ls.h:175
index
int index
Definition: pack.cc:508
operations_research::bop::NonOrderedSetHasher
Definition: bop_ls.h:200
operations_research::bop::NonOrderedSetHasher::IgnoreElement
void IgnoreElement(IntType e)
Definition: bop_ls.h:214
int32
int int32
Definition: integral_types.h:33
operations_research::bop::SatWrapper::deterministic_time
double deterministic_time() const
Definition: bop_ls.cc:665
operations_research::sat::SatSolver
Definition: sat_solver.h:58
operations_research::bop::LocalSearchAssignmentIterator::DebugString
std::string DebugString() const
Definition: bop_ls.cc:822
operations_research::bop::OneFlipConstraintRepairer::kInvalidTerm
static const TermIndex kInvalidTerm
Definition: bop_ls.h:444
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::ConstraintValue
int64 ConstraintValue(ConstraintIndex constraint) const
Definition: bop_ls.h:351
operations_research::bop::NonOrderedSetHasher::IsInitialized
bool IsInitialized() const
Definition: bop_ls.h:230
operations_research::ACMRandom::Rand64
uint64 Rand64()
Definition: random.h:33
operations_research::bop::LocalSearchAssignmentIterator
Definition: bop_ls.h:501
operations_research::bop::SatWrapper::IsModelUnsat
bool IsModelUnsat() const
Definition: bop_ls.h:62
random.h
operations_research::sat::Literal
Definition: sat_base.h:64
operations_research::bop::OneFlipConstraintRepairer::ConstraintTerm::ConstraintTerm
ConstraintTerm(VariableIndex v, int64 w)
Definition: bop_ls.h:478
operations_research::bop::BacktrackableIntegerSet::BacktrackOneLevel
void BacktrackOneLevel()
Definition: bop_ls.cc:145
a
int64 a
Definition: constraint_solver/table.cc:42
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::ConstraintIsFeasible
bool ConstraintIsFeasible(ConstraintIndex constraint) const
Definition: bop_ls.h:356
operations_research::bop::SatWrapper::SatAssignment
const sat::VariablesAssignment & SatAssignment() const
Definition: bop_ls.h:65
operations_research::bop::OneFlipConstraintRepairer::kInvalidConstraint
static const ConstraintIndex kInvalidConstraint
Definition: bop_ls.h:442
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::PotentialOneFlipRepairs
const std::vector< sat::Literal > & PotentialOneFlipRepairs()
Definition: bop_ls.cc:344
operations_research::bop::LocalSearchAssignmentIterator::SynchronizeSatWrapper
void SynchronizeSatWrapper()
Definition: bop_ls.cc:719
time_limit
SharedTimeLimit * time_limit
Definition: cp_model_solver.cc:2025
operations_research::bop::OneFlipConstraintRepairer::RepairIsValid
bool RepairIsValid(ConstraintIndex ct_index, TermIndex term_index) const
Definition: bop_ls.cc:571
operations_research::bop::OneFlipConstraintRepairer::ConstraintToRepair
ConstraintIndex ConstraintToRepair() const
Definition: bop_ls.cc:488
bop_types.h
operations_research::bop::OneFlipConstraintRepairer::GetFlip
sat::Literal GetFlip(ConstraintIndex ct_index, TermIndex term_index) const
Definition: bop_ls.cc:588
operations_research::TimeLimit
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
operations_research::bop::BopOptimizerBase
Definition: bop_base.h:40
boolean_problem.pb.h
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::DebugString
std::string DebugString() const
Definition: bop_ls.cc:378
operations_research::bop::BacktrackableIntegerSet::AddBacktrackingLevel
void AddBacktrackingLevel()
Definition: bop_ls.cc:139
operations_research::bop::LocalSearchOptimizer::~LocalSearchOptimizer
~LocalSearchOptimizer() override
Definition: bop_ls.cc:41
uint64
uint64_t uint64
Definition: integral_types.h:39
operations_research::bop::OneFlipConstraintRepairer::ConstraintTerm::weight
int64 weight
Definition: bop_ls.h:480
operations_research::bop::NonOrderedSetHasher::Hash
uint64 Hash(const std::vector< IntType > &set) const
Definition: bop_ls.h:219
operations_research::bop::OneFlipConstraintRepairer::NextRepairingTerm
TermIndex NextRepairingTerm(ConstraintIndex ct_index, TermIndex init_term_index, TermIndex start_term_index) const
Definition: bop_ls.cc:541
operations_research::sat::SatSolver::Assignment
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:363
operations_research::bop::LocalSearchAssignmentIterator::deterministic_time
double deterministic_time() const
Definition: bop_ls.cc:818
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::BacktrackAll
void BacktrackAll()
Definition: bop_ls.cc:339
operations_research::sat::SatSolver::IsModelUnsat
bool IsModelUnsat() const
Definition: sat_solver.h:137
operations_research::bop::SatWrapper::ApplyDecision
int ApplyDecision(sat::Literal decision_literal, std::vector< sat::Literal > *propagated_literals)
Definition: bop_ls.cc:628
operations_research::bop::SatWrapper::BacktrackAll
void BacktrackAll()
Definition: bop_ls.cc:617
operations_research::bop::LocalSearchAssignmentIterator::LocalSearchAssignmentIterator
LocalSearchAssignmentIterator(const ProblemState &problem_state, int max_num_decisions, int max_num_broken_constraints, SatWrapper *sat_wrapper)
Definition: bop_ls.cc:673
operations_research::bop::BopSolution
Definition: bop_solution.h:31
operations_research::bop::OneFlipConstraintRepairer::OneFlipConstraintRepairer
OneFlipConstraintRepairer(const sat::LinearBooleanProblem &problem, const AssignmentAndConstraintFeasibilityMaintainer &maintainer, const sat::VariablesAssignment &sat_assignment)
Definition: bop_ls.cc:436
operations_research::bop::BopOptimizerBase::name
const std::string & name() const
Definition: bop_base.h:46
operations_research::bop::SatWrapper
Definition: bop_ls.h:50
operations_research::bop::OneFlipConstraintRepairer::ConstraintTerm
Definition: bop_ls.h:477
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::Assign
void Assign(const std::vector< sat::Literal > &literals)
Definition: bop_ls.cc:295
hash.h
delta
int64 delta
Definition: resource.cc:1684
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::Assignment
bool Assignment(VariableIndex var) const
Definition: bop_ls.h:333
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::IsFeasible
bool IsFeasible() const
Definition: bop_ls.h:311
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::AddBacktrackingLevel
void AddBacktrackingLevel()
Definition: bop_ls.cc:316
operations_research::bop::BacktrackableIntegerSet::BacktrackableIntegerSet
BacktrackableIntegerSet()
Definition: bop_ls.h:158
gtl::ITIVector< IntType, uint64 >
operations_research::bop::LocalSearchAssignmentIterator::NextAssignment
bool NextAssignment()
Definition: bop_ls.cc:758
operations_research::bop::LocalSearchOptimizer
Definition: bop_ls.h:114
bop_base.h
literal
Literal literal
Definition: optimization.cc:84
operations_research::bop::LocalSearchAssignmentIterator::~LocalSearchAssignmentIterator
~LocalSearchAssignmentIterator()
Definition: bop_ls.cc:694
operations_research::bop::LocalSearchAssignmentIterator::LastReferenceAssignment
const BopSolution & LastReferenceAssignment() const
Definition: bop_ls.h:529
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::kObjectiveConstraint
static const ConstraintIndex kObjectiveConstraint
Definition: bop_ls.h:271
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::PossiblyInfeasibleConstraints
const std::vector< ConstraintIndex > & PossiblyInfeasibleConstraints() const
Definition: bop_ls.h:321
operations_research::bop::OneFlipConstraintRepairer::kInitTerm
static const TermIndex kInitTerm
Definition: bop_ls.h:443
parameters
SatParameters parameters
Definition: cp_model_fz_solver.cc:107
operations_research::bop::BopOptimizerBase::Status
Status
Definition: bop_base.h:61
operations_research::bop::SatWrapper::ExtractLearnedInfo
void ExtractLearnedInfo(LearnedInfo *info)
Definition: bop_ls.cc:661
operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer
Definition: bop_ls.h:262