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"
42#include "ortools/sat/boolean_problem.pb.h"
44
45namespace operations_research {
46namespace 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.
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.
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.
104class 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.
157template <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().
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).
201template <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.
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.
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.
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
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
const std::vector< ConstraintIndex > & PossiblyInfeasibleConstraints() const
Definition: bop_ls.h:323
void Assign(const std::vector< sat::Literal > &literals)
Definition: bop_ls.cc:301
const std::vector< sat::Literal > & PotentialOneFlipRepairs()
Definition: bop_ls.cc:350
void ChangeState(IntType i, bool should_be_inside)
Definition: bop_ls.cc:133
const std::vector< IntType > & Superset() const
Definition: bop_ls.h:177
const std::string & name() const
Definition: bop_base.h:49
bool Value(VariableIndex var) const
Definition: bop_solution.h:46
const BopSolution & LastReferenceAssignment() const
Definition: bop_ls.h:533
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
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
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 sat::VariablesAssignment & SatAssignment() const
Definition: bop_ls.h:67
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