27#ifndef ORTOOLS_BOP_BOP_LS_H_
28#define ORTOOLS_BOP_BOP_LS_H_
38#include "absl/container/flat_hash_map.h"
39#include "absl/container/flat_hash_set.h"
40#include "absl/random/bit_gen_ref.h"
41#include "absl/random/random.h"
42#include "absl/strings/string_view.h"
43#include "absl/types/span.h"
82 return sat_solver_->Assignment();
96 std::vector<sat::Literal>* propagated_literals);
117class LocalSearchAssignmentIterator;
136 bool ShouldBeRun(
const ProblemState& problem_state)
const override;
141 int64_t state_update_stamp_;
146 const int max_num_decisions_;
155 std::unique_ptr<LocalSearchAssignmentIterator> assignment_iterator_;
158 absl::BitGenRef random_;
173template <
typename IntType>
186 void ChangeState(IntType i,
bool should_be_inside);
190 int size()
const {
return size_; }
193 const std::vector<IntType>&
Superset()
const {
return stack_; }
206 std::vector<IntType> stack_;
207 std::vector<bool> in_stack_;
211 std::vector<int> saved_sizes_;
212 std::vector<int> saved_stack_sizes_;
217template <
typename IntType>
224 hashes_.resize(size);
225 for (IntType i(0); i < size; ++i) {
226 hashes_[i] = absl::Uniform<uint64_t>(random_);
237 uint64_t
Hash(
const std::vector<IntType>& set)
const {
239 for (
const IntType i : set) hash ^= hashes_[i];
245 uint64_t
Hash(IntType e)
const {
return hashes_[e]; }
251 absl::BitGenRef random_;
311 void Assign(absl::Span<const sat::Literal> literals);
335 bool IsFeasible()
const {
return infeasible_constraint_set_.size() == 0; }
341 return infeasible_constraint_set_.size();
346 return infeasible_constraint_set_.
Superset();
351 size_t NumConstraints()
const {
return constraint_lower_bounds_.size(); }
357 bool Assignment(VariableIndex var)
const {
return assignment_.Value(var); }
364 return constraint_lower_bounds_[constraint];
369 return constraint_upper_bounds_[constraint];
376 return constraint_values_[constraint];
390 void InitializeConstraintSetHasher();
398 ConstraintIndexWithDirection FromConstraintIndex(ConstraintIndex index,
400 return ConstraintIndexWithDirection(2 * index.value() + (up ? 1 : 0));
405 void MakeObjectiveConstraintInfeasible(
int delta);
409 struct ConstraintEntry {
410 ConstraintEntry(ConstraintIndex c, int64_t
w) : constraint(c), weight(
w) {}
411 ConstraintIndex constraint;
415 util_intops::StrongVector<
416 VariableIndex, util_intops::StrongVector<EntryIndex, ConstraintEntry>>
418 util_intops::StrongVector<ConstraintIndex, int64_t> constraint_lower_bounds_;
419 util_intops::StrongVector<ConstraintIndex, int64_t> constraint_upper_bounds_;
421 BopSolution assignment_;
422 BopSolution reference_;
424 util_intops::StrongVector<ConstraintIndex, int64_t> constraint_values_;
425 BacktrackableIntegerSet<ConstraintIndex> infeasible_constraint_set_;
430 std::vector<int> flipped_var_trail_backtrack_levels_;
431 std::vector<VariableIndex> flipped_var_trail_;
434 std::vector<sat::Literal> tmp_potential_repairs_;
435 NonOrderedSetHasher<ConstraintIndexWithDirection> constraint_set_hasher_;
436 absl::flat_hash_map<uint64_t, std::vector<sat::Literal>>
437 hash_to_potential_repairs_;
492 TermIndex init_term_index,
493 TermIndex start_term_index)
const;
497 bool RepairIsValid(ConstraintIndex ct_index, TermIndex term_index)
const;
514 void SortTermsOfEachConstraints(
int num_variables);
518 by_constraint_matrix_;
531 int max_num_decisions,
532 int max_num_broken_constraints,
533 absl::BitGenRef random,
546 use_potential_one_flip_repairs_ = v;
570 return better_solution_has_been_found_;
583 void UseCurrentStateAsReference();
586 static constexpr size_t kStoredMaxDecisions = 4;
594 SearchNode(ConstraintIndex c, TermIndex t) : constraint(c), term_index(t) {}
595 ConstraintIndex constraint;
596 TermIndex term_index;
600 void ApplyDecision(sat::Literal literal);
611 bool NewStateIsInTranspositionTable(sat::Literal l);
614 void InsertInTranspositionTable();
618 void InitializeTranspositionTableKey(
619 std::array<int32_t, kStoredMaxDecisions>* a);
624 bool EnqueueNextRepairingTermIfAny(ConstraintIndex ct_to_repair,
627 const int max_num_decisions_;
628 const int max_num_broken_constraints_;
629 bool better_solution_has_been_found_;
630 AssignmentAndConstraintFeasibilityMaintainer maintainer_;
631 SatWrapper*
const sat_wrapper_;
632 OneFlipConstraintRepairer repairer_;
633 std::vector<SearchNode> search_nodes_;
634 util_intops::StrongVector<ConstraintIndex, TermIndex> initial_term_index_;
637 std::vector<sat::Literal> tmp_propagated_literals_;
652 bool use_transposition_table_;
653 absl::flat_hash_set<std::array<int32_t, kStoredMaxDecisions>>
654 transposition_table_;
656 bool use_potential_one_flip_repairs_;
662 int64_t num_skipped_nodes_;
666 int64_t num_improvements_;
667 int64_t num_improvements_by_one_flip_repairs_;
668 int64_t num_inspected_one_flip_repairs_;
void SetReferenceSolution(const BopSolution &reference_solution)
int64_t ConstraintUpperBound(ConstraintIndex constraint) const
void Assign(absl::Span< const sat::Literal > literals)
void AddBacktrackingLevel()
bool Assignment(VariableIndex var) const
int64_t ConstraintValue(ConstraintIndex constraint) const
AssignmentAndConstraintFeasibilityMaintainer & operator=(const AssignmentAndConstraintFeasibilityMaintainer &)=delete
void UseCurrentStateAsReference()
std::string DebugString() const
const BopSolution & reference() const
const std::vector< ConstraintIndex > & PossiblyInfeasibleConstraints() const
int64_t ConstraintLowerBound(ConstraintIndex constraint) const
static const ConstraintIndex kObjectiveConstraint
const std::vector< sat::Literal > & PotentialOneFlipRepairs()
int NumInfeasibleConstraints() const
AssignmentAndConstraintFeasibilityMaintainer(const sat::LinearBooleanProblem &problem, absl::BitGenRef random)
bool ConstraintIsFeasible(ConstraintIndex constraint) const
size_t NumConstraints() const
BacktrackableIntegerSet()=default
void AddBacktrackingLevel()
void ChangeState(IntType i, bool should_be_inside)
void ClearAndResize(IntType n)
const std::vector< IntType > & Superset() const
BopOptimizerBase(absl::string_view name)
const std::string & name() const
const BopSolution & LastReferenceAssignment() const
~LocalSearchAssignmentIterator()
void UsePotentialOneFlipRepairs(bool v)
void UseTranspositionTable(bool v)
std::string DebugString() const
double deterministic_time() const
LocalSearchAssignmentIterator(const ProblemState &problem_state, int max_num_decisions, int max_num_broken_constraints, absl::BitGenRef random, SatWrapper *sat_wrapper)
bool BetterSolutionHasBeenFound() const
void Synchronize(const ProblemState &problem_state)
void SynchronizeSatWrapper()
LocalSearchAssignmentIterator & operator=(const LocalSearchAssignmentIterator &)=delete
LocalSearchOptimizer(absl::string_view name, int max_num_decisions, absl::BitGenRef random, sat::SatSolver *sat_propagator)
~LocalSearchOptimizer() override
uint64_t Hash(const std::vector< IntType > &set) const
void IgnoreElement(IntType e)
bool IsInitialized() const
void Initialize(int size)
NonOrderedSetHasher(absl::BitGenRef random)
OneFlipConstraintRepairer(const sat::LinearBooleanProblem &problem, const AssignmentAndConstraintFeasibilityMaintainer &maintainer, const sat::VariablesAssignment &sat_assignment)
static const ConstraintIndex kInvalidConstraint
bool RepairIsValid(ConstraintIndex ct_index, TermIndex term_index) const
static const TermIndex kInitTerm
ConstraintIndex ConstraintToRepair() const
OneFlipConstraintRepairer & operator=(const OneFlipConstraintRepairer &)=delete
TermIndex NextRepairingTerm(ConstraintIndex ct_index, TermIndex init_term_index, TermIndex start_term_index) const
sat::Literal GetFlip(ConstraintIndex ct_index, TermIndex term_index) const
static const TermIndex kInvalidTerm
int ApplyDecision(sat::Literal decision_literal, std::vector< sat::Literal > *propagated_literals)
void ExtractLearnedInfo(LearnedInfo *info)
const sat::VariablesAssignment & SatAssignment() const
SatWrapper(const SatWrapper &)=delete
SatWrapper(sat::SatSolver *sat_solver)
bool IsModelUnsat() const
SatWrapper & operator=(const SatWrapper &)=delete
double deterministic_time() const
std::vector< sat::Literal > FullSatTrail() const
trees with all degrees equal w the current value of w
#define DEFINE_STRONG_INDEX_TYPE(index_type_name)
ConstraintTerm(VariableIndex v, int64_t w)