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