Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
integer_search.h
Go to the documentation of this file.
1// Copyright 2010-2025 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 <stdint.h>
27
28#include <functional>
29#include <vector>
30
31#include "absl/container/flat_hash_set.h"
32#include "absl/types/span.h"
33#include "ortools/sat/clause.h"
37#include "ortools/sat/integer.h"
39#include "ortools/sat/model.h"
40#include "ortools/sat/probing.h"
47#include "ortools/sat/util.h"
50
51namespace operations_research {
52namespace sat {
53
54// This is used to hold the next decision the solver will take. It is either
55// a pure Boolean literal decision or correspond to an IntegerLiteral one.
56//
57// At most one of the two options should be set.
73
74// Model struct that contains the search heuristics used to find a feasible
75// solution to an integer problem.
76//
77// This is reset by ConfigureSearchHeuristics() and used by
78// SolveIntegerProblem(), see below.
80 // Decision and restart heuristics. The two vectors must be of the same size
81 // and restart_policies[i] will always be used in conjunction with
82 // decision_policies[i].
83 std::vector<std::function<BooleanOrIntegerLiteral()>> decision_policies;
84 std::vector<std::function<bool()>> restart_policies;
85
86 // Index in the vectors above that indicate the current configuration.
88
89 // Special decision functions that are constructed at loading time.
90 // These are used by ConfigureSearchHeuristics() to fill the policies above.
91
92 // Contains the search specified by the user in CpModelProto.
93 std::function<BooleanOrIntegerLiteral()> user_search = nullptr;
94
95 // Heuristic search build after introspecting the model. It can be used as
96 // a replacement of the user search. This can include dedicated scheduling or
97 // routing heuristics.
98 std::function<BooleanOrIntegerLiteral()> heuristic_search = nullptr;
99
100 // Default integer heuristic that will fix all integer variables.
102
103 // Fixed search, built from above building blocks.
104 std::function<BooleanOrIntegerLiteral()> fixed_search = nullptr;
105
106 // The search heuristic aims at following the given hint with minimum
107 // deviation.
108 std::function<BooleanOrIntegerLiteral()> hint_search = nullptr;
109
110 // Some search strategy need to take more than one decision at once. They can
111 // set this function that will be called on the next decision. It will be
112 // automatically deleted the first time it returns an empty decision.
114};
115
116// Given a base "fixed_search" function that should mainly control in which
117// order integer variables are lazily instantiated (and at what value), this
118// uses the current solver parameters to set the SearchHeuristics class in the
119// given model.
121
122// Resets the solver to the given assumptions before calling
123// SolveIntegerProblem().
125 const std::vector<Literal>& assumptions, Model* model);
126
127// Only used in tests. Move to a test utility file.
128//
129// This configures the model SearchHeuristics with a simple default heuristic
130// and then call ResetAndSolveIntegerProblem() without any assumptions.
132
133// Returns decision corresponding to var at its lower bound.
134// Returns an invalid literal if the variable is fixed.
135IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail* integer_trail);
136
137// If a variable appear in the objective, branch on its best objective value.
139 IntegerVariable var, IntegerTrail* integer_trail,
140 ObjectiveDefinition* objective_definition);
141
142// Returns decision corresponding to var >= lb + max(1, (ub - lb) / 2). It also
143// CHECKs that the variable is not fixed.
145 IntegerTrail* integer_trail);
146
147// This method first tries var <= value. If this does not reduce the domain it
148// tries var >= value. If that also does not reduce the domain then returns
149// an invalid literal.
150IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value,
151 Model* model);
152
153// Returns decision corresponding to var <= round(lp_value). If the variable
154// does not appear in the LP, this method returns an invalid literal.
155IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model* model);
156
157// Returns decision corresponding to var <= best_solution[var]. If no solution
158// has been found, this method returns a literal with kNoIntegerVariable. This
159// was suggested in paper: "Solution-Based Phase Saving for CP" (2018) by Emir
160// Demirovic, Geoffrey Chu, and Peter J. Stuckey.
162 Model* model);
163
164// Decision heuristic for SolveIntegerProblemWithLazyEncoding(). Returns a
165// function that will return the literal corresponding to the fact that the
166// first currently non-fixed variable value is <= its min. The function will
167// return kNoLiteralIndex if all the given variables are fixed.
168//
169// Note that this function will create the associated literal if needed.
171 absl::Span<const IntegerVariable> vars, Model* model);
172
173// Choose the variable with most fractional LP value.
175
176// Variant used for LbTreeSearch experimentation. Note that each decision is in
177// O(num_variables), but it is kind of ok with LbTreeSearch as we only call this
178// for "new" decision, not when we move around in the tree.
181
182// Decision heuristic for SolveIntegerProblemWithLazyEncoding(). Like
183// FirstUnassignedVarAtItsMinHeuristic() but the function will return the
184// literal corresponding to the fact that the currently non-assigned variable
185// with the lowest min has a value <= this min.
186std::function<BooleanOrIntegerLiteral()>
188 absl::Span<const IntegerVariable> vars, Model* model);
189
190// Set the first unassigned Literal/Variable to its value.
191//
192// TODO(user): This is currently quadratic as we scan all variables to find the
193// first unassigned one. Fix. Note that this is also the case in many other
194// heuristics and should be fixed.
196 BooleanVariable bool_var = kNoBooleanVariable;
197 IntegerVariable int_var = kNoIntegerVariable;
198};
199std::function<BooleanOrIntegerLiteral()> FollowHint(
200 absl::Span<const BooleanOrIntegerVariable> vars,
201 absl::Span<const IntegerValue> values, Model* model);
202
203// Combines search heuristics in order: if the i-th one returns kNoLiteralIndex,
204// ask the (i+1)-th. If every heuristic returned kNoLiteralIndex,
205// returns kNoLiteralIndex.
207 std::vector<std::function<BooleanOrIntegerLiteral()>> heuristics);
208
209// Changes the value of the given decision by 'var_selection_heuristic'. We try
210// to see if the decision is "associated" with an IntegerVariable, and if it is
211// the case, we choose the new value by the first 'value_selection_heuristics'
212// that is applicable. If none of the heuristics are applicable then the given
213// decision by 'var_selection_heuristic' is returned.
215 std::vector<std::function<IntegerLiteral(IntegerVariable)>>
216 value_selection_heuristics,
217 std::function<BooleanOrIntegerLiteral()> var_selection_heuristic,
218 Model* model);
219
220// Changes the value of the given decision by 'var_selection_heuristic'
221// according to various value selection heuristics. Looks at the code to know
222// exactly what heuristic we use.
224 std::function<BooleanOrIntegerLiteral()> var_selection_heuristic,
225 Model* model);
226
227// Returns the BooleanOrIntegerLiteral advised by the underlying SAT solver.
228std::function<BooleanOrIntegerLiteral()> SatSolverHeuristic(Model* model);
229
230// Gets the branching variable using pseudo costs and combines it with a value
231// for branching.
232std::function<BooleanOrIntegerLiteral()> PseudoCost(Model* model);
233
234// Simple scheduling heuristic that looks at all the no-overlap constraints
235// and try to assign and perform the intervals that can be scheduled first.
237 Model* model);
238
239// Compared to SchedulingSearchHeuristic() this one take decision on precedences
240// between tasks. Lazily creating a precedence Boolean for the task in
241// disjunction.
242//
243// Note that this one is meant to be used when all Boolean has been fixed, so
244// more as a "completion" heuristic rather than a fixed search one.
246 Model* model);
248 Model* model);
249
250// Returns true if the number of variables in the linearized part represent
251// a large enough proportion of all the problem variables.
252bool LinearizedPartIsLarge(Model* model);
253
254// A restart policy that restarts every k failures.
255std::function<bool()> RestartEveryKFailures(int k, SatSolver* solver);
256
257// A restart policy that uses the underlying sat solver's policy.
258std::function<bool()> SatSolverRestartPolicy(Model* model);
259
260// Concatenates each input_heuristic with a default heuristic that instantiate
261// all the problem's Boolean variables, into a new vector.
262std::vector<std::function<BooleanOrIntegerLiteral()>> CompleteHeuristics(
263 absl::Span<const std::function<BooleanOrIntegerLiteral()>>
264 incomplete_heuristics,
265 const std::function<BooleanOrIntegerLiteral()>& completion_heuristic);
266
267// An helper class to share the code used by the different kind of search.
269 public:
270 explicit IntegerSearchHelper(Model* model);
271
272 // Executes some code before a new decision.
273 // Returns false if model is UNSAT.
275
276 // Calls the decision heuristics and extract a non-fixed literal.
277 // Note that we do not want to copy the function here.
278 //
279 // Returns false if a conflict was found while trying to take a decision.
280 bool GetDecision(const std::function<BooleanOrIntegerLiteral()>& f,
281 LiteralIndex* decision);
282
283 // Inner function used by GetDecision().
284 // It will create a new associated literal if needed.
285 LiteralIndex GetDecisionLiteral(const BooleanOrIntegerLiteral& decision);
286
287 // Functions passed to GetDecision() might call this to notify a conflict
288 // was detected.
290 must_process_conflict_ = true;
291 }
292
293 // Tries to take the current decision, this might backjump.
294 // Returns false if the model is UNSAT.
295 bool TakeDecision(Literal decision);
296
297 // Tries to find a feasible solution to the current model.
298 //
299 // This function continues from the current state of the solver and loop until
300 // all variables are instantiated (i.e. the next decision is kNoLiteralIndex)
301 // or a search limit is reached. It uses the heuristic from the
302 // SearchHeuristics class in the model to decide when to restart and what next
303 // decision to take.
304 //
305 // Each time a restart happen, this increment the policy index modulo the
306 // number of heuristics to act as a portfolio search.
308
309 private:
310 const SatParameters& parameters_;
311 Model* model_;
312 SatSolver* sat_solver_;
313 IntegerTrail* integer_trail_;
314 IntegerEncoder* encoder_;
315 ImpliedBounds* implied_bounds_;
316 Prober* prober_;
317 ProductDetector* product_detector_;
318 TimeLimit* time_limit_;
319 PseudoCosts* pseudo_costs_;
320 Inprocessing* inprocessing_;
321
322 bool must_process_conflict_ = false;
323};
324
325// This class will loop continuously on model variables and try to probe/shave
326// its bounds.
328 public:
329 // The model_proto is just used to construct the lists of variable to probe.
330 ContinuousProber(const CpModelProto& model_proto, Model* model);
331
332 // Starts or continues probing variables and their bounds.
333 // It returns:
334 // - SatSolver::INFEASIBLE if the problem is proven infeasible.
335 // - SatSolver::FEASIBLE when a feasible solution is found
336 // - SatSolver::LIMIT_REACHED if the limit stored in the model is reached
337 // Calling Probe() after it has returned FEASIBLE or LIMIT_REACHED will resume
338 // probing from its previous state.
340
341 private:
342 static const int kTestLimitPeriod = 20;
343 static const int kLogPeriod = 5000;
344 static const int kSyncPeriod = 50;
345
346 SatSolver::Status ShaveLiteral(Literal literal);
347 bool ReportStatus(SatSolver::Status status);
348 void LogStatistics();
349 SatSolver::Status PeriodicSyncAndCheck();
350
351 // Variables to probe.
352 std::vector<BooleanVariable> bool_vars_;
353 std::vector<IntegerVariable> int_vars_;
354
355 // Model object.
356 Model* model_;
357 SatSolver* sat_solver_;
358 TimeLimit* time_limit_;
359 BinaryImplicationGraph* binary_implication_graph_;
360 ClauseManager* clause_manager_;
361 Trail* trail_;
362 IntegerTrail* integer_trail_;
363 IntegerEncoder* encoder_;
364 Inprocessing* inprocessing_;
365 const SatParameters parameters_;
366 LevelZeroCallbackHelper* level_zero_callbacks_;
367 Prober* prober_;
368 SharedResponseManager* shared_response_manager_;
369 SharedBoundsManager* shared_bounds_manager_;
370 ModelRandomGenerator* random_;
371
372 // Statistics.
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;
378
379 // Period counters;
380 int num_logs_remaining_ = 0;
381 int num_syncs_remaining_ = 0;
382 int num_test_limit_remaining_ = 0;
383
384 // Shaving management.
385 bool use_shaving_ = false;
386 int trail_index_at_start_of_iteration_ = 0;
387 int integer_trail_index_at_start_of_iteration_ = 0;
388
389 // Current state of the probe.
390 double active_limit_;
391 // TODO(user): use 2 vector<bool>.
392 absl::flat_hash_set<BooleanVariable> probed_bool_vars_;
393 absl::flat_hash_set<LiteralIndex> shaved_literals_;
394 int iteration_ = 1;
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_;
403};
404
405} // namespace sat
406} // namespace operations_research
407
408#endif // OR_TOOLS_SAT_INTEGER_SEARCH_H_
ContinuousProber(const CpModelProto &model_proto, Model *model)
The model_proto is just used to construct the lists of variable to probe.
LiteralIndex GetDecisionLiteral(const BooleanOrIntegerLiteral &decision)
bool GetDecision(const std::function< BooleanOrIntegerLiteral()> &f, LiteralIndex *decision)
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.
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.