23#ifndef OR_TOOLS_SAT_INTEGER_SEARCH_H_
24#define OR_TOOLS_SAT_INTEGER_SEARCH_H_
31#include "absl/container/flat_hash_set.h"
32#include "absl/types/span.h"
125 const std::vector<Literal>& assumptions,
Model* model);
171 absl::Span<const IntegerVariable> vars,
Model* model);
188 absl::Span<const IntegerVariable> vars,
Model* model);
200 absl::Span<const BooleanOrIntegerVariable> vars,
201 absl::Span<const IntegerValue> values,
Model* model);
216 value_selection_heuristics,
264 incomplete_heuristics,
281 LiteralIndex* decision);
290 must_process_conflict_ =
true;
322 bool must_process_conflict_ =
false;
342 static const int kTestLimitPeriod = 20;
343 static const int kLogPeriod = 5000;
344 static const int kSyncPeriod = 50;
348 void LogStatistics();
352 std::vector<BooleanVariable> bool_vars_;
353 std::vector<IntegerVariable> int_vars_;
373 int64_t num_literals_probed_ = 0;
374 int64_t num_bounds_shaved_ = 0;
375 int64_t num_bounds_tried_ = 0;
376 int64_t num_at_least_one_probed_ = 0;
377 int64_t num_at_most_one_probed_ = 0;
380 int num_logs_remaining_ = 0;
381 int num_syncs_remaining_ = 0;
382 int num_test_limit_remaining_ = 0;
385 bool use_shaving_ =
false;
386 int trail_index_at_start_of_iteration_ = 0;
387 int integer_trail_index_at_start_of_iteration_ = 0;
390 double active_limit_;
392 absl::flat_hash_set<BooleanVariable> probed_bool_vars_;
393 absl::flat_hash_set<LiteralIndex> shaved_literals_;
395 int current_int_var_ = 0;
396 int current_bool_var_ = 0;
397 int current_bv1_ = 0;
398 int current_bv2_ = 0;
399 int random_pair_of_bool_vars_probed_ = 0;
400 int random_triplet_of_bool_vars_probed_ = 0;
401 std::vector<std::vector<Literal>> tmp_dnf_;
402 std::vector<Literal> tmp_literals_;
SatSolver::Status Probe()
ContinuousProber(const CpModelProto &model_proto, Model *model)
The model_proto is just used to construct the lists of variable to probe.
IntegerSearchHelper(Model *model)
bool TakeDecision(Literal decision)
LiteralIndex GetDecisionLiteral(const BooleanOrIntegerLiteral &decision)
bool GetDecision(const std::function< BooleanOrIntegerLiteral()> &f, LiteralIndex *decision)
bool BeforeTakingDecision()
void NotifyThatConflictWasFoundDuringGetDecision()
SatSolver::Status SolveIntegerProblem()
void ConfigureSearchHeuristics(Model *model)
std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic(absl::Span< const IntegerVariable > vars, Model *model)
const LiteralIndex kNoLiteralIndex(-1)
std::function< BooleanOrIntegerLiteral()> DisjunctivePrecedenceSearchHeuristic(Model *model)
std::vector< std::function< BooleanOrIntegerLiteral()> > CompleteHeuristics(absl::Span< const std::function< BooleanOrIntegerLiteral()> > incomplete_heuristics, const std::function< BooleanOrIntegerLiteral()> &completion_heuristic)
std::function< BooleanOrIntegerLiteral()> BoolPseudoCostHeuristic(Model *model)
std::function< BooleanOrIntegerLiteral()> SequentialValueSelection(std::vector< std::function< IntegerLiteral(IntegerVariable)> > value_selection_heuristics, std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic(std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model *model)
const IntegerVariable kNoIntegerVariable(-1)
std::function< BooleanOrIntegerLiteral()> UnassignedVarWithLowestMinAtItsMinHeuristic(absl::Span< const IntegerVariable > vars, Model *model)
IntegerLiteral ChooseBestObjectiveValue(IntegerVariable var, IntegerTrail *integer_trail, ObjectiveDefinition *objective_definition)
If a variable appear in the objective, branch on its best objective value.
IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail *integer_trail)
SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model *model)
std::function< BooleanOrIntegerLiteral()> PseudoCost(Model *model)
std::function< BooleanOrIntegerLiteral()> SchedulingSearchHeuristic(Model *model)
A simple heuristic for scheduling models.
IntegerLiteral SplitDomainUsingBestSolutionValue(IntegerVariable var, Model *model)
std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic(Model *model)
Returns the BooleanOrIntegerLiteral advised by the underlying SAT solver.
std::function< bool()> RestartEveryKFailures(int k, SatSolver *solver)
A restart policy that restarts every k failures.
std::function< BooleanOrIntegerLiteral()> FollowHint(absl::Span< const BooleanOrIntegerVariable > vars, absl::Span< const IntegerValue > values, Model *model)
bool LinearizedPartIsLarge(Model *model)
IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value, Model *model)
const BooleanVariable kNoBooleanVariable(-1)
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, Model *model)
std::function< bool()> SatSolverRestartPolicy(Model *model)
A restart policy that uses the underlying sat solver's policy.
std::function< BooleanOrIntegerLiteral()> LpPseudoCostHeuristic(Model *model)
IntegerLiteral GreaterOrEqualToMiddleValue(IntegerVariable var, IntegerTrail *integer_trail)
std::function< BooleanOrIntegerLiteral()> MostFractionalHeuristic(Model *model)
Choose the variable with most fractional LP value.
std::function< BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(Model *model)
std::function< BooleanOrIntegerLiteral()> SequentialSearch(std::vector< std::function< BooleanOrIntegerLiteral()> > heuristics)
In SWIG mode, we don't want anything besides these top-level includes.
LiteralIndex boolean_literal_index
BooleanOrIntegerLiteral(LiteralIndex index)
BooleanOrIntegerLiteral()=default
IntegerLiteral integer_literal
BooleanOrIntegerLiteral(IntegerLiteral i_lit)
std::function< BooleanOrIntegerLiteral()> fixed_search
Fixed search, built from above building blocks.
std::function< BooleanOrIntegerLiteral()> heuristic_search
std::vector< std::function< bool()> > restart_policies
std::function< BooleanOrIntegerLiteral()> user_search
Contains the search specified by the user in CpModelProto.
std::vector< std::function< BooleanOrIntegerLiteral()> > decision_policies
std::function< BooleanOrIntegerLiteral()> hint_search
std::function< BooleanOrIntegerLiteral()> next_decision_override
std::function< BooleanOrIntegerLiteral()> integer_completion_search
Default integer heuristic that will fix all integer variables.
int policy_index
Index in the vectors above that indicate the current configuration.