27 #ifndef OR_TOOLS_BOP_BOP_LS_H_
28 #define OR_TOOLS_BOP_BOP_LS_H_
36 #include "absl/container/flat_hash_map.h"
37 #include "absl/container/flat_hash_set.h"
38 #include "absl/random/random.h"
44 #include "ortools/sat/boolean_problem.pb.h"
85 std::vector<sat::Literal>* propagated_literals);
107 class LocalSearchAssignmentIterator;
126 bool ShouldBeRun(
const ProblemState& problem_state)
const override;
131 int64_t state_update_stamp_;
136 const int max_num_decisions_;
145 std::unique_ptr<LocalSearchAssignmentIterator> assignment_iterator_;
148 absl::BitGenRef random_;
163 template <
typename IntType>
176 void ChangeState(IntType i,
bool should_be_inside);
180 int size()
const {
return size_; }
183 const std::vector<IntType>&
Superset()
const {
return stack_; }
196 std::vector<IntType> stack_;
197 std::vector<bool> in_stack_;
201 std::vector<int> saved_sizes_;
202 std::vector<int> saved_stack_sizes_;
207 template <
typename IntType>
215 for (IntType i(0); i < size; ++i) {
216 hashes_[i] = absl::Uniform<uint64_t>(random_);
227 uint64_t
Hash(
const std::vector<IntType>& set)
const {
229 for (
const IntType i : set)
hash ^= hashes_[i];
235 uint64_t
Hash(IntType e)
const {
return hashes_[e]; }
241 absl::BitGenRef random_;
275 const sat::LinearBooleanProblem& problem, absl::BitGenRef random);
295 void Assign(
const std::vector<sat::Literal>& literals);
325 return infeasible_constraint_set_.
size();
330 return infeasible_constraint_set_.
Superset();
348 return constraint_lower_bounds_[constraint];
353 return constraint_upper_bounds_[constraint];
360 return constraint_values_[constraint];
374 void InitializeConstraintSetHasher();
381 DEFINE_STRONG_INDEX_TYPE(ConstraintIndexWithDirection);
382 ConstraintIndexWithDirection FromConstraintIndex(ConstraintIndex
index,
384 return ConstraintIndexWithDirection(2 *
index.value() + (up ? 1 : 0));
389 void MakeObjectiveConstraintInfeasible(
int delta);
393 struct ConstraintEntry {
394 ConstraintEntry(ConstraintIndex c, int64_t w) : constraint(c),
weight(w) {}
395 ConstraintIndex constraint;
405 BopSolution assignment_;
406 BopSolution reference_;
409 BacktrackableIntegerSet<ConstraintIndex> infeasible_constraint_set_;
414 std::vector<int> flipped_var_trail_backtrack_levels_;
415 std::vector<VariableIndex> flipped_var_trail_;
418 std::vector<sat::Literal> tmp_potential_repairs_;
419 NonOrderedSetHasher<ConstraintIndexWithDirection> constraint_set_hasher_;
420 absl::flat_hash_map<uint64_t, std::vector<sat::Literal>>
421 hash_to_potential_repairs_;
447 const sat::LinearBooleanProblem& problem,
473 TermIndex init_term_index,
474 TermIndex start_term_index)
const;
478 bool RepairIsValid(ConstraintIndex ct_index, TermIndex term_index)
const;
495 void SortTermsOfEachConstraints(
int num_variables);
499 by_constraint_matrix_;
514 int max_num_decisions,
515 int max_num_broken_constraints,
516 absl::BitGenRef random,
523 use_potential_one_flip_repairs_ = v;
547 return better_solution_has_been_found_;
560 void UseCurrentStateAsReference();
563 static constexpr
size_t kStoredMaxDecisions = 4;
571 SearchNode(ConstraintIndex c, TermIndex t) : constraint(c), term_index(t) {}
572 ConstraintIndex constraint;
573 TermIndex term_index;
577 void ApplyDecision(sat::Literal
literal);
588 bool NewStateIsInTranspositionTable(sat::Literal l);
591 void InsertInTranspositionTable();
595 void InitializeTranspositionTableKey(
596 std::array<int32_t, kStoredMaxDecisions>*
a);
601 bool EnqueueNextRepairingTermIfAny(ConstraintIndex ct_to_repair,
604 const int max_num_decisions_;
605 const int max_num_broken_constraints_;
606 bool better_solution_has_been_found_;
607 AssignmentAndConstraintFeasibilityMaintainer maintainer_;
608 SatWrapper*
const sat_wrapper_;
609 OneFlipConstraintRepairer repairer_;
610 std::vector<SearchNode> search_nodes_;
614 std::vector<sat::Literal> tmp_propagated_literals_;
629 bool use_transposition_table_;
630 absl::flat_hash_set<std::array<int32_t, kStoredMaxDecisions>>
631 transposition_table_;
633 bool use_potential_one_flip_repairs_;
639 int64_t num_skipped_nodes_;
643 int64_t num_improvements_;
644 int64_t num_improvements_by_one_flip_repairs_;
645 int64_t num_inspected_one_flip_repairs_;
void resize(size_type new_size)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
int64_t ConstraintLowerBound(ConstraintIndex constraint) const
const BopSolution & reference() const
const std::vector< ConstraintIndex > & PossiblyInfeasibleConstraints() const
AssignmentAndConstraintFeasibilityMaintainer(const sat::LinearBooleanProblem &problem, absl::BitGenRef random)
void AddBacktrackingLevel()
void UseCurrentStateAsReference()
static const ConstraintIndex kObjectiveConstraint
int NumInfeasibleConstraints() const
std::string DebugString() const
void SetReferenceSolution(const BopSolution &reference_solution)
int64_t ConstraintUpperBound(ConstraintIndex constraint) const
size_t NumConstraints() const
bool ConstraintIsFeasible(ConstraintIndex constraint) const
int64_t ConstraintValue(ConstraintIndex constraint) const
bool Assignment(VariableIndex var) const
void Assign(const std::vector< sat::Literal > &literals)
const std::vector< sat::Literal > & PotentialOneFlipRepairs()
const std::vector< IntType > & Superset() const
void ClearAndResize(IntType n)
void AddBacktrackingLevel()
BacktrackableIntegerSet()
void ChangeState(IntType i, bool should_be_inside)
const std::string & name() const
bool Value(VariableIndex var) const
~LocalSearchAssignmentIterator()
void SynchronizeSatWrapper()
void UseTranspositionTable(bool v)
std::string DebugString() const
LocalSearchAssignmentIterator(const ProblemState &problem_state, int max_num_decisions, int max_num_broken_constraints, absl::BitGenRef random, SatWrapper *sat_wrapper)
void UsePotentialOneFlipRepairs(bool v)
void Synchronize(const ProblemState &problem_state)
double deterministic_time() const
const BopSolution & LastReferenceAssignment() const
bool BetterSolutionHasBeenFound() const
LocalSearchOptimizer(const std::string &name, int max_num_decisions, absl::BitGenRef random, sat::SatSolver *sat_propagator)
~LocalSearchOptimizer() override
bool IsInitialized() const
void Initialize(int size)
NonOrderedSetHasher(absl::BitGenRef random)
uint64_t Hash(IntType e) const
void IgnoreElement(IntType e)
uint64_t Hash(const std::vector< IntType > &set) const
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
OneFlipConstraintRepairer(const sat::LinearBooleanProblem &problem, const AssignmentAndConstraintFeasibilityMaintainer &maintainer, const sat::VariablesAssignment &sat_assignment)
static const ConstraintIndex kInvalidConstraint
const sat::VariablesAssignment & SatAssignment() 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
double deterministic_time() const
const VariablesAssignment & Assignment() const
bool IsModelUnsat() const
ModelSharedTimeLimit * time_limit
Collection of objects used to extend the Constraint Solver library.
ConstraintTerm(VariableIndex v, int64_t w)