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"
24
25namespace operations_research {
26namespace bop {
27
28using ::operations_research::sat::LinearBooleanConstraint;
29using ::operations_research::sat::LinearBooleanProblem;
30using ::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
47bool LocalSearchOptimizer::ShouldBeRun(
48 const ProblemState& problem_state) const {
49 return problem_state.solution().IsFeasible();
50}
51
52BopOptimizerBase::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
123template <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
132template <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
142template <typename IntType>
144 saved_stack_sizes_.push_back(stack_.size());
145 saved_sizes_.push_back(size_);
146}
147
148template <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
163template <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
245const ConstraintIndex
247
248void 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
272void 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
283void 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
301void 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
322void AssignmentAndConstraintFeasibilityMaintainer::AddBacktrackingLevel() {
323 flipped_var_trail_backtrack_levels_.push_back(flipped_var_trail_.size());
324 infeasible_constraint_set_.AddBacktrackingLevel();
325}
326
327void 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
345void AssignmentAndConstraintFeasibilityMaintainer::BacktrackAll() {
346 while (!flipped_var_trail_backtrack_levels_.empty()) BacktrackOneLevel();
347}
348
349const std::vector<sat::Literal>&
350AssignmentAndConstraintFeasibilityMaintainer::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
384std::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
409void 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
442OneFlipConstraintRepairer::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
490const ConstraintIndex OneFlipConstraintRepairer::kInvalidConstraint(-1);
491const TermIndex OneFlipConstraintRepairer::kInitTerm(-1);
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
577bool 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
601void OneFlipConstraintRepairer::SortTermsOfEachConstraints(int num_variables) {
602 absl::StrongVector<VariableIndex, int64_t> objective(num_variables, 0);
603 for (const ConstraintTerm& term :
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
621SatWrapper::SatWrapper(sat::SatSolver* sat_solver) : sat_solver_(sat_solver) {}
622
623void SatWrapper::BacktrackAll() { sat_solver_->Backtrack(0); }
624
625std::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
745void 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
838void 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
860void 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
877bool 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
895void 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
907bool 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
927bool 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();
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
961void 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
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
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
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
BooleanVariable Variable() const
Definition: sat_base.h:80
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
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