19#include "absl/memory/memory.h"
20#include "absl/strings/str_format.h"
28using ::operations_research::sat::LinearBooleanConstraint;
29using ::operations_research::sat::LinearBooleanProblem;
30using ::operations_research::sat::LinearObjective;
37 int max_num_decisions,
41 max_num_decisions_(max_num_decisions),
42 sat_wrapper_(sat_propagator),
43 assignment_iterator_() {}
47bool LocalSearchOptimizer::ShouldBeRun(
53 const BopParameters&
parameters,
const ProblemState& problem_state,
55 CHECK(learned_info !=
nullptr);
57 learned_info->Clear();
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_);
65 if (state_update_stamp_ != problem_state.update_stamp()) {
67 state_update_stamp_ = problem_state.update_stamp();
68 assignment_iterator_->Synchronize(problem_state);
70 assignment_iterator_->SynchronizeSatWrapper();
72 double prev_deterministic_time = assignment_iterator_->deterministic_time();
73 assignment_iterator_->UseTranspositionTable(
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();
80 while (!
time_limit->LimitReached() && num_assignments_to_explore > 0 &&
81 assignment_iterator_->NextAssignment()) {
83 assignment_iterator_->deterministic_time() - prev_deterministic_time);
84 prev_deterministic_time = assignment_iterator_->deterministic_time();
85 --num_assignments_to_explore;
90 return problem_state.solution().IsFeasible()
98 if (assignment_iterator_->BetterSolutionHasBeenFound()) {
100 learned_info->solution = assignment_iterator_->LastReferenceAssignment();
109 if (num_assignments_to_explore <= 0) {
123template <
typename IntType>
126 saved_sizes_.clear();
127 saved_stack_sizes_.clear();
129 in_stack_.assign(n.value(),
false);
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;
142template <
typename IntType>
144 saved_stack_sizes_.push_back(stack_.size());
145 saved_sizes_.push_back(size_);
148template <
typename IntType>
150 if (saved_stack_sizes_.empty()) {
153 for (
int i = saved_stack_sizes_.back(); i < stack_.size(); ++i) {
154 in_stack_[stack_[i].value()] =
false;
156 stack_.resize(saved_stack_sizes_.back());
157 saved_stack_sizes_.pop_back();
158 size_ = saved_sizes_.back();
159 saved_sizes_.pop_back();
163template <
typename IntType>
165 for (
int i = 0; i < stack_.size(); ++i) {
166 in_stack_[stack_[i].value()] =
false;
169 saved_stack_sizes_.clear();
171 saved_sizes_.clear();
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_() {
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) {
198 CHECK_NE(objective.coefficients(i), 0);
200 const VariableIndex
var(objective.literals(i) - 1);
201 const int64_t
weight = objective.coefficients(i);
202 by_variable_matrix_[
var].push_back(
206 constraint_values_.push_back(0);
210 ConstraintIndex num_constraints_with_objective(1);
211 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
212 if (constraint.literals_size() <= 2) {
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));
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()
234 ++num_constraints_with_objective;
238 infeasible_constraint_set_.ClearAndResize(
239 ConstraintIndex(constraint_values_.size()));
241 CHECK_EQ(constraint_values_.size(), constraint_lower_bounds_.size());
242 CHECK_EQ(constraint_values_.size(), constraint_upper_bounds_.size());
248void AssignmentAndConstraintFeasibilityMaintainer::SetReferenceSolution(
251 infeasible_constraint_set_.BacktrackAll();
253 assignment_ = reference_solution;
254 reference_ = assignment_;
255 flipped_var_trail_backtrack_levels_.clear();
256 flipped_var_trail_.clear();
257 AddBacktrackingLevel();
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;
269 MakeObjectiveConstraintInfeasible(1);
272void AssignmentAndConstraintFeasibilityMaintainer::
273 UseCurrentStateAsReference() {
274 for (
const VariableIndex
var : flipped_var_trail_) {
275 reference_.SetValue(
var, assignment_.Value(
var));
277 flipped_var_trail_.clear();
278 flipped_var_trail_backtrack_levels_.clear();
279 AddBacktrackingLevel();
280 MakeObjectiveConstraintInfeasible(1);
283void AssignmentAndConstraintFeasibilityMaintainer::
284 MakeObjectiveConstraintInfeasible(
int delta) {
286 CHECK(flipped_var_trail_.empty());
289 infeasible_constraint_set_.BacktrackAll();
291 infeasible_constraint_set_.AddBacktrackingLevel();
293 CHECK(!IsFeasible());
295 for (ConstraintIndex
ct(1);
ct < NumConstraints(); ++
ct) {
296 CHECK(ConstraintIsFeasible(
ct));
301void AssignmentAndConstraintFeasibilityMaintainer::Assign(
302 const std::vector<sat::Literal>& literals) {
304 const VariableIndex
var(
literal.Variable().value());
306 if (assignment_.Value(
var) !=
value) {
307 flipped_var_trail_.push_back(
var);
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,
322void AssignmentAndConstraintFeasibilityMaintainer::AddBacktrackingLevel() {
323 flipped_var_trail_backtrack_levels_.push_back(flipped_var_trail_.size());
324 infeasible_constraint_set_.AddBacktrackingLevel();
327void AssignmentAndConstraintFeasibilityMaintainer::BacktrackOneLevel() {
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);
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;
340 flipped_var_trail_.resize(flipped_var_trail_backtrack_levels_.back());
341 flipped_var_trail_backtrack_levels_.pop_back();
342 infeasible_constraint_set_.BacktrackOneLevel();
345void AssignmentAndConstraintFeasibilityMaintainer::BacktrackAll() {
346 while (!flipped_var_trail_backtrack_levels_.empty()) BacktrackOneLevel();
349const std::vector<sat::Literal>&
350AssignmentAndConstraintFeasibilityMaintainer::PotentialOneFlipRepairs() {
351 if (!constraint_set_hasher_.IsInitialized()) {
352 InitializeConstraintSetHasher();
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));
370 tmp_potential_repairs_.clear();
371 const auto it = hash_to_potential_repairs_.find(
hash);
372 if (it != hash_to_potential_repairs_.end()) {
375 if (assignment_.Value(VariableIndex(
literal.Variable().value())) !=
377 tmp_potential_repairs_.push_back(
literal);
381 return tmp_potential_repairs_;
384std::string AssignmentAndConstraintFeasibilityMaintainer::DebugString()
const {
387 for (
bool value : assignment_) {
388 str +=
value ?
" 1 " :
" 0 ";
390 str +=
"\nFlipped variables: ";
392 for (
const VariableIndex
var : flipped_var_trail_) {
393 str += absl::StrFormat(
" %d",
var.value());
395 str +=
"\nmin curr max\n";
396 for (ConstraintIndex
ct(0);
ct < constraint_values_.size(); ++
ct) {
398 str += absl::StrFormat(
"- %d %d\n", constraint_values_[
ct],
399 constraint_upper_bounds_[
ct]);
402 absl::StrFormat(
"%d %d %d\n", constraint_lower_bounds_[
ct],
403 constraint_values_[
ct], constraint_upper_bounds_[
ct]);
409void AssignmentAndConstraintFeasibilityMaintainer::
410 InitializeConstraintSetHasher() {
411 const int num_constraints_with_objective = constraint_upper_bounds_.size();
416 constraint_set_hasher_.Initialize(2 * num_constraints_with_objective);
417 constraint_set_hasher_.IgnoreElement(
419 constraint_set_hasher_.IgnoreElement(
421 for (VariableIndex
var(0);
var < by_variable_matrix_.size(); ++
var) {
424 for (
const bool flip_is_positive : {
true,
false}) {
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(
430 flip_is_positive ? coeff_is_positive : !coeff_is_positive));
432 hash_to_potential_repairs_[
hash].push_back(
433 sat::Literal(sat::BooleanVariable(
var.value()), flip_is_positive));
442OneFlipConstraintRepairer::OneFlipConstraintRepairer(
443 const LinearBooleanProblem& problem,
446 : by_constraint_matrix_(problem.constraints_size() + 1),
447 maintainer_(maintainer),
448 sat_assignment_(sat_assignment) {
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) {
460 CHECK_NE(objective.coefficients(i), 0);
462 const VariableIndex
var(objective.literals(i) - 1);
463 const int64_t
weight = objective.coefficients(i);
464 by_constraint_matrix_[num_constraint].push_back(
469 for (
const LinearBooleanConstraint& constraint : problem.constraints()) {
470 if (constraint.literals_size() <= 2) {
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(
487 SortTermsOfEachConstraints(problem.num_variables());
502 const std::vector<ConstraintIndex>& infeasible_constraints =
504 for (
int index = infeasible_constraints.size() - 1;
index >= 0; --
index) {
505 const ConstraintIndex& i = infeasible_constraints[
index];
507 --num_infeasible_constraints_left;
512 if (num_infeasible_constraints_left == 0 &&
521 int32_t num_branches = 0;
524 sat::BooleanVariable(term.var.value()))) {
527 const int64_t new_value =
529 (maintainer_.
Assignment(term.var) ? -term.weight : term.weight);
530 if (new_value >= lb && new_value <= ub) {
532 if (num_branches >= selected_num_branches)
break;
537 if (num_branches == 0)
continue;
538 if (num_branches < selected_num_branches) {
540 selected_num_branches = num_branches;
541 if (num_branches == 1)
break;
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);
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());
564 sat::BooleanVariable(term.
var.value()))) {
567 const int64_t new_value =
570 if (new_value >= lb && new_value <= ub) {
578 TermIndex term_index)
const {
580 const ConstraintTerm term = by_constraint_matrix_[ct_index][term_index];
582 sat::BooleanVariable(term.
var.value()))) {
585 const int64_t new_value =
591 return (new_value >= lb && new_value <= ub);
595 TermIndex term_index)
const {
596 const ConstraintTerm term = by_constraint_matrix_[ct_index][term_index];
601void OneFlipConstraintRepairer::SortTermsOfEachConstraints(
int num_variables) {
603 for (
const ConstraintTerm& term :
606 objective[term.var] = std::abs(term.weight);
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];
626 std::vector<sat::Literal> propagated_literals;
628 for (
int trail_index = 0; trail_index < trail.
Index(); ++trail_index) {
629 propagated_literals.push_back(trail[trail_index]);
631 return propagated_literals;
635 std::vector<sat::Literal>* propagated_literals) {
638 CHECK(propagated_literals !=
nullptr);
640 propagated_literals->clear();
642 const int new_trail_index =
645 return old_decision_level + 1;
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]);
662 if (old_decision_level > 0) {
663 sat_solver_->
Backtrack(old_decision_level - 1);
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()),
690 problem_state.original_problem().constraints_size() + 1,
692 use_transposition_table_(false),
693 use_potential_one_flip_repairs_(false),
695 num_skipped_nodes_(0),
696 num_improvements_(0),
697 num_improvements_by_one_flip_repairs_(0),
698 num_inspected_one_flip_repairs_(0) {}
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_;
711 better_solution_has_been_found_ =
false;
713 for (
const SearchNode& node : search_nodes_) {
714 initial_term_index_[node.constraint] = node.term_index;
716 search_nodes_.
clear();
717 transposition_table_.clear();
719 num_skipped_nodes_ = 0;
726 CHECK_EQ(better_solution_has_been_found_,
false);
727 const std::vector<SearchNode> copy = search_nodes_;
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));
745void LocalSearchAssignmentIterator::UseCurrentStateAsReference() {
746 better_solution_has_been_found_ =
true;
754 for (
const SearchNode& node : search_nodes_) {
755 initial_term_index_[node.constraint] = node.term_index;
757 search_nodes_.
clear();
758 transposition_table_.clear();
760 num_skipped_nodes_ = 0;
767 UseCurrentStateAsReference();
776 if (use_potential_one_flip_repairs_ &&
777 search_nodes_.size() == max_num_decisions_) {
783 ++num_inspected_one_flip_repairs_;
788 num_improvements_by_one_flip_repairs_++;
789 UseCurrentStateAsReference();
805 if (search_nodes_.empty()) {
806 VLOG(1) << std::string(27,
' ') +
"LS " << max_num_decisions_
808 <<
" #explored:" << num_nodes_
809 <<
" #stored:" << transposition_table_.size()
810 <<
" #skipped:" << num_skipped_nodes_;
815 const SearchNode node = search_nodes_.back();
816 ApplyDecision(repairer_.
GetFlip(node.constraint, node.term_index));
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());
840 const int num_backtracks =
844 if (num_backtracks == 0) {
846 maintainer_.
Assign(tmp_propagated_literals_);
849 CHECK_LE(num_backtracks, search_nodes_.size());
852 for (
int i = 0; i < num_backtracks - 1; ++i) {
855 maintainer_.
Assign(tmp_propagated_literals_);
856 search_nodes_.resize(search_nodes_.size() - num_backtracks);
860void LocalSearchAssignmentIterator::InitializeTranspositionTableKey(
861 std::array<int32_t, kStoredMaxDecisions>*
a) {
863 for (
const SearchNode& n : search_nodes_) {
871 while (i < kStoredMaxDecisions) {
877bool LocalSearchAssignmentIterator::NewStateIsInTranspositionTable(
879 if (search_nodes_.size() + 1 > kStoredMaxDecisions)
return false;
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());
887 if (transposition_table_.find(
a) == transposition_table_.end()) {
890 ++num_skipped_nodes_;
895void LocalSearchAssignmentIterator::InsertInTranspositionTable() {
897 if (search_nodes_.size() > kStoredMaxDecisions)
return;
900 std::array<int32_t, kStoredMaxDecisions>
a;
901 InitializeTranspositionTableKey(&
a);
902 std::sort(
a.begin(),
a.begin() + search_nodes_.size());
904 transposition_table_.insert(
a);
907bool LocalSearchAssignmentIterator::EnqueueNextRepairingTermIfAny(
908 ConstraintIndex ct_to_repair, TermIndex term_index) {
909 if (term_index == initial_term_index_[ct_to_repair])
return false;
911 term_index = initial_term_index_[ct_to_repair];
915 ct_to_repair, initial_term_index_[ct_to_repair], term_index);
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));
923 if (term_index == initial_term_index_[ct_to_repair])
return false;
927bool LocalSearchAssignmentIterator::GoDeeper() {
929 if (search_nodes_.size() >= max_num_decisions_) {
957 return EnqueueNextRepairingTermIfAny(ct_to_repair,
961void LocalSearchAssignmentIterator::Backtrack() {
962 while (!search_nodes_.empty()) {
967 if (use_transposition_table_) InsertInTranspositionTable();
969 const SearchNode last_node = search_nodes_.back();
970 search_nodes_.pop_back();
973 if (EnqueueNextRepairingTermIfAny(last_node.constraint,
974 last_node.term_index)) {
#define CHECK_EQ(val1, val2)
#define CHECK_GT(val1, val2)
#define CHECK_NE(val1, val2)
#define CHECK_LE(val1, val2)
#define DCHECK_EQ(val1, val2)
#define VLOG(verboselevel)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
AssignmentAndConstraintFeasibilityMaintainer(const sat::LinearBooleanProblem &problem)
int64_t ConstraintLowerBound(ConstraintIndex constraint) const
void AddBacktrackingLevel()
void UseCurrentStateAsReference()
int NumInfeasibleConstraints() const
void SetReferenceSolution(const BopSolution &reference_solution)
int64_t ConstraintUpperBound(ConstraintIndex constraint) const
bool ConstraintIsFeasible(ConstraintIndex constraint) const
int64_t ConstraintValue(ConstraintIndex constraint) const
const std::vector< ConstraintIndex > & PossiblyInfeasibleConstraints() const
bool Assignment(VariableIndex var) const
void Assign(const std::vector< sat::Literal > &literals)
const std::vector< sat::Literal > & PotentialOneFlipRepairs()
void ClearAndResize(IntType n)
void AddBacktrackingLevel()
void ChangeState(IntType i, bool should_be_inside)
~LocalSearchAssignmentIterator()
void SynchronizeSatWrapper()
LocalSearchAssignmentIterator(const ProblemState &problem_state, int max_num_decisions, int max_num_broken_constraints, SatWrapper *sat_wrapper)
std::string DebugString() const
void Synchronize(const ProblemState &problem_state)
double deterministic_time() const
LocalSearchOptimizer(const std::string &name, int max_num_decisions, sat::SatSolver *sat_propagator)
~LocalSearchOptimizer() override
sat::Literal GetFlip(ConstraintIndex ct_index, TermIndex term_index) const
static const TermIndex kInvalidTerm
ConstraintIndex ConstraintToRepair() const
bool RepairIsValid(ConstraintIndex ct_index, TermIndex term_index) const
TermIndex NextRepairingTerm(ConstraintIndex ct_index, TermIndex init_term_index, TermIndex start_term_index) const
static const TermIndex kInitTerm
static const ConstraintIndex kInvalidConstraint
const BopSolution & solution() const
SatWrapper(sat::SatSolver *sat_solver)
std::vector< sat::Literal > FullSatTrail() const
int ApplyDecision(sat::Literal decision_literal, std::vector< sat::Literal > *propagated_literals)
void ExtractLearnedInfo(LearnedInfo *info)
bool IsModelUnsat() const
const sat::VariablesAssignment & SatAssignment() const
double deterministic_time() const
BooleanVariable Variable() const
const VariablesAssignment & Assignment() const
const Trail & LiteralTrail() const
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void Backtrack(int target_level)
bool IsModelUnsat() const
int CurrentDecisionLevel() const
double deterministic_time() const
bool VariableIsAssigned(BooleanVariable var) const
SharedTimeLimit * time_limit
void ExtractLearnedInfoFromSatSolver(sat::SatSolver *solver, LearnedInfo *info)
constexpr int kObjectiveConstraint
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...