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