OR-Tools  8.1
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"
29 #include "ortools/sat/sat_base.h"
30 #include "ortools/sat/sat_solver.h"
31 
32 namespace operations_research {
33 namespace 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.
112 IntegerLiteral 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.
125 IntegerLiteral 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.
130 IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model* model);
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.
152 std::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 };
165 std::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.
198 std::function<BooleanOrIntegerLiteral()> PseudoCost(Model* model);
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.
205 std::function<bool()> RestartEveryKFailures(int k, SatSolver* solver);
206 
207 // A restart policy that uses the underlying sat solver's policy.
208 std::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.
212 std::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_
operations_research::sat::LevelZeroCallbackHelper::callbacks
std::vector< std::function< bool()> > callbacks
Definition: integer_search.h:85
operations_research::sat::GreaterOrEqualToMiddleValue
IntegerLiteral GreaterOrEqualToMiddleValue(IntegerVariable var, IntegerTrail *integer_trail)
Definition: integer_search.cc:59
var
IntVar * var
Definition: expr_array.cc:1858
operations_research::sat::SatSolver::Status
Status
Definition: sat_solver.h:181
operations_research::sat::RestartEveryKFailures
std::function< bool()> RestartEveryKFailures(int k, SatSolver *solver)
Definition: integer_search.cc:499
operations_research::sat::IntegerTrail
Definition: integer.h:533
operations_research::sat::BooleanOrIntegerLiteral
Definition: integer_search.h:39
operations_research::sat::kNoIntegerVariable
const IntegerVariable kNoIntegerVariable(-1)
operations_research::sat::ChooseBestObjectiveValue
IntegerLiteral ChooseBestObjectiveValue(IntegerVariable var, Model *model)
Definition: integer_search.cc:47
operations_research::sat::SearchHeuristics::policy_index
int policy_index
Definition: integer_search.h:68
operations_research::sat::kNoLiteralIndex
const LiteralIndex kNoLiteralIndex(-1)
operations_research::sat::SatSolver
Definition: sat_solver.h:58
operations_research::sat::SearchHeuristics::hint_search
std::function< BooleanOrIntegerLiteral()> hint_search
Definition: integer_search.h:73
value
int64 value
Definition: demon_profiler.cc:43
operations_research::sat::SolveIntegerProblem
SatSolver::Status SolveIntegerProblem(Model *model)
Definition: integer_search.cc:652
operations_research::sat::FollowHint
std::function< BooleanOrIntegerLiteral()> FollowHint(const std::vector< BooleanOrIntegerVariable > &vars, const std::vector< IntegerValue > &values, Model *model)
Definition: integer_search.cc:469
operations_research::sat::SequentialValueSelection
std::function< BooleanOrIntegerLiteral()> SequentialValueSelection(std::vector< std::function< IntegerLiteral(IntegerVariable)>> value_selection_heuristics, std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
Definition: integer_search.cc:199
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::SearchHeuristics::restart_policies
std::vector< std::function< bool()> > restart_policies
Definition: integer_search.h:65
operations_research::sat::CompleteHeuristics
std::vector< std::function< BooleanOrIntegerLiteral()> > CompleteHeuristics(const std::vector< std::function< BooleanOrIntegerLiteral()>> &incomplete_heuristics, const std::function< BooleanOrIntegerLiteral()> &completion_heuristic)
Definition: integer_search.cc:639
sat_solver.h
index
int index
Definition: pack.cc:508
sat_base.h
operations_research::sat::BooleanOrIntegerLiteral::BooleanOrIntegerLiteral
BooleanOrIntegerLiteral(IntegerLiteral i_lit)
Definition: integer_search.h:43
operations_research::sat::IntegerLiteral::var
IntegerVariable var
Definition: integer.h:189
operations_research::sat::ResetAndSolveIntegerProblem
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, Model *model)
Definition: integer_search.cc:891
operations_research::sat::UnassignedVarWithLowestMinAtItsMinHeuristic
std::function< BooleanOrIntegerLiteral()> UnassignedVarWithLowestMinAtItsMinHeuristic(const std::vector< IntegerVariable > &vars, Model *model)
Definition: integer_search.cc:168
operations_research::sat::IntegerValueSelectionHeuristic
std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic(std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
Definition: integer_search.cc:259
operations_research::sat::SatSolverHeuristic
std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic(Model *model)
Definition: integer_search.cc:316
operations_research::sat::BooleanOrIntegerLiteral::boolean_literal_index
LiteralIndex boolean_literal_index
Definition: integer_search.h:51
operations_research::sat::SatSolverRestartPolicy
std::function< bool()> SatSolverRestartPolicy(Model *model)
Definition: integer_search.cc:513
operations_research::sat::BooleanOrIntegerVariable::bool_var
BooleanVariable bool_var
Definition: integer_search.h:162
operations_research::sat::FirstUnassignedVarAtItsMinHeuristic
std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic(const std::vector< IntegerVariable > &vars, Model *model)
Definition: integer_search.cc:153
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::IntegerLiteral
Definition: integer.h:153
operations_research::sat::kNoBooleanVariable
const BooleanVariable kNoBooleanVariable(-1)
operations_research::sat::BooleanOrIntegerLiteral::integer_literal
IntegerLiteral integer_literal
Definition: integer_search.h:52
operations_research::sat::BooleanOrIntegerVariable::int_var
IntegerVariable int_var
Definition: integer_search.h:163
operations_research::sat::AtMinValue
IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail *integer_trail)
Definition: integer_search.cc:39
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::SearchHeuristics
Definition: integer_search.h:60
operations_research::sat::SequentialSearch
std::function< BooleanOrIntegerLiteral()> SequentialSearch(std::vector< std::function< BooleanOrIntegerLiteral()>> heuristics)
Definition: integer_search.cc:188
operations_research::sat::BooleanOrIntegerLiteral::BooleanOrIntegerLiteral
BooleanOrIntegerLiteral()
Definition: integer_search.h:40
operations_research::sat::LevelZeroCallbackHelper
Definition: integer_search.h:84
operations_research::sat::BooleanOrIntegerLiteral::BooleanOrIntegerLiteral
BooleanOrIntegerLiteral(LiteralIndex index)
Definition: integer_search.h:41
operations_research::sat::SplitDomainUsingBestSolutionValue
IntegerLiteral SplitDomainUsingBestSolutionValue(IntegerVariable var, Model *model)
operations_research::sat::BooleanOrIntegerVariable
Definition: integer_search.h:161
operations_research::sat::SplitAroundGivenValue
IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value, Model *model)
Definition: integer_search.cc:70
operations_research::sat::LinearizedPartIsLarge
bool LinearizedPartIsLarge(Model *model)
Definition: integer_search.cc:246
operations_research::sat::SplitAroundLpValue
IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model *model)
Definition: integer_search.cc:98
operations_research::sat::SearchHeuristics::decision_policies
std::vector< std::function< BooleanOrIntegerLiteral()> > decision_policies
Definition: integer_search.h:64
operations_research::sat::ConfigureSearchHeuristics
void ConfigureSearchHeuristics(Model *model)
Definition: integer_search.cc:527
operations_research::sat::ContinuousProbing
SatSolver::Status ContinuousProbing(const std::vector< BooleanVariable > &bool_vars, const std::vector< IntegerVariable > &int_vars, const std::function< void()> &feasible_solution_observer, Model *model)
Definition: integer_search.cc:926
operations_research::sat::PseudoCost
std::function< BooleanOrIntegerLiteral()> PseudoCost(Model *model)
Definition: integer_search.cc:329
integer.h
operations_research::sat::SolveIntegerProblemWithLazyEncoding
SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model *model)
Definition: integer_search.cc:909
operations_research::sat::SearchHeuristics::fixed_search
std::function< BooleanOrIntegerLiteral()> fixed_search
Definition: integer_search.h:72
operations_research::sat::BooleanOrIntegerLiteral::HasValue
bool HasValue() const
Definition: integer_search.h:46