OR-Tools  8.2
integer_search.h
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14// This file contains all the top-level logic responsible for driving the search
15// of a satisfiability integer problem. What decision we take next, which new
16// Literal associated to an IntegerLiteral we create and when we restart.
17//
18// For an optimization problem, our algorithm solves a sequence of decision
19// problem using this file as an entry point. Note that some heuristics here
20// still use the objective if there is one in order to orient the search towards
21// good feasible solution though.
22
23#ifndef OR_TOOLS_SAT_INTEGER_SEARCH_H_
24#define OR_TOOLS_SAT_INTEGER_SEARCH_H_
25
26#include <vector>
27
28#include "ortools/sat/integer.h"
31
32namespace operations_research {
33namespace sat {
34
35// This is used to hold the next decision the solver will take. It is either
36// a pure Boolean literal decision or correspond to an IntegerLiteral one.
37//
38// At most one of the two options should be set.
41 explicit BooleanOrIntegerLiteral(LiteralIndex index)
44 : integer_literal(i_lit) {}
45
46 bool HasValue() const {
49 }
50
53};
54
55// Model struct that contains the search heuristics used to find a feasible
56// solution to an integer problem.
57//
58// This is reset by ConfigureSearchHeuristics() and used by
59// SolveIntegerProblem(), see below.
61 // Decision and restart heuristics. The two vectors must be of the same size
62 // and restart_policies[i] will always be used in conjunction with
63 // decision_policies[i].
64 std::vector<std::function<BooleanOrIntegerLiteral()>> decision_policies;
65 std::vector<std::function<bool()>> restart_policies;
66
67 // Index in the vectors above that indicate the current configuration.
69
70 // Two special decision functions that are constructed at loading time.
71 // These are used by ConfigureSearchHeuristics() to fill the policies above.
72 std::function<BooleanOrIntegerLiteral()> fixed_search = nullptr;
73 std::function<BooleanOrIntegerLiteral()> hint_search = nullptr;
74};
75
76// Given a base "fixed_search" function that should mainly control in which
77// order integer variables are lazily instantiated (and at what value), this
78// uses the current solver parameters to set the SearchHeuristics class in the
79// given model.
81
82// Callbacks that will be called when the search goes back to level 0.
83// Callbacks should return false if the propagation fails.
85 std::vector<std::function<bool()>> callbacks;
86};
87
88// Tries to find a feasible solution to the current model.
89//
90// This function continues from the current state of the solver and loop until
91// all variables are instantiated (i.e. the next decision is kNoLiteralIndex) or
92// a search limit is reached. It uses the heuristic from the SearchHeuristics
93// class in the model to decide when to restart and what next decision to take.
94//
95// Each time a restart happen, this increment the policy index modulo the number
96// of heuristics to act as a portfolio search.
98
99// Resets the solver to the given assumptions before calling
100// SolveIntegerProblem().
102 const std::vector<Literal>& assumptions, Model* model);
103
104// Only used in tests. Move to a test utility file.
105//
106// This configures the model SearchHeuristics with a simple default heuristic
107// and then call ResetAndSolveIntegerProblem() without any assumptions.
109
110// Returns decision corresponding to var at its lower bound.
111// Returns an invalid literal if the variable is fixed.
112IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail* integer_trail);
113
114// If a variable appear in the objective, branch on its best objective value.
116
117// Returns decision corresponding to var >= lb + max(1, (ub - lb) / 2). It also
118// CHECKs that the variable is not fixed.
120 IntegerTrail* integer_trail);
121
122// This method first tries var <= value. If this does not reduce the domain it
123// tries var >= value. If that also does not reduce the domain then returns
124// an invalid literal.
125IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value,
126 Model* model);
127
128// Returns decision corresponding to var <= round(lp_value). If the variable
129// does not appear in the LP, this method returns an invalid literal.
131
132// Returns decision corresponding to var <= best_solution[var]. If no solution
133// has been found, this method returns a literal with kNoIntegerVariable. This
134// was suggested in paper: "Solution-Based Phase Saving for CP" (2018) by Emir
135// Demirovic, Geoffrey Chu, and Peter J. Stuckey.
137 Model* model);
138
139// Decision heuristic for SolveIntegerProblemWithLazyEncoding(). Returns a
140// function that will return the literal corresponding to the fact that the
141// first currently non-fixed variable value is <= its min. The function will
142// return kNoLiteralIndex if all the given variables are fixed.
143//
144// Note that this function will create the associated literal if needed.
146 const std::vector<IntegerVariable>& vars, Model* model);
147
148// Decision heuristic for SolveIntegerProblemWithLazyEncoding(). Like
149// FirstUnassignedVarAtItsMinHeuristic() but the function will return the
150// literal corresponding to the fact that the currently non-assigned variable
151// with the lowest min has a value <= this min.
152std::function<BooleanOrIntegerLiteral()>
154 const std::vector<IntegerVariable>& vars, Model* model);
155
156// Set the first unassigned Literal/Variable to its value.
157//
158// TODO(user): This is currently quadratic as we scan all variables to find the
159// first unassigned one. Fix. Note that this is also the case in many other
160// heuristics and should be fixed.
162 BooleanVariable bool_var = kNoBooleanVariable;
163 IntegerVariable int_var = kNoIntegerVariable;
164};
165std::function<BooleanOrIntegerLiteral()> FollowHint(
166 const std::vector<BooleanOrIntegerVariable>& vars,
167 const std::vector<IntegerValue>& values, Model* model);
168
169// Combines search heuristics in order: if the i-th one returns kNoLiteralIndex,
170// ask the (i+1)-th. If every heuristic returned kNoLiteralIndex,
171// returns kNoLiteralIndex.
173 std::vector<std::function<BooleanOrIntegerLiteral()>> heuristics);
174
175// Changes the value of the given decision by 'var_selection_heuristic'. We try
176// to see if the decision is "associated" with an IntegerVariable, and if it is
177// the case, we choose the new value by the first 'value_selection_heuristics'
178// that is applicable. If none of the heuristics are applicable then the given
179// decision by 'var_selection_heuristic' is returned.
181 std::vector<std::function<IntegerLiteral(IntegerVariable)>>
182 value_selection_heuristics,
183 std::function<BooleanOrIntegerLiteral()> var_selection_heuristic,
184 Model* model);
185
186// Changes the value of the given decision by 'var_selection_heuristic'
187// according to various value selection heuristics. Looks at the code to know
188// exactly what heuristic we use.
190 std::function<BooleanOrIntegerLiteral()> var_selection_heuristic,
191 Model* model);
192
193// Returns the BooleanOrIntegerLiteral advised by the underliying SAT solver.
195
196// Gets the branching variable using pseudo costs and combines it with a value
197// for branching.
199
200// Returns true if the number of variables in the linearized part represent
201// a large enough proportion of all the problem variables.
203
204// A restart policy that restarts every k failures.
205std::function<bool()> RestartEveryKFailures(int k, SatSolver* solver);
206
207// A restart policy that uses the underlying sat solver's policy.
208std::function<bool()> SatSolverRestartPolicy(Model* model);
209
210// Concatenates each input_heuristic with a default heuristic that instantiate
211// all the problem's Boolean variables, into a new vector.
212std::vector<std::function<BooleanOrIntegerLiteral()>> CompleteHeuristics(
213 const std::vector<std::function<BooleanOrIntegerLiteral()>>&
214 incomplete_heuristics,
215 const std::function<BooleanOrIntegerLiteral()>& completion_heuristic);
216
217// Specialized search that will continuously probe Boolean variables and bounds
218// of integer variables.
220 const std::vector<BooleanVariable>& bool_vars,
221 const std::vector<IntegerVariable>& int_vars,
222 const std::function<void()>& feasible_solution_observer, Model* model);
223} // namespace sat
224} // namespace operations_research
225
226#endif // OR_TOOLS_SAT_INTEGER_SEARCH_H_
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
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)
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)
const IntegerVariable kNoIntegerVariable(-1)
std::function< bool()> RestartEveryKFailures(int k, SatSolver *solver)
IntegerLiteral SplitDomainUsingBestSolutionValue(IntegerVariable var, Model *model)
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)
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)
bool LinearizedPartIsLarge(Model *model)
std::function< BooleanOrIntegerLiteral()> PseudoCost(Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int index
Definition: pack.cc:508
std::vector< std::function< bool()> > callbacks
std::vector< std::function< bool()> > restart_policies
std::function< BooleanOrIntegerLiteral()> hint_search
std::function< BooleanOrIntegerLiteral()> fixed_search
std::vector< std::function< BooleanOrIntegerLiteral()> > decision_policies