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