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
6// http://www.apache.org/licenses/LICENSE-2.0
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.
17package operations_research.sat;
19option csharp_namespace = "Google.OrTools.Sat";
20option go_package = "github.com/google/or-tools/ortools/sat/proto/satparameters";
21option java_package = "com.google.ortools.sat";
22option java_multiple_files = true;
24// Contains the definitions for all the sat algorithm parameters and their
28message SatParameters {
29 // In some context, like in a portfolio of search, it makes sense to name a
30 // given parameters set for logging purpose.
31 optional string name = 171 [default = ""];
33 // ==========================================================================
34 // Branching and polarity
35 // ==========================================================================
37 // Variables without activity (i.e. at the beginning of the search) will be
38 // tried in this preferred order.
40 IN_ORDER = 0; // As specified by the problem.
44 optional VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
46 // Specifies the initial polarity (true/false) when the solver branches on a
47 // variable. This can be modified later by the user, or the phase saving
50 // Note(user): POLARITY_FALSE is usually a good choice because of the
51 // "natural" way to express a linear boolean problem.
57 optional Polarity initial_polarity = 2 [default = POLARITY_FALSE];
59 // If this is true, then the polarity of a variable will be the last value it
60 // was assigned to, or its default polarity if it was never assigned since the
61 // call to ResetDecisionHeuristic().
63 // Actually, we use a newer version where we follow the last value in the
64 // longest non-conflicting partial assignment in the current phase.
66 // This is called 'literal phase saving'. For details see 'A Lightweight
67 // Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and
68 // A.Darwiche, In 10th International Conference on Theory and Applications of
69 // Satisfiability Testing, 2007.
70 optional bool use_phase_saving = 44 [default = true];
72 // If non-zero, then we change the polarity heuristic after that many number
73 // of conflicts in an arithmetically increasing fashion. So x the first time,
74 // 2 * x the second time, etc...
75 optional int32 polarity_rephase_increment = 168 [default = 1000];
77 // If true and we have first solution LS workers, tries in some phase to
78 // follow a LS solutions that violates has litle constraints as possible.
79 optional bool polarity_exploit_ls_hints = 309 [default = false];
81 // The proportion of polarity chosen at random. Note that this take
82 // precedence over the phase saving heuristic. This is different from
83 // initial_polarity:POLARITY_RANDOM because it will select a new random
84 // polarity each time the variable is branched upon instead of selecting one
85 // initially and then always taking this choice.
86 optional double random_polarity_ratio = 45 [default = 0.0];
88 // A number between 0 and 1 that indicates the proportion of branching
89 // variables that are selected randomly instead of choosing the first variable
90 // from the given variable_ordering strategy.
91 optional double random_branches_ratio = 32 [default = 0.0];
93 // Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as
94 // described in "Learning Rate Based Branching Heuristic for SAT solvers",
95 // J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.
96 optional bool use_erwa_heuristic = 75 [default = false];
98 // The initial value of the variables activity. A non-zero value only make
99 // sense when use_erwa_heuristic is true. Experiments with a value of 1e-2
100 // together with the ERWA heuristic showed slighthly better result than simply
101 // using zero. The idea is that when the "learning rate" of a variable becomes
102 // lower than this value, then we prefer to branch on never explored before
103 // variables. This is not in the ERWA paper.
104 optional double initial_variables_activity = 76 [default = 0.0];
106 // When this is true, then the variables that appear in any of the reason of
107 // the variables in a conflict have their activity bumped. This is addition to
108 // the variables in the conflict, and the one that were used during conflict
110 optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];
112 // ==========================================================================
114 // ==========================================================================
116 // Do we try to minimize conflicts (greedily) when creating them.
117 enum ConflictMinimizationAlgorithm {
123 optional ConflictMinimizationAlgorithm minimization_algorithm = 4
124 [default = RECURSIVE];
126 // Whether to expoit the binary clause to minimize learned clauses further.
127 enum BinaryMinizationAlgorithm {
128 NO_BINARY_MINIMIZATION = 0;
129 BINARY_MINIMIZATION_FIRST = 1;
130 BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION = 4;
131 BINARY_MINIMIZATION_WITH_REACHABILITY = 2;
132 EXPERIMENTAL_BINARY_MINIMIZATION = 3;
134 optional BinaryMinizationAlgorithm binary_minimization_algorithm = 34
135 [default = BINARY_MINIMIZATION_FIRST];
137 // At a really low cost, during the 1-UIP conflict computation, it is easy to
138 // detect if some of the involved reasons are subsumed by the current
139 // conflict. When this is true, such clauses are detached and later removed
141 optional bool subsumption_during_conflict_analysis = 56 [default = true];
143 // ==========================================================================
144 // Clause database management
145 // ==========================================================================
147 // Trigger a cleanup when this number of "deletable" clauses is learned.
148 optional int32 clause_cleanup_period = 11 [default = 10000];
150 // During a cleanup, we will always keep that number of "deletable" clauses.
151 // Note that this doesn't include the "protected" clauses.
152 optional int32 clause_cleanup_target = 13 [default = 0];
154 // During a cleanup, if clause_cleanup_target is 0, we will delete the
155 // clause_cleanup_ratio of "deletable" clauses instead of aiming for a fixed
156 // target of clauses to keep.
157 optional double clause_cleanup_ratio = 190 [default = 0.5];
159 // Each time a clause activity is bumped, the clause has a chance to be
160 // protected during the next cleanup phase. Note that clauses used as a reason
161 // are always protected.
162 enum ClauseProtection {
163 PROTECTION_NONE = 0; // No protection.
164 PROTECTION_ALWAYS = 1; // Protect all clauses whose activity is bumped.
165 PROTECTION_LBD = 2; // Only protect clause with a better LBD.
167 optional ClauseProtection clause_cleanup_protection = 58
168 [default = PROTECTION_NONE];
170 // All the clauses with a LBD (literal blocks distance) lower or equal to this
171 // parameters will always be kept.
172 optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
174 // The clauses that will be kept during a cleanup are the ones that come
175 // first under this order. We always keep or exclude ties together.
176 enum ClauseOrdering {
177 // Order clause by decreasing activity, then by increasing LBD.
179 // Order clause by increasing LBD, then by decreasing activity.
182 optional ClauseOrdering clause_cleanup_ordering = 60
183 [default = CLAUSE_ACTIVITY];
185 // Same as for the clauses, but for the learned pseudo-Boolean constraints.
186 optional int32 pb_cleanup_increment = 46 [default = 200];
187 optional double pb_cleanup_ratio = 47 [default = 0.5];
189 // ==========================================================================
190 // Variable and clause activities
191 // ==========================================================================
193 // Each time a conflict is found, the activities of some variables are
194 // increased by one. Then, the activity of all variables are multiplied by
195 // variable_activity_decay.
197 // To implement this efficiently, the activity of all the variables is not
198 // decayed at each conflict. Instead, the activity increment is multiplied by
199 // 1 / decay. When an activity reach max_variable_activity_value, all the
200 // activity are multiplied by 1 / max_variable_activity_value.
201 optional double variable_activity_decay = 15 [default = 0.8];
202 optional double max_variable_activity_value = 16 [default = 1e100];
204 // The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until
205 // 0.95. This "hack" seems to work well and comes from:
207 // Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013
208 // http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136
209 optional double glucose_max_decay = 22 [default = 0.95];
210 optional double glucose_decay_increment = 23 [default = 0.01];
211 optional int32 glucose_decay_increment_period = 24 [default = 5000];
213 // Clause activity parameters (same effect as the one on the variables).
214 optional double clause_activity_decay = 17 [default = 0.999];
215 optional double max_clause_activity_value = 18 [default = 1e20];
217 // ==========================================================================
219 // ==========================================================================
221 // Restart algorithms.
223 // A reference for the more advanced ones is:
224 // Gilles Audemard, Laurent Simon, "Refining Restarts Strategies for SAT
225 // and UNSAT", Principles and Practice of Constraint Programming Lecture
226 // Notes in Computer Science 2012, pp 118-126
227 enum RestartAlgorithm {
230 // Just follow a Luby sequence times restart_period.
233 // Moving average restart based on the decision level of conflicts.
234 DL_MOVING_AVERAGE_RESTART = 2;
236 // Moving average restart based on the LBD of conflicts.
237 LBD_MOVING_AVERAGE_RESTART = 3;
239 // Fixed period restart every restart period.
243 // The restart strategies will change each time the strategy_counter is
244 // increased. The current strategy will simply be the one at index
245 // strategy_counter modulo the number of strategy. Note that if this list
246 // includes a NO_RESTART, nothing will change when it is reached because the
247 // strategy_counter will only increment after a restart.
249 // The idea of switching of search strategy tailored for SAT/UNSAT comes from
250 // Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/.
251 // But more generally, it seems REALLY beneficial to try different strategy.
252 repeated RestartAlgorithm restart_algorithms = 61;
253 optional string default_restart_algorithms = 70
255 "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
257 // Restart period for the FIXED_RESTART strategy. This is also the multiplier
258 // used by the LUBY_RESTART strategy.
259 optional int32 restart_period = 30 [default = 50];
261 // Size of the window for the moving average restarts.
262 optional int32 restart_running_window_size = 62 [default = 50];
264 // In the moving average restart algorithms, a restart is triggered if the
265 // window average times this ratio is greater that the global average.
266 optional double restart_dl_average_ratio = 63 [default = 1.0];
267 optional double restart_lbd_average_ratio = 71 [default = 1.0];
269 // Block a moving restart algorithm if the trail size of the current conflict
270 // is greater than the multiplier times the moving average of the trail size
271 // at the previous conflicts.
272 optional bool use_blocking_restart = 64 [default = false];
273 optional int32 blocking_restart_window_size = 65 [default = 5000];
274 optional double blocking_restart_multiplier = 66 [default = 1.4];
276 // After each restart, if the number of conflict since the last strategy
277 // change is greater that this, then we increment a "strategy_counter" that
278 // can be use to change the search strategy used by the following restarts.
279 optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];
281 // The parameter num_conflicts_before_strategy_changes is increased by that
282 // much after each strategy change.
283 optional double strategy_change_increase_ratio = 69 [default = 0.0];
285 // ==========================================================================
287 // ==========================================================================
289 // Maximum time allowed in seconds to solve a problem.
290 // The counter will starts at the beginning of the Solve() call.
291 optional double max_time_in_seconds = 36 [default = inf];
293 // Maximum time allowed in deterministic time to solve a problem.
294 // The deterministic time should be correlated with the real time used by the
295 // solver, the time unit being as close as possible to a second.
296 optional double max_deterministic_time = 67 [default = inf];
298 // Stops after that number of batches has been scheduled. This only make sense
299 // when interleave_search is true.
300 optional int32 max_num_deterministic_batches = 291 [default = 0];
302 // Maximum number of conflicts allowed to solve a problem.
304 // TODO(user): Maybe change the way the conflict limit is enforced?
305 // currently it is enforced on each independent internal SAT solve, rather
306 // than on the overall number of conflicts across all solves. So in the
307 // context of an optimization problem, this is not really usable directly by a
309 optional int64 max_number_of_conflicts = 37
310 [default = 0x7FFFFFFFFFFFFFFF]; // kint64max
312 // Maximum memory allowed for the whole thread containing the solver. The
313 // solver will abort as soon as it detects that this limit is crossed. As a
314 // result, this limit is approximative, but usually the solver will not go too
317 // TODO(user): This is only used by the pure SAT solver, generalize to CP-SAT.
318 optional int64 max_memory_in_mb = 40 [default = 10000];
320 // Stop the search when the gap between the best feasible objective (O) and
321 // our best objective bound (B) is smaller than a limit.
322 // The exact definition is:
323 // - Absolute: abs(O - B)
324 // - Relative: abs(O - B) / max(1, abs(O)).
326 // Important: The relative gap depends on the objective offset! If you
327 // artificially shift the objective, you will get widely different value of
330 // Note that if the gap is reached, the search status will be OPTIMAL. But
331 // one can check the best objective bound to see the actual gap.
333 // If the objective is integer, then any absolute gap < 1 will lead to a true
334 // optimal. If the objective is floating point, a gap of zero make little
335 // sense so is is why we use a non-zero default value. At the end of the
336 // search, we will display a warning if OPTIMAL is reported yet the gap is
337 // greater than this absolute gap.
338 optional double absolute_gap_limit = 159 [default = 1e-4];
339 optional double relative_gap_limit = 160 [default = 0.0];
341 // ==========================================================================
343 // ==========================================================================
345 // At the beginning of each solve, the random number generator used in some
346 // part of the solver is reinitialized to this seed. If you change the random
347 // seed, the solver may make different choices during the solving process.
349 // For some problems, the running time may vary a lot depending on small
350 // change in the solving algorithm. Running the solver with different seeds
351 // enables to have more robust benchmarks when evaluating new features.
352 optional int32 random_seed = 31 [default = 1];
354 // This is mainly here to test the solver variability. Note that in tests, if
355 // not explicitly set to false, all 3 options will be set to true so that
356 // clients do not rely on the solver returning a specific solution if they are
357 // many equivalent optimal solutions.
358 optional bool permute_variable_randomly = 178 [default = false];
359 optional bool permute_presolve_constraint_order = 179 [default = false];
360 optional bool use_absl_random = 180 [default = false];
362 // Whether the solver should log the search progress. This is the maing
363 // logging parameter and if this is false, none of the logging (callbacks,
364 // log_to_stdout, log_to_response, ...) will do anything.
365 optional bool log_search_progress = 41 [default = false];
367 // Whether the solver should display per sub-solver search statistics.
368 // This is only useful is log_search_progress is set to true, and if the
369 // number of search workers is > 1. Note that in all case we display a bit
370 // of stats with one line per subsolver.
371 optional bool log_subsolver_statistics = 189 [default = false];
373 // Add a prefix to all logs.
374 optional string log_prefix = 185 [default = ""];
377 optional bool log_to_stdout = 186 [default = true];
379 // Log to response proto.
380 optional bool log_to_response = 187 [default = false];
382 // Whether to use pseudo-Boolean resolution to analyze a conflict. Note that
383 // this option only make sense if your problem is modelized using
384 // pseudo-Boolean constraints. If you only have clauses, this shouldn't change
385 // anything (except slow the solver down).
386 optional bool use_pb_resolution = 43 [default = false];
388 // A different algorithm during PB resolution. It minimizes the number of
389 // calls to ReduceCoefficients() which can be time consuming. However, the
390 // search space will be different and if the coefficients are large, this may
391 // lead to integer overflows that could otherwise be prevented.
392 optional bool minimize_reduction_during_pb_resolution = 48 [default = false];
394 // Whether or not the assumption levels are taken into account during the LBD
395 // computation. According to the reference below, not counting them improves
396 // the solver in some situation. Note that this only impact solves under
399 // Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for
400 // Incremental SAT Solving with Assumptions: Application to MUS Extraction"
401 // Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes
402 // in Computer Science Volume 7962, 2013, pp 309-317.
403 optional bool count_assumption_levels_in_lbd = 49 [default = true];
405 // ==========================================================================
407 // ==========================================================================
409 // During presolve, only try to perform the bounded variable elimination (BVE)
410 // of a variable x if the number of occurrences of x times the number of
411 // occurrences of not(x) is not greater than this parameter.
412 optional int32 presolve_bve_threshold = 54 [default = 500];
414 // During presolve, we apply BVE only if this weight times the number of
415 // clauses plus the number of clause literals is not increased.
416 optional int32 presolve_bve_clause_weight = 55 [default = 3];
418 // The maximum "deterministic" time limit to spend in probing. A value of
419 // zero will disable the probing.
421 // TODO(user): Clean up. The first one is used in CP-SAT, the other in pure
423 optional double probing_deterministic_time_limit = 226 [default = 1.0];
424 optional double presolve_probing_deterministic_time_limit = 57
427 // Whether we use an heuristic to detect some basic case of blocked clause
428 // in the SAT presolve.
429 optional bool presolve_blocked_clause = 88 [default = true];
431 // Whether or not we use Bounded Variable Addition (BVA) in the presolve.
432 optional bool presolve_use_bva = 72 [default = true];
434 // Apply Bounded Variable Addition (BVA) if the number of clauses is reduced
435 // by stricly more than this threshold. The algorithm described in the paper
436 // uses 0, but quick experiments showed that 1 is a good value. It may not be
437 // worth it to add a new variable just to remove one clause.
438 optional int32 presolve_bva_threshold = 73 [default = 1];
440 // In case of large reduction in a presolve iteration, we perform multiple
441 // presolve iterations. This parameter controls the maximum number of such
442 // presolve iterations.
443 optional int32 max_presolve_iterations = 138 [default = 3];
445 // Whether we presolve the cp_model before solving it.
446 optional bool cp_model_presolve = 86 [default = true];
448 // How much effort do we spend on probing. 0 disables it completely.
449 optional int32 cp_model_probing_level = 110 [default = 2];
451 // Whether we also use the sat presolve when cp_model_presolve is true.
452 optional bool cp_model_use_sat_presolve = 93 [default = true];
454 // If cp_model_presolve is true and there is a large proportion of fixed
455 // variable after the first model copy, remap all the model to a dense set of
456 // variable before the full presolve even starts. This should help for LNS on
458 optional bool remove_fixed_variables_early = 310 [default = true];
460 // If true, we detect variable that are unique to a table constraint and only
461 // there to encode a cost on each tuple. This is usually the case when a WCSP
462 // (weighted constraint program) is encoded into CP-SAT format.
464 // This can lead to a dramatic speed-up for such problems but is still
465 // experimental at this point.
466 optional bool detect_table_with_cost = 216 [default = false];
468 // How much we try to "compress" a table constraint. Compressing more leads to
469 // less Booleans and faster propagation but can reduced the quality of the lp
470 // relaxation. Values goes from 0 to 3 where we always try to fully compress a
471 // table. At 2, we try to automatically decide if it is worth it.
472 optional int32 table_compression_level = 217 [default = 2];
474 // If true, expand all_different constraints that are not permutations.
475 // Permutations (#Variables = #Values) are always expanded.
476 optional bool expand_alldiff_constraints = 170 [default = false];
478 // If true, expand the reservoir constraints by creating booleans for all
479 // possible precedences between event and encoding the constraint.
480 optional bool expand_reservoir_constraints = 182 [default = true];
482 // Mainly useful for testing.
484 // If this and expand_reservoir_constraints is true, we use a different
485 // encoding of the reservoir constraint using circuit instead of precedences.
486 // Note that this is usually slower, but can exercise different part of the
487 // solver. Note that contrary to the precedence encoding, this easily support
490 // WARNING: with this encoding, the constraint takes a slightly different
491 // meaning. There must exist a permutation of the events occurring at the same
492 // time such that the level is within the reservoir after each of these events
493 // (in this permuted order). So we cannot have +100 and -100 at the same time
494 // if the level must be between 0 and 10 (as authorized by the reservoir
496 optional bool expand_reservoir_using_circuit = 288 [default = false];
498 // Encore cumulative with fixed demands and capacity as a reservoir
499 // constraint. The only reason you might want to do that is to test the
500 // reservoir propagation code!
501 optional bool encode_cumulative_as_reservoir = 287 [default = false];
503 // If the number of expressions in the lin_max is less that the max size
504 // parameter, model expansion replaces target = max(xi) by linear constraint
505 // with the introduction of new booleans bi such that bi => target == xi.
507 // This is mainly for experimenting compared to a custom lin_max propagator.
508 optional int32 max_lin_max_size_for_expansion = 280 [default = 0];
510 // If true, it disable all constraint expansion.
511 // This should only be used to test the presolve of expanded constraints.
512 optional bool disable_constraint_expansion = 181 [default = false];
514 // Linear constraint with a complex right hand side (more than a single
515 // interval) need to be expanded, there is a couple of way to do that.
516 optional bool encode_complex_linear_constraint_with_integer = 223
519 // During presolve, we use a maximum clique heuristic to merge together
520 // no-overlap constraints or at most one constraints. This code can be slow,
521 // so we have a limit in place on the number of explored nodes in the
522 // underlying graph. The internal limit is an int64, but we use double here to
523 // simplify manual input.
524 optional double merge_no_overlap_work_limit = 145 [default = 1e12];
525 optional double merge_at_most_one_work_limit = 146 [default = 1e8];
527 // How much substitution (also called free variable aggregation in MIP
528 // litterature) should we perform at presolve. This currently only concerns
529 // variable appearing only in linear constraints. For now the value 0 turns it
530 // off and any positive value performs substitution.
531 optional int32 presolve_substitution_level = 147 [default = 1];
533 // If true, we will extract from linear constraints, enforcement literals of
534 // the form "integer variable at bound => simplified constraint". This should
535 // always be beneficial except that we don't always handle them as efficiently
536 // as we could for now. This causes problem on manna81.mps (LP relaxation not
537 // as tight it seems) and on neos-3354841-apure.mps.gz (too many literals
538 // created this way).
539 optional bool presolve_extract_integer_enforcement = 174 [default = false];
541 // A few presolve operations involve detecting constraints included in other
542 // constraint. Since there can be a quadratic number of such pairs, and
543 // processing them usually involve scanning them, the complexity of these
544 // operations can be big. This enforce a local deterministic limit on the
545 // number of entries scanned. Default is 1e8.
547 // A value of zero will disable these presolve rules completely.
548 optional int64 presolve_inclusion_work_limit = 201 [default = 100000000];
550 // If true, we don't keep names in our internal copy of the user given model.
551 optional bool ignore_names = 202 [default = true];
553 // Run a max-clique code amongst all the x != y we can find and try to infer
554 // set of variables that are all different. This allows to close neos16.mps
555 // for instance. Note that we only run this code if there is no all_diff
556 // already in the model so that if a user want to add some all_diff, we assume
557 // it is well done and do not try to add more.
559 // This will also detect and add no_overlap constraints, if all the relations
560 // x != y have "offsets" between them. I.e. x > y + offset.
561 optional bool infer_all_diffs = 233 [default = true];
563 // Try to find large "rectangle" in the linear constraint matrix with
564 // identical lines. If such rectangle is big enough, we can introduce a new
565 // integer variable corresponding to the common expression and greatly reduce
566 // the number of non-zero.
567 optional bool find_big_linear_overlap = 234 [default = true];
569 // ==========================================================================
571 // ==========================================================================
573 // Enable or disable "inprocessing" which is some SAT presolving done at
574 // each restart to the root level.
575 optional bool use_sat_inprocessing = 163 [default = true];
577 // Proportion of deterministic time we should spend on inprocessing.
578 // At each "restart", if the proportion is below this ratio, we will do some
579 // inprocessing, otherwise, we skip it for this restart.
580 optional double inprocessing_dtime_ratio = 273 [default = 0.2];
582 // The amount of dtime we should spend on probing for each inprocessing round.
583 optional double inprocessing_probing_dtime = 274 [default = 1.0];
585 // Parameters for an heuristic similar to the one described in "An effective
586 // learnt clause minimization approach for CDCL Sat Solvers",
587 // https://www.ijcai.org/proceedings/2017/0098.pdf
589 // This is the amount of dtime we should spend on this technique during each
590 // inprocessing phase.
592 // The minimization technique is the same as the one used to minimize core in
593 // max-sat. We also minimize problem clauses and not just the learned clause
594 // that we keep forever like in the paper.
595 optional double inprocessing_minimization_dtime = 275 [default = 1.0];
596 optional bool inprocessing_minimization_use_conflict_analysis = 297
598 optional bool inprocessing_minimization_use_all_orderings = 298
601 // ==========================================================================
603 // ==========================================================================
605 // Specify the number of parallel workers (i.e. threads) to use during search.
606 // This should usually be lower than your number of available cpus +
607 // hyperthread in your machine.
609 // A value of 0 means the solver will try to use all cores on the machine.
610 // A number of 1 means no parallelism.
612 // Note that 'num_workers' is the preferred name, but if it is set to zero,
613 // we will still read the deprecated 'num_search_workers'.
615 // As of 2020-04-10, if you're using SAT via MPSolver (to solve integer
616 // programs) this field is overridden with a value of 8, if the field is not
617 // set *explicitly*. Thus, always set this field explicitly or via
618 // MPSolver::SetNumThreads().
619 optional int32 num_workers = 206 [default = 0];
620 optional int32 num_search_workers = 100 [default = 0];
622 // We distinguish subsolvers that consume a full thread, and the ones that are
623 // always interleaved. If left at zero, we will fix this with a default
624 // formula that depends on num_workers. But if you start modifying what runs,
625 // you might want to fix that to a given value depending on the num_workers
627 optional int32 num_full_subsolvers = 294 [default = 0];
629 // In multi-thread, the solver can be mainly seen as a portfolio of solvers
630 // with different parameters. This field indicates the names of the parameters
631 // that are used in multithread. This only applies to "full" subsolvers.
633 // See cp_model_search.cc to see a list of the names and the default value (if
634 // left empty) that looks like:
635 // - default_lp (linearization_level:1)
636 // - fixed (only if fixed search specified or scheduling)
637 // - no_lp (linearization_level:0)
638 // - max_lp (linearization_level:2)
639 // - pseudo_costs (only if objective, change search heuristic)
640 // - reduced_costs (only if objective, change search heuristic)
641 // - quick_restart (kind of probing)
642 // - quick_restart_no_lp (kind of probing with linearization_level:0)
643 // - lb_tree_search (to improve lower bound, MIP like tree search)
644 // - probing (continuous probing and shaving)
646 // Also, note that some set of parameters will be ignored if they do not make
647 // sense. For instance if there is no objective, pseudo_cost or reduced_cost
648 // search will be ignored. Core based search will only work if the objective
649 // has many terms. If there is no fixed strategy fixed will be ignored. And so
652 // The order is important, as only the first num_full_subsolvers will be
653 // scheduled. You can see in the log which one are selected for a given run.
654 repeated string subsolvers = 207;
656 // A convenient way to add more workers types.
657 // These will be added at the beginning of the list.
658 repeated string extra_subsolvers = 219;
660 // Rather than fully specifying subsolvers, it is often convenient to just
661 // remove the ones that are not useful on a given problem or only keep
662 // specific ones for testing. Each string is interpreted as a "glob", so we
663 // support '*' and '?'.
665 // The way this work is that we will only accept a name that match a filter
666 // pattern (if non-empty) and do not match an ignore pattern. Note also that
667 // these fields work on LNS or LS names even if these are currently not
668 // specified via the subsolvers field.
669 repeated string ignore_subsolvers = 209;
670 repeated string filter_subsolvers = 293;
672 // It is possible to specify additional subsolver configuration. These can be
673 // referred by their params.name() in the fields above. Note that only the
674 // specified field will "overwrite" the ones of the base parameter. If a
675 // subsolver_params has the name of an existing subsolver configuration, the
676 // named parameters will be merged into the subsolver configuration.
677 repeated SatParameters subsolver_params = 210;
679 // Experimental. If this is true, then we interleave all our major search
680 // strategy and distribute the work amongst num_workers.
682 // The search is deterministic (independently of num_workers!), and we
683 // schedule and wait for interleave_batch_size task to be completed before
684 // synchronizing and scheduling the next batch of tasks.
685 optional bool interleave_search = 136 [default = false];
686 optional int32 interleave_batch_size = 134 [default = 0];
688 // Allows objective sharing between workers.
689 optional bool share_objective_bounds = 113 [default = true];
691 // Allows sharing of the bounds of modified variables at level 0.
692 optional bool share_level_zero_bounds = 114 [default = true];
694 // Allows sharing of new learned binary clause between workers.
695 optional bool share_binary_clauses = 203 [default = true];
697 // Allows sharing of short glue clauses between workers.
698 // Implicitly disabled if share_binary_clauses is false.
699 optional bool share_glue_clauses = 285 [default = false];
701 // Minimize and detect subsumption of shared clauses immediately after they
703 optional bool minimize_shared_clauses = 300 [default = true];
705 // ==========================================================================
706 // Debugging parameters
707 // ==========================================================================
709 // We have two different postsolve code. The default one should be better and
710 // it allows for a more powerful presolve, but it can be useful to postsolve
711 // using the full solver instead.
712 optional bool debug_postsolve_with_full_solver = 162 [default = false];
714 // If positive, try to stop just after that many presolve rules have been
715 // applied. This is mainly useful for debugging presolve.
716 optional int32 debug_max_num_presolve_operations = 151 [default = 0];
718 // Crash if we do not manage to complete the hint into a full solution.
719 optional bool debug_crash_on_bad_hint = 195 [default = false];
721 // Crash if presolve breaks a feasible hint.
722 optional bool debug_crash_if_presolve_breaks_hint = 306 [default = false];
724 // ==========================================================================
725 // Max-sat parameters
726 // ==========================================================================
728 // For an optimization problem, whether we follow some hints in order to find
729 // a better first solution. For a variable with hint, the solver will always
730 // try to follow the hint. It will revert to the variable_branching default
732 optional bool use_optimization_hints = 35 [default = true];
734 // If positive, we spend some effort on each core:
735 // - At level 1, we use a simple heuristic to try to minimize an UNSAT core.
736 // - At level 2, we use propagation to minimize the core but also identify
737 // literal in at most one relationship in this core.
738 optional int32 core_minimization_level = 50 [default = 2];
740 // Whether we try to find more independent cores for a given set of
741 // assumptions in the core based max-SAT algorithms.
742 optional bool find_multiple_cores = 84 [default = true];
744 // If true, when the max-sat algo find a core, we compute the minimal number
745 // of literals in the core that needs to be true to have a feasible solution.
746 // This is also called core exhaustion in more recent max-SAT papers.
747 optional bool cover_optimization = 89 [default = true];
749 // In what order do we add the assumptions in a core-based max-sat algorithm
750 enum MaxSatAssumptionOrder {
751 DEFAULT_ASSUMPTION_ORDER = 0;
752 ORDER_ASSUMPTION_BY_DEPTH = 1;
753 ORDER_ASSUMPTION_BY_WEIGHT = 2;
755 optional MaxSatAssumptionOrder max_sat_assumption_order = 51
756 [default = DEFAULT_ASSUMPTION_ORDER];
758 // If true, adds the assumption in the reverse order of the one defined by
759 // max_sat_assumption_order.
760 optional bool max_sat_reverse_assumption_order = 52 [default = false];
762 // What stratification algorithm we use in the presence of weight.
763 enum MaxSatStratificationAlgorithm {
764 // No stratification of the problem.
765 STRATIFICATION_NONE = 0;
767 // Start with literals with the highest weight, and when SAT, add the
768 // literals with the next highest weight and so on.
769 STRATIFICATION_DESCENT = 1;
771 // Start with all literals. Each time a core is found with a given minimum
772 // weight, do not consider literals with a lower weight for the next core
773 // computation. If the subproblem is SAT, do like in STRATIFICATION_DESCENT
774 // and just add the literals with the next highest weight.
775 STRATIFICATION_ASCENT = 2;
777 optional MaxSatStratificationAlgorithm max_sat_stratification = 53
778 [default = STRATIFICATION_DESCENT];
780 // ==========================================================================
781 // Constraint programming parameters
782 // ==========================================================================
784 // Some search decisions might cause a really large number of propagations to
785 // happen when integer variables with large domains are only reduced by 1 at
786 // each step. If we propagate more than the number of variable times this
787 // parameters we try to take counter-measure. Setting this to 0.0 disable this
790 // TODO(user): Setting this to something like 10 helps in most cases, but the
791 // code is currently buggy and can cause the solve to enter a bad state where
792 // no progress is made.
793 optional double propagation_loop_detection_factor = 221 [default = 10.0];
795 // When this is true, then a disjunctive constraint will try to use the
796 // precedence relations between time intervals to propagate their bounds
797 // further. For instance if task A and B are both before C and task A and B
798 // are in disjunction, then we can deduce that task C must start after
799 // duration(A) + duration(B) instead of simply max(duration(A), duration(B)),
800 // provided that the start time for all task was currently zero.
802 // This always result in better propagation, but it is usually slow, so
803 // depending on the problem, turning this off may lead to a faster solution.
804 optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];
806 // Create one literal for each disjunction of two pairs of tasks. This slows
807 // down the solve time, but improves the lower bound of the objective in the
808 // makespan case. This will be triggered if the number of intervals is less or
809 // equal than the parameter and if use_strong_propagation_in_disjunctive is
811 optional int32 max_size_to_create_precedence_literals_in_disjunctive = 229
814 // Enable stronger and more expensive propagation on no_overlap constraint.
815 optional bool use_strong_propagation_in_disjunctive = 230 [default = false];
817 // Whether we try to branch on decision "interval A before interval B" rather
818 // than on intervals bounds. This usually works better, but slow down a bit
819 // the time to find the first solution.
821 // These parameters are still EXPERIMENTAL, the result should be correct, but
822 // it some corner cases, they can cause some failing CHECK in the solver.
823 optional bool use_dynamic_precedence_in_disjunctive = 263 [default = false];
824 optional bool use_dynamic_precedence_in_cumulative = 268 [default = false];
826 // When this is true, the cumulative constraint is reinforced with overload
827 // checking, i.e., an additional level of reasoning based on energy. This
828 // additional level supplements the default level of reasoning as well as
829 // timetable edge finding.
831 // This always result in better propagation, but it is usually slow, so
832 // depending on the problem, turning this off may lead to a faster solution.
833 optional bool use_overload_checker_in_cumulative = 78 [default = false];
835 // Enable a heuristic to solve cumulative constraints using a modified energy
836 // constraint. We modify the usual energy definition by applying a
837 // super-additive function (also called "conservative scale" or "dual-feasible
838 // function") to the demand and the durations of the tasks.
840 // This heuristic is fast but for most problems it does not help much to find
842 optional bool use_conservative_scale_overload_checker = 286 [default = false];
844 // When this is true, the cumulative constraint is reinforced with timetable
845 // edge finding, i.e., an additional level of reasoning based on the
846 // conjunction of energy and mandatory parts. This additional level
847 // supplements the default level of reasoning as well as overload_checker.
849 // This always result in better propagation, but it is usually slow, so
850 // depending on the problem, turning this off may lead to a faster solution.
851 optional bool use_timetable_edge_finding_in_cumulative = 79 [default = false];
853 // Max number of intervals for the timetable_edge_finding algorithm to
854 // propagate. A value of 0 disables the constraint.
855 optional int32 max_num_intervals_for_timetable_edge_finding = 260
858 // If true, detect and create constraint for integer variable that are "after"
859 // a set of intervals in the same cumulative constraint.
861 // Experimental: by default we just use "direct" precedences. If
862 // exploit_all_precedences is true, we explore the full precedence graph. This
863 // assumes we have a DAG otherwise it fails.
864 optional bool use_hard_precedences_in_cumulative = 215 [default = false];
865 optional bool exploit_all_precedences = 220 [default = false];
867 // When this is true, the cumulative constraint is reinforced with propagators
868 // from the disjunctive constraint to improve the inference on a set of tasks
869 // that are disjunctive at the root of the problem. This additional level
870 // supplements the default level of reasoning.
872 // Propagators of the cumulative constraint will not be used at all if all the
873 // tasks are disjunctive at root node.
875 // This always result in better propagation, but it is usually slow, so
876 // depending on the problem, turning this off may lead to a faster solution.
877 optional bool use_disjunctive_constraint_in_cumulative = 80 [default = true];
879 // When this is true, the no_overlap_2d constraint is reinforced with
880 // propagators from the cumulative constraints. It consists of ignoring the
881 // position of rectangles in one position and projecting the no_overlap_2d on
882 // the other dimension to create a cumulative constraint. This is done on both
883 // axis. This additional level supplements the default level of reasoning.
884 optional bool use_timetabling_in_no_overlap_2d = 200 [default = false];
886 // When this is true, the no_overlap_2d constraint is reinforced with
887 // energetic reasoning. This additional level supplements the default level of
889 optional bool use_energetic_reasoning_in_no_overlap_2d = 213
892 // When this is true, the no_overlap_2d constraint is reinforced with
893 // an energetic reasoning that uses an area-based energy. This can be combined
894 // with the two other overlap heuristics above.
895 optional bool use_area_energetic_reasoning_in_no_overlap_2d = 271
898 optional bool use_try_edge_reasoning_in_no_overlap_2d = 299 [default = false];
900 // If the number of pairs to look is below this threshold, do an extra step of
901 // propagation in the no_overlap_2d constraint by looking at all pairs of
903 optional int32 max_pairs_pairwise_reasoning_in_no_overlap_2d = 276
906 // Detects when the space where items of a no_overlap_2d constraint can placed
907 // is disjoint (ie., fixed boxes split the domain). When it is the case, we
908 // can introduce a boolean for each pair <item, component> encoding whether
909 // the item is in the component or not. Then we replace the original
910 // no_overlap_2d constraint by one no_overlap_2d constraint for each
911 // component, with the new booleans as the enforcement_literal of the
912 // intervals. This is equivalent to expanding the original no_overlap_2d
913 // constraint into a bin packing problem with each connected component being a
914 // bin. This heuristic is only done when the number of regions to split
915 // is less than this parameter and <= 1 disables it.
916 optional int32 maximum_regions_to_split_in_disconnected_no_overlap_2d = 315
919 // When set, it activates a few scheduling parameters to improve the lower
920 // bound of scheduling problems. This is only effective with multiple workers
921 // as it modifies the reduced_cost, lb_tree_search, and probing workers.
922 optional bool use_dual_scheduling_heuristics = 214 [default = true];
924 // Turn on extra propagation for the circuit constraint.
925 // This can be quite slow.
926 optional bool use_all_different_for_circuit = 311 [default = false];
928 // If the size of a subset of nodes of a RoutesConstraint is less than this
929 // value, use linear constraints of size 1 and 2 (such as capacity and time
930 // window constraints) enforced by the arc literals to compute cuts for this
931 // subset (unless the subset size is less than
932 // routing_cut_subset_size_for_tight_binary_relation_bound, in which case the
933 // corresponding algorithm is used instead). The algorithm for these cuts has
934 // a O(n^3) complexity, where n is the subset size. Hence the value of this
935 // parameter should not be too large (e.g. 10 or 20).
936 optional int32 routing_cut_subset_size_for_binary_relation_bound = 312
939 // Similar to above, but with a different algorithm producing better cuts, at
940 // the price of a higher O(2^n) complexity, where n is the subset size. Hence
941 // the value of this parameter should be small (e.g. less than 10).
942 optional int32 routing_cut_subset_size_for_tight_binary_relation_bound = 313
945 // The amount of "effort" to spend in dynamic programming for computing
946 // routing cuts. This is in term of basic operations needed by the algorithm
947 // in the worst case, so a value like 1e8 should take less than a second to
949 optional double routing_cut_dp_effort = 314 [default = 1e7];
951 // The search branching will be used to decide how to branch on unfixed nodes.
952 enum SearchBranching {
953 // Try to fix all literals using the underlying SAT solver's heuristics,
954 // then generate and fix literals until integer variables are fixed. New
955 // literals on integer variables are generated using the fixed search
956 // specified by the user or our default one.
957 AUTOMATIC_SEARCH = 0;
959 // If used then all decisions taken by the solver are made using a fixed
960 // order as specified in the API or in the CpModelProto search_strategy
964 // Simple portfolio search used by LNS workers.
965 PORTFOLIO_SEARCH = 2;
967 // If used, the solver will use heuristics from the LP relaxation. This
968 // exploit the reduced costs of the variables in the relaxation.
971 // If used, the solver uses the pseudo costs for branching. Pseudo costs
972 // are computed using the historical change in objective bounds when some
973 // decision are taken. Note that this works whether we use an LP or not.
974 PSEUDO_COST_SEARCH = 4;
976 // Mainly exposed here for testing. This quickly tries a lot of randomized
977 // heuristics with a low conflict limit. It usually provides a good first
979 PORTFOLIO_WITH_QUICK_RESTART_SEARCH = 5;
981 // Mainly used internally. This is like FIXED_SEARCH, except we follow the
982 // solution_hint field of the CpModelProto rather than using the information
983 // provided in the search_strategy.
986 // Similar to FIXED_SEARCH, but differ in how the variable not listed into
987 // the fixed search heuristics are branched on. This will always start the
988 // search tree according to the specified fixed search strategy, but will
989 // complete it using the default automatic search.
990 PARTIAL_FIXED_SEARCH = 7;
992 // Randomized search. Used to increase entropy in the search.
993 RANDOMIZED_SEARCH = 8;
995 optional SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
997 // Conflict limit used in the phase that exploit the solution hint.
998 optional int32 hint_conflict_limit = 153 [default = 10];
1000 // If true, the solver tries to repair the solution given in the hint. This
1001 // search terminates after the 'hint_conflict_limit' is reached and the solver
1002 // switches to regular search. If false, then we do a FIXED_SEARCH using the
1003 // hint until the hint_conflict_limit is reached.
1004 optional bool repair_hint = 167 [default = false];
1006 // If true, variables appearing in the solution hints will be fixed to their
1008 optional bool fix_variables_to_their_hinted_value = 192 [default = false];
1010 // If true, search will continuously probe Boolean variables, and integer
1011 // variable bounds. This parameter is set to true in parallel on the probing
1013 optional bool use_probing_search = 176 [default = false];
1015 // Use extended probing (probe bool_or, at_most_one, exactly_one).
1016 optional bool use_extended_probing = 269 [default = true];
1018 // How many combinations of pairs or triplets of variables we want to scan.
1019 optional int32 probing_num_combinations_limit = 272 [default = 20000];
1021 // Add a shaving phase (where the solver tries to prove that the lower or
1022 // upper bound of a variable are infeasible) to the probing search.
1023 optional bool use_shaving_in_probing_search = 204 [default = true];
1025 // Specifies the amount of deterministic time spent of each try at shaving a
1026 // bound in the shaving search.
1027 optional double shaving_search_deterministic_time = 205 [default = 0.001];
1029 // Specifies the threshold between two modes in the shaving procedure.
1030 // If the range of the variable/objective is less than this threshold, then
1031 // the shaving procedure will try to remove values one by one. Otherwise, it
1032 // will try to remove one range at a time.
1033 optional int64 shaving_search_threshold = 290 [default = 64];
1035 // If true, search will search in ascending max objective value (when
1036 // minimizing) starting from the lower bound of the objective.
1037 optional bool use_objective_lb_search = 228 [default = false];
1039 // This search differs from the previous search as it will not use assumptions
1040 // to bound the objective, and it will recreate a full model with the
1041 // hardcoded objective value.
1042 optional bool use_objective_shaving_search = 253 [default = false];
1044 // This search takes all Boolean or integer variables, and maximize or
1045 // minimize them in order to reduce their domain.
1046 optional bool use_variables_shaving_search = 289 [default = false];
1048 // The solver ignores the pseudo costs of variables with number of recordings
1049 // less than this threshold.
1050 optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
1052 // The default optimization method is a simple "linear scan", each time trying
1053 // to find a better solution than the previous one. If this is true, then we
1054 // use a core-based approach (like in max-SAT) when we try to increase the
1055 // lower bound instead.
1056 optional bool optimize_with_core = 83 [default = false];
1058 // Do a more conventional tree search (by opposition to SAT based one) where
1059 // we keep all the explored node in a tree. This is meant to be used in a
1060 // portfolio and focus on improving the objective lower bound. Keeping the
1061 // whole tree allow us to report a better objective lower bound coming from
1062 // the worst open node in the tree.
1063 optional bool optimize_with_lb_tree_search = 188 [default = false];
1065 // Experimental. Save the current LP basis at each node of the search tree so
1066 // that when we jump around, we can load it and reduce the number of LP
1067 // iterations needed.
1069 // It currently works okay if we do not change the lp with cuts or
1070 // simplification... More work is needed to make it robust in all cases.
1071 optional bool save_lp_basis_in_lb_tree_search = 284 [default = false];
1073 // If non-negative, perform a binary search on the objective variable in order
1074 // to find an [min, max] interval outside of which the solver proved unsat/sat
1075 // under this amount of conflict. This can quickly reduce the objective domain
1076 // on some problems.
1077 optional int32 binary_search_num_conflicts = 99 [default = -1];
1079 // This has no effect if optimize_with_core is false. If true, use a different
1080 // core-based algorithm similar to the max-HS algo for max-SAT. This is a
1081 // hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT
1082 // one. This is also related to the PhD work of tobyodavies@
1083 // "Automatic Logic-Based Benders Decomposition with MiniZinc"
1084 // http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489
1085 optional bool optimize_with_max_hs = 85 [default = false];
1087 // Parameters for an heuristic similar to the one described in the paper:
1088 // "Feasibility Jump: an LP-free Lagrangian MIP heuristic", Bjørnar
1089 // Luteberget, Giorgio Sartor, 2023, Mathematical Programming Computation.
1090 optional bool use_feasibility_jump = 265 [default = true];
1092 // Disable every other type of subsolver, setting this turns CP-SAT into a
1093 // pure local-search solver.
1094 optional bool use_ls_only = 240 [default = false];
1096 // On each restart, we randomly choose if we use decay (with this parameter)
1098 optional double feasibility_jump_decay = 242 [default = 0.95];
1100 // How much do we linearize the problem in the local search code.
1101 optional int32 feasibility_jump_linearization_level = 257 [default = 2];
1103 // This is a factor that directly influence the work before each restart.
1104 // Increasing it leads to longer restart.
1105 optional int32 feasibility_jump_restart_factor = 258 [default = 1];
1107 // How much dtime for each LS batch.
1108 optional double feasibility_jump_batch_dtime = 292 [default = 0.1];
1110 // Probability for a variable to have a non default value upon restarts or
1112 optional double feasibility_jump_var_randomization_probability = 247
1115 // Max distance between the default value and the pertubated value relative to
1116 // the range of the domain of the variable.
1117 optional double feasibility_jump_var_perburbation_range_ratio = 248
1120 // When stagnating, feasibility jump will either restart from a default
1121 // solution (with some possible randomization), or randomly pertubate the
1122 // current solution. This parameter selects the first option.
1123 optional bool feasibility_jump_enable_restarts = 250 [default = true];
1125 // Maximum size of no_overlap or no_overlap_2d constraint for a quadratic
1126 // expansion. This might look a lot, but by expanding such constraint, we get
1127 // a linear time evaluation per single variable moves instead of a slow O(n
1129 optional int32 feasibility_jump_max_expanded_constraint_size = 264
1132 // This will create incomplete subsolvers (that are not LNS subsolvers)
1133 // that use the feasibility jump code to find improving solution, treating
1134 // the objective improvement as a hard constraint.
1135 optional int32 num_violation_ls = 244 [default = 0];
1137 // How long violation_ls should wait before perturbating a solution.
1138 optional int32 violation_ls_perturbation_period = 249 [default = 100];
1140 // Probability of using compound move search each restart.
1141 // TODO(user): Add reference to paper when published.
1142 optional double violation_ls_compound_move_probability = 259 [default = 0.5];
1144 // Enables shared tree search.
1145 // If positive, start this many complete worker threads to explore a shared
1146 // search tree. These workers communicate objective bounds and simple decision
1147 // nogoods relating to the shared prefix of the tree, and will avoid exploring
1148 // the same subtrees as one another.
1149 // Specifying a negative number uses a heuristic to select an appropriate
1150 // number of shared tree workeres based on the total number of workers.
1151 optional int32 shared_tree_num_workers = 235 [default = 0];
1153 // Set on shared subtree workers. Users should not set this directly.
1154 optional bool use_shared_tree_search = 236 [default = false];
1156 // Minimum restarts before a worker will replace a subtree
1157 // that looks "bad" based on the average LBD of learned clauses.
1158 optional int32 shared_tree_worker_min_restarts_per_subtree = 282
1161 // If true, workers share more of the information from their local trail.
1162 // Specifically, literals implied by the shared tree decisions.
1163 optional bool shared_tree_worker_enable_trail_sharing = 295 [default = true];
1165 // If true, shared tree workers share their target phase when returning an
1166 // assigned subtree for the next worker to use.
1167 optional bool shared_tree_worker_enable_phase_sharing = 304 [default = true];
1169 // How many open leaf nodes should the shared tree maintain per worker.
1170 optional double shared_tree_open_leaves_per_worker = 281 [default = 2.0];
1172 // In order to limit total shared memory and communication overhead, limit the
1173 // total number of nodes that may be generated in the shared tree. If the
1174 // shared tree runs out of unassigned leaves, workers act as portfolio
1175 // workers. Note: this limit includes interior nodes, not just leaves.
1176 optional int32 shared_tree_max_nodes_per_worker = 238 [default = 10000];
1178 enum SharedTreeSplitStrategy {
1179 // Uses the default strategy, currently equivalent to
1180 // SPLIT_STRATEGY_DISCREPANCY.
1181 SPLIT_STRATEGY_AUTO = 0;
1182 // Only accept splits if the node to be split's depth+discrepancy is minimal
1183 // for the desired number of leaves.
1184 // The preferred child for discrepancy calculation is the one with the
1185 // lowest objective lower bound or the original branch direction if the
1186 // bounds are equal. This rule allows twice as many workers to work in the
1187 // preferred subtree as non-preferred.
1188 SPLIT_STRATEGY_DISCREPANCY = 1;
1189 // Only split nodes with an objective lb equal to the global lb. If there is
1190 // no objective, this is equivalent to SPLIT_STRATEGY_FIRST_PROPOSAL.
1191 SPLIT_STRATEGY_OBJECTIVE_LB = 2;
1192 // Attempt to keep the shared tree balanced.
1193 SPLIT_STRATEGY_BALANCED_TREE = 3;
1194 // Workers race to split their subtree, the winner's proposal is accepted.
1195 SPLIT_STRATEGY_FIRST_PROPOSAL = 4;
1197 optional SharedTreeSplitStrategy shared_tree_split_strategy = 239
1198 [default = SPLIT_STRATEGY_AUTO];
1200 // How much deeper compared to the ideal max depth of the tree is considered
1201 // "balanced" enough to still accept a split. Without such a tolerance,
1202 // sometimes the tree can only be split by a single worker, and they may not
1203 // generate a split for some time. In contrast, with a tolerance of 1, at
1204 // least half of all workers should be able to split the tree as soon as a
1205 // split becomes required. This only has an effect on
1206 // SPLIT_STRATEGY_BALANCED_TREE and SPLIT_STRATEGY_DISCREPANCY.
1207 optional int32 shared_tree_balance_tolerance = 305 [default = 1];
1209 // Whether we enumerate all solutions of a problem without objective. Note
1210 // that setting this to true automatically disable some presolve reduction
1211 // that can remove feasible solution. That is it has the same effect as
1212 // setting keep_all_feasible_solutions_in_presolve.
1214 // TODO(user): Do not do that and let the user choose what behavior is best by
1215 // setting keep_all_feasible_solutions_in_presolve ?
1216 optional bool enumerate_all_solutions = 87 [default = false];
1218 // If true, we disable the presolve reductions that remove feasible solutions
1219 // from the search space. Such solution are usually dominated by a "better"
1220 // solution that is kept, but depending on the situation, we might want to
1221 // keep all solutions.
1223 // A trivial example is when a variable is unused. If this is true, then the
1224 // presolve will not fix it to an arbitrary value and it will stay in the
1226 optional bool keep_all_feasible_solutions_in_presolve = 173 [default = false];
1228 // If true, add information about the derived variable domains to the
1229 // CpSolverResponse. It is an option because it makes the response slighly
1230 // bigger and there is a bit more work involved during the postsolve to
1231 // construct it, but it should still have a low overhead. See the
1232 // tightened_variables field in CpSolverResponse for more details.
1233 optional bool fill_tightened_domains_in_response = 132 [default = false];
1235 // If true, the final response addition_solutions field will be filled with
1236 // all solutions from our solutions pool.
1238 // Note that if both this field and enumerate_all_solutions is true, we will
1239 // copy to the pool all of the solution found. So if solution_pool_size is big
1240 // enough, you can get all solutions this way instead of using the solution
1243 // Note that this only affect the "final" solution, not the one passed to the
1244 // solution callbacks.
1245 optional bool fill_additional_solutions_in_response = 194 [default = false];
1247 // If true, the solver will add a default integer branching strategy to the
1248 // already defined search strategy. If not, some variable might still not be
1249 // fixed at the end of the search. For now we assume these variable can just
1250 // be set to their lower bound.
1251 optional bool instantiate_all_variables = 106 [default = true];
1253 // If true, then the precedences propagator try to detect for each variable if
1254 // it has a set of "optional incoming arc" for which at least one of them is
1255 // present. This is usually useful to have but can be slow on model with a lot
1257 optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];
1259 // For an optimization problem, stop the solver as soon as we have a solution.
1260 optional bool stop_after_first_solution = 98 [default = false];
1262 // Mainly used when improving the presolver. When true, stops the solver after
1263 // the presolve is complete (or after loading and root level propagation).
1264 optional bool stop_after_presolve = 149 [default = false];
1265 optional bool stop_after_root_propagation = 252 [default = false];
1269 // Initial parameters for neighborhood generation.
1270 optional double lns_initial_difficulty = 307 [default = 0.5];
1271 optional double lns_initial_deterministic_limit = 308 [default = 0.1];
1273 // Testing parameters used to disable all lns workers.
1274 optional bool use_lns = 283 [default = true];
1276 // Experimental parameters to disable everything but lns.
1277 optional bool use_lns_only = 101 [default = false];
1279 // Size of the top-n different solutions kept by the solver.
1280 // This parameter must be > 0.
1281 // Currently this only impact the "base" solution chosen for a LNS fragment.
1282 optional int32 solution_pool_size = 193 [default = 3];
1284 // Turns on relaxation induced neighborhood generator.
1285 optional bool use_rins_lns = 129 [default = true];
1287 // Adds a feasibility pump subsolver along with lns subsolvers.
1288 optional bool use_feasibility_pump = 164 [default = true];
1290 // Turns on neighborhood generator based on local branching LP. Based on Huang
1291 // et al., "Local Branching Relaxation Heuristics for Integer Linear
1293 optional bool use_lb_relax_lns = 255 [default = true];
1295 // Only use lb-relax if we have at least that many workers.
1296 optional int32 lb_relax_num_workers_threshold = 296 [default = 16];
1298 // Rounding method to use for feasibility pump.
1299 enum FPRoundingMethod {
1300 // Rounds to the nearest integer value.
1301 NEAREST_INTEGER = 0;
1303 // Counts the number of linear constraints restricting the variable in the
1304 // increasing values (up locks) and decreasing values (down locks). Rounds
1305 // the variable in the direction of lesser locks.
1308 // Similar to lock based rounding except this only considers locks of active
1309 // constraints from the last lp solve.
1310 ACTIVE_LOCK_BASED = 3;
1312 // This is expensive rounding algorithm. We round variables one by one and
1313 // propagate the bounds in between. If none of the rounded values fall in
1314 // the continuous domain specified by lower and upper bound, we use the
1315 // current lower/upper bound (whichever one is closest) instead of rounding
1316 // the fractional lp solution value. If both the rounded values are in the
1317 // domain, we round to nearest integer.
1318 PROPAGATION_ASSISTED = 2;
1320 optional FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];
1322 // If true, registers more lns subsolvers with different parameters.
1323 optional bool diversify_lns_params = 137 [default = false];
1325 // Randomize fixed search.
1326 optional bool randomize_search = 103 [default = false];
1328 // Search randomization will collect the top
1329 // 'search_random_variable_pool_size' valued variables, and pick one randomly.
1330 // The value of the variable is specific to each strategy.
1331 optional int64 search_random_variable_pool_size = 104 [default = 0];
1333 // Experimental code: specify if the objective pushes all tasks toward the
1334 // start of the schedule.
1335 optional bool push_all_tasks_toward_start = 262 [default = false];
1337 // If true, we automatically detect variables whose constraint are always
1338 // enforced by the same literal and we mark them as optional. This allows
1339 // to propagate them as if they were present in some situation.
1341 // TODO(user): This is experimental and seems to lead to wrong optimal in
1342 // some situation. It should however gives correct solutions. Fix.
1343 optional bool use_optional_variables = 108 [default = false];
1345 // The solver usually exploit the LP relaxation of a model. If this option is
1346 // true, then whatever is infered by the LP will be used like an heuristic to
1347 // compute EXACT propagation on the IP. So with this option, there is no
1348 // numerical imprecision issues.
1349 optional bool use_exact_lp_reason = 109 [default = true];
1351 // This can be beneficial if there is a lot of no-overlap constraints but a
1352 // relatively low number of different intervals in the problem. Like 1000
1353 // intervals, but 1M intervals in the no-overlap constraints covering them.
1354 optional bool use_combined_no_overlap = 133 [default = false];
1356 // All at_most_one constraints with a size <= param will be replaced by a
1357 // quadratic number of binary implications.
1358 optional int32 at_most_one_max_expansion_size = 270 [default = 3];
1360 // Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals
1361 // when calling solve. If set, catching the SIGINT signal will terminate the
1362 // search gracefully, as if a time limit was reached.
1363 optional bool catch_sigint_signal = 135 [default = true];
1365 // Stores and exploits "implied-bounds" in the solver. That is, relations of
1366 // the form literal => (var >= bound). This is currently used to derive
1368 optional bool use_implied_bounds = 144 [default = true];
1370 // Whether we try to do a few degenerate iteration at the end of an LP solve
1371 // to minimize the fractionality of the integer variable in the basis. This
1372 // helps on some problems, but not so much on others. It also cost of bit of
1373 // time to do such polish step.
1374 optional bool polish_lp_solution = 175 [default = false];
1376 // The internal LP tolerances used by CP-SAT. These applies to the internal
1377 // and scaled problem. If the domains of your variables are large it might be
1378 // good to use lower tolerances. If your problem is binary with low
1379 // coefficients, it might be good to use higher ones to speed-up the lp
1381 optional double lp_primal_tolerance = 266 [default = 1e-7];
1382 optional double lp_dual_tolerance = 267 [default = 1e-7];
1384 // Temporary flag util the feature is more mature. This convert intervals to
1385 // the newer proto format that support affine start/var/end instead of just
1387 optional bool convert_intervals = 177 [default = true];
1389 // Whether we try to automatically detect the symmetries in a model and
1390 // exploit them. Currently, at level 1 we detect them in presolve and try
1391 // to fix Booleans. At level 2, we also do some form of dynamic symmetry
1392 // breaking during search. At level 3, we also detect symmetries for very
1393 // large models, which can be slow. At level 4, we try to break as much
1394 // symmetry as possible in presolve.
1395 optional int32 symmetry_level = 183 [default = 2];
1397 // When we have symmetry, it is possible to "fold" all variables from the same
1398 // orbit into a single variable, while having the same power of LP relaxation.
1399 // This can help significantly on symmetric problem. However there is
1400 // currently a bit of overhead as the rest of the solver need to do some
1401 // translation between the folded LP and the rest of the problem.
1402 optional bool use_symmetry_in_lp = 301 [default = false];
1404 // Experimental. This will compute the symmetry of the problem once and for
1405 // all. All presolve operations we do should keep the symmetry group intact
1406 // or modify it properly. For now we have really little support for this. We
1407 // will disable a bunch of presolve operations that could be supported.
1408 optional bool keep_symmetry_in_presolve = 303 [default = false];
1410 // Deterministic time limit for symmetry detection.
1411 optional double symmetry_detection_deterministic_time_limit = 302
1414 // The new linear propagation code treat all constraints at once and use
1415 // an adaptation of Bellman-Ford-Tarjan to propagate constraint in a smarter
1416 // order and potentially detect propagation cycle earlier.
1417 optional bool new_linear_propagation = 224 [default = true];
1419 // Linear constraints that are not pseudo-Boolean and that are longer than
1420 // this size will be split into sqrt(size) intermediate sums in order to have
1421 // faster propation in the CP engine.
1422 optional int32 linear_split_size = 256 [default = 100];
1424 // ==========================================================================
1425 // Linear programming relaxation
1426 // ==========================================================================
1428 // A non-negative level indicating the type of constraints we consider in the
1429 // LP relaxation. At level zero, no LP relaxation is used. At level 1, only
1430 // the linear constraint and full encoding are added. At level 2, we also add
1431 // all the Boolean constraints.
1432 optional int32 linearization_level = 90 [default = 1];
1434 // A non-negative level indicating how much we should try to fully encode
1435 // Integer variables as Boolean.
1436 optional int32 boolean_encoding_level = 107 [default = 1];
1438 // When loading a*x + b*y ==/!= c when x and y are both fully encoded.
1439 // The solver may decide to replace the linear equation by a set of clauses.
1440 // This is triggered if the sizes of the domains of x and y are below the
1442 optional int32 max_domain_size_when_encoding_eq_neq_constraints = 191
1445 // The limit on the number of cuts in our cut pool. When this is reached we do
1446 // not generate cuts anymore.
1448 // TODO(user): We should probably remove this parameters, and just always
1449 // generate cuts but only keep the best n or something.
1450 optional int32 max_num_cuts = 91 [default = 10000];
1452 // Control the global cut effort. Zero will turn off all cut. For now we just
1453 // have one level. Note also that most cuts are only used at linearization
1455 optional int32 cut_level = 196 [default = 1];
1457 // For the cut that can be generated at any level, this control if we only
1458 // try to generate them at the root node.
1459 optional bool only_add_cuts_at_level_zero = 92 [default = false];
1461 // When the LP objective is fractional, do we add the cut that forces the
1462 // linear objective expression to be greater or equal to this fractional value
1463 // rounded up? We can always do that since our objective is integer, and
1464 // combined with MIR heuristic to reduce the coefficient of such cut, it can
1466 optional bool add_objective_cut = 197 [default = false];
1468 // Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
1469 // Note that for now, this is not heavily tuned.
1470 optional bool add_cg_cuts = 117 [default = true];
1472 // Whether we generate MIR cuts at root node.
1473 // Note that for now, this is not heavily tuned.
1474 optional bool add_mir_cuts = 120 [default = true];
1476 // Whether we generate Zero-Half cuts at root node.
1477 // Note that for now, this is not heavily tuned.
1478 optional bool add_zero_half_cuts = 169 [default = true];
1480 // Whether we generate clique cuts from the binary implication graph. Note
1481 // that as the search goes on, this graph will contains new binary clauses
1482 // learned by the SAT engine.
1483 optional bool add_clique_cuts = 172 [default = true];
1485 // Whether we generate RLT cuts. This is still experimental but can help on
1486 // binary problem with a lot of clauses of size 3.
1487 optional bool add_rlt_cuts = 279 [default = true];
1489 // Cut generator for all diffs can add too many cuts for large all_diff
1490 // constraints. This parameter restricts the large all_diff constraints to
1491 // have a cut generator.
1492 optional int32 max_all_diff_cut_size = 148 [default = 64];
1494 // For the lin max constraints, generates the cuts described in "Strong
1495 // mixed-integer programming formulations for trained neural networks" by Ross
1496 // Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)
1497 optional bool add_lin_max_cuts = 152 [default = true];
1499 // In the integer rounding procedure used for MIR and Gomory cut, the maximum
1500 // "scaling" we use (must be positive). The lower this is, the lower the
1501 // integer coefficients of the cut will be. Note that cut generated by lower
1502 // values are not necessarily worse than cut generated by larger value. There
1503 // is no strict dominance relationship.
1505 // Setting this to 2 result in the "strong fractional rouding" of Letchford
1507 optional int32 max_integer_rounding_scaling = 119 [default = 600];
1509 // If true, we start by an empty LP, and only add constraints not satisfied
1510 // by the current LP solution batch by batch. A constraint that is only added
1511 // like this is known as a "lazy" constraint in the literature, except that we
1512 // currently consider all constraints as lazy here.
1513 optional bool add_lp_constraints_lazily = 112 [default = true];
1515 // Even at the root node, we do not want to spend too much time on the LP if
1516 // it is "difficult". So we solve it in "chunks" of that many iterations. The
1517 // solve will be continued down in the tree or the next time we go back to the
1519 optional int32 root_lp_iterations = 227 [default = 2000];
1521 // While adding constraints, skip the constraints which have orthogonality
1522 // less than 'min_orthogonality_for_lp_constraints' with already added
1523 // constraints during current call. Orthogonality is defined as 1 -
1524 // cosine(vector angle between constraints). A value of zero disable this
1526 optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];
1528 // Max number of time we perform cut generation and resolve the LP at level 0.
1529 optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];
1531 // If a constraint/cut in LP is not active for that many consecutive OPTIMAL
1532 // solves, remove it from the LP. Note that it might be added again later if
1533 // it become violated by the current LP solution.
1534 optional int32 max_consecutive_inactive_count = 121 [default = 100];
1536 // These parameters are similar to sat clause management activity parameters.
1537 // They are effective only if the number of generated cuts exceed the storage
1538 // limit. Default values are based on a few experiments on miplib instances.
1539 optional double cut_max_active_count_value = 155 [default = 1e10];
1540 optional double cut_active_count_decay = 156 [default = 0.8];
1542 // Target number of constraints to remove during cleanup.
1543 optional int32 cut_cleanup_target = 157 [default = 1000];
1545 // Add that many lazy constraints (or cuts) at once in the LP. Note that at
1546 // the beginning of the solve, we do add more than this.
1547 optional int32 new_constraints_batch_size = 122 [default = 50];
1549 // All the "exploit_*" parameters below work in the same way: when branching
1550 // on an IntegerVariable, these parameters affect the value the variable is
1551 // branched on. Currently the first heuristic that triggers win in the order
1552 // in which they appear below.
1554 // TODO(user): Maybe do like for the restart algorithm, introduce an enum
1555 // and a repeated field that control the order on which these are applied?
1557 // If true and the Lp relaxation of the problem has an integer optimal
1558 // solution, try to exploit it. Note that since the LP relaxation may not
1559 // contain all the constraints, such a solution is not necessarily a solution
1560 // of the full problem.
1561 optional bool exploit_integer_lp_solution = 94 [default = true];
1563 // If true and the Lp relaxation of the problem has a solution, try to exploit
1564 // it. This is same as above except in this case the lp solution might not be
1565 // an integer solution.
1566 optional bool exploit_all_lp_solution = 116 [default = true];
1568 // When branching on a variable, follow the last best solution value.
1569 optional bool exploit_best_solution = 130 [default = false];
1571 // When branching on a variable, follow the last best relaxation solution
1572 // value. We use the relaxation with the tightest bound on the objective as
1573 // the best relaxation solution.
1574 optional bool exploit_relaxation_solution = 161 [default = false];
1576 // When branching an a variable that directly affect the objective,
1577 // branch on the value that lead to the best objective first.
1578 optional bool exploit_objective = 131 [default = true];
1580 // Infer products of Boolean or of Boolean time IntegerVariable from the
1581 // linear constrainst in the problem. This can be used in some cuts, altough
1582 // for now we don't really exploit it.
1583 optional bool detect_linearized_product = 277 [default = false];
1585 // ==========================================================================
1586 // MIP -> CP-SAT (i.e. IP with integer coeff) conversion parameters that are
1587 // used by our automatic "scaling" algorithm.
1589 // Note that it is hard to do a meaningful conversion automatically and if
1590 // you have a model with continuous variables, it is best if you scale the
1591 // domain of the variable yourself so that you have a relevant precision for
1592 // the application at hand. Same for the coefficients and constraint bounds.
1593 // ==========================================================================
1595 // We need to bound the maximum magnitude of the variables for CP-SAT, and
1596 // that is the bound we use. If the MIP model expect larger variable value in
1597 // the solution, then the converted model will likely not be relevant.
1598 optional double mip_max_bound = 124 [default = 1e7];
1600 // All continuous variable of the problem will be multiplied by this factor.
1601 // By default, we don't do any variable scaling and rely on the MIP model to
1602 // specify continuous variable domain with the wanted precision.
1603 optional double mip_var_scaling = 125 [default = 1.0];
1605 // If this is false, then mip_var_scaling is only applied to variables with
1606 // "small" domain. If it is true, we scale all floating point variable
1607 // independenlty of their domain.
1608 optional bool mip_scale_large_domain = 225 [default = false];
1610 // If true, some continuous variable might be automatically scaled. For now,
1611 // this is only the case where we detect that a variable is actually an
1612 // integer multiple of a constant. For instance, variables of the form k * 0.5
1613 // are quite frequent, and if we detect this, we will scale such variable
1614 // domain by 2 to make it implied integer.
1615 optional bool mip_automatically_scale_variables = 166 [default = true];
1617 // If one try to solve a MIP model with CP-SAT, because we assume all variable
1618 // to be integer after scaling, we will not necessarily have the correct
1619 // optimal. Note however that all feasible solutions are valid since we will
1620 // just solve a more restricted version of the original problem.
1622 // This parameters is here to prevent user to think the solution is optimal
1623 // when it might not be. One will need to manually set this to false to solve
1624 // a MIP model where the optimal might be different.
1626 // Note that this is tested after some MIP presolve steps, so even if not
1627 // all original variable are integer, we might end up with a pure IP after
1628 // presolve and after implied integer detection.
1629 optional bool only_solve_ip = 222 [default = false];
1631 // When scaling constraint with double coefficients to integer coefficients,
1632 // we will multiply by a power of 2 and round the coefficients. We will choose
1633 // the lowest power such that we have no potential overflow (see
1634 // mip_max_activity_exponent) and the worst case constraint activity error
1635 // does not exceed this threshold.
1637 // Note that we also detect constraint with rational coefficients and scale
1638 // them accordingly when it seems better instead of using a power of 2.
1640 // We also relax all constraint bounds by this absolute value. For pure
1641 // integer constraint, if this value if lower than one, this will not change
1642 // anything. However it is needed when scaling MIP problems.
1644 // If we manage to scale a constraint correctly, the maximum error we can make
1645 // will be twice this value (once for the scaling error and once for the
1646 // relaxed bounds). If we are not able to scale that well, we will display
1647 // that fact but still scale as best as we can.
1648 optional double mip_wanted_precision = 126 [default = 1e-6];
1650 // To avoid integer overflow, we always force the maximum possible constraint
1651 // activity (and objective value) according to the initial variable domain to
1652 // be smaller than 2 to this given power. Because of this, we cannot always
1653 // reach the "mip_wanted_precision" parameter above.
1655 // This can go as high as 62, but some internal algo currently abort early if
1656 // they might run into integer overflow, so it is better to keep it a bit
1658 optional int32 mip_max_activity_exponent = 127 [default = 53];
1660 // As explained in mip_precision and mip_max_activity_exponent, we cannot
1661 // always reach the wanted precision during scaling. We use this threshold to
1662 // enphasize in the logs when the precision seems bad.
1663 optional double mip_check_precision = 128 [default = 1e-4];
1665 // Even if we make big error when scaling the objective, we can always derive
1666 // a correct lower bound on the original objective by using the exact lower
1667 // bound on the scaled integer version of the objective. This should be fast,
1668 // but if you don't care about having a precise lower bound, you can turn it
1670 optional bool mip_compute_true_objective_bound = 198 [default = true];
1672 // Any finite values in the input MIP must be below this threshold, otherwise
1673 // the model will be reported invalid. This is needed to avoid floating point
1674 // overflow when evaluating bounds * coeff for instance. We are a bit more
1675 // defensive, but in practice, users shouldn't use super large values in a
1677 optional double mip_max_valid_magnitude = 199 [default = 1e20];
1679 // By default, any variable/constraint bound with a finite value and a
1680 // magnitude greater than the mip_max_valid_magnitude will result with a
1681 // invalid model. This flags change the behavior such that such bounds are
1682 // silently transformed to +∞ or -∞.
1684 // It is recommended to keep it at false, and create valid bounds.
1685 optional bool mip_treat_high_magnitude_bounds_as_infinity = 278
1688 // Any value in the input mip with a magnitude lower than this will be set to
1689 // zero. This is to avoid some issue in LP presolving.
1690 optional double mip_drop_tolerance = 232 [default = 1e-16];
1692 // When solving a MIP, we do some basic floating point presolving before
1693 // scaling the problem to integer to be handled by CP-SAT. This control how
1694 // much of that presolve we do. It can help to better scale floating point
1695 // model, but it is not always behaving nicely.
1696 optional int32 mip_presolve_level = 261 [default = 2];