20#include "absl/container/flat_hash_set.h"
21#include "absl/types/span.h"
32#include "ortools/sat/sat_parameters.pb.h"
48 const auto& variables =
51 if (variables.contains(
var)) {
65 const IntegerValue chosen_value =
66 var_lb +
std::max(IntegerValue(1), (var_ub - var_lb) / IntegerValue(2));
74 const IntegerValue ub = integer_trail->UpperBound(
var);
76 const absl::flat_hash_set<IntegerVariable>& variables =
84 const bool branch_down_feasible =
value >= lb &&
value < ub;
85 const bool branch_up_feasible =
value > lb &&
value <= ub;
86 if (variables.contains(
var) && branch_down_feasible) {
88 }
else if (variables.contains(
NegationOf(
var)) && branch_up_feasible) {
90 }
else if (branch_down_feasible) {
92 }
else if (branch_up_feasible) {
102 DCHECK(!integer_trail->IsCurrentlyIgnored(
var));
119 const IntegerValue
value = IntegerValue(
136 const int proto_var =
154 const std::vector<IntegerVariable>& vars,
Model*
model) {
156 return [ vars, integer_trail]() {
157 for (
const IntegerVariable
var : vars) {
159 if (integer_trail->IsCurrentlyIgnored(
var))
continue;
167std::function<BooleanOrIntegerLiteral()>
169 const std::vector<IntegerVariable>& vars,
Model*
model) {
171 return [ vars, integer_trail]() {
173 IntegerValue candidate_lb;
174 for (
const IntegerVariable
var : vars) {
175 if (integer_trail->IsCurrentlyIgnored(
var))
continue;
176 const IntegerValue lb = integer_trail->LowerBound(
var);
190 return [heuristics]() {
191 for (
const auto& h : heuristics) {
193 if (decision.
HasValue())
return decision;
201 value_selection_heuristics,
210 if (!current_decision.
HasValue())
return current_decision;
215 sat_policy->InStablePhase()) {
216 return current_decision;
221 for (
const auto& value_heuristic : value_selection_heuristics) {
226 return current_decision;
233 if (integer_trail->IsCurrentlyIgnored(l.var))
continue;
236 for (
const auto& value_heuristic : value_selection_heuristics) {
242 return current_decision;
247 auto* lp_constraints =
249 int num_lp_variables = 0;
251 num_lp_variables += lp->NumVariables();
253 const int num_integer_variables =
255 return (num_integer_variables <= 2 * num_lp_variables);
262 const SatParameters&
parameters = *(
model->GetOrCreate<SatParameters>());
264 value_selection_heuristics;
273 value_selection_heuristics.push_back([
model](IntegerVariable
var) {
281 if (response_manager !=
nullptr) {
282 VLOG(2) <<
"Using best solution value selection heuristic.";
283 value_selection_heuristics.push_back(
284 [
model, response_manager](IntegerVariable
var) {
286 var, response_manager->SolutionsRepository(),
model);
292 if (
parameters.exploit_relaxation_solution()) {
296 value_selection_heuristics.push_back(
298 VLOG(2) <<
"Using relaxation solution value selection heuristic.";
307 value_selection_heuristics.push_back([
model](IntegerVariable
var) {
313 var_selection_heuristic,
model);
320 return [sat_solver, trail, decision_policy] {
321 const bool all_assigned = trail->Index() == sat_solver->
NumVariables();
323 const Literal result = decision_policy->NextBranch();
331 const bool has_objective =
333 if (!has_objective) {
339 return [pseudo_costs, integer_trail]() {
340 const IntegerVariable chosen_var = pseudo_costs->GetBestDecisionVar();
363 std::discrete_distribution<int> var_dist{3 , 1 };
367 value_selection_heuristics;
368 std::vector<int> value_selection_weight;
371 value_selection_heuristics.push_back([
model](IntegerVariable
var) {
374 value_selection_weight.push_back(8);
378 if (response_manager !=
nullptr) {
379 value_selection_heuristics.push_back(
380 [
model, response_manager](IntegerVariable
var) {
382 var, response_manager->SolutionsRepository(),
model);
384 value_selection_weight.push_back(5);
390 value_selection_heuristics.push_back(
395 value_selection_weight.push_back(3);
400 value_selection_heuristics.push_back([integer_trail](IntegerVariable
var) {
403 value_selection_weight.push_back(1);
406 value_selection_heuristics.push_back([integer_trail](IntegerVariable
var) {
409 value_selection_weight.push_back(1);
412 value_selection_weight.push_back(10);
416 std::discrete_distribution<int> val_dist(value_selection_weight.begin(),
417 value_selection_weight.end());
419 int policy_index = 0;
420 int val_policy_index = 0;
422 return [=]()
mutable {
426 decision_policy->ResetDecisionHeuristic();
429 policy_index = var_dist(*(random));
432 val_policy_index = val_dist(*(random));
437 if (!current_decision.
HasValue())
return current_decision;
440 if (val_policy_index >= value_selection_heuristics.size()) {
441 return current_decision;
446 value_selection_heuristics[val_policy_index](
449 return current_decision;
455 if (integer_trail->IsCurrentlyIgnored(l.var))
continue;
459 value_selection_heuristics[val_policy_index](l.var);
464 return current_decision;
470 const std::vector<BooleanOrIntegerVariable>& vars,
471 const std::vector<IntegerValue>& values,
Model*
model) {
475 for (
int i = 0; i < vars.size(); ++i) {
476 const IntegerValue
value = values[i];
482 const IntegerVariable integer_var = vars[i].int_var;
483 if (integer_trail->IsCurrentlyIgnored(integer_var))
continue;
484 if (integer_trail->IsFixed(integer_var))
continue;
500 bool reset_at_next_call =
true;
501 int next_num_failures = 0;
502 return [=]()
mutable {
503 if (reset_at_next_call) {
505 reset_at_next_call =
false;
506 }
else if (solver->
num_failures() >= next_num_failures) {
507 reset_at_next_call =
true;
509 return reset_at_next_call;
520std::function<BooleanOrIntegerLiteral()> WrapIntegerLiteralHeuristic(
521 std::function<IntegerLiteral()> f) {
522 return [f]() {
return BooleanOrIntegerLiteral(f()); };
534 const SatParameters&
parameters = *(
model->GetOrCreate<SatParameters>());
536 case SatParameters::AUTOMATIC_SEARCH: {
550 case SatParameters::FIXED_SEARCH: {
563 auto no_restart = []() {
return false; };
567 case SatParameters::HINT_SEARCH: {
572 auto no_restart = []() {
return false; };
576 case SatParameters::PORTFOLIO_SEARCH: {
582 for (
const auto&
ct :
584 base_heuristics.push_back(WrapIntegerLiteralHeuristic(
585 ct->HeuristicLpReducedCostBinary(
model)));
586 base_heuristics.push_back(WrapIntegerLiteralHeuristic(
587 ct->HeuristicLpMostInfeasibleBinary(
model)));
599 case SatParameters::LP_SEARCH: {
601 for (
const auto&
ct :
603 lp_heuristics.push_back(WrapIntegerLiteralHeuristic(
604 ct->HeuristicLpReducedCostAverageBranching()));
606 if (lp_heuristics.empty()) {
619 case SatParameters::PSEUDO_COST_SEARCH: {
628 case SatParameters::PORTFOLIO_WITH_QUICK_RESTART_SEARCH: {
641 incomplete_heuristics,
644 complete_heuristics.reserve(incomplete_heuristics.size());
645 for (
const auto& incomplete : incomplete_heuristics) {
646 complete_heuristics.push_back(
649 return complete_heuristics;
665 if (objective !=
nullptr) objective_var = objective->
objective_var;
691 const SatParameters& sat_parameters = *(
model->GetOrCreate<SatParameters>());
695 const int64 conflict_limit = sat_parameters.max_number_of_conflicts();
696 int64 num_decisions_since_last_lp_record_ = 0;
697 int64 num_decisions_without_probing = 0;
699 (sat_solver->
num_failures() - old_num_conflicts < conflict_limit)) {
712 if (integer_trail->HasPendingRootLevelDeduction()) {
720 if (!implied_bounds->EnqueueNewDeductions()) {
724 auto* level_zero_callbacks =
726 for (
const auto& cb : level_zero_callbacks->callbacks) {
732 if (sat_parameters.use_sat_inprocessing() &&
741 if (integer_trail->InPropagationLoop()) {
742 const IntegerVariable
var =
743 integer_trail->NextVariableToBranchOnInPropagationLoop();
753 integer_trail->CurrentBranchHadAnIncompletePropagation()) {
754 const IntegerVariable
var = integer_trail->FirstUnassignedVariable();
759 if (!new_decision.
HasValue())
break;
779 VLOG(1) <<
"Trying to take a decision that is already assigned!"
780 <<
" Fix this. Continuing for now...";
786 sat_parameters.probing_period_at_root() > 0 &&
787 ++num_decisions_without_probing >=
788 sat_parameters.probing_period_at_root()) {
789 num_decisions_without_probing = 0;
792 if (!prober->ProbeOneVariable(
Literal(decision).Variable())) {
823 if (
model->GetOrCreate<SatParameters>()->use_optimization_hints()) {
825 const auto& trail = *
model->GetOrCreate<
Trail>();
826 for (
int i = 0; i < trail.Index(); ++i) {
827 sat_decision->SetAssignmentPreference(trail[i], 0.0);
834 const std::vector<PseudoCosts::VariableBoundChange> bound_changes =
839 old_obj_lb = integer_trail->LowerBound(objective_var);
840 old_obj_ub = integer_trail->UpperBound(objective_var);
851 implied_bounds->ProcessIntegerTrail(
Literal(decision));
857 const IntegerValue new_obj_lb = integer_trail->LowerBound(objective_var);
858 const IntegerValue new_obj_ub = integer_trail->UpperBound(objective_var);
859 const IntegerValue objective_bound_change =
860 (new_obj_lb - old_obj_lb) + (old_obj_ub - new_obj_ub);
861 pseudo_costs->
UpdateCost(bound_changes, objective_bound_change);
878 num_decisions_since_last_lp_record_++;
879 if (num_decisions_since_last_lp_record_ >= 100) {
884 num_decisions_since_last_lp_record_ = 0;
888 return SatSolver::Status::LIMIT_REACHED;
892 const std::vector<Literal>& assumptions,
Model*
model) {
898 for (
const auto& cb : level_zero_callbacks->callbacks) {
910 const IntegerVariable num_vars =
912 std::vector<IntegerVariable> all_variables;
913 for (IntegerVariable
var(0);
var < num_vars; ++
var) {
914 all_variables.push_back(
var);
927 const std::vector<BooleanVariable>& bool_vars,
928 const std::vector<IntegerVariable>& int_vars,
929 const std::function<
void()>& feasible_solution_observer,
Model*
model) {
930 VLOG(1) <<
"Start continuous probing with " << bool_vars.size()
931 <<
" Boolean variables, and " << int_vars.size()
932 <<
" integer variables";
938 const SatParameters& sat_parameters = *(
model->GetOrCreate<SatParameters>());
942 std::vector<BooleanVariable> active_vars;
943 std::vector<BooleanVariable> integer_bounds;
944 absl::flat_hash_set<BooleanVariable> integer_bounds_set;
948 VLOG(1) <<
"Probing loop " << loop++;
951 auto SyncBounds = [solver, &level_zero_callbacks]() {
953 for (
const auto& cb : level_zero_callbacks->callbacks) {
954 if (!cb())
return false;
963 if (sat_parameters.use_sat_inprocessing() &&
971 absl::flat_hash_set<BooleanVariable> probed;
975 for (
const IntegerVariable int_var : int_vars) {
976 if (integer_trail->IsFixed(int_var) ||
977 integer_trail->IsOptional(int_var)) {
981 const BooleanVariable shave_lb =
984 int_var, integer_trail->LowerBound(int_var)))
986 if (!probed.contains(shave_lb)) {
987 probed.insert(shave_lb);
988 if (!prober->ProbeOneVariable(shave_lb)) {
993 const BooleanVariable shave_ub =
996 int_var, integer_trail->UpperBound(int_var)))
998 if (!probed.contains(shave_ub)) {
999 probed.insert(shave_ub);
1000 if (!prober->ProbeOneVariable(shave_ub)) {
1005 if (!SyncBounds()) {
1014 for (
const BooleanVariable& bool_var : bool_vars) {
1019 if (!SyncBounds()) {
1022 if (!probed.contains(bool_var)) {
1023 probed.insert(bool_var);
1024 if (!prober->ProbeOneVariable(bool_var)) {
#define DCHECK_LE(val1, val2)
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK(condition)
#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...
bool IsCurrentlyIgnored(IntegerVariable i) const
IntegerValue UpperBound(IntegerVariable i) const
IntegerValue LowerBound(IntegerVariable i) const
double GetSolutionValue(IntegerVariable variable) const
bool SolutionIsInteger() const
LiteralIndex Index() const
Class that owns everything related to a particular optimization model.
void UpdateCost(const std::vector< VariableBoundChange > &bound_changes, IntegerValue obj_bound_improvement)
int64 num_failures() const
const VariablesAssignment & Assignment() const
Status UnsatStatus() const
void AdvanceDeterministicTime(TimeLimit *limit)
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void Backtrack(int target_level)
bool RestoreSolverToAssumptionLevel()
bool ReapplyAssumptionsIfNeeded()
bool ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)
int CurrentDecisionLevel() const
ValueType GetVariableValueInSolution(int var_index, int solution_index) const
const VariablesAssignment & Assignment() const
bool LiteralIsAssigned(Literal literal) const
bool VariableIsAssigned(BooleanVariable var) const
SharedRelaxationSolutionRepository * relaxation_solutions
SharedTimeLimit * time_limit
const Collection::value_type::second_type & FindWithDefault(const Collection &collection, const typename Collection::value_type::first_type &key, const typename Collection::value_type::second_type &value)
std::vector< std::function< BooleanOrIntegerLiteral()> > CompleteHeuristics(const std::vector< std::function< BooleanOrIntegerLiteral()> > &incomplete_heuristics, const std::function< BooleanOrIntegerLiteral()> &completion_heuristic)
std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic(const std::vector< IntegerVariable > &vars, Model *model)
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, 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()> SequentialSearch(std::vector< std::function< BooleanOrIntegerLiteral()> > heuristics)
IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail *integer_trail)
void RecordLPRelaxationValues(Model *model)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const LiteralIndex kNoLiteralIndex(-1)
IntegerLiteral GreaterOrEqualToMiddleValue(IntegerVariable var, IntegerTrail *integer_trail)
IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value, Model *model)
std::function< BooleanOrIntegerLiteral()> UnassignedVarWithLowestMinAtItsMinHeuristic(const std::vector< IntegerVariable > &vars, Model *model)
SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model *model)
std::function< bool()> SatSolverRestartPolicy(Model *model)
std::function< BooleanOrIntegerLiteral()> FollowHint(const std::vector< BooleanOrIntegerVariable > &vars, const std::vector< IntegerValue > &values, Model *model)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
const IntegerVariable kNoIntegerVariable(-1)
std::function< bool()> RestartEveryKFailures(int k, SatSolver *solver)
IntegerVariable PositiveVariable(IntegerVariable i)
IntegerLiteral ChooseBestObjectiveValue(IntegerVariable var, Model *model)
const BooleanVariable kNoBooleanVariable(-1)
void ConfigureSearchHeuristics(Model *model)
std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic(std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
SatSolver::Status SolveIntegerProblem(Model *model)
std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic(Model *model)
std::vector< PseudoCosts::VariableBoundChange > GetBoundChanges(LiteralIndex decision, Model *model)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
SatSolver::Status ContinuousProbing(const std::vector< BooleanVariable > &bool_vars, const std::vector< IntegerVariable > &int_vars, const std::function< void()> &feasible_solution_observer, Model *model)
IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model *model)
std::function< BooleanOrIntegerLiteral()> RandomizeOnRestartHeuristic(Model *model)
bool LinearizedPartIsLarge(Model *model)
void RandomizeDecisionHeuristic(URBG *random, SatParameters *parameters)
std::function< BooleanOrIntegerLiteral()> PseudoCost(Model *model)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntegerLiteral SplitUsingBestSolutionValueInRepository(IntegerVariable var, const SharedSolutionRepository< int64 > &solution_repo, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
LiteralIndex boolean_literal_index
IntegerLiteral integer_literal
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
IntegerVariable objective_var
std::vector< std::function< bool()> > restart_policies
std::function< BooleanOrIntegerLiteral()> hint_search
std::function< BooleanOrIntegerLiteral()> fixed_search
std::vector< std::function< BooleanOrIntegerLiteral()> > decision_policies