OR-Tools  8.2
bop_ls.cc
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 #include "ortools/bop/bop_ls.h"
15 
16 #include <cstdint>
17 #include <limits>
18 
19 #include "absl/memory/memory.h"
20 #include "absl/strings/str_format.h"
22 #include "ortools/bop/bop_util.h"
24 
25 namespace operations_research {
26 namespace bop {
27 
28 using ::operations_research::sat::LinearBooleanConstraint;
29 using ::operations_research::sat::LinearBooleanProblem;
30 using ::operations_research::sat::LinearObjective;
31 
32 //------------------------------------------------------------------------------
33 // LocalSearchOptimizer
34 //------------------------------------------------------------------------------
35 
37  int max_num_decisions,
38  sat::SatSolver* sat_propagator)
40  state_update_stamp_(ProblemState::kInitialStampValue),
41  max_num_decisions_(max_num_decisions),
42  sat_wrapper_(sat_propagator),
43  assignment_iterator_() {}
44 
46 
47 bool LocalSearchOptimizer::ShouldBeRun(
48  const ProblemState& problem_state) const {
49  return problem_state.solution().IsFeasible();
50 }
51 
52 BopOptimizerBase::Status LocalSearchOptimizer::Optimize(
53  const BopParameters& parameters, const ProblemState& problem_state,
54  LearnedInfo* learned_info, TimeLimit* time_limit) {
55  CHECK(learned_info != nullptr);
56  CHECK(time_limit != nullptr);
57  learned_info->Clear();
58 
59  if (assignment_iterator_ == nullptr) {
60  assignment_iterator_ = absl::make_unique<LocalSearchAssignmentIterator>(
61  problem_state, max_num_decisions_,
62  parameters.max_num_broken_constraints_in_ls(), &sat_wrapper_);
63  }
64 
65  if (state_update_stamp_ != problem_state.update_stamp()) {
66  // We have a new problem_state.
67  state_update_stamp_ = problem_state.update_stamp();
68  assignment_iterator_->Synchronize(problem_state);
69  }
70  assignment_iterator_->SynchronizeSatWrapper();
71 
72  double prev_deterministic_time = assignment_iterator_->deterministic_time();
73  assignment_iterator_->UseTranspositionTable(
74  parameters.use_transposition_table_in_ls());
75  assignment_iterator_->UsePotentialOneFlipRepairs(
76  parameters.use_potential_one_flip_repairs_in_ls());
77  int64_t num_assignments_to_explore =
78  parameters.max_number_of_explored_assignments_per_try_in_ls();
79 
80  while (!time_limit->LimitReached() && num_assignments_to_explore > 0 &&
81  assignment_iterator_->NextAssignment()) {
82  time_limit->AdvanceDeterministicTime(
83  assignment_iterator_->deterministic_time() - prev_deterministic_time);
84  prev_deterministic_time = assignment_iterator_->deterministic_time();
85  --num_assignments_to_explore;
86  }
87  if (sat_wrapper_.IsModelUnsat()) {
88  // TODO(user): we do that all the time, return an UNSAT satus instead and
89  // do this only once.
90  return problem_state.solution().IsFeasible()
93  }
94 
95  // TODO(user): properly abort when we found a new solution and then finished
96  // the ls? note that this is minor.
97  sat_wrapper_.ExtractLearnedInfo(learned_info);
98  if (assignment_iterator_->BetterSolutionHasBeenFound()) {
99  // TODO(user): simply use vector<bool> instead of a BopSolution internally.
100  learned_info->solution = assignment_iterator_->LastReferenceAssignment();
102  }
103 
104  if (time_limit->LimitReached()) {
105  // The time limit is reached without finding a solution.
107  }
108 
109  if (num_assignments_to_explore <= 0) {
110  // Explore the remaining assignments in a future call to Optimize().
112  }
113 
114  // All assignments reachable in max_num_decisions_ or less have been explored,
115  // don't call optimize() with the same initial solution again.
117 }
118 
119 //------------------------------------------------------------------------------
120 // BacktrackableIntegerSet
121 //------------------------------------------------------------------------------
122 
123 template <typename IntType>
125  size_ = 0;
126  saved_sizes_.clear();
127  saved_stack_sizes_.clear();
128  stack_.clear();
129  in_stack_.assign(n.value(), false);
130 }
131 
132 template <typename IntType>
134  bool should_be_inside) {
135  size_ += should_be_inside ? 1 : -1;
136  if (!in_stack_[i.value()]) {
137  in_stack_[i.value()] = true;
138  stack_.push_back(i);
139  }
140 }
141 
142 template <typename IntType>
144  saved_stack_sizes_.push_back(stack_.size());
145  saved_sizes_.push_back(size_);
146 }
147 
148 template <typename IntType>
150  if (saved_stack_sizes_.empty()) {
151  BacktrackAll();
152  } else {
153  for (int i = saved_stack_sizes_.back(); i < stack_.size(); ++i) {
154  in_stack_[stack_[i].value()] = false;
155  }
156  stack_.resize(saved_stack_sizes_.back());
157  saved_stack_sizes_.pop_back();
158  size_ = saved_sizes_.back();
159  saved_sizes_.pop_back();
160  }
161 }
162 
163 template <typename IntType>
165  for (int i = 0; i < stack_.size(); ++i) {
166  in_stack_[stack_[i].value()] = false;
167  }
168  stack_.clear();
169  saved_stack_sizes_.clear();
170  size_ = 0;
171  saved_sizes_.clear();
172 }
173 
174 // Explicit instantiation of BacktrackableIntegerSet.
175 // TODO(user): move the code in a separate .h and -inl.h to avoid this.
177 
178 //------------------------------------------------------------------------------
179 // AssignmentAndConstraintFeasibilityMaintainer
180 //------------------------------------------------------------------------------
181 
184  const LinearBooleanProblem& problem)
185  : by_variable_matrix_(problem.num_variables()),
186  constraint_lower_bounds_(),
187  constraint_upper_bounds_(),
188  assignment_(problem, "Assignment"),
189  reference_(problem, "Assignment"),
190  constraint_values_(),
191  flipped_var_trail_backtrack_levels_(),
192  flipped_var_trail_() {
193  // Add the objective constraint as the first constraint.
194  const LinearObjective& objective = problem.objective();
195  CHECK_EQ(objective.literals_size(), objective.coefficients_size());
196  for (int i = 0; i < objective.literals_size(); ++i) {
197  CHECK_GT(objective.literals(i), 0);
198  CHECK_NE(objective.coefficients(i), 0);
199 
200  const VariableIndex var(objective.literals(i) - 1);
201  const int64_t weight = objective.coefficients(i);
202  by_variable_matrix_[var].push_back(
203  ConstraintEntry(kObjectiveConstraint, weight));
204  }
205  constraint_lower_bounds_.push_back(std::numeric_limits<int64_t>::min());
206  constraint_values_.push_back(0);
207  constraint_upper_bounds_.push_back(std::numeric_limits<int64_t>::max());
208 
209  // Add each constraint.
210  ConstraintIndex num_constraints_with_objective(1);
211  for (const LinearBooleanConstraint& constraint : problem.constraints()) {
212  if (constraint.literals_size() <= 2) {
213  // Infeasible binary constraints are automatically repaired by propagation
214  // (when possible). Then there are no needs to consider the binary
215  // constraints here, the propagation is delegated to the SAT propagator.
216  continue;
217  }
218 
219  CHECK_EQ(constraint.literals_size(), constraint.coefficients_size());
220  for (int i = 0; i < constraint.literals_size(); ++i) {
221  const VariableIndex var(constraint.literals(i) - 1);
222  const int64_t weight = constraint.coefficients(i);
223  by_variable_matrix_[var].push_back(
224  ConstraintEntry(num_constraints_with_objective, weight));
225  }
226  constraint_lower_bounds_.push_back(
227  constraint.has_lower_bound() ? constraint.lower_bound()
229  constraint_values_.push_back(0);
230  constraint_upper_bounds_.push_back(
231  constraint.has_upper_bound() ? constraint.upper_bound()
233 
234  ++num_constraints_with_objective;
235  }
236 
237  // Initialize infeasible_constraint_set_;
238  infeasible_constraint_set_.ClearAndResize(
239  ConstraintIndex(constraint_values_.size()));
240 
241  CHECK_EQ(constraint_values_.size(), constraint_lower_bounds_.size());
242  CHECK_EQ(constraint_values_.size(), constraint_upper_bounds_.size());
243 }
244 
245 const ConstraintIndex
247 
248 void AssignmentAndConstraintFeasibilityMaintainer::SetReferenceSolution(
249  const BopSolution& reference_solution) {
250  CHECK(reference_solution.IsFeasible());
251  infeasible_constraint_set_.BacktrackAll();
252 
253  assignment_ = reference_solution;
254  reference_ = assignment_;
255  flipped_var_trail_backtrack_levels_.clear();
256  flipped_var_trail_.clear();
257  AddBacktrackingLevel(); // To handle initial propagation.
258 
259  // Recompute the value of all constraints.
260  constraint_values_.assign(NumConstraints(), 0);
261  for (VariableIndex var(0); var < assignment_.Size(); ++var) {
262  if (assignment_.Value(var)) {
263  for (const ConstraintEntry& entry : by_variable_matrix_[var]) {
264  constraint_values_[entry.constraint] += entry.weight;
265  }
266  }
267  }
268 
269  MakeObjectiveConstraintInfeasible(1);
270 }
271 
272 void AssignmentAndConstraintFeasibilityMaintainer::
273  UseCurrentStateAsReference() {
274  for (const VariableIndex var : flipped_var_trail_) {
275  reference_.SetValue(var, assignment_.Value(var));
276  }
277  flipped_var_trail_.clear();
278  flipped_var_trail_backtrack_levels_.clear();
279  AddBacktrackingLevel(); // To handle initial propagation.
280  MakeObjectiveConstraintInfeasible(1);
281 }
282 
283 void AssignmentAndConstraintFeasibilityMaintainer::
284  MakeObjectiveConstraintInfeasible(int delta) {
285  CHECK(IsFeasible());
286  CHECK(flipped_var_trail_.empty());
287  constraint_upper_bounds_[kObjectiveConstraint] =
288  constraint_values_[kObjectiveConstraint] - delta;
289  infeasible_constraint_set_.BacktrackAll();
290  infeasible_constraint_set_.ChangeState(kObjectiveConstraint, true);
291  infeasible_constraint_set_.AddBacktrackingLevel();
292  CHECK(!ConstraintIsFeasible(kObjectiveConstraint));
293  CHECK(!IsFeasible());
294  if (DEBUG_MODE) {
295  for (ConstraintIndex ct(1); ct < NumConstraints(); ++ct) {
296  CHECK(ConstraintIsFeasible(ct));
297  }
298  }
299 }
300 
301 void AssignmentAndConstraintFeasibilityMaintainer::Assign(
302  const std::vector<sat::Literal>& literals) {
303  for (const sat::Literal& literal : literals) {
304  const VariableIndex var(literal.Variable().value());
305  const bool value = literal.IsPositive();
306  if (assignment_.Value(var) != value) {
307  flipped_var_trail_.push_back(var);
308  assignment_.SetValue(var, value);
309  for (const ConstraintEntry& entry : by_variable_matrix_[var]) {
310  const bool was_feasible = ConstraintIsFeasible(entry.constraint);
311  constraint_values_[entry.constraint] +=
312  value ? entry.weight : -entry.weight;
313  if (ConstraintIsFeasible(entry.constraint) != was_feasible) {
314  infeasible_constraint_set_.ChangeState(entry.constraint,
315  was_feasible);
316  }
317  }
318  }
319  }
320 }
321 
322 void AssignmentAndConstraintFeasibilityMaintainer::AddBacktrackingLevel() {
323  flipped_var_trail_backtrack_levels_.push_back(flipped_var_trail_.size());
324  infeasible_constraint_set_.AddBacktrackingLevel();
325 }
326 
327 void AssignmentAndConstraintFeasibilityMaintainer::BacktrackOneLevel() {
328  // Backtrack each literal of the last level.
329  for (int i = flipped_var_trail_backtrack_levels_.back();
330  i < flipped_var_trail_.size(); ++i) {
331  const VariableIndex var(flipped_var_trail_[i]);
332  const bool new_value = !assignment_.Value(var);
333  DCHECK_EQ(new_value, reference_.Value(var));
334  assignment_.SetValue(var, new_value);
335  for (const ConstraintEntry& entry : by_variable_matrix_[var]) {
336  constraint_values_[entry.constraint] +=
337  new_value ? entry.weight : -entry.weight;
338  }
339  }
340  flipped_var_trail_.resize(flipped_var_trail_backtrack_levels_.back());
341  flipped_var_trail_backtrack_levels_.pop_back();
342  infeasible_constraint_set_.BacktrackOneLevel();
343 }
344 
345 void AssignmentAndConstraintFeasibilityMaintainer::BacktrackAll() {
346  while (!flipped_var_trail_backtrack_levels_.empty()) BacktrackOneLevel();
347 }
348 
349 const std::vector<sat::Literal>&
350 AssignmentAndConstraintFeasibilityMaintainer::PotentialOneFlipRepairs() {
351  if (!constraint_set_hasher_.IsInitialized()) {
352  InitializeConstraintSetHasher();
353  }
354 
355  // First, we compute the hash that a Literal should have in order to repair
356  // all the infeasible constraint (ignoring the objective).
357  //
358  // TODO(user): If this starts to show-up in a performance profile, we can
359  // easily maintain this hash incrementally.
360  uint64_t hash = 0;
361  for (const ConstraintIndex ci : PossiblyInfeasibleConstraints()) {
362  const int64_t value = ConstraintValue(ci);
363  if (value > ConstraintUpperBound(ci)) {
364  hash ^= constraint_set_hasher_.Hash(FromConstraintIndex(ci, false));
365  } else if (value < ConstraintLowerBound(ci)) {
366  hash ^= constraint_set_hasher_.Hash(FromConstraintIndex(ci, true));
367  }
368  }
369 
370  tmp_potential_repairs_.clear();
371  const auto it = hash_to_potential_repairs_.find(hash);
372  if (it != hash_to_potential_repairs_.end()) {
373  for (const sat::Literal literal : it->second) {
374  // We only returns the flips.
375  if (assignment_.Value(VariableIndex(literal.Variable().value())) !=
376  literal.IsPositive()) {
377  tmp_potential_repairs_.push_back(literal);
378  }
379  }
380  }
381  return tmp_potential_repairs_;
382 }
383 
384 std::string AssignmentAndConstraintFeasibilityMaintainer::DebugString() const {
385  std::string str;
386  str += "curr: ";
387  for (bool value : assignment_) {
388  str += value ? " 1 " : " 0 ";
389  }
390  str += "\nFlipped variables: ";
391  // TODO(user): show the backtrack levels.
392  for (const VariableIndex var : flipped_var_trail_) {
393  str += absl::StrFormat(" %d", var.value());
394  }
395  str += "\nmin curr max\n";
396  for (ConstraintIndex ct(0); ct < constraint_values_.size(); ++ct) {
397  if (constraint_lower_bounds_[ct] == std::numeric_limits<int64_t>::min()) {
398  str += absl::StrFormat("- %d %d\n", constraint_values_[ct],
399  constraint_upper_bounds_[ct]);
400  } else {
401  str +=
402  absl::StrFormat("%d %d %d\n", constraint_lower_bounds_[ct],
403  constraint_values_[ct], constraint_upper_bounds_[ct]);
404  }
405  }
406  return str;
407 }
408 
409 void AssignmentAndConstraintFeasibilityMaintainer::
410  InitializeConstraintSetHasher() {
411  const int num_constraints_with_objective = constraint_upper_bounds_.size();
412 
413  // Initialize the potential one flip repair. Note that we ignore the
414  // objective constraint completely so that we consider a repair even if the
415  // objective constraint is not infeasible.
416  constraint_set_hasher_.Initialize(2 * num_constraints_with_objective);
417  constraint_set_hasher_.IgnoreElement(
418  FromConstraintIndex(kObjectiveConstraint, true));
419  constraint_set_hasher_.IgnoreElement(
420  FromConstraintIndex(kObjectiveConstraint, false));
421  for (VariableIndex var(0); var < by_variable_matrix_.size(); ++var) {
422  // We add two entries, one for a positive flip (from false to true) and one
423  // for a negative flip (from true to false).
424  for (const bool flip_is_positive : {true, false}) {
425  uint64_t hash = 0;
426  for (const ConstraintEntry& entry : by_variable_matrix_[var]) {
427  const bool coeff_is_positive = entry.weight > 0;
428  hash ^= constraint_set_hasher_.Hash(FromConstraintIndex(
429  entry.constraint,
430  /*up=*/flip_is_positive ? coeff_is_positive : !coeff_is_positive));
431  }
432  hash_to_potential_repairs_[hash].push_back(
433  sat::Literal(sat::BooleanVariable(var.value()), flip_is_positive));
434  }
435  }
436 }
437 
438 //------------------------------------------------------------------------------
439 // OneFlipConstraintRepairer
440 //------------------------------------------------------------------------------
441 
442 OneFlipConstraintRepairer::OneFlipConstraintRepairer(
443  const LinearBooleanProblem& problem,
445  const sat::VariablesAssignment& sat_assignment)
446  : by_constraint_matrix_(problem.constraints_size() + 1),
447  maintainer_(maintainer),
448  sat_assignment_(sat_assignment) {
449  // Fill the by_constraint_matrix_.
450  //
451  // IMPORTANT: The order of the constraint needs to exactly match the one of
452  // the constraint in the AssignmentAndConstraintFeasibilityMaintainer.
453 
454  // Add the objective constraint as the first constraint.
455  ConstraintIndex num_constraint(0);
456  const LinearObjective& objective = problem.objective();
457  CHECK_EQ(objective.literals_size(), objective.coefficients_size());
458  for (int i = 0; i < objective.literals_size(); ++i) {
459  CHECK_GT(objective.literals(i), 0);
460  CHECK_NE(objective.coefficients(i), 0);
461 
462  const VariableIndex var(objective.literals(i) - 1);
463  const int64_t weight = objective.coefficients(i);
464  by_constraint_matrix_[num_constraint].push_back(
466  }
467 
468  // Add the non-binary problem constraints.
469  for (const LinearBooleanConstraint& constraint : problem.constraints()) {
470  if (constraint.literals_size() <= 2) {
471  // Infeasible binary constraints are automatically repaired by propagation
472  // (when possible). Then there are no needs to consider the binary
473  // constraints here, the propagation is delegated to the SAT propagator.
474  continue;
475  }
476 
477  ++num_constraint;
478  CHECK_EQ(constraint.literals_size(), constraint.coefficients_size());
479  for (int i = 0; i < constraint.literals_size(); ++i) {
480  const VariableIndex var(constraint.literals(i) - 1);
481  const int64_t weight = constraint.coefficients(i);
482  by_constraint_matrix_[num_constraint].push_back(
484  }
485  }
486 
487  SortTermsOfEachConstraints(problem.num_variables());
488 }
489 
490 const ConstraintIndex OneFlipConstraintRepairer::kInvalidConstraint(-1);
491 const TermIndex OneFlipConstraintRepairer::kInitTerm(-1);
492 const TermIndex OneFlipConstraintRepairer::kInvalidTerm(-2);
493 
495  ConstraintIndex selected_ct = kInvalidConstraint;
496  int32_t selected_num_branches = std::numeric_limits<int32_t>::max();
497  int num_infeasible_constraints_left = maintainer_.NumInfeasibleConstraints();
498 
499  // Optimization: We inspect the constraints in reverse order because the
500  // objective one will always be first (in our current code) and with some
501  // luck, we will break early instead of fully exploring it.
502  const std::vector<ConstraintIndex>& infeasible_constraints =
503  maintainer_.PossiblyInfeasibleConstraints();
504  for (int index = infeasible_constraints.size() - 1; index >= 0; --index) {
505  const ConstraintIndex& i = infeasible_constraints[index];
506  if (maintainer_.ConstraintIsFeasible(i)) continue;
507  --num_infeasible_constraints_left;
508 
509  // Optimization: We return the only candidate without inspecting it.
510  // This is critical at the beginning of the search or later if the only
511  // candidate is the objective constraint which can be really long.
512  if (num_infeasible_constraints_left == 0 &&
513  selected_ct == kInvalidConstraint) {
514  return i;
515  }
516 
517  const int64_t constraint_value = maintainer_.ConstraintValue(i);
518  const int64_t lb = maintainer_.ConstraintLowerBound(i);
519  const int64_t ub = maintainer_.ConstraintUpperBound(i);
520 
521  int32_t num_branches = 0;
522  for (const ConstraintTerm& term : by_constraint_matrix_[i]) {
523  if (sat_assignment_.VariableIsAssigned(
524  sat::BooleanVariable(term.var.value()))) {
525  continue;
526  }
527  const int64_t new_value =
528  constraint_value +
529  (maintainer_.Assignment(term.var) ? -term.weight : term.weight);
530  if (new_value >= lb && new_value <= ub) {
531  ++num_branches;
532  if (num_branches >= selected_num_branches) break;
533  }
534  }
535 
536  // The constraint can't be repaired in one decision.
537  if (num_branches == 0) continue;
538  if (num_branches < selected_num_branches) {
539  selected_ct = i;
540  selected_num_branches = num_branches;
541  if (num_branches == 1) break;
542  }
543  }
544  return selected_ct;
545 }
546 
548  ConstraintIndex ct_index, TermIndex init_term_index,
549  TermIndex start_term_index) const {
551  by_constraint_matrix_[ct_index];
552  const int64_t constraint_value = maintainer_.ConstraintValue(ct_index);
553  const int64_t lb = maintainer_.ConstraintLowerBound(ct_index);
554  const int64_t ub = maintainer_.ConstraintUpperBound(ct_index);
555 
556  const TermIndex end_term_index(terms.size() + init_term_index + 1);
557  for (TermIndex loop_term_index(
558  start_term_index + 1 +
559  (start_term_index < init_term_index ? terms.size() : 0));
560  loop_term_index < end_term_index; ++loop_term_index) {
561  const TermIndex term_index(loop_term_index % terms.size());
562  const ConstraintTerm term = terms[term_index];
563  if (sat_assignment_.VariableIsAssigned(
564  sat::BooleanVariable(term.var.value()))) {
565  continue;
566  }
567  const int64_t new_value =
568  constraint_value +
569  (maintainer_.Assignment(term.var) ? -term.weight : term.weight);
570  if (new_value >= lb && new_value <= ub) {
571  return term_index;
572  }
573  }
574  return kInvalidTerm;
575 }
576 
577 bool OneFlipConstraintRepairer::RepairIsValid(ConstraintIndex ct_index,
578  TermIndex term_index) const {
579  if (maintainer_.ConstraintIsFeasible(ct_index)) return false;
580  const ConstraintTerm term = by_constraint_matrix_[ct_index][term_index];
581  if (sat_assignment_.VariableIsAssigned(
582  sat::BooleanVariable(term.var.value()))) {
583  return false;
584  }
585  const int64_t new_value =
586  maintainer_.ConstraintValue(ct_index) +
587  (maintainer_.Assignment(term.var) ? -term.weight : term.weight);
588 
589  const int64_t lb = maintainer_.ConstraintLowerBound(ct_index);
590  const int64_t ub = maintainer_.ConstraintUpperBound(ct_index);
591  return (new_value >= lb && new_value <= ub);
592 }
593 
595  TermIndex term_index) const {
596  const ConstraintTerm term = by_constraint_matrix_[ct_index][term_index];
597  const bool value = maintainer_.Assignment(term.var);
598  return sat::Literal(sat::BooleanVariable(term.var.value()), !value);
599 }
600 
601 void OneFlipConstraintRepairer::SortTermsOfEachConstraints(int num_variables) {
602  absl::StrongVector<VariableIndex, int64_t> objective(num_variables, 0);
603  for (const ConstraintTerm& term :
604  by_constraint_matrix_[AssignmentAndConstraintFeasibilityMaintainer::
606  objective[term.var] = std::abs(term.weight);
607  }
609  by_constraint_matrix_) {
610  std::sort(terms.begin(), terms.end(),
611  [&objective](const ConstraintTerm& a, const ConstraintTerm& b) {
612  return objective[a.var] > objective[b.var];
613  });
614  }
615 }
616 
617 //------------------------------------------------------------------------------
618 // SatWrapper
619 //------------------------------------------------------------------------------
620 
621 SatWrapper::SatWrapper(sat::SatSolver* sat_solver) : sat_solver_(sat_solver) {}
622 
623 void SatWrapper::BacktrackAll() { sat_solver_->Backtrack(0); }
624 
625 std::vector<sat::Literal> SatWrapper::FullSatTrail() const {
626  std::vector<sat::Literal> propagated_literals;
627  const sat::Trail& trail = sat_solver_->LiteralTrail();
628  for (int trail_index = 0; trail_index < trail.Index(); ++trail_index) {
629  propagated_literals.push_back(trail[trail_index]);
630  }
631  return propagated_literals;
632 }
633 
635  std::vector<sat::Literal>* propagated_literals) {
636  CHECK(!sat_solver_->Assignment().VariableIsAssigned(
637  decision_literal.Variable()));
638  CHECK(propagated_literals != nullptr);
639 
640  propagated_literals->clear();
641  const int old_decision_level = sat_solver_->CurrentDecisionLevel();
642  const int new_trail_index =
643  sat_solver_->EnqueueDecisionAndBackjumpOnConflict(decision_literal);
644  if (sat_solver_->IsModelUnsat()) {
645  return old_decision_level + 1;
646  }
647 
648  // Return the propagated literals, whenever there is a conflict or not.
649  // In case of conflict, these literals will have to be added to the last
650  // decision point after backtrack.
651  const sat::Trail& propagation_trail = sat_solver_->LiteralTrail();
652  for (int trail_index = new_trail_index;
653  trail_index < propagation_trail.Index(); ++trail_index) {
654  propagated_literals->push_back(propagation_trail[trail_index]);
655  }
656 
657  return old_decision_level + 1 - sat_solver_->CurrentDecisionLevel();
658 }
659 
661  const int old_decision_level = sat_solver_->CurrentDecisionLevel();
662  if (old_decision_level > 0) {
663  sat_solver_->Backtrack(old_decision_level - 1);
664  }
665 }
666 
668  bop::ExtractLearnedInfoFromSatSolver(sat_solver_, info);
669 }
670 
672  return sat_solver_->deterministic_time();
673 }
674 
675 //------------------------------------------------------------------------------
676 // LocalSearchAssignmentIterator
677 //------------------------------------------------------------------------------
678 
680  const ProblemState& problem_state, int max_num_decisions,
681  int max_num_broken_constraints, SatWrapper* sat_wrapper)
682  : max_num_decisions_(max_num_decisions),
683  max_num_broken_constraints_(max_num_broken_constraints),
684  maintainer_(problem_state.original_problem()),
685  sat_wrapper_(sat_wrapper),
686  repairer_(problem_state.original_problem(), maintainer_,
687  sat_wrapper->SatAssignment()),
688  search_nodes_(),
689  initial_term_index_(
690  problem_state.original_problem().constraints_size() + 1,
691  OneFlipConstraintRepairer::kInitTerm),
692  use_transposition_table_(false),
693  use_potential_one_flip_repairs_(false),
694  num_nodes_(0),
695  num_skipped_nodes_(0),
696  num_improvements_(0),
697  num_improvements_by_one_flip_repairs_(0),
698  num_inspected_one_flip_repairs_(0) {}
699 
701  VLOG(1) << "LS " << max_num_decisions_
702  << "\n num improvements: " << num_improvements_
703  << "\n num improvements with one flip repairs: "
704  << num_improvements_by_one_flip_repairs_
705  << "\n num inspected one flip repairs: "
706  << num_inspected_one_flip_repairs_;
707 }
708 
710  const ProblemState& problem_state) {
711  better_solution_has_been_found_ = false;
712  maintainer_.SetReferenceSolution(problem_state.solution());
713  for (const SearchNode& node : search_nodes_) {
714  initial_term_index_[node.constraint] = node.term_index;
715  }
716  search_nodes_.clear();
717  transposition_table_.clear();
718  num_nodes_ = 0;
719  num_skipped_nodes_ = 0;
720 }
721 
722 // In order to restore the synchronization from any state, we backtrack
723 // everything and retry to take the same decisions as before. We stop at the
724 // first one that can't be taken.
726  CHECK_EQ(better_solution_has_been_found_, false);
727  const std::vector<SearchNode> copy = search_nodes_;
728  sat_wrapper_->BacktrackAll();
729  maintainer_.BacktrackAll();
730 
731  // Note(user): at this stage, the sat trail contains the fixed variables.
732  // There will almost always be at the same value in the reference solution.
733  // However since the objective may be over-constrained in the sat_solver, it
734  // is possible that some variable where propagated to some other values.
735  maintainer_.Assign(sat_wrapper_->FullSatTrail());
736 
737  search_nodes_.clear();
738  for (const SearchNode& node : copy) {
739  if (!repairer_.RepairIsValid(node.constraint, node.term_index)) break;
740  search_nodes_.push_back(node);
741  ApplyDecision(repairer_.GetFlip(node.constraint, node.term_index));
742  }
743 }
744 
745 void LocalSearchAssignmentIterator::UseCurrentStateAsReference() {
746  better_solution_has_been_found_ = true;
747  maintainer_.UseCurrentStateAsReference();
748  sat_wrapper_->BacktrackAll();
749 
750  // Note(user): Here, there should be no discrepancies between the fixed
751  // variable and the new reference, so there is no need to do:
752  // maintainer_.Assign(sat_wrapper_->FullSatTrail());
753 
754  for (const SearchNode& node : search_nodes_) {
755  initial_term_index_[node.constraint] = node.term_index;
756  }
757  search_nodes_.clear();
758  transposition_table_.clear();
759  num_nodes_ = 0;
760  num_skipped_nodes_ = 0;
761  ++num_improvements_;
762 }
763 
765  if (sat_wrapper_->IsModelUnsat()) return false;
766  if (maintainer_.IsFeasible()) {
767  UseCurrentStateAsReference();
768  return true;
769  }
770 
771  // We only look for potential one flip repairs if we reached the end of the
772  // LS tree. I tried to do that at every level, but it didn't change the
773  // result much on the set-partitionning example I was using.
774  //
775  // TODO(user): Perform more experiments with this.
776  if (use_potential_one_flip_repairs_ &&
777  search_nodes_.size() == max_num_decisions_) {
778  for (const sat::Literal literal : maintainer_.PotentialOneFlipRepairs()) {
779  if (sat_wrapper_->SatAssignment().VariableIsAssigned(
780  literal.Variable())) {
781  continue;
782  }
783  ++num_inspected_one_flip_repairs_;
784 
785  // Temporarily apply the potential repair and see if it worked!
786  ApplyDecision(literal);
787  if (maintainer_.IsFeasible()) {
788  num_improvements_by_one_flip_repairs_++;
789  UseCurrentStateAsReference();
790  return true;
791  }
792  maintainer_.BacktrackOneLevel();
793  sat_wrapper_->BacktrackOneLevel();
794  }
795  }
796 
797  // If possible, go deeper, i.e. take one more decision.
798  if (!GoDeeper()) {
799  // If not, backtrack to the first node that still has untried way to fix
800  // its associated constraint. Update it to the next untried way.
801  Backtrack();
802  }
803 
804  // All nodes have been explored.
805  if (search_nodes_.empty()) {
806  VLOG(1) << std::string(27, ' ') + "LS " << max_num_decisions_
807  << " finished."
808  << " #explored:" << num_nodes_
809  << " #stored:" << transposition_table_.size()
810  << " #skipped:" << num_skipped_nodes_;
811  return false;
812  }
813 
814  // Apply the next decision, i.e. the literal of the flipped variable.
815  const SearchNode node = search_nodes_.back();
816  ApplyDecision(repairer_.GetFlip(node.constraint, node.term_index));
817  return true;
818 }
819 
820 // TODO(user): The 1.2 multiplier is an approximation only based on the time
821 // spent in the SAT wrapper. So far experiments show a good
822 // correlation with real time, but we might want to be more
823 // accurate.
825  return sat_wrapper_->deterministic_time() * 1.2;
826 }
827 
829  std::string str = "Search nodes:\n";
830  for (int i = 0; i < search_nodes_.size(); ++i) {
831  str += absl::StrFormat(" %d: %d %d\n", i,
832  search_nodes_[i].constraint.value(),
833  search_nodes_[i].term_index.value());
834  }
835  return str;
836 }
837 
838 void LocalSearchAssignmentIterator::ApplyDecision(sat::Literal literal) {
839  ++num_nodes_;
840  const int num_backtracks =
841  sat_wrapper_->ApplyDecision(literal, &tmp_propagated_literals_);
842 
843  // Sync the maintainer with SAT.
844  if (num_backtracks == 0) {
845  maintainer_.AddBacktrackingLevel();
846  maintainer_.Assign(tmp_propagated_literals_);
847  } else {
848  CHECK_GT(num_backtracks, 0);
849  CHECK_LE(num_backtracks, search_nodes_.size());
850 
851  // Only backtrack -1 decisions as the last one has not been pushed yet.
852  for (int i = 0; i < num_backtracks - 1; ++i) {
853  maintainer_.BacktrackOneLevel();
854  }
855  maintainer_.Assign(tmp_propagated_literals_);
856  search_nodes_.resize(search_nodes_.size() - num_backtracks);
857  }
858 }
859 
860 void LocalSearchAssignmentIterator::InitializeTranspositionTableKey(
861  std::array<int32_t, kStoredMaxDecisions>* a) {
862  int i = 0;
863  for (const SearchNode& n : search_nodes_) {
864  // Negated because we already fliped this variable, so GetFlip() will
865  // returns the old value.
866  (*a)[i] = -repairer_.GetFlip(n.constraint, n.term_index).SignedValue();
867  ++i;
868  }
869 
870  // 'a' is not zero-initialized, so we need to complete it with zeros.
871  while (i < kStoredMaxDecisions) {
872  (*a)[i] = 0;
873  ++i;
874  }
875 }
876 
877 bool LocalSearchAssignmentIterator::NewStateIsInTranspositionTable(
878  sat::Literal l) {
879  if (search_nodes_.size() + 1 > kStoredMaxDecisions) return false;
880 
881  // Fill the transposition table element, i.e the array 'a' of decisions.
882  std::array<int32_t, kStoredMaxDecisions> a;
883  InitializeTranspositionTableKey(&a);
884  a[search_nodes_.size()] = l.SignedValue();
885  std::sort(a.begin(), a.begin() + 1 + search_nodes_.size());
886 
887  if (transposition_table_.find(a) == transposition_table_.end()) {
888  return false;
889  } else {
890  ++num_skipped_nodes_;
891  return true;
892  }
893 }
894 
895 void LocalSearchAssignmentIterator::InsertInTranspositionTable() {
896  // If there is more decision that kStoredMaxDecisions, do nothing.
897  if (search_nodes_.size() > kStoredMaxDecisions) return;
898 
899  // Fill the transposition table element, i.e the array 'a' of decisions.
900  std::array<int32_t, kStoredMaxDecisions> a;
901  InitializeTranspositionTableKey(&a);
902  std::sort(a.begin(), a.begin() + search_nodes_.size());
903 
904  transposition_table_.insert(a);
905 }
906 
907 bool LocalSearchAssignmentIterator::EnqueueNextRepairingTermIfAny(
908  ConstraintIndex ct_to_repair, TermIndex term_index) {
909  if (term_index == initial_term_index_[ct_to_repair]) return false;
910  if (term_index == OneFlipConstraintRepairer::kInvalidTerm) {
911  term_index = initial_term_index_[ct_to_repair];
912  }
913  while (true) {
914  term_index = repairer_.NextRepairingTerm(
915  ct_to_repair, initial_term_index_[ct_to_repair], term_index);
916  if (term_index == OneFlipConstraintRepairer::kInvalidTerm) return false;
917  if (!use_transposition_table_ ||
918  !NewStateIsInTranspositionTable(
919  repairer_.GetFlip(ct_to_repair, term_index))) {
920  search_nodes_.push_back(SearchNode(ct_to_repair, term_index));
921  return true;
922  }
923  if (term_index == initial_term_index_[ct_to_repair]) return false;
924  }
925 }
926 
927 bool LocalSearchAssignmentIterator::GoDeeper() {
928  // Can we add one more decision?
929  if (search_nodes_.size() >= max_num_decisions_) {
930  return false;
931  }
932 
933  // Is the number of infeasible constraints reasonable?
934  //
935  // TODO(user): Make this parameters dynamic. We can either try lower value
936  // first and increase it later, or try to dynamically change it during the
937  // search. Another idea is to have instead a "max number of constraints that
938  // can be repaired in one decision" and to take into account the number of
939  // decisions left.
940  if (maintainer_.NumInfeasibleConstraints() > max_num_broken_constraints_) {
941  return false;
942  }
943 
944  // Can we find a constraint that can be repaired in one decision?
945  const ConstraintIndex ct_to_repair = repairer_.ConstraintToRepair();
946  if (ct_to_repair == OneFlipConstraintRepairer::kInvalidConstraint) {
947  return false;
948  }
949 
950  // Add the new decision.
951  //
952  // TODO(user): Store the last explored term index to not start from -1 each
953  // time. This will be very useful when a backtrack occurred due to the SAT
954  // propagator. Note however that this behavior is already enforced when we use
955  // the transposition table, since we will not explore again the branches
956  // already explored.
957  return EnqueueNextRepairingTermIfAny(ct_to_repair,
959 }
960 
961 void LocalSearchAssignmentIterator::Backtrack() {
962  while (!search_nodes_.empty()) {
963  // We finished exploring this node. Store it in the transposition table so
964  // that the same decisions will not be explored again. Note that the SAT
965  // solver may have learned more the second time the exact same decisions are
966  // seen, but we assume that it is not worth exploring again.
967  if (use_transposition_table_) InsertInTranspositionTable();
968 
969  const SearchNode last_node = search_nodes_.back();
970  search_nodes_.pop_back();
971  maintainer_.BacktrackOneLevel();
972  sat_wrapper_->BacktrackOneLevel();
973  if (EnqueueNextRepairingTermIfAny(last_node.constraint,
974  last_node.term_index)) {
975  return;
976  }
977  }
978 }
979 
980 } // namespace bop
981 } // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
#define VLOG(verboselevel)
Definition: base/logging.h:978
size_type size() 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
void ChangeState(IntType i, bool should_be_inside)
Definition: bop_ls.cc:133
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
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
static const ConstraintIndex kInvalidConstraint
Definition: bop_ls.h:445
const BopSolution & solution() const
Definition: bop_base.h:196
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
BooleanVariable Variable() const
Definition: sat_base.h:80
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
Definition: sat_solver.cc:499
void Backtrack(int target_level)
Definition: sat_solver.cc:888
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
SatParameters parameters
SharedTimeLimit * time_limit
const std::string name
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
const bool DEBUG_MODE
Definition: macros.h:24
int64 hash
Definition: matrix_utils.cc:60
void ExtractLearnedInfoFromSatSolver(sat::SatSolver *solver, LearnedInfo *info)
Definition: bop_util.cc:99
constexpr int kObjectiveConstraint
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