SatParametersOrBuilder

Detailed Description

Definition at line 6 of file SatParametersOrBuilder.java.

Public Member Functions
boolean	hasName ()
java.lang.String	getName ()
com.google.protobuf.ByteString	getNameBytes ()
boolean	hasPreferredVariableOrder ()
	optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER]; More...
com.google.ortools.sat.SatParameters.VariableOrder	getPreferredVariableOrder ()
	optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER]; More...
boolean	hasInitialPolarity ()
	optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE]; More...
com.google.ortools.sat.SatParameters.Polarity	getInitialPolarity ()
	optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE]; More...
boolean	hasUsePhaseSaving ()
boolean	getUsePhaseSaving ()
boolean	hasPolarityRephaseIncrement ()
int	getPolarityRephaseIncrement ()
boolean	hasRandomPolarityRatio ()
double	getRandomPolarityRatio ()
boolean	hasRandomBranchesRatio ()
double	getRandomBranchesRatio ()
boolean	hasUseErwaHeuristic ()
boolean	getUseErwaHeuristic ()
boolean	hasInitialVariablesActivity ()
double	getInitialVariablesActivity ()
boolean	hasAlsoBumpVariablesInConflictReasons ()
boolean	getAlsoBumpVariablesInConflictReasons ()
boolean	hasMinimizationAlgorithm ()
	optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE]; More...
com.google.ortools.sat.SatParameters.ConflictMinimizationAlgorithm	getMinimizationAlgorithm ()
	optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE]; More...
boolean	hasBinaryMinimizationAlgorithm ()
	optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST]; More...
com.google.ortools.sat.SatParameters.BinaryMinizationAlgorithm	getBinaryMinimizationAlgorithm ()
	optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST]; More...
boolean	hasSubsumptionDuringConflictAnalysis ()
boolean	getSubsumptionDuringConflictAnalysis ()
boolean	hasClauseCleanupPeriod ()
int	getClauseCleanupPeriod ()
boolean	hasClauseCleanupTarget ()
int	getClauseCleanupTarget ()
boolean	hasClauseCleanupProtection ()
	optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE]; More...
com.google.ortools.sat.SatParameters.ClauseProtection	getClauseCleanupProtection ()
	optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE]; More...
boolean	hasClauseCleanupLbdBound ()
int	getClauseCleanupLbdBound ()
boolean	hasClauseCleanupOrdering ()
	optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY]; More...
com.google.ortools.sat.SatParameters.ClauseOrdering	getClauseCleanupOrdering ()
	optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY]; More...
boolean	hasPbCleanupIncrement ()
int	getPbCleanupIncrement ()
boolean	hasPbCleanupRatio ()
	optional double pb_cleanup_ratio = 47 [default = 0.5]; More...
double	getPbCleanupRatio ()
	optional double pb_cleanup_ratio = 47 [default = 0.5]; More...
boolean	hasMinimizeWithPropagationRestartPeriod ()
int	getMinimizeWithPropagationRestartPeriod ()
boolean	hasMinimizeWithPropagationNumDecisions ()
	optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000]; More...
int	getMinimizeWithPropagationNumDecisions ()
	optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000]; More...
boolean	hasVariableActivityDecay ()
double	getVariableActivityDecay ()
boolean	hasMaxVariableActivityValue ()
	optional double max_variable_activity_value = 16 [default = 1e+100]; More...
double	getMaxVariableActivityValue ()
	optional double max_variable_activity_value = 16 [default = 1e+100]; More...
boolean	hasGlucoseMaxDecay ()
double	getGlucoseMaxDecay ()
boolean	hasGlucoseDecayIncrement ()
	optional double glucose_decay_increment = 23 [default = 0.01]; More...
double	getGlucoseDecayIncrement ()
	optional double glucose_decay_increment = 23 [default = 0.01]; More...
boolean	hasGlucoseDecayIncrementPeriod ()
	optional int32 glucose_decay_increment_period = 24 [default = 5000]; More...
int	getGlucoseDecayIncrementPeriod ()
	optional int32 glucose_decay_increment_period = 24 [default = 5000]; More...
boolean	hasClauseActivityDecay ()
double	getClauseActivityDecay ()
boolean	hasMaxClauseActivityValue ()
	optional double max_clause_activity_value = 18 [default = 1e+20]; More...
double	getMaxClauseActivityValue ()
	optional double max_clause_activity_value = 18 [default = 1e+20]; More...
java.util.List< com.google.ortools.sat.SatParameters.RestartAlgorithm >	getRestartAlgorithmsList ()
int	getRestartAlgorithmsCount ()
com.google.ortools.sat.SatParameters.RestartAlgorithm	getRestartAlgorithms (int index)
boolean	hasDefaultRestartAlgorithms ()
	optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"]; More...
java.lang.String	getDefaultRestartAlgorithms ()
	optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"]; More...
com.google.protobuf.ByteString	getDefaultRestartAlgorithmsBytes ()
	optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"]; More...
boolean	hasRestartPeriod ()
int	getRestartPeriod ()
boolean	hasRestartRunningWindowSize ()
int	getRestartRunningWindowSize ()
boolean	hasRestartDlAverageRatio ()
double	getRestartDlAverageRatio ()
boolean	hasRestartLbdAverageRatio ()
	optional double restart_lbd_average_ratio = 71 [default = 1]; More...
double	getRestartLbdAverageRatio ()
	optional double restart_lbd_average_ratio = 71 [default = 1]; More...
boolean	hasUseBlockingRestart ()
boolean	getUseBlockingRestart ()
boolean	hasBlockingRestartWindowSize ()
	optional int32 blocking_restart_window_size = 65 [default = 5000]; More...
int	getBlockingRestartWindowSize ()
	optional int32 blocking_restart_window_size = 65 [default = 5000]; More...
boolean	hasBlockingRestartMultiplier ()
	optional double blocking_restart_multiplier = 66 [default = 1.4]; More...
double	getBlockingRestartMultiplier ()
	optional double blocking_restart_multiplier = 66 [default = 1.4]; More...
boolean	hasNumConflictsBeforeStrategyChanges ()
int	getNumConflictsBeforeStrategyChanges ()
boolean	hasStrategyChangeIncreaseRatio ()
double	getStrategyChangeIncreaseRatio ()
boolean	hasMaxTimeInSeconds ()
double	getMaxTimeInSeconds ()
boolean	hasMaxDeterministicTime ()
double	getMaxDeterministicTime ()
boolean	hasMaxNumberOfConflicts ()
long	getMaxNumberOfConflicts ()
boolean	hasMaxMemoryInMb ()
long	getMaxMemoryInMb ()
boolean	hasAbsoluteGapLimit ()
double	getAbsoluteGapLimit ()
boolean	hasRelativeGapLimit ()
	optional double relative_gap_limit = 160 [default = 0]; More...
double	getRelativeGapLimit ()
	optional double relative_gap_limit = 160 [default = 0]; More...
boolean	hasTreatBinaryClausesSeparately ()
boolean	getTreatBinaryClausesSeparately ()
boolean	hasRandomSeed ()
int	getRandomSeed ()
boolean	hasPermuteVariableRandomly ()
boolean	getPermuteVariableRandomly ()
boolean	hasPermutePresolveConstraintOrder ()
	optional bool permute_presolve_constraint_order = 179 [default = false]; More...
boolean	getPermutePresolveConstraintOrder ()
	optional bool permute_presolve_constraint_order = 179 [default = false]; More...
boolean	hasUseAbslRandom ()
	optional bool use_absl_random = 180 [default = false]; More...
boolean	getUseAbslRandom ()
	optional bool use_absl_random = 180 [default = false]; More...
boolean	hasLogSearchProgress ()
boolean	getLogSearchProgress ()
boolean	hasFillLogsInResponse ()
boolean	getFillLogsInResponse ()
boolean	hasUsePbResolution ()
boolean	getUsePbResolution ()
boolean	hasMinimizeReductionDuringPbResolution ()
boolean	getMinimizeReductionDuringPbResolution ()
boolean	hasCountAssumptionLevelsInLbd ()
boolean	getCountAssumptionLevelsInLbd ()
boolean	hasPresolveBveThreshold ()
int	getPresolveBveThreshold ()
boolean	hasPresolveBveClauseWeight ()
int	getPresolveBveClauseWeight ()
boolean	hasPresolveProbingDeterministicTimeLimit ()
double	getPresolveProbingDeterministicTimeLimit ()
boolean	hasPresolveBlockedClause ()
boolean	getPresolveBlockedClause ()
boolean	hasPresolveUseBva ()
boolean	getPresolveUseBva ()
boolean	hasPresolveBvaThreshold ()
int	getPresolveBvaThreshold ()
boolean	hasMaxPresolveIterations ()
int	getMaxPresolveIterations ()
boolean	hasCpModelPresolve ()
boolean	getCpModelPresolve ()
boolean	hasCpModelPostsolveWithFullSolver ()
boolean	getCpModelPostsolveWithFullSolver ()
boolean	hasCpModelMaxNumPresolveOperations ()
int	getCpModelMaxNumPresolveOperations ()
boolean	hasCpModelProbingLevel ()
int	getCpModelProbingLevel ()
boolean	hasCpModelUseSatPresolve ()
boolean	getCpModelUseSatPresolve ()
boolean	hasUseSatInprocessing ()
	optional bool use_sat_inprocessing = 163 [default = false]; More...
boolean	getUseSatInprocessing ()
	optional bool use_sat_inprocessing = 163 [default = false]; More...
boolean	hasExpandElementConstraints ()
boolean	getExpandElementConstraints ()
boolean	hasExpandAutomatonConstraints ()
boolean	getExpandAutomatonConstraints ()
boolean	hasExpandTableConstraints ()
boolean	getExpandTableConstraints ()
boolean	hasExpandAlldiffConstraints ()
boolean	getExpandAlldiffConstraints ()
boolean	hasExpandReservoirConstraints ()
boolean	getExpandReservoirConstraints ()
boolean	hasDisableConstraintExpansion ()
boolean	getDisableConstraintExpansion ()
boolean	hasMergeNoOverlapWorkLimit ()
double	getMergeNoOverlapWorkLimit ()
boolean	hasMergeAtMostOneWorkLimit ()
	optional double merge_at_most_one_work_limit = 146 [default = 100000000]; More...
double	getMergeAtMostOneWorkLimit ()
	optional double merge_at_most_one_work_limit = 146 [default = 100000000]; More...
boolean	hasPresolveSubstitutionLevel ()
int	getPresolveSubstitutionLevel ()
boolean	hasPresolveExtractIntegerEnforcement ()
boolean	getPresolveExtractIntegerEnforcement ()
boolean	hasUseOptimizationHints ()
boolean	getUseOptimizationHints ()
boolean	hasMinimizeCore ()
boolean	getMinimizeCore ()
boolean	hasFindMultipleCores ()
boolean	getFindMultipleCores ()
boolean	hasCoverOptimization ()
boolean	getCoverOptimization ()
boolean	hasMaxSatAssumptionOrder ()
	optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER]; More...
com.google.ortools.sat.SatParameters.MaxSatAssumptionOrder	getMaxSatAssumptionOrder ()
	optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER]; More...
boolean	hasMaxSatReverseAssumptionOrder ()
boolean	getMaxSatReverseAssumptionOrder ()
boolean	hasMaxSatStratification ()
	optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT]; More...
com.google.ortools.sat.SatParameters.MaxSatStratificationAlgorithm	getMaxSatStratification ()
	optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT]; More...
boolean	hasUsePrecedencesInDisjunctiveConstraint ()
boolean	getUsePrecedencesInDisjunctiveConstraint ()
boolean	hasUseOverloadCheckerInCumulativeConstraint ()
boolean	getUseOverloadCheckerInCumulativeConstraint ()
boolean	hasUseTimetableEdgeFindingInCumulativeConstraint ()
boolean	getUseTimetableEdgeFindingInCumulativeConstraint ()
boolean	hasUseDisjunctiveConstraintInCumulativeConstraint ()
boolean	getUseDisjunctiveConstraintInCumulativeConstraint ()
boolean	hasLinearizationLevel ()
int	getLinearizationLevel ()
boolean	hasBooleanEncodingLevel ()
int	getBooleanEncodingLevel ()
boolean	hasMaxNumCuts ()
int	getMaxNumCuts ()
boolean	hasOnlyAddCutsAtLevelZero ()
boolean	getOnlyAddCutsAtLevelZero ()
boolean	hasAddKnapsackCuts ()
boolean	getAddKnapsackCuts ()
boolean	hasAddCgCuts ()
boolean	getAddCgCuts ()
boolean	hasAddMirCuts ()
boolean	getAddMirCuts ()
boolean	hasAddZeroHalfCuts ()
boolean	getAddZeroHalfCuts ()
boolean	hasAddCliqueCuts ()
boolean	getAddCliqueCuts ()
boolean	hasMaxAllDiffCutSize ()
int	getMaxAllDiffCutSize ()
boolean	hasAddLinMaxCuts ()
boolean	getAddLinMaxCuts ()
boolean	hasMaxIntegerRoundingScaling ()
int	getMaxIntegerRoundingScaling ()
boolean	hasAddLpConstraintsLazily ()
boolean	getAddLpConstraintsLazily ()
boolean	hasMinOrthogonalityForLpConstraints ()
double	getMinOrthogonalityForLpConstraints ()
boolean	hasMaxCutRoundsAtLevelZero ()
int	getMaxCutRoundsAtLevelZero ()
boolean	hasMaxConsecutiveInactiveCount ()
int	getMaxConsecutiveInactiveCount ()
boolean	hasCutMaxActiveCountValue ()
double	getCutMaxActiveCountValue ()
boolean	hasCutActiveCountDecay ()
	optional double cut_active_count_decay = 156 [default = 0.8]; More...
double	getCutActiveCountDecay ()
	optional double cut_active_count_decay = 156 [default = 0.8]; More...
boolean	hasCutCleanupTarget ()
int	getCutCleanupTarget ()
boolean	hasNewConstraintsBatchSize ()
int	getNewConstraintsBatchSize ()
boolean	hasSearchBranching ()
	optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH]; More...
com.google.ortools.sat.SatParameters.SearchBranching	getSearchBranching ()
	optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH]; More...
boolean	hasHintConflictLimit ()
int	getHintConflictLimit ()
boolean	hasRepairHint ()
boolean	getRepairHint ()
boolean	hasExploitIntegerLpSolution ()
boolean	getExploitIntegerLpSolution ()
boolean	hasExploitAllLpSolution ()
boolean	getExploitAllLpSolution ()
boolean	hasExploitBestSolution ()
boolean	getExploitBestSolution ()
boolean	hasExploitRelaxationSolution ()
boolean	getExploitRelaxationSolution ()
boolean	hasExploitObjective ()
boolean	getExploitObjective ()
boolean	hasProbingPeriodAtRoot ()
long	getProbingPeriodAtRoot ()
boolean	hasUseProbingSearch ()
boolean	getUseProbingSearch ()
boolean	hasPseudoCostReliabilityThreshold ()
long	getPseudoCostReliabilityThreshold ()
boolean	hasOptimizeWithCore ()
boolean	getOptimizeWithCore ()
boolean	hasBinarySearchNumConflicts ()
int	getBinarySearchNumConflicts ()
boolean	hasOptimizeWithMaxHs ()
boolean	getOptimizeWithMaxHs ()
boolean	hasEnumerateAllSolutions ()
boolean	getEnumerateAllSolutions ()
boolean	hasKeepAllFeasibleSolutionsInPresolve ()
boolean	getKeepAllFeasibleSolutionsInPresolve ()
boolean	hasFillTightenedDomainsInResponse ()
boolean	getFillTightenedDomainsInResponse ()
boolean	hasInstantiateAllVariables ()
boolean	getInstantiateAllVariables ()
boolean	hasAutoDetectGreaterThanAtLeastOneOf ()
boolean	getAutoDetectGreaterThanAtLeastOneOf ()
boolean	hasStopAfterFirstSolution ()
boolean	getStopAfterFirstSolution ()
boolean	hasStopAfterPresolve ()
boolean	getStopAfterPresolve ()
boolean	hasNumSearchWorkers ()
int	getNumSearchWorkers ()
boolean	hasInterleaveSearch ()
boolean	getInterleaveSearch ()
boolean	hasInterleaveBatchSize ()
	optional int32 interleave_batch_size = 134 [default = 1]; More...
int	getInterleaveBatchSize ()
	optional int32 interleave_batch_size = 134 [default = 1]; More...
boolean	hasReduceMemoryUsageInInterleaveMode ()
boolean	getReduceMemoryUsageInInterleaveMode ()
boolean	hasShareObjectiveBounds ()
boolean	getShareObjectiveBounds ()
boolean	hasShareLevelZeroBounds ()
boolean	getShareLevelZeroBounds ()
boolean	hasUseLnsOnly ()
boolean	getUseLnsOnly ()
boolean	hasLnsFocusOnDecisionVariables ()
	optional bool lns_focus_on_decision_variables = 105 [default = false]; More...
boolean	getLnsFocusOnDecisionVariables ()
	optional bool lns_focus_on_decision_variables = 105 [default = false]; More...
boolean	hasLnsExpandIntervalsInConstraintGraph ()
	optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true]; More...
boolean	getLnsExpandIntervalsInConstraintGraph ()
	optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true]; More...
boolean	hasUseRinsLns ()
boolean	getUseRinsLns ()
boolean	hasUseFeasibilityPump ()
boolean	getUseFeasibilityPump ()
boolean	hasFpRounding ()
	optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED]; More...
com.google.ortools.sat.SatParameters.FPRoundingMethod	getFpRounding ()
	optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED]; More...
boolean	hasUseRelaxationLns ()
boolean	getUseRelaxationLns ()
boolean	hasDiversifyLnsParams ()
boolean	getDiversifyLnsParams ()
boolean	hasRandomizeSearch ()
boolean	getRandomizeSearch ()
boolean	hasSearchRandomizationTolerance ()
long	getSearchRandomizationTolerance ()
boolean	hasUseOptionalVariables ()
boolean	getUseOptionalVariables ()
boolean	hasUseExactLpReason ()
boolean	getUseExactLpReason ()
boolean	hasUseBranchingInLp ()
boolean	getUseBranchingInLp ()
boolean	hasUseCombinedNoOverlap ()
boolean	getUseCombinedNoOverlap ()
boolean	hasCatchSigintSignal ()
boolean	getCatchSigintSignal ()
boolean	hasUseImpliedBounds ()
boolean	getUseImpliedBounds ()
boolean	hasPolishLpSolution ()
boolean	getPolishLpSolution ()
boolean	hasConvertIntervals ()
boolean	getConvertIntervals ()
boolean	hasSymmetryLevel ()
int	getSymmetryLevel ()
boolean	hasMipMaxBound ()
double	getMipMaxBound ()
boolean	hasMipVarScaling ()
double	getMipVarScaling ()
boolean	hasMipAutomaticallyScaleVariables ()
boolean	getMipAutomaticallyScaleVariables ()
boolean	hasMipWantedPrecision ()
double	getMipWantedPrecision ()
boolean	hasMipMaxActivityExponent ()
int	getMipMaxActivityExponent ()
boolean	hasMipCheckPrecision ()
double	getMipCheckPrecision ()

Member Function Documentation

getAbsoluteGapLimit()

double getAbsoluteGapLimit

(

)

Stop the search when the gap between the best feasible objective (O) and
our best objective bound (B) is smaller than a limit.
The exact definition is:

Absolute: abs(O - B)
Relative: abs(O - B) / max(1, abs(O)).
Important: The relative gap depends on the objective offset! If you
artificially shift the objective, you will get widely different value of
the relative gap.
Note that if the gap is reached, the search status will be OPTIMAL. But
one can check the best objective bound to see the actual gap.

optional double absolute_gap_limit = 159 [default = 0];
Returns
The absoluteGapLimit.

Implemented in SatParameters.Builder, and SatParameters.

getAddCgCuts()

boolean getAddCgCuts

(

)

Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
Note that for now, this is not heavily tuned.

optional bool add_cg_cuts = 117 [default = true];

Returns

The addCgCuts.

Implemented in SatParameters.Builder, and SatParameters.

getAddCliqueCuts()

boolean getAddCliqueCuts

(

)

Whether we generate clique cuts from the binary implication graph. Note
that as the search goes on, this graph will contains new binary clauses
learned by the SAT engine.

optional bool add_clique_cuts = 172 [default = true];

Returns

The addCliqueCuts.

Implemented in SatParameters.Builder, and SatParameters.

getAddKnapsackCuts()

boolean getAddKnapsackCuts

(

)

Whether we generate knapsack cuts. Note that in our setting where all
variables are integer and bounded on both side, such a cut could be applied
to any constraint.

optional bool add_knapsack_cuts = 111 [default = false];

Returns

The addKnapsackCuts.

Implemented in SatParameters.Builder, and SatParameters.

getAddLinMaxCuts()

boolean getAddLinMaxCuts

(

)

For the lin max constraints, generates the cuts described in "Strong
mixed-integer programming formulations for trained neural networks" by Ross
Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)

optional bool add_lin_max_cuts = 152 [default = true];

Returns

The addLinMaxCuts.

Implemented in SatParameters.Builder, and SatParameters.

getAddLpConstraintsLazily()

boolean getAddLpConstraintsLazily

(

)

If true, we start by an empty LP, and only add constraints not satisfied
by the current LP solution batch by batch. A constraint that is only added
like this is known as a "lazy" constraint in the literature, except that we
currently consider all constraints as lazy here.

optional bool add_lp_constraints_lazily = 112 [default = true];

Returns

The addLpConstraintsLazily.

Implemented in SatParameters.Builder, and SatParameters.

getAddMirCuts()

boolean getAddMirCuts

(

)

Whether we generate MIR cuts at root node.
Note that for now, this is not heavily tuned.

optional bool add_mir_cuts = 120 [default = true];

Returns

The addMirCuts.

Implemented in SatParameters.Builder, and SatParameters.

getAddZeroHalfCuts()

boolean getAddZeroHalfCuts

(

)

Whether we generate Zero-Half cuts at root node.
Note that for now, this is not heavily tuned.

optional bool add_zero_half_cuts = 169 [default = true];

Returns

The addZeroHalfCuts.

Implemented in SatParameters.Builder, and SatParameters.

getAlsoBumpVariablesInConflictReasons()

boolean getAlsoBumpVariablesInConflictReasons

(

)

When this is true, then the variables that appear in any of the reason of
the variables in a conflict have their activity bumped. This is addition to
the variables in the conflict, and the one that were used during conflict
resolution.

optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];

Returns

The alsoBumpVariablesInConflictReasons.

Implemented in SatParameters.Builder, and SatParameters.

getAutoDetectGreaterThanAtLeastOneOf()

boolean getAutoDetectGreaterThanAtLeastOneOf

(

)

If true, then the precedences propagator try to detect for each variable if
it has a set of "optional incoming arc" for which at least one of them is
present. This is usually useful to have but can be slow on model with a lot
of precedence.

optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];

Returns

The autoDetectGreaterThanAtLeastOneOf.

Implemented in SatParameters.Builder, and SatParameters.

getBinaryMinimizationAlgorithm()

com.google.ortools.sat.SatParameters.BinaryMinizationAlgorithm getBinaryMinimizationAlgorithm

(

)

optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];

Returns

The binaryMinimizationAlgorithm.

Implemented in SatParameters.Builder, and SatParameters.

getBinarySearchNumConflicts()

int getBinarySearchNumConflicts

(

)

If non-negative, perform a binary search on the objective variable in order
to find an [min, max] interval outside of which the solver proved unsat/sat
under this amount of conflict. This can quickly reduce the objective domain
on some problems.

optional int32 binary_search_num_conflicts = 99 [default = -1];

Returns

The binarySearchNumConflicts.

Implemented in SatParameters.Builder, and SatParameters.

getBlockingRestartMultiplier()

double getBlockingRestartMultiplier

(

)

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns

The blockingRestartMultiplier.

Implemented in SatParameters.Builder, and SatParameters.

getBlockingRestartWindowSize()

int getBlockingRestartWindowSize

(

)

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns

The blockingRestartWindowSize.

Implemented in SatParameters.Builder, and SatParameters.

getBooleanEncodingLevel()

int getBooleanEncodingLevel

(

)

A non-negative level indicating how much we should try to fully encode
Integer variables as Boolean.

optional int32 boolean_encoding_level = 107 [default = 1];

Returns

The booleanEncodingLevel.

Implemented in SatParameters.Builder, and SatParameters.

getCatchSigintSignal()

boolean getCatchSigintSignal

(

)

Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals
when calling solve. If set, catching the SIGINT signal will terminate the
search gracefully, as if a time limit was reached.

optional bool catch_sigint_signal = 135 [default = true];

Returns

The catchSigintSignal.

Implemented in SatParameters.Builder, and SatParameters.

getClauseActivityDecay()

double getClauseActivityDecay

(

)

Clause activity parameters (same effect as the one on the variables).

optional double clause_activity_decay = 17 [default = 0.999];

Returns

The clauseActivityDecay.

Implemented in SatParameters.Builder, and SatParameters.

getClauseCleanupLbdBound()

int getClauseCleanupLbdBound

(

)

All the clauses with a LBD (literal blocks distance) lower or equal to this
parameters will always be kept.

optional int32 clause_cleanup_lbd_bound = 59 [default = 5];

Returns

The clauseCleanupLbdBound.

Implemented in SatParameters.Builder, and SatParameters.

getClauseCleanupOrdering()

com.google.ortools.sat.SatParameters.ClauseOrdering getClauseCleanupOrdering

(

)

optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];

Returns

The clauseCleanupOrdering.

Implemented in SatParameters.Builder, and SatParameters.

getClauseCleanupPeriod()

int getClauseCleanupPeriod

(

)

Trigger a cleanup when this number of "deletable" clauses is learned.

optional int32 clause_cleanup_period = 11 [default = 10000];

Returns

The clauseCleanupPeriod.

Implemented in SatParameters.Builder, and SatParameters.

getClauseCleanupProtection()

com.google.ortools.sat.SatParameters.ClauseProtection getClauseCleanupProtection

(

)

optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];

Returns

The clauseCleanupProtection.

Implemented in SatParameters.Builder, and SatParameters.

getClauseCleanupTarget()

int getClauseCleanupTarget

(

)

During a cleanup, we will always keep that number of "deletable" clauses.
Note that this doesn't include the "protected" clauses.

optional int32 clause_cleanup_target = 13 [default = 10000];

Returns

The clauseCleanupTarget.

Implemented in SatParameters.Builder, and SatParameters.

getConvertIntervals()

boolean getConvertIntervals

(

)

Temporary flag util the feature is more mature. This convert intervals to
the newer proto format that support affine start/var/end instead of just
variables. It changes a bit the search and is not always better currently.

optional bool convert_intervals = 177 [default = false];

Returns

The convertIntervals.

Implemented in SatParameters.Builder, and SatParameters.

getCountAssumptionLevelsInLbd()

boolean getCountAssumptionLevelsInLbd

(

)

Whether or not the assumption levels are taken into account during the LBD
computation. According to the reference below, not counting them improves
the solver in some situation. Note that this only impact solves under
assumptions.
Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for
Incremental SAT Solving with Assumptions: Application to MUS Extraction"
Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes
in Computer Science Volume 7962, 2013, pp 309-317.

optional bool count_assumption_levels_in_lbd = 49 [default = true];

Returns

The countAssumptionLevelsInLbd.

Implemented in SatParameters.Builder, and SatParameters.

getCoverOptimization()

boolean getCoverOptimization

(

)

If true, when the max-sat algo find a core, we compute the minimal number
of literals in the core that needs to be true to have a feasible solution.

optional bool cover_optimization = 89 [default = true];

Returns

The coverOptimization.

Implemented in SatParameters.Builder, and SatParameters.

getCpModelMaxNumPresolveOperations()

int getCpModelMaxNumPresolveOperations

(

)

If positive, try to stop just after that many presolve rules have been
applied. This is mainly useful for debugging presolve.

optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];

Returns

The cpModelMaxNumPresolveOperations.

Implemented in SatParameters.Builder, and SatParameters.

getCpModelPostsolveWithFullSolver()

boolean getCpModelPostsolveWithFullSolver

(

)

Advanced usage. We have two different postsolve code. The default one
should be better and it allows for a more powerful presolve, but some
rarely used features like not fully assigning all variables require the
other one.

optional bool cp_model_postsolve_with_full_solver = 162 [default = false];

Returns

The cpModelPostsolveWithFullSolver.

Implemented in SatParameters.Builder, and SatParameters.

getCpModelPresolve()

boolean getCpModelPresolve

(

)

Whether we presolve the cp_model before solving it.

optional bool cp_model_presolve = 86 [default = true];

Returns

The cpModelPresolve.

Implemented in SatParameters.Builder, and SatParameters.

getCpModelProbingLevel()

int getCpModelProbingLevel

(

)

How much effort do we spend on probing. 0 disables it completely.

optional int32 cp_model_probing_level = 110 [default = 2];

Returns

The cpModelProbingLevel.

Implemented in SatParameters.Builder, and SatParameters.

getCpModelUseSatPresolve()

boolean getCpModelUseSatPresolve

(

)

Whether we also use the sat presolve when cp_model_presolve is true.

optional bool cp_model_use_sat_presolve = 93 [default = true];

Returns

The cpModelUseSatPresolve.

Implemented in SatParameters.Builder, and SatParameters.

getCutActiveCountDecay()

double getCutActiveCountDecay

(

)

optional double cut_active_count_decay = 156 [default = 0.8];

Returns

The cutActiveCountDecay.

Implemented in SatParameters.Builder, and SatParameters.

getCutCleanupTarget()

int getCutCleanupTarget

(

)

Target number of constraints to remove during cleanup.

optional int32 cut_cleanup_target = 157 [default = 1000];

Returns

The cutCleanupTarget.

Implemented in SatParameters.Builder, and SatParameters.

getCutMaxActiveCountValue()

double getCutMaxActiveCountValue

(

)

These parameters are similar to sat clause management activity parameters.
They are effective only if the number of generated cuts exceed the storage
limit. Default values are based on a few experiments on miplib instances.

optional double cut_max_active_count_value = 155 [default = 10000000000];

Returns

The cutMaxActiveCountValue.

Implemented in SatParameters.Builder, and SatParameters.

getDefaultRestartAlgorithms()

java.lang.String getDefaultRestartAlgorithms

(

)

optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];

Returns

The defaultRestartAlgorithms.

Implemented in SatParameters.Builder, and SatParameters.

getDefaultRestartAlgorithmsBytes()

com.google.protobuf.ByteString getDefaultRestartAlgorithmsBytes

(

)

optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];

Returns

The bytes for defaultRestartAlgorithms.

Implemented in SatParameters.Builder, and SatParameters.

getDisableConstraintExpansion()

boolean getDisableConstraintExpansion

(

)

If true, it disable all constraint expansion.
This should only be used to test the presolve of expanded constraints.

optional bool disable_constraint_expansion = 181 [default = false];

Returns

The disableConstraintExpansion.

Implemented in SatParameters.Builder, and SatParameters.

getDiversifyLnsParams()

boolean getDiversifyLnsParams

(

)

If true, registers more lns subsolvers with different parameters.

optional bool diversify_lns_params = 137 [default = false];

Returns

The diversifyLnsParams.

Implemented in SatParameters.Builder, and SatParameters.

getEnumerateAllSolutions()

boolean getEnumerateAllSolutions

(

)

Whether we enumerate all solutions of a problem without objective. Note
that setting this to true automatically disable the presolve. This is
because the presolve rules only guarantee the existence of one feasible
solution to the presolved problem.
TODO(user): Do not disable the presolve and let the user choose what
behavior is best by setting keep_all_feasible_solutions_in_presolve.

optional bool enumerate_all_solutions = 87 [default = false];

Returns

The enumerateAllSolutions.

Implemented in SatParameters.Builder, and SatParameters.

getExpandAlldiffConstraints()

boolean getExpandAlldiffConstraints

(

)

If true, expand all_different constraints that are not permutations.
Permutations (#Variables = #Values) are always expanded.

optional bool expand_alldiff_constraints = 170 [default = false];

Returns

The expandAlldiffConstraints.

Implemented in SatParameters.Builder, and SatParameters.

getExpandAutomatonConstraints()

boolean getExpandAutomatonConstraints

(

)

If true, the automaton constraints are expanded.

optional bool expand_automaton_constraints = 143 [default = true];

Returns

The expandAutomatonConstraints.

Implemented in SatParameters.Builder, and SatParameters.

getExpandElementConstraints()

boolean getExpandElementConstraints

(

)

If true, the element constraints are expanded into many
linear constraints of the form (index == i) => (element[i] == target).

optional bool expand_element_constraints = 140 [default = true];

Returns

The expandElementConstraints.

Implemented in SatParameters.Builder, and SatParameters.

getExpandReservoirConstraints()

boolean getExpandReservoirConstraints

(

)

If true, expand the reservoir constraints by creating booleans for all
possible precedences between event and encoding the constraint.

optional bool expand_reservoir_constraints = 182 [default = true];

Returns

The expandReservoirConstraints.

Implemented in SatParameters.Builder, and SatParameters.

getExpandTableConstraints()

boolean getExpandTableConstraints

(

)

If true, the positive table constraints are expanded.
Note that currently, negative table constraints are always expanded.

optional bool expand_table_constraints = 158 [default = true];

Returns

The expandTableConstraints.

Implemented in SatParameters.Builder, and SatParameters.

getExploitAllLpSolution()

boolean getExploitAllLpSolution

(

)

If true and the Lp relaxation of the problem has a solution, try to exploit
it. This is same as above except in this case the lp solution might not be
an integer solution.

optional bool exploit_all_lp_solution = 116 [default = true];

Returns

The exploitAllLpSolution.

Implemented in SatParameters.Builder, and SatParameters.

getExploitBestSolution()

boolean getExploitBestSolution

(

)

When branching on a variable, follow the last best solution value.

optional bool exploit_best_solution = 130 [default = false];

Returns

The exploitBestSolution.

Implemented in SatParameters.Builder, and SatParameters.

getExploitIntegerLpSolution()

boolean getExploitIntegerLpSolution

(

)

If true and the Lp relaxation of the problem has an integer optimal
solution, try to exploit it. Note that since the LP relaxation may not
contain all the constraints, such a solution is not necessarily a solution
of the full problem.

optional bool exploit_integer_lp_solution = 94 [default = true];

Returns

The exploitIntegerLpSolution.

Implemented in SatParameters.Builder, and SatParameters.

getExploitObjective()

boolean getExploitObjective

(

)

When branching an a variable that directly affect the objective,
branch on the value that lead to the best objective first.

optional bool exploit_objective = 131 [default = true];

Returns

The exploitObjective.

Implemented in SatParameters.Builder, and SatParameters.

getExploitRelaxationSolution()

boolean getExploitRelaxationSolution

(

)

When branching on a variable, follow the last best relaxation solution
value. We use the relaxation with the tightest bound on the objective as
the best relaxation solution.

optional bool exploit_relaxation_solution = 161 [default = false];

Returns

The exploitRelaxationSolution.

Implemented in SatParameters.Builder, and SatParameters.

getFillLogsInResponse()

boolean getFillLogsInResponse

(

)

Whether logs should be stored in the response proto.

optional bool fill_logs_in_response = 185 [default = false];

Returns

The fillLogsInResponse.

Implemented in SatParameters.Builder, and SatParameters.

getFillTightenedDomainsInResponse()

boolean getFillTightenedDomainsInResponse

(

)

If true, add information about the derived variable domains to the
CpSolverResponse. It is an option because it makes the response slighly
bigger and there is a bit more work involved during the postsolve to
construct it, but it should still have a low overhead. See the
tightened_variables field in CpSolverResponse for more details.

optional bool fill_tightened_domains_in_response = 132 [default = false];

Returns

The fillTightenedDomainsInResponse.

Implemented in SatParameters.Builder, and SatParameters.

getFindMultipleCores()

boolean getFindMultipleCores

(

)

Whether we try to find more independent cores for a given set of
assumptions in the core based max-SAT algorithms.

optional bool find_multiple_cores = 84 [default = true];

Returns

The findMultipleCores.

Implemented in SatParameters.Builder, and SatParameters.

getFpRounding()

com.google.ortools.sat.SatParameters.FPRoundingMethod getFpRounding

(

)

optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];

Returns

The fpRounding.

Implemented in SatParameters.Builder, and SatParameters.

getGlucoseDecayIncrement()

double getGlucoseDecayIncrement

(

)

optional double glucose_decay_increment = 23 [default = 0.01];

Returns

The glucoseDecayIncrement.

Implemented in SatParameters.Builder, and SatParameters.

getGlucoseDecayIncrementPeriod()

int getGlucoseDecayIncrementPeriod

(

)

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns

The glucoseDecayIncrementPeriod.

Implemented in SatParameters.Builder, and SatParameters.

getGlucoseMaxDecay()

double getGlucoseMaxDecay

(

)

The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until
0.95. This "hack" seems to work well and comes from:
Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013
http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136

optional double glucose_max_decay = 22 [default = 0.95];

Returns

The glucoseMaxDecay.

Implemented in SatParameters.Builder, and SatParameters.

getHintConflictLimit()

int getHintConflictLimit

(

)

Conflict limit used in the phase that exploit the solution hint.

optional int32 hint_conflict_limit = 153 [default = 10];

Returns

The hintConflictLimit.

Implemented in SatParameters.Builder, and SatParameters.

getInitialPolarity()

com.google.ortools.sat.SatParameters.Polarity getInitialPolarity

(

)

optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];

Returns

The initialPolarity.

Implemented in SatParameters.Builder, and SatParameters.

getInitialVariablesActivity()

double getInitialVariablesActivity

(

)

The initial value of the variables activity. A non-zero value only make
sense when use_erwa_heuristic is true. Experiments with a value of 1e-2
together with the ERWA heuristic showed slighthly better result than simply
using zero. The idea is that when the "learning rate" of a variable becomes
lower than this value, then we prefer to branch on never explored before
variables. This is not in the ERWA paper.

optional double initial_variables_activity = 76 [default = 0];

Returns

The initialVariablesActivity.

Implemented in SatParameters.Builder, and SatParameters.

getInstantiateAllVariables()

boolean getInstantiateAllVariables

(

)

If true, the solver will add a default integer branching strategy to the
already defined search strategy.

optional bool instantiate_all_variables = 106 [default = true];

Returns

The instantiateAllVariables.

Implemented in SatParameters.Builder, and SatParameters.

getInterleaveBatchSize()

int getInterleaveBatchSize

(

)

optional int32 interleave_batch_size = 134 [default = 1];

Returns

The interleaveBatchSize.

Implemented in SatParameters.Builder, and SatParameters.

getInterleaveSearch()

boolean getInterleaveSearch

(

)

Experimental. If this is true, then we interleave all our major search
strategy and distribute the work amongst num_search_workers.
The search is deterministic (independently of num_search_workers!), and we
schedule and wait for interleave_batch_size task to be completed before
synchronizing and scheduling the next batch of tasks.

optional bool interleave_search = 136 [default = false];

Returns

The interleaveSearch.

Implemented in SatParameters.Builder, and SatParameters.

getKeepAllFeasibleSolutionsInPresolve()

boolean getKeepAllFeasibleSolutionsInPresolve

(

)

If true, we disable the presolve reductions that remove feasible solutions
from the search space. Such solution are usually dominated by a "better"
solution that is kept, but depending on the situation, we might want to
keep all solutions.
A trivial example is when a variable is unused. If this is true, then the
presolve will not fix it to an arbitrary value and it will stay in the
search space.

optional bool keep_all_feasible_solutions_in_presolve = 173 [default = false];

Returns

The keepAllFeasibleSolutionsInPresolve.

Implemented in SatParameters.Builder, and SatParameters.

getLinearizationLevel()

int getLinearizationLevel

(

)

A non-negative level indicating the type of constraints we consider in the
LP relaxation. At level zero, no LP relaxation is used. At level 1, only
the linear constraint and full encoding are added. At level 2, we also add
all the Boolean constraints.

optional int32 linearization_level = 90 [default = 1];

Returns

The linearizationLevel.

Implemented in SatParameters.Builder, and SatParameters.

getLnsExpandIntervalsInConstraintGraph()

boolean getLnsExpandIntervalsInConstraintGraph

(

)

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns

The lnsExpandIntervalsInConstraintGraph.

Implemented in SatParameters.Builder, and SatParameters.

getLnsFocusOnDecisionVariables()

boolean getLnsFocusOnDecisionVariables

(

)

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns

The lnsFocusOnDecisionVariables.

Implemented in SatParameters.Builder, and SatParameters.

getLogSearchProgress()

boolean getLogSearchProgress

(

)

Whether the solver should log the search progress to LOG(INFO).

optional bool log_search_progress = 41 [default = false];

Returns

The logSearchProgress.

Implemented in SatParameters.Builder, and SatParameters.

getMaxAllDiffCutSize()

int getMaxAllDiffCutSize

(

)

Cut generator for all diffs can add too many cuts for large all_diff
constraints. This parameter restricts the large all_diff constraints to
have a cut generator.

optional int32 max_all_diff_cut_size = 148 [default = 7];

Returns

The maxAllDiffCutSize.

Implemented in SatParameters.Builder, and SatParameters.

getMaxClauseActivityValue()

double getMaxClauseActivityValue

(

)

optional double max_clause_activity_value = 18 [default = 1e+20];

Returns

The maxClauseActivityValue.

Implemented in SatParameters.Builder, and SatParameters.

getMaxConsecutiveInactiveCount()

int getMaxConsecutiveInactiveCount

(

)

If a constraint/cut in LP is not active for that many consecutive OPTIMAL
solves, remove it from the LP. Note that it might be added again later if
it become violated by the current LP solution.

optional int32 max_consecutive_inactive_count = 121 [default = 100];

Returns

The maxConsecutiveInactiveCount.

Implemented in SatParameters.Builder, and SatParameters.

getMaxCutRoundsAtLevelZero()

int getMaxCutRoundsAtLevelZero

(

)

Max number of time we perform cut generation and resolve the LP at level 0.

optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];

Returns

The maxCutRoundsAtLevelZero.

Implemented in SatParameters.Builder, and SatParameters.

getMaxDeterministicTime()

double getMaxDeterministicTime

(

)

Maximum time allowed in deterministic time to solve a problem.
The deterministic time should be correlated with the real time used by the
solver, the time unit being as close as possible to a second.

optional double max_deterministic_time = 67 [default = inf];

Returns

The maxDeterministicTime.

Implemented in SatParameters.Builder, and SatParameters.

getMaxIntegerRoundingScaling()

int getMaxIntegerRoundingScaling

(

)

In the integer rounding procedure used for MIR and Gomory cut, the maximum
"scaling" we use (must be positive). The lower this is, the lower the
integer coefficients of the cut will be. Note that cut generated by lower
values are not necessarily worse than cut generated by larger value. There
is no strict dominance relationship.
Setting this to 2 result in the "strong fractional rouding" of Letchford
and Lodi.

optional int32 max_integer_rounding_scaling = 119 [default = 600];

Returns

The maxIntegerRoundingScaling.

Implemented in SatParameters.Builder, and SatParameters.

getMaxMemoryInMb()

long getMaxMemoryInMb

(

)

Maximum memory allowed for the whole thread containing the solver. The
solver will abort as soon as it detects that this limit is crossed. As a
result, this limit is approximative, but usually the solver will not go too
much over.

optional int64 max_memory_in_mb = 40 [default = 10000];

Returns

The maxMemoryInMb.

Implemented in SatParameters.Builder, and SatParameters.

getMaxNumberOfConflicts()

long getMaxNumberOfConflicts

(

)

Maximum number of conflicts allowed to solve a problem.
TODO(user,user): Maybe change the way the conflict limit is enforced?
currently it is enforced on each independent internal SAT solve, rather
than on the overall number of conflicts across all solves. So in the
context of an optimization problem, this is not really usable directly by a
client.

optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];

Returns

The maxNumberOfConflicts.

Implemented in SatParameters.Builder, and SatParameters.

getMaxNumCuts()

int getMaxNumCuts

(

)

The limit on the number of cuts in our cut pool. When this is reached we do
not generate cuts anymore.
TODO(user): We should probably remove this parameters, and just always
generate cuts but only keep the best n or something.

optional int32 max_num_cuts = 91 [default = 10000];

Returns

The maxNumCuts.

Implemented in SatParameters.Builder, and SatParameters.

getMaxPresolveIterations()

int getMaxPresolveIterations

(

)

In case of large reduction in a presolve iteration, we perform multiple
presolve iterations. This parameter controls the maximum number of such
presolve iterations.

optional int32 max_presolve_iterations = 138 [default = 3];

Returns

The maxPresolveIterations.

Implemented in SatParameters.Builder, and SatParameters.

getMaxSatAssumptionOrder()

com.google.ortools.sat.SatParameters.MaxSatAssumptionOrder getMaxSatAssumptionOrder

(

)

optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];

Returns

The maxSatAssumptionOrder.

Implemented in SatParameters.Builder, and SatParameters.

getMaxSatReverseAssumptionOrder()

boolean getMaxSatReverseAssumptionOrder

(

)

If true, adds the assumption in the reverse order of the one defined by
max_sat_assumption_order.

optional bool max_sat_reverse_assumption_order = 52 [default = false];

Returns

The maxSatReverseAssumptionOrder.

Implemented in SatParameters.Builder, and SatParameters.

getMaxSatStratification()

com.google.ortools.sat.SatParameters.MaxSatStratificationAlgorithm getMaxSatStratification

(

)

optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];

Returns

The maxSatStratification.

Implemented in SatParameters.Builder, and SatParameters.

getMaxTimeInSeconds()

double getMaxTimeInSeconds

(

)

Maximum time allowed in seconds to solve a problem.
The counter will starts at the beginning of the Solve() call.

optional double max_time_in_seconds = 36 [default = inf];

Returns

The maxTimeInSeconds.

Implemented in SatParameters.Builder, and SatParameters.

getMaxVariableActivityValue()

double getMaxVariableActivityValue

(

)

optional double max_variable_activity_value = 16 [default = 1e+100];

Returns

The maxVariableActivityValue.

Implemented in SatParameters.Builder, and SatParameters.

getMergeAtMostOneWorkLimit()

double getMergeAtMostOneWorkLimit

(

)

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns

The mergeAtMostOneWorkLimit.

Implemented in SatParameters.Builder, and SatParameters.

getMergeNoOverlapWorkLimit()

double getMergeNoOverlapWorkLimit

(

)

During presolve, we use a maximum clique heuristic to merge together
no-overlap constraints or at most one constraints. This code can be slow,
so we have a limit in place on the number of explored nodes in the
underlying graph. The internal limit is an int64, but we use double here to
simplify manual input.

optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];

Returns

The mergeNoOverlapWorkLimit.

Implemented in SatParameters.Builder, and SatParameters.

getMinimizationAlgorithm()

com.google.ortools.sat.SatParameters.ConflictMinimizationAlgorithm getMinimizationAlgorithm

(

)

optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];

Returns

The minimizationAlgorithm.

Implemented in SatParameters.Builder, and SatParameters.

getMinimizeCore()

boolean getMinimizeCore

(

)

Whether we use a simple heuristic to try to minimize an UNSAT core.

optional bool minimize_core = 50 [default = true];

Returns

The minimizeCore.

Implemented in SatParameters.Builder, and SatParameters.

getMinimizeReductionDuringPbResolution()

boolean getMinimizeReductionDuringPbResolution

(

)

A different algorithm during PB resolution. It minimizes the number of
calls to ReduceCoefficients() which can be time consuming. However, the
search space will be different and if the coefficients are large, this may
lead to integer overflows that could otherwise be prevented.

optional bool minimize_reduction_during_pb_resolution = 48 [default = false];

Returns

The minimizeReductionDuringPbResolution.

Implemented in SatParameters.Builder, and SatParameters.

getMinimizeWithPropagationNumDecisions()

int getMinimizeWithPropagationNumDecisions

(

)

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns

The minimizeWithPropagationNumDecisions.

Implemented in SatParameters.Builder, and SatParameters.

getMinimizeWithPropagationRestartPeriod()

int getMinimizeWithPropagationRestartPeriod

(

)

Parameters for an heuristic similar to the one descibed in "An effective
learnt clause minimization approach for CDCL Sat Solvers",
https://www.ijcai.org/proceedings/2017/0098.pdf
For now, we have a somewhat simpler implementation where every x restart we
spend y decisions on clause minimization. The minimization technique is the
same as the one used to minimize core in max-sat. We also minimize problem
clauses and not just the learned clause that we keep forever like in the
paper.
Changing these parameters or the kind of clause we minimize seems to have
a big impact on the overall perf on our benchmarks. So this technique seems
definitely useful, but it is hard to tune properly.

optional int32 minimize_with_propagation_restart_period = 96 [default = 10];

Returns

The minimizeWithPropagationRestartPeriod.

Implemented in SatParameters.Builder, and SatParameters.

getMinOrthogonalityForLpConstraints()

double getMinOrthogonalityForLpConstraints

(

)

While adding constraints, skip the constraints which have orthogonality
less than 'min_orthogonality_for_lp_constraints' with already added
constraints during current call. Orthogonality is defined as 1 -
cosine(vector angle between constraints). A value of zero disable this
feature.

optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];

Returns

The minOrthogonalityForLpConstraints.

Implemented in SatParameters.Builder, and SatParameters.

getMipAutomaticallyScaleVariables()

boolean getMipAutomaticallyScaleVariables

(

)

If true, some continuous variable might be automatially scaled. For now,
this is only the case where we detect that a variable is actually an
integer multiple of a constant. For instance, variables of the form k * 0.5
are quite frequent, and if we detect this, we will scale such variable
domain by 2 to make it implied integer.

optional bool mip_automatically_scale_variables = 166 [default = true];

Returns

The mipAutomaticallyScaleVariables.

Implemented in SatParameters.Builder, and SatParameters.

getMipCheckPrecision()

double getMipCheckPrecision

(

)

As explained in mip_precision and mip_max_activity_exponent, we cannot
always reach the wanted precision during scaling. We use this threshold to
enphasize in the logs when the precision seems bad.

optional double mip_check_precision = 128 [default = 0.0001];

Returns

The mipCheckPrecision.

Implemented in SatParameters.Builder, and SatParameters.

getMipMaxActivityExponent()

int getMipMaxActivityExponent

(

)

To avoid integer overflow, we always force the maximum possible constraint
activity (and objective value) according to the initial variable domain to
be smaller than 2 to this given power. Because of this, we cannot always
reach the "mip_wanted_precision" parameter above.
This can go as high as 62, but some internal algo currently abort early if
they might run into integer overflow, so it is better to keep it a bit
lower than this.

optional int32 mip_max_activity_exponent = 127 [default = 53];

Returns

The mipMaxActivityExponent.

Implemented in SatParameters.Builder, and SatParameters.

getMipMaxBound()

double getMipMaxBound

(

)

We need to bound the maximum magnitude of the variables for CP-SAT, and
that is the bound we use. If the MIP model expect larger variable value in
the solution, then the converted model will likely not be relevant.

optional double mip_max_bound = 124 [default = 10000000];

Returns

The mipMaxBound.

Implemented in SatParameters.Builder, and SatParameters.

getMipVarScaling()

double getMipVarScaling

(

)

All continuous variable of the problem will be multiplied by this factor.
By default, we don't do any variable scaling and rely on the MIP model to
specify continuous variable domain with the wanted precision.

optional double mip_var_scaling = 125 [default = 1];

Returns

The mipVarScaling.

Implemented in SatParameters.Builder, and SatParameters.

getMipWantedPrecision()

double getMipWantedPrecision

(

)

When scaling constraint with double coefficients to integer coefficients,
we will multiply by a power of 2 and round the coefficients. We will choose
the lowest power such that we have no potential overflow and the worst case
constraint activity error do not exceed this threshold relative to the
constraint bounds.
We also use this to decide by how much we relax the constraint bounds so
that we can have a feasible integer solution of constraints involving
continuous variable. This is required for instance when you have an == rhs
constraint as in many situation you cannot have a perfect equality with
integer variables and coefficients.

optional double mip_wanted_precision = 126 [default = 1e-06];

Returns

The mipWantedPrecision.

Implemented in SatParameters.Builder, and SatParameters.

getName()

java.lang.String getName

(

)

In some context, like in a portfolio of search, it makes sense to name a
given parameters set for logging purpose.

optional string name = 171 [default = ""];

Returns

The name.

Implemented in SatParameters.Builder, and SatParameters.

getNameBytes()

com.google.protobuf.ByteString getNameBytes

(

)

In some context, like in a portfolio of search, it makes sense to name a
given parameters set for logging purpose.

optional string name = 171 [default = ""];

Returns

The bytes for name.

Implemented in SatParameters.Builder, and SatParameters.

getNewConstraintsBatchSize()

int getNewConstraintsBatchSize

(

)

Add that many lazy constraints (or cuts) at once in the LP. Note that at
the beginning of the solve, we do add more than this.

optional int32 new_constraints_batch_size = 122 [default = 50];

Returns

The newConstraintsBatchSize.

Implemented in SatParameters.Builder, and SatParameters.

getNumConflictsBeforeStrategyChanges()

int getNumConflictsBeforeStrategyChanges

(

)

After each restart, if the number of conflict since the last strategy
change is greater that this, then we increment a "strategy_counter" that
can be use to change the search strategy used by the following restarts.

optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];

Returns

The numConflictsBeforeStrategyChanges.

Implemented in SatParameters.Builder, and SatParameters.

getNumSearchWorkers()

int getNumSearchWorkers

(

)

Specify the number of parallel workers to use during search.
A number <= 1 means no parallelism.
As of 2020-04-10, if you're using SAT via MPSolver (to solve integer
programs) this field is overridden with a value of 8, if the field is not
set *explicitly*. Thus, always set this field explicitly or via
MPSolver::SetNumThreads().

optional int32 num_search_workers = 100 [default = 1];

Returns

The numSearchWorkers.

Implemented in SatParameters.Builder, and SatParameters.

getOnlyAddCutsAtLevelZero()

boolean getOnlyAddCutsAtLevelZero

(

)

For the cut that can be generated at any level, this control if we only
try to generate them at the root node.

optional bool only_add_cuts_at_level_zero = 92 [default = false];

Returns

The onlyAddCutsAtLevelZero.

Implemented in SatParameters.Builder, and SatParameters.

getOptimizeWithCore()

boolean getOptimizeWithCore

(

)

The default optimization method is a simple "linear scan", each time trying
to find a better solution than the previous one. If this is true, then we
use a core-based approach (like in max-SAT) when we try to increase the
lower bound instead.

optional bool optimize_with_core = 83 [default = false];

Returns

The optimizeWithCore.

Implemented in SatParameters.Builder, and SatParameters.

getOptimizeWithMaxHs()

boolean getOptimizeWithMaxHs

(

)

This has no effect if optimize_with_core is false. If true, use a different
core-based algorithm similar to the max-HS algo for max-SAT. This is a
hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT
one. This is also related to the PhD work of tobyodavies@
"Automatic Logic-Based Benders Decomposition with MiniZinc"
http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489

optional bool optimize_with_max_hs = 85 [default = false];

Returns

The optimizeWithMaxHs.

Implemented in SatParameters.Builder, and SatParameters.

getPbCleanupIncrement()

int getPbCleanupIncrement

(

)

Same as for the clauses, but for the learned pseudo-Boolean constraints.

optional int32 pb_cleanup_increment = 46 [default = 200];

Returns

The pbCleanupIncrement.

Implemented in SatParameters.Builder, and SatParameters.

getPbCleanupRatio()

double getPbCleanupRatio

(

)

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns

The pbCleanupRatio.

Implemented in SatParameters.Builder, and SatParameters.

getPermutePresolveConstraintOrder()

boolean getPermutePresolveConstraintOrder

(

)

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns

The permutePresolveConstraintOrder.

Implemented in SatParameters.Builder, and SatParameters.

getPermuteVariableRandomly()

boolean getPermuteVariableRandomly

(

)

This is mainly here to test the solver variability. Note that in tests, if
not explicitly set to false, all 3 options will be set to true so that
clients do not rely on the solver returning a specific solution if they are
many equivalent optimal solutions.

optional bool permute_variable_randomly = 178 [default = false];

Returns

The permuteVariableRandomly.

Implemented in SatParameters.Builder, and SatParameters.

getPolarityRephaseIncrement()

int getPolarityRephaseIncrement

(

)

If non-zero, then we change the polarity heuristic after that many number
of conflicts in an arithmetically increasing fashion. So x the first time,
2 * x the second time, etc...

optional int32 polarity_rephase_increment = 168 [default = 1000];

Returns

The polarityRephaseIncrement.

Implemented in SatParameters.Builder, and SatParameters.

getPolishLpSolution()

boolean getPolishLpSolution

(

)

Whether we try to do a few degenerate iteration at the end of an LP solve
to minimize the fractionality of the integer variable in the basis. This
helps on some problems, but not so much on others. It also cost of bit of
time to do such polish step.

optional bool polish_lp_solution = 175 [default = false];

Returns

The polishLpSolution.

Implemented in SatParameters.Builder, and SatParameters.

getPreferredVariableOrder()

com.google.ortools.sat.SatParameters.VariableOrder getPreferredVariableOrder

(

)

optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];

Returns

The preferredVariableOrder.

Implemented in SatParameters.Builder, and SatParameters.

getPresolveBlockedClause()

boolean getPresolveBlockedClause

(

)

Whether we use an heuristic to detect some basic case of blocked clause
in the SAT presolve.

optional bool presolve_blocked_clause = 88 [default = true];

Returns

The presolveBlockedClause.

Implemented in SatParameters.Builder, and SatParameters.

getPresolveBvaThreshold()

int getPresolveBvaThreshold

(

)

Apply Bounded Variable Addition (BVA) if the number of clauses is reduced
by stricly more than this threshold. The algorithm described in the paper
uses 0, but quick experiments showed that 1 is a good value. It may not be
worth it to add a new variable just to remove one clause.

optional int32 presolve_bva_threshold = 73 [default = 1];

Returns

The presolveBvaThreshold.

Implemented in SatParameters.Builder, and SatParameters.

getPresolveBveClauseWeight()

int getPresolveBveClauseWeight

(

)

During presolve, we apply BVE only if this weight times the number of
clauses plus the number of clause literals is not increased.

optional int32 presolve_bve_clause_weight = 55 [default = 3];

Returns

The presolveBveClauseWeight.

Implemented in SatParameters.Builder, and SatParameters.

getPresolveBveThreshold()

int getPresolveBveThreshold

(

)

During presolve, only try to perform the bounded variable elimination (BVE)
of a variable x if the number of occurrences of x times the number of
occurrences of not(x) is not greater than this parameter.

optional int32 presolve_bve_threshold = 54 [default = 500];

Returns

The presolveBveThreshold.

Implemented in SatParameters.Builder, and SatParameters.

getPresolveExtractIntegerEnforcement()

boolean getPresolveExtractIntegerEnforcement

(

)

If true, we will extract from linear constraints, enforcement literals of
the form "integer variable at bound => simplified constraint". This should
always be beneficial except that we don't always handle them as efficiently
as we could for now. This causes problem on manna81.mps (LP relaxation not
as tight it seems) and on neos-3354841-apure.mps.gz (too many literals
created this way).

optional bool presolve_extract_integer_enforcement = 174 [default = false];

Returns

The presolveExtractIntegerEnforcement.

Implemented in SatParameters.Builder, and SatParameters.

getPresolveProbingDeterministicTimeLimit()

double getPresolveProbingDeterministicTimeLimit

(

)

The maximum "deterministic" time limit to spend in probing. A value of
zero will disable the probing.

optional double presolve_probing_deterministic_time_limit = 57 [default = 30];

Returns

The presolveProbingDeterministicTimeLimit.

Implemented in SatParameters.Builder, and SatParameters.

getPresolveSubstitutionLevel()

int getPresolveSubstitutionLevel

(

)

How much substitution (also called free variable aggregation in MIP
litterature) should we perform at presolve. This currently only concerns
variable appearing only in linear constraints. For now the value 0 turns it
off and any positive value performs substitution.

optional int32 presolve_substitution_level = 147 [default = 1];

Returns

The presolveSubstitutionLevel.

Implemented in SatParameters.Builder, and SatParameters.

getPresolveUseBva()

boolean getPresolveUseBva

(

)

Whether or not we use Bounded Variable Addition (BVA) in the presolve.

optional bool presolve_use_bva = 72 [default = true];

Returns

The presolveUseBva.

Implemented in SatParameters.Builder, and SatParameters.

getProbingPeriodAtRoot()

long getProbingPeriodAtRoot

(

)

If set at zero (the default), it is disabled. Otherwise the solver attempts
probing at every 'probing_period' root node. Period of 1 enables probing at
every root node.

optional int64 probing_period_at_root = 142 [default = 0];

Returns

The probingPeriodAtRoot.

Implemented in SatParameters.Builder, and SatParameters.

getPseudoCostReliabilityThreshold()

long getPseudoCostReliabilityThreshold

(

)

The solver ignores the pseudo costs of variables with number of recordings
less than this threshold.

optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];

Returns

The pseudoCostReliabilityThreshold.

Implemented in SatParameters.Builder, and SatParameters.

getRandomBranchesRatio()

double getRandomBranchesRatio

(

)

A number between 0 and 1 that indicates the proportion of branching
variables that are selected randomly instead of choosing the first variable
from the given variable_ordering strategy.

optional double random_branches_ratio = 32 [default = 0];

Returns

The randomBranchesRatio.

Implemented in SatParameters.Builder, and SatParameters.

getRandomizeSearch()

boolean getRandomizeSearch

(

)

Randomize fixed search.

optional bool randomize_search = 103 [default = false];

Returns

The randomizeSearch.

Implemented in SatParameters.Builder, and SatParameters.

getRandomPolarityRatio()

double getRandomPolarityRatio

(

)

The proportion of polarity chosen at random. Note that this take
precedence over the phase saving heuristic. This is different from
initial_polarity:POLARITY_RANDOM because it will select a new random
polarity each time the variable is branched upon instead of selecting one
initially and then always taking this choice.

optional double random_polarity_ratio = 45 [default = 0];

Returns

The randomPolarityRatio.

Implemented in SatParameters.Builder, and SatParameters.

getRandomSeed()

int getRandomSeed

(

)

At the beginning of each solve, the random number generator used in some
part of the solver is reinitialized to this seed. If you change the random
seed, the solver may make different choices during the solving process.
For some problems, the running time may vary a lot depending on small
change in the solving algorithm. Running the solver with different seeds
enables to have more robust benchmarks when evaluating new features.

optional int32 random_seed = 31 [default = 1];

Returns

The randomSeed.

Implemented in SatParameters.Builder, and SatParameters.

getReduceMemoryUsageInInterleaveMode()

boolean getReduceMemoryUsageInInterleaveMode

(

)

Temporary parameter until the memory usage is more optimized.

optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];

Returns

The reduceMemoryUsageInInterleaveMode.

Implemented in SatParameters.Builder, and SatParameters.

getRelativeGapLimit()

double getRelativeGapLimit

(

)

optional double relative_gap_limit = 160 [default = 0];

Returns

The relativeGapLimit.

Implemented in SatParameters.Builder, and SatParameters.

getRepairHint()

boolean getRepairHint

(

)

If true, the solver tries to repair the solution given in the hint. This
search terminates after the 'hint_conflict_limit' is reached and the solver
switches to regular search. If false, then  we do a FIXED_SEARCH using the
hint until the hint_conflict_limit is reached.

optional bool repair_hint = 167 [default = false];

Returns

The repairHint.

Implemented in SatParameters.Builder, and SatParameters.

getRestartAlgorithms()

com.google.ortools.sat.SatParameters.RestartAlgorithm getRestartAlgorithms

(

int

index

)

The restart strategies will change each time the strategy_counter is
increased. The current strategy will simply be the one at index
strategy_counter modulo the number of strategy. Note that if this list
includes a NO_RESTART, nothing will change when it is reached because the
strategy_counter will only increment after a restart.
The idea of switching of search strategy tailored for SAT/UNSAT comes from
Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/.
But more generally, it seems REALLY beneficial to try different strategy.

repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;

Parameters

index

The index of the element to return.

Returns

The restartAlgorithms at the given index.

Implemented in SatParameters.Builder, and SatParameters.

getRestartAlgorithmsCount()

int getRestartAlgorithmsCount

(

)

The restart strategies will change each time the strategy_counter is
increased. The current strategy will simply be the one at index
strategy_counter modulo the number of strategy. Note that if this list
includes a NO_RESTART, nothing will change when it is reached because the
strategy_counter will only increment after a restart.
The idea of switching of search strategy tailored for SAT/UNSAT comes from
Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/.
But more generally, it seems REALLY beneficial to try different strategy.

repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;

Returns

The count of restartAlgorithms.

Implemented in SatParameters.Builder, and SatParameters.

getRestartAlgorithmsList()

java.util.List<com.google.ortools.sat.SatParameters.RestartAlgorithm> getRestartAlgorithmsList

(

)

The restart strategies will change each time the strategy_counter is
increased. The current strategy will simply be the one at index
strategy_counter modulo the number of strategy. Note that if this list
includes a NO_RESTART, nothing will change when it is reached because the
strategy_counter will only increment after a restart.
The idea of switching of search strategy tailored for SAT/UNSAT comes from
Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/.
But more generally, it seems REALLY beneficial to try different strategy.

repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;

Returns

A list containing the restartAlgorithms.

Implemented in SatParameters.Builder, and SatParameters.

getRestartDlAverageRatio()

double getRestartDlAverageRatio

(

)

In the moving average restart algorithms, a restart is triggered if the
window average times this ratio is greater that the global average.

optional double restart_dl_average_ratio = 63 [default = 1];

Returns

The restartDlAverageRatio.

Implemented in SatParameters.Builder, and SatParameters.

getRestartLbdAverageRatio()

double getRestartLbdAverageRatio

(

)

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns

The restartLbdAverageRatio.

Implemented in SatParameters.Builder, and SatParameters.

getRestartPeriod()

int getRestartPeriod

(

)

Restart period for the FIXED_RESTART strategy. This is also the multiplier
used by the LUBY_RESTART strategy.

optional int32 restart_period = 30 [default = 50];

Returns

The restartPeriod.

Implemented in SatParameters.Builder, and SatParameters.

getRestartRunningWindowSize()

int getRestartRunningWindowSize

(

)

Size of the window for the moving average restarts.

optional int32 restart_running_window_size = 62 [default = 50];

Returns

The restartRunningWindowSize.

Implemented in SatParameters.Builder, and SatParameters.

getSearchBranching()

com.google.ortools.sat.SatParameters.SearchBranching getSearchBranching

(

)

optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];

Returns

The searchBranching.

Implemented in SatParameters.Builder, and SatParameters.

getSearchRandomizationTolerance()

long getSearchRandomizationTolerance

(

)

Search randomization will collect equivalent 'max valued' variables, and
pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST,
all unassigned variables are equivalent. If the variable strategy is
CHOOSE_LOWEST_MIN, and `lm` is the current lowest min of all unassigned
variables, then the set of max valued variables will be all unassigned
variables where
   lm <= variable min <= lm + search_randomization_tolerance

optional int64 search_randomization_tolerance = 104 [default = 0];

Returns

The searchRandomizationTolerance.

Implemented in SatParameters.Builder, and SatParameters.

getShareLevelZeroBounds()

boolean getShareLevelZeroBounds

(

)

Allows sharing of the bounds of modified variables at level 0.

optional bool share_level_zero_bounds = 114 [default = true];

Returns

The shareLevelZeroBounds.

Implemented in SatParameters.Builder, and SatParameters.

getShareObjectiveBounds()

boolean getShareObjectiveBounds

(

)

Allows objective sharing between workers.

optional bool share_objective_bounds = 113 [default = true];

Returns

The shareObjectiveBounds.

Implemented in SatParameters.Builder, and SatParameters.

getStopAfterFirstSolution()

boolean getStopAfterFirstSolution

(

)

For an optimization problem, stop the solver as soon as we have a solution.

optional bool stop_after_first_solution = 98 [default = false];

Returns

The stopAfterFirstSolution.

Implemented in SatParameters.Builder, and SatParameters.

getStopAfterPresolve()

boolean getStopAfterPresolve

(

)

Mainly used when improving the presolver. When true, stops the solver after
the presolve is complete.

optional bool stop_after_presolve = 149 [default = false];

Returns

The stopAfterPresolve.

Implemented in SatParameters.Builder, and SatParameters.

getStrategyChangeIncreaseRatio()

double getStrategyChangeIncreaseRatio

(

)

The parameter num_conflicts_before_strategy_changes is increased by that
much after each strategy change.

optional double strategy_change_increase_ratio = 69 [default = 0];

Returns

The strategyChangeIncreaseRatio.

Implemented in SatParameters.Builder, and SatParameters.

getSubsumptionDuringConflictAnalysis()

boolean getSubsumptionDuringConflictAnalysis

(

)

At a really low cost, during the 1-UIP conflict computation, it is easy to
detect if some of the involved reasons are subsumed by the current
conflict. When this is true, such clauses are detached and later removed
from the problem.

optional bool subsumption_during_conflict_analysis = 56 [default = true];

Returns

The subsumptionDuringConflictAnalysis.

Implemented in SatParameters.Builder, and SatParameters.

getSymmetryLevel()

int getSymmetryLevel

(

)

Whether we try to automatically detect the symmetries in a model and
exploit them. Currently, at level 1 we detect them in presolve and try
to fix Booleans. At level 2, we also do some form of dynamic symmetry
breaking during search.

optional int32 symmetry_level = 183 [default = 2];

Returns

The symmetryLevel.

Implemented in SatParameters.Builder, and SatParameters.

getTreatBinaryClausesSeparately()

boolean getTreatBinaryClausesSeparately

(

)

If true, the binary clauses are treated separately from the others. This
should be faster and uses less memory. However it changes the propagation
order.

optional bool treat_binary_clauses_separately = 33 [default = true];

Returns

The treatBinaryClausesSeparately.

Implemented in SatParameters.Builder, and SatParameters.

getUseAbslRandom()

boolean getUseAbslRandom

(

)

optional bool use_absl_random = 180 [default = false];

Returns

The useAbslRandom.

Implemented in SatParameters.Builder, and SatParameters.

getUseBlockingRestart()

boolean getUseBlockingRestart

(

)

Block a moving restart algorithm if the trail size of the current conflict
is greater than the multiplier times the moving average of the trail size
at the previous conflicts.

optional bool use_blocking_restart = 64 [default = false];

Returns

The useBlockingRestart.

Implemented in SatParameters.Builder, and SatParameters.

getUseBranchingInLp()

boolean getUseBranchingInLp

(

)

If true, the solver attemts to generate more info inside lp propagator by
branching on some variables if certain criteria are met during the search
tree exploration.

optional bool use_branching_in_lp = 139 [default = false];

Returns

The useBranchingInLp.

Implemented in SatParameters.Builder, and SatParameters.

getUseCombinedNoOverlap()

boolean getUseCombinedNoOverlap

(

)

This can be beneficial if there is a lot of no-overlap constraints but a
relatively low number of different intervals in the problem. Like 1000
intervals, but 1M intervals in the no-overlap constraints covering them.

optional bool use_combined_no_overlap = 133 [default = false];

Returns

The useCombinedNoOverlap.

Implemented in SatParameters.Builder, and SatParameters.

getUseDisjunctiveConstraintInCumulativeConstraint()

boolean getUseDisjunctiveConstraintInCumulativeConstraint

(

)

When this is true, the cumulative constraint is reinforced with propagators
from the disjunctive constraint to improve the inference on a set of tasks
that are disjunctive at the root of the problem. This additional level
supplements the default level of reasoning.
Propagators of the cumulative constraint will not be used at all if all the
tasks are disjunctive at root node.
This always result in better propagation, but it is usually slow, so
depending on the problem, turning this off may lead to a faster solution.

optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];

Returns

The useDisjunctiveConstraintInCumulativeConstraint.

Implemented in SatParameters.Builder, and SatParameters.

getUseErwaHeuristic()

boolean getUseErwaHeuristic

(

)

Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as
described in "Learning Rate Based Branching Heuristic for SAT solvers",
J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.

optional bool use_erwa_heuristic = 75 [default = false];

Returns

The useErwaHeuristic.

Implemented in SatParameters.Builder, and SatParameters.

getUseExactLpReason()

boolean getUseExactLpReason

(

)

The solver usually exploit the LP relaxation of a model. If this option is
true, then whatever is infered by the LP will be used like an heuristic to
compute EXACT propagation on the IP. So with this option, there is no
numerical imprecision issues.

optional bool use_exact_lp_reason = 109 [default = true];

Returns

The useExactLpReason.

Implemented in SatParameters.Builder, and SatParameters.

getUseFeasibilityPump()

boolean getUseFeasibilityPump

(

)

Adds a feasibility pump subsolver along with lns subsolvers.

optional bool use_feasibility_pump = 164 [default = true];

Returns

The useFeasibilityPump.

Implemented in SatParameters.Builder, and SatParameters.

getUseImpliedBounds()

boolean getUseImpliedBounds

(

)

Stores and exploits "implied-bounds" in the solver. That is, relations of
the form literal => (var >= bound). This is currently used to derive
stronger cuts.

optional bool use_implied_bounds = 144 [default = true];

Returns

The useImpliedBounds.

Implemented in SatParameters.Builder, and SatParameters.

getUseLnsOnly()

boolean getUseLnsOnly

(

)

LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns

The useLnsOnly.

Implemented in SatParameters.Builder, and SatParameters.

getUseOptimizationHints()

boolean getUseOptimizationHints

(

)

For an optimization problem, whether we follow some hints in order to find
a better first solution. For a variable with hint, the solver will always
try to follow the hint. It will revert to the variable_branching default
otherwise.

optional bool use_optimization_hints = 35 [default = true];

Returns

The useOptimizationHints.

Implemented in SatParameters.Builder, and SatParameters.

getUseOptionalVariables()

boolean getUseOptionalVariables

(

)

If true, we automatically detect variables whose constraint are always
enforced by the same literal and we mark them as optional. This allows
to propagate them as if they were present in some situation.

optional bool use_optional_variables = 108 [default = true];

Returns

The useOptionalVariables.

Implemented in SatParameters.Builder, and SatParameters.

getUseOverloadCheckerInCumulativeConstraint()

boolean getUseOverloadCheckerInCumulativeConstraint

(

)

When this is true, the cumulative constraint is reinforced with overload
checking, i.e., an additional level of reasoning based on energy. This
additional level supplements the default level of reasoning as well as
timetable edge finding.
This always result in better propagation, but it is usually slow, so
depending on the problem, turning this off may lead to a faster solution.

optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];

Returns

The useOverloadCheckerInCumulativeConstraint.

Implemented in SatParameters.Builder, and SatParameters.

getUsePbResolution()

boolean getUsePbResolution

(

)

Whether to use pseudo-Boolean resolution to analyze a conflict. Note that
this option only make sense if your problem is modelized using
pseudo-Boolean constraints. If you only have clauses, this shouldn't change
anything (except slow the solver down).

optional bool use_pb_resolution = 43 [default = false];

Returns

The usePbResolution.

Implemented in SatParameters.Builder, and SatParameters.

getUsePhaseSaving()

boolean getUsePhaseSaving

(

)

If this is true, then the polarity of a variable will be the last value it
was assigned to, or its default polarity if it was never assigned since the
call to ResetDecisionHeuristic().
Actually, we use a newer version where we follow the last value in the
longest non-conflicting partial assignment in the current phase.
This is called 'literal phase saving'. For details see 'A Lightweight
Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and
A.Darwiche, In 10th International Conference on Theory and Applications of
Satisfiability Testing, 2007.

optional bool use_phase_saving = 44 [default = true];

Returns

The usePhaseSaving.

Implemented in SatParameters.Builder, and SatParameters.

getUsePrecedencesInDisjunctiveConstraint()

boolean getUsePrecedencesInDisjunctiveConstraint

(

)

When this is true, then a disjunctive constraint will try to use the
precedence relations between time intervals to propagate their bounds
further. For instance if task A and B are both before C and task A and B
are in disjunction, then we can deduce that task C must start after
duration(A) + duration(B) instead of simply max(duration(A), duration(B)),
provided that the start time for all task was currently zero.
This always result in better propagation, but it is usually slow, so
depending on the problem, turning this off may lead to a faster solution.

optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];

Returns

The usePrecedencesInDisjunctiveConstraint.

Implemented in SatParameters.Builder, and SatParameters.

getUseProbingSearch()

boolean getUseProbingSearch

(

)

If true, search will continuously probe Boolean variables, and integer
variable bounds.

optional bool use_probing_search = 176 [default = false];

Returns

The useProbingSearch.

Implemented in SatParameters.Builder, and SatParameters.

getUseRelaxationLns()

boolean getUseRelaxationLns

(

)

Turns on a lns worker which solves relaxed version of the original problem
by removing constraints from the problem in order to get better bounds.

optional bool use_relaxation_lns = 150 [default = false];

Returns

The useRelaxationLns.

Implemented in SatParameters.Builder, and SatParameters.

getUseRinsLns()

boolean getUseRinsLns

(

)

Turns on relaxation induced neighborhood generator.

optional bool use_rins_lns = 129 [default = true];

Returns

The useRinsLns.

Implemented in SatParameters.Builder, and SatParameters.

getUseSatInprocessing()

boolean getUseSatInprocessing

(

)

optional bool use_sat_inprocessing = 163 [default = false];

Returns

The useSatInprocessing.

Implemented in SatParameters.Builder, and SatParameters.

getUseTimetableEdgeFindingInCumulativeConstraint()

boolean getUseTimetableEdgeFindingInCumulativeConstraint

(

)

When this is true, the cumulative constraint is reinforced with timetable
edge finding, i.e., an additional level of reasoning based on the
conjunction of energy and mandatory parts. This additional level
supplements the default level of reasoning as well as overload_checker.
This always result in better propagation, but it is usually slow, so
depending on the problem, turning this off may lead to a faster solution.

optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];

Returns

The useTimetableEdgeFindingInCumulativeConstraint.

Implemented in SatParameters.Builder, and SatParameters.

getVariableActivityDecay()

double getVariableActivityDecay

(

)

Each time a conflict is found, the activities of some variables are
increased by one. Then, the activity of all variables are multiplied by
variable_activity_decay.
To implement this efficiently, the activity of all the variables is not
decayed at each conflict. Instead, the activity increment is multiplied by
1 / decay. When an activity reach max_variable_activity_value, all the
activity are multiplied by 1 / max_variable_activity_value.

optional double variable_activity_decay = 15 [default = 0.8];

Returns

The variableActivityDecay.

Implemented in SatParameters.Builder, and SatParameters.

hasAbsoluteGapLimit()

boolean hasAbsoluteGapLimit

(

)

Stop the search when the gap between the best feasible objective (O) and
our best objective bound (B) is smaller than a limit.
The exact definition is:

Absolute: abs(O - B)
Relative: abs(O - B) / max(1, abs(O)).
Important: The relative gap depends on the objective offset! If you
artificially shift the objective, you will get widely different value of
the relative gap.
Note that if the gap is reached, the search status will be OPTIMAL. But
one can check the best objective bound to see the actual gap.

optional double absolute_gap_limit = 159 [default = 0];
Returns
Whether the absoluteGapLimit field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAddCgCuts()

boolean hasAddCgCuts

(

)

Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
Note that for now, this is not heavily tuned.

optional bool add_cg_cuts = 117 [default = true];

Returns

Whether the addCgCuts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAddCliqueCuts()

boolean hasAddCliqueCuts

(

)

Whether we generate clique cuts from the binary implication graph. Note
that as the search goes on, this graph will contains new binary clauses
learned by the SAT engine.

optional bool add_clique_cuts = 172 [default = true];

Returns

Whether the addCliqueCuts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAddKnapsackCuts()

boolean hasAddKnapsackCuts

(

)

Whether we generate knapsack cuts. Note that in our setting where all
variables are integer and bounded on both side, such a cut could be applied
to any constraint.

optional bool add_knapsack_cuts = 111 [default = false];

Returns

Whether the addKnapsackCuts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAddLinMaxCuts()

boolean hasAddLinMaxCuts

(

)

For the lin max constraints, generates the cuts described in "Strong
mixed-integer programming formulations for trained neural networks" by Ross
Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)

optional bool add_lin_max_cuts = 152 [default = true];

Returns

Whether the addLinMaxCuts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAddLpConstraintsLazily()

boolean hasAddLpConstraintsLazily

(

)

If true, we start by an empty LP, and only add constraints not satisfied
by the current LP solution batch by batch. A constraint that is only added
like this is known as a "lazy" constraint in the literature, except that we
currently consider all constraints as lazy here.

optional bool add_lp_constraints_lazily = 112 [default = true];

Returns

Whether the addLpConstraintsLazily field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAddMirCuts()

boolean hasAddMirCuts

(

)

Whether we generate MIR cuts at root node.
Note that for now, this is not heavily tuned.

optional bool add_mir_cuts = 120 [default = true];

Returns

Whether the addMirCuts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAddZeroHalfCuts()

boolean hasAddZeroHalfCuts

(

)

Whether we generate Zero-Half cuts at root node.
Note that for now, this is not heavily tuned.

optional bool add_zero_half_cuts = 169 [default = true];

Returns

Whether the addZeroHalfCuts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAlsoBumpVariablesInConflictReasons()

boolean hasAlsoBumpVariablesInConflictReasons

(

)

When this is true, then the variables that appear in any of the reason of
the variables in a conflict have their activity bumped. This is addition to
the variables in the conflict, and the one that were used during conflict
resolution.

optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];

Returns

Whether the alsoBumpVariablesInConflictReasons field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasAutoDetectGreaterThanAtLeastOneOf()

boolean hasAutoDetectGreaterThanAtLeastOneOf

(

)

If true, then the precedences propagator try to detect for each variable if
it has a set of "optional incoming arc" for which at least one of them is
present. This is usually useful to have but can be slow on model with a lot
of precedence.

optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];

Returns

Whether the autoDetectGreaterThanAtLeastOneOf field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasBinaryMinimizationAlgorithm()

boolean hasBinaryMinimizationAlgorithm

(

)

optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];

Returns

Whether the binaryMinimizationAlgorithm field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasBinarySearchNumConflicts()

boolean hasBinarySearchNumConflicts

(

)

If non-negative, perform a binary search on the objective variable in order
to find an [min, max] interval outside of which the solver proved unsat/sat
under this amount of conflict. This can quickly reduce the objective domain
on some problems.

optional int32 binary_search_num_conflicts = 99 [default = -1];

Returns

Whether the binarySearchNumConflicts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasBlockingRestartMultiplier()

boolean hasBlockingRestartMultiplier

(

)

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns

Whether the blockingRestartMultiplier field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasBlockingRestartWindowSize()

boolean hasBlockingRestartWindowSize

(

)

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns

Whether the blockingRestartWindowSize field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasBooleanEncodingLevel()

boolean hasBooleanEncodingLevel

(

)

A non-negative level indicating how much we should try to fully encode
Integer variables as Boolean.

optional int32 boolean_encoding_level = 107 [default = 1];

Returns

Whether the booleanEncodingLevel field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCatchSigintSignal()

boolean hasCatchSigintSignal

(

)

Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals
when calling solve. If set, catching the SIGINT signal will terminate the
search gracefully, as if a time limit was reached.

optional bool catch_sigint_signal = 135 [default = true];

Returns

Whether the catchSigintSignal field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasClauseActivityDecay()

boolean hasClauseActivityDecay

(

)

Clause activity parameters (same effect as the one on the variables).

optional double clause_activity_decay = 17 [default = 0.999];

Returns

Whether the clauseActivityDecay field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasClauseCleanupLbdBound()

boolean hasClauseCleanupLbdBound

(

)

All the clauses with a LBD (literal blocks distance) lower or equal to this
parameters will always be kept.

optional int32 clause_cleanup_lbd_bound = 59 [default = 5];

Returns

Whether the clauseCleanupLbdBound field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasClauseCleanupOrdering()

boolean hasClauseCleanupOrdering

(

)

optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];

Returns

Whether the clauseCleanupOrdering field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasClauseCleanupPeriod()

boolean hasClauseCleanupPeriod

(

)

Trigger a cleanup when this number of "deletable" clauses is learned.

optional int32 clause_cleanup_period = 11 [default = 10000];

Returns

Whether the clauseCleanupPeriod field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasClauseCleanupProtection()

boolean hasClauseCleanupProtection

(

)

optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];

Returns

Whether the clauseCleanupProtection field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasClauseCleanupTarget()

boolean hasClauseCleanupTarget

(

)

During a cleanup, we will always keep that number of "deletable" clauses.
Note that this doesn't include the "protected" clauses.

optional int32 clause_cleanup_target = 13 [default = 10000];

Returns

Whether the clauseCleanupTarget field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasConvertIntervals()

boolean hasConvertIntervals

(

)

Temporary flag util the feature is more mature. This convert intervals to
the newer proto format that support affine start/var/end instead of just
variables. It changes a bit the search and is not always better currently.

optional bool convert_intervals = 177 [default = false];

Returns

Whether the convertIntervals field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCountAssumptionLevelsInLbd()

boolean hasCountAssumptionLevelsInLbd

(

)

Whether or not the assumption levels are taken into account during the LBD
computation. According to the reference below, not counting them improves
the solver in some situation. Note that this only impact solves under
assumptions.
Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for
Incremental SAT Solving with Assumptions: Application to MUS Extraction"
Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes
in Computer Science Volume 7962, 2013, pp 309-317.

optional bool count_assumption_levels_in_lbd = 49 [default = true];

Returns

Whether the countAssumptionLevelsInLbd field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCoverOptimization()

boolean hasCoverOptimization

(

)

If true, when the max-sat algo find a core, we compute the minimal number
of literals in the core that needs to be true to have a feasible solution.

optional bool cover_optimization = 89 [default = true];

Returns

Whether the coverOptimization field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCpModelMaxNumPresolveOperations()

boolean hasCpModelMaxNumPresolveOperations

(

)

If positive, try to stop just after that many presolve rules have been
applied. This is mainly useful for debugging presolve.

optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];

Returns

Whether the cpModelMaxNumPresolveOperations field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCpModelPostsolveWithFullSolver()

boolean hasCpModelPostsolveWithFullSolver

(

)

Advanced usage. We have two different postsolve code. The default one
should be better and it allows for a more powerful presolve, but some
rarely used features like not fully assigning all variables require the
other one.

optional bool cp_model_postsolve_with_full_solver = 162 [default = false];

Returns

Whether the cpModelPostsolveWithFullSolver field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCpModelPresolve()

boolean hasCpModelPresolve

(

)

Whether we presolve the cp_model before solving it.

optional bool cp_model_presolve = 86 [default = true];

Returns

Whether the cpModelPresolve field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCpModelProbingLevel()

boolean hasCpModelProbingLevel

(

)

How much effort do we spend on probing. 0 disables it completely.

optional int32 cp_model_probing_level = 110 [default = 2];

Returns

Whether the cpModelProbingLevel field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCpModelUseSatPresolve()

boolean hasCpModelUseSatPresolve

(

)

Whether we also use the sat presolve when cp_model_presolve is true.

optional bool cp_model_use_sat_presolve = 93 [default = true];

Returns

Whether the cpModelUseSatPresolve field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCutActiveCountDecay()

boolean hasCutActiveCountDecay

(

)

optional double cut_active_count_decay = 156 [default = 0.8];

Returns

Whether the cutActiveCountDecay field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCutCleanupTarget()

boolean hasCutCleanupTarget

(

)

Target number of constraints to remove during cleanup.

optional int32 cut_cleanup_target = 157 [default = 1000];

Returns

Whether the cutCleanupTarget field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasCutMaxActiveCountValue()

boolean hasCutMaxActiveCountValue

(

)

These parameters are similar to sat clause management activity parameters.
They are effective only if the number of generated cuts exceed the storage
limit. Default values are based on a few experiments on miplib instances.

optional double cut_max_active_count_value = 155 [default = 10000000000];

Returns

Whether the cutMaxActiveCountValue field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasDefaultRestartAlgorithms()

boolean hasDefaultRestartAlgorithms

(

)

optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];

Returns

Whether the defaultRestartAlgorithms field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasDisableConstraintExpansion()

boolean hasDisableConstraintExpansion

(

)

If true, it disable all constraint expansion.
This should only be used to test the presolve of expanded constraints.

optional bool disable_constraint_expansion = 181 [default = false];

Returns

Whether the disableConstraintExpansion field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasDiversifyLnsParams()

boolean hasDiversifyLnsParams

(

)

If true, registers more lns subsolvers with different parameters.

optional bool diversify_lns_params = 137 [default = false];

Returns

Whether the diversifyLnsParams field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasEnumerateAllSolutions()

boolean hasEnumerateAllSolutions

(

)

Whether we enumerate all solutions of a problem without objective. Note
that setting this to true automatically disable the presolve. This is
because the presolve rules only guarantee the existence of one feasible
solution to the presolved problem.
TODO(user): Do not disable the presolve and let the user choose what
behavior is best by setting keep_all_feasible_solutions_in_presolve.

optional bool enumerate_all_solutions = 87 [default = false];

Returns

Whether the enumerateAllSolutions field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExpandAlldiffConstraints()

boolean hasExpandAlldiffConstraints

(

)

If true, expand all_different constraints that are not permutations.
Permutations (#Variables = #Values) are always expanded.

optional bool expand_alldiff_constraints = 170 [default = false];

Returns

Whether the expandAlldiffConstraints field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExpandAutomatonConstraints()

boolean hasExpandAutomatonConstraints

(

)

If true, the automaton constraints are expanded.

optional bool expand_automaton_constraints = 143 [default = true];

Returns

Whether the expandAutomatonConstraints field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExpandElementConstraints()

boolean hasExpandElementConstraints

(

)

If true, the element constraints are expanded into many
linear constraints of the form (index == i) => (element[i] == target).

optional bool expand_element_constraints = 140 [default = true];

Returns

Whether the expandElementConstraints field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExpandReservoirConstraints()

boolean hasExpandReservoirConstraints

(

)

If true, expand the reservoir constraints by creating booleans for all
possible precedences between event and encoding the constraint.

optional bool expand_reservoir_constraints = 182 [default = true];

Returns

Whether the expandReservoirConstraints field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExpandTableConstraints()

boolean hasExpandTableConstraints

(

)

If true, the positive table constraints are expanded.
Note that currently, negative table constraints are always expanded.

optional bool expand_table_constraints = 158 [default = true];

Returns

Whether the expandTableConstraints field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExploitAllLpSolution()

boolean hasExploitAllLpSolution

(

)

If true and the Lp relaxation of the problem has a solution, try to exploit
it. This is same as above except in this case the lp solution might not be
an integer solution.

optional bool exploit_all_lp_solution = 116 [default = true];

Returns

Whether the exploitAllLpSolution field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExploitBestSolution()

boolean hasExploitBestSolution

(

)

When branching on a variable, follow the last best solution value.

optional bool exploit_best_solution = 130 [default = false];

Returns

Whether the exploitBestSolution field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExploitIntegerLpSolution()

boolean hasExploitIntegerLpSolution

(

)

If true and the Lp relaxation of the problem has an integer optimal
solution, try to exploit it. Note that since the LP relaxation may not
contain all the constraints, such a solution is not necessarily a solution
of the full problem.

optional bool exploit_integer_lp_solution = 94 [default = true];

Returns

Whether the exploitIntegerLpSolution field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExploitObjective()

boolean hasExploitObjective

(

)

When branching an a variable that directly affect the objective,
branch on the value that lead to the best objective first.

optional bool exploit_objective = 131 [default = true];

Returns

Whether the exploitObjective field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasExploitRelaxationSolution()

boolean hasExploitRelaxationSolution

(

)

When branching on a variable, follow the last best relaxation solution
value. We use the relaxation with the tightest bound on the objective as
the best relaxation solution.

optional bool exploit_relaxation_solution = 161 [default = false];

Returns

Whether the exploitRelaxationSolution field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasFillLogsInResponse()

boolean hasFillLogsInResponse

(

)

Whether logs should be stored in the response proto.

optional bool fill_logs_in_response = 185 [default = false];

Returns

Whether the fillLogsInResponse field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasFillTightenedDomainsInResponse()

boolean hasFillTightenedDomainsInResponse

(

)

If true, add information about the derived variable domains to the
CpSolverResponse. It is an option because it makes the response slighly
bigger and there is a bit more work involved during the postsolve to
construct it, but it should still have a low overhead. See the
tightened_variables field in CpSolverResponse for more details.

optional bool fill_tightened_domains_in_response = 132 [default = false];

Returns

Whether the fillTightenedDomainsInResponse field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasFindMultipleCores()

boolean hasFindMultipleCores

(

)

Whether we try to find more independent cores for a given set of
assumptions in the core based max-SAT algorithms.

optional bool find_multiple_cores = 84 [default = true];

Returns

Whether the findMultipleCores field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasFpRounding()

boolean hasFpRounding

(

)

optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];

Returns

Whether the fpRounding field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasGlucoseDecayIncrement()

boolean hasGlucoseDecayIncrement

(

)

optional double glucose_decay_increment = 23 [default = 0.01];

Returns

Whether the glucoseDecayIncrement field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasGlucoseDecayIncrementPeriod()

boolean hasGlucoseDecayIncrementPeriod

(

)

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns

Whether the glucoseDecayIncrementPeriod field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasGlucoseMaxDecay()

boolean hasGlucoseMaxDecay

(

)

The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until
0.95. This "hack" seems to work well and comes from:
Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013
http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136

optional double glucose_max_decay = 22 [default = 0.95];

Returns

Whether the glucoseMaxDecay field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasHintConflictLimit()

boolean hasHintConflictLimit

(

)

Conflict limit used in the phase that exploit the solution hint.

optional int32 hint_conflict_limit = 153 [default = 10];

Returns

Whether the hintConflictLimit field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasInitialPolarity()

boolean hasInitialPolarity

(

)

optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];

Returns

Whether the initialPolarity field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasInitialVariablesActivity()

boolean hasInitialVariablesActivity

(

)

The initial value of the variables activity. A non-zero value only make
sense when use_erwa_heuristic is true. Experiments with a value of 1e-2
together with the ERWA heuristic showed slighthly better result than simply
using zero. The idea is that when the "learning rate" of a variable becomes
lower than this value, then we prefer to branch on never explored before
variables. This is not in the ERWA paper.

optional double initial_variables_activity = 76 [default = 0];

Returns

Whether the initialVariablesActivity field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasInstantiateAllVariables()

boolean hasInstantiateAllVariables

(

)

If true, the solver will add a default integer branching strategy to the
already defined search strategy.

optional bool instantiate_all_variables = 106 [default = true];

Returns

Whether the instantiateAllVariables field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasInterleaveBatchSize()

boolean hasInterleaveBatchSize

(

)

optional int32 interleave_batch_size = 134 [default = 1];

Returns

Whether the interleaveBatchSize field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasInterleaveSearch()

boolean hasInterleaveSearch

(

)

Experimental. If this is true, then we interleave all our major search
strategy and distribute the work amongst num_search_workers.
The search is deterministic (independently of num_search_workers!), and we
schedule and wait for interleave_batch_size task to be completed before
synchronizing and scheduling the next batch of tasks.

optional bool interleave_search = 136 [default = false];

Returns

Whether the interleaveSearch field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasKeepAllFeasibleSolutionsInPresolve()

boolean hasKeepAllFeasibleSolutionsInPresolve

(

)

If true, we disable the presolve reductions that remove feasible solutions
from the search space. Such solution are usually dominated by a "better"
solution that is kept, but depending on the situation, we might want to
keep all solutions.
A trivial example is when a variable is unused. If this is true, then the
presolve will not fix it to an arbitrary value and it will stay in the
search space.

optional bool keep_all_feasible_solutions_in_presolve = 173 [default = false];

Returns

Whether the keepAllFeasibleSolutionsInPresolve field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasLinearizationLevel()

boolean hasLinearizationLevel

(

)

A non-negative level indicating the type of constraints we consider in the
LP relaxation. At level zero, no LP relaxation is used. At level 1, only
the linear constraint and full encoding are added. At level 2, we also add
all the Boolean constraints.

optional int32 linearization_level = 90 [default = 1];

Returns

Whether the linearizationLevel field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasLnsExpandIntervalsInConstraintGraph()

boolean hasLnsExpandIntervalsInConstraintGraph

(

)

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns

Whether the lnsExpandIntervalsInConstraintGraph field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasLnsFocusOnDecisionVariables()

boolean hasLnsFocusOnDecisionVariables

(

)

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns

Whether the lnsFocusOnDecisionVariables field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasLogSearchProgress()

boolean hasLogSearchProgress

(

)

Whether the solver should log the search progress to LOG(INFO).

optional bool log_search_progress = 41 [default = false];

Returns

Whether the logSearchProgress field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxAllDiffCutSize()

boolean hasMaxAllDiffCutSize

(

)

Cut generator for all diffs can add too many cuts for large all_diff
constraints. This parameter restricts the large all_diff constraints to
have a cut generator.

optional int32 max_all_diff_cut_size = 148 [default = 7];

Returns

Whether the maxAllDiffCutSize field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxClauseActivityValue()

boolean hasMaxClauseActivityValue

(

)

optional double max_clause_activity_value = 18 [default = 1e+20];

Returns

Whether the maxClauseActivityValue field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxConsecutiveInactiveCount()

boolean hasMaxConsecutiveInactiveCount

(

)

If a constraint/cut in LP is not active for that many consecutive OPTIMAL
solves, remove it from the LP. Note that it might be added again later if
it become violated by the current LP solution.

optional int32 max_consecutive_inactive_count = 121 [default = 100];

Returns

Whether the maxConsecutiveInactiveCount field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxCutRoundsAtLevelZero()

boolean hasMaxCutRoundsAtLevelZero

(

)

Max number of time we perform cut generation and resolve the LP at level 0.

optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];

Returns

Whether the maxCutRoundsAtLevelZero field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxDeterministicTime()

boolean hasMaxDeterministicTime

(

)

Maximum time allowed in deterministic time to solve a problem.
The deterministic time should be correlated with the real time used by the
solver, the time unit being as close as possible to a second.

optional double max_deterministic_time = 67 [default = inf];

Returns

Whether the maxDeterministicTime field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxIntegerRoundingScaling()

boolean hasMaxIntegerRoundingScaling

(

)

In the integer rounding procedure used for MIR and Gomory cut, the maximum
"scaling" we use (must be positive). The lower this is, the lower the
integer coefficients of the cut will be. Note that cut generated by lower
values are not necessarily worse than cut generated by larger value. There
is no strict dominance relationship.
Setting this to 2 result in the "strong fractional rouding" of Letchford
and Lodi.

optional int32 max_integer_rounding_scaling = 119 [default = 600];

Returns

Whether the maxIntegerRoundingScaling field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxMemoryInMb()

boolean hasMaxMemoryInMb

(

)

Maximum memory allowed for the whole thread containing the solver. The
solver will abort as soon as it detects that this limit is crossed. As a
result, this limit is approximative, but usually the solver will not go too
much over.

optional int64 max_memory_in_mb = 40 [default = 10000];

Returns

Whether the maxMemoryInMb field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxNumberOfConflicts()

boolean hasMaxNumberOfConflicts

(

)

Maximum number of conflicts allowed to solve a problem.
TODO(user,user): Maybe change the way the conflict limit is enforced?
currently it is enforced on each independent internal SAT solve, rather
than on the overall number of conflicts across all solves. So in the
context of an optimization problem, this is not really usable directly by a
client.

optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];

Returns

Whether the maxNumberOfConflicts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxNumCuts()

boolean hasMaxNumCuts

(

)

The limit on the number of cuts in our cut pool. When this is reached we do
not generate cuts anymore.
TODO(user): We should probably remove this parameters, and just always
generate cuts but only keep the best n or something.

optional int32 max_num_cuts = 91 [default = 10000];

Returns

Whether the maxNumCuts field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxPresolveIterations()

boolean hasMaxPresolveIterations

(

)

In case of large reduction in a presolve iteration, we perform multiple
presolve iterations. This parameter controls the maximum number of such
presolve iterations.

optional int32 max_presolve_iterations = 138 [default = 3];

Returns

Whether the maxPresolveIterations field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxSatAssumptionOrder()

boolean hasMaxSatAssumptionOrder

(

)

optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];

Returns

Whether the maxSatAssumptionOrder field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxSatReverseAssumptionOrder()

boolean hasMaxSatReverseAssumptionOrder

(

)

If true, adds the assumption in the reverse order of the one defined by
max_sat_assumption_order.

optional bool max_sat_reverse_assumption_order = 52 [default = false];

Returns

Whether the maxSatReverseAssumptionOrder field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxSatStratification()

boolean hasMaxSatStratification

(

)

optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];

Returns

Whether the maxSatStratification field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxTimeInSeconds()

boolean hasMaxTimeInSeconds

(

)

Maximum time allowed in seconds to solve a problem.
The counter will starts at the beginning of the Solve() call.

optional double max_time_in_seconds = 36 [default = inf];

Returns

Whether the maxTimeInSeconds field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMaxVariableActivityValue()

boolean hasMaxVariableActivityValue

(

)

optional double max_variable_activity_value = 16 [default = 1e+100];

Returns

Whether the maxVariableActivityValue field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMergeAtMostOneWorkLimit()

boolean hasMergeAtMostOneWorkLimit

(

)

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns

Whether the mergeAtMostOneWorkLimit field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMergeNoOverlapWorkLimit()

boolean hasMergeNoOverlapWorkLimit

(

)

During presolve, we use a maximum clique heuristic to merge together
no-overlap constraints or at most one constraints. This code can be slow,
so we have a limit in place on the number of explored nodes in the
underlying graph. The internal limit is an int64, but we use double here to
simplify manual input.

optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];

Returns

Whether the mergeNoOverlapWorkLimit field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMinimizationAlgorithm()

boolean hasMinimizationAlgorithm

(

)

optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];

Returns

Whether the minimizationAlgorithm field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMinimizeCore()

boolean hasMinimizeCore

(

)

Whether we use a simple heuristic to try to minimize an UNSAT core.

optional bool minimize_core = 50 [default = true];

Returns

Whether the minimizeCore field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMinimizeReductionDuringPbResolution()

boolean hasMinimizeReductionDuringPbResolution

(

)

A different algorithm during PB resolution. It minimizes the number of
calls to ReduceCoefficients() which can be time consuming. However, the
search space will be different and if the coefficients are large, this may
lead to integer overflows that could otherwise be prevented.

optional bool minimize_reduction_during_pb_resolution = 48 [default = false];

Returns

Whether the minimizeReductionDuringPbResolution field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMinimizeWithPropagationNumDecisions()

boolean hasMinimizeWithPropagationNumDecisions

(

)

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns

Whether the minimizeWithPropagationNumDecisions field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMinimizeWithPropagationRestartPeriod()

boolean hasMinimizeWithPropagationRestartPeriod

(

)

Parameters for an heuristic similar to the one descibed in "An effective
learnt clause minimization approach for CDCL Sat Solvers",
https://www.ijcai.org/proceedings/2017/0098.pdf
For now, we have a somewhat simpler implementation where every x restart we
spend y decisions on clause minimization. The minimization technique is the
same as the one used to minimize core in max-sat. We also minimize problem
clauses and not just the learned clause that we keep forever like in the
paper.
Changing these parameters or the kind of clause we minimize seems to have
a big impact on the overall perf on our benchmarks. So this technique seems
definitely useful, but it is hard to tune properly.

optional int32 minimize_with_propagation_restart_period = 96 [default = 10];

Returns

Whether the minimizeWithPropagationRestartPeriod field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMinOrthogonalityForLpConstraints()

boolean hasMinOrthogonalityForLpConstraints

(

)

While adding constraints, skip the constraints which have orthogonality
less than 'min_orthogonality_for_lp_constraints' with already added
constraints during current call. Orthogonality is defined as 1 -
cosine(vector angle between constraints). A value of zero disable this
feature.

optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];

Returns

Whether the minOrthogonalityForLpConstraints field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMipAutomaticallyScaleVariables()

boolean hasMipAutomaticallyScaleVariables

(

)

If true, some continuous variable might be automatially scaled. For now,
this is only the case where we detect that a variable is actually an
integer multiple of a constant. For instance, variables of the form k * 0.5
are quite frequent, and if we detect this, we will scale such variable
domain by 2 to make it implied integer.

optional bool mip_automatically_scale_variables = 166 [default = true];

Returns

Whether the mipAutomaticallyScaleVariables field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMipCheckPrecision()

boolean hasMipCheckPrecision

(

)

As explained in mip_precision and mip_max_activity_exponent, we cannot
always reach the wanted precision during scaling. We use this threshold to
enphasize in the logs when the precision seems bad.

optional double mip_check_precision = 128 [default = 0.0001];

Returns

Whether the mipCheckPrecision field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMipMaxActivityExponent()

boolean hasMipMaxActivityExponent

(

)

To avoid integer overflow, we always force the maximum possible constraint
activity (and objective value) according to the initial variable domain to
be smaller than 2 to this given power. Because of this, we cannot always
reach the "mip_wanted_precision" parameter above.
This can go as high as 62, but some internal algo currently abort early if
they might run into integer overflow, so it is better to keep it a bit
lower than this.

optional int32 mip_max_activity_exponent = 127 [default = 53];

Returns

Whether the mipMaxActivityExponent field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMipMaxBound()

boolean hasMipMaxBound

(

)

We need to bound the maximum magnitude of the variables for CP-SAT, and
that is the bound we use. If the MIP model expect larger variable value in
the solution, then the converted model will likely not be relevant.

optional double mip_max_bound = 124 [default = 10000000];

Returns

Whether the mipMaxBound field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMipVarScaling()

boolean hasMipVarScaling

(

)

All continuous variable of the problem will be multiplied by this factor.
By default, we don't do any variable scaling and rely on the MIP model to
specify continuous variable domain with the wanted precision.

optional double mip_var_scaling = 125 [default = 1];

Returns

Whether the mipVarScaling field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasMipWantedPrecision()

boolean hasMipWantedPrecision

(

)

When scaling constraint with double coefficients to integer coefficients,
we will multiply by a power of 2 and round the coefficients. We will choose
the lowest power such that we have no potential overflow and the worst case
constraint activity error do not exceed this threshold relative to the
constraint bounds.
We also use this to decide by how much we relax the constraint bounds so
that we can have a feasible integer solution of constraints involving
continuous variable. This is required for instance when you have an == rhs
constraint as in many situation you cannot have a perfect equality with
integer variables and coefficients.

optional double mip_wanted_precision = 126 [default = 1e-06];

Returns

Whether the mipWantedPrecision field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasName()

boolean hasName

(

)

In some context, like in a portfolio of search, it makes sense to name a
given parameters set for logging purpose.

optional string name = 171 [default = ""];

Returns

Whether the name field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasNewConstraintsBatchSize()

boolean hasNewConstraintsBatchSize

(

)

Add that many lazy constraints (or cuts) at once in the LP. Note that at
the beginning of the solve, we do add more than this.

optional int32 new_constraints_batch_size = 122 [default = 50];

Returns

Whether the newConstraintsBatchSize field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasNumConflictsBeforeStrategyChanges()

boolean hasNumConflictsBeforeStrategyChanges

(

)

After each restart, if the number of conflict since the last strategy
change is greater that this, then we increment a "strategy_counter" that
can be use to change the search strategy used by the following restarts.

optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];

Returns

Whether the numConflictsBeforeStrategyChanges field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasNumSearchWorkers()

boolean hasNumSearchWorkers

(

)

Specify the number of parallel workers to use during search.
A number <= 1 means no parallelism.
As of 2020-04-10, if you're using SAT via MPSolver (to solve integer
programs) this field is overridden with a value of 8, if the field is not
set *explicitly*. Thus, always set this field explicitly or via
MPSolver::SetNumThreads().

optional int32 num_search_workers = 100 [default = 1];

Returns

Whether the numSearchWorkers field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasOnlyAddCutsAtLevelZero()

boolean hasOnlyAddCutsAtLevelZero

(

)

For the cut that can be generated at any level, this control if we only
try to generate them at the root node.

optional bool only_add_cuts_at_level_zero = 92 [default = false];

Returns

Whether the onlyAddCutsAtLevelZero field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasOptimizeWithCore()

boolean hasOptimizeWithCore

(

)

The default optimization method is a simple "linear scan", each time trying
to find a better solution than the previous one. If this is true, then we
use a core-based approach (like in max-SAT) when we try to increase the
lower bound instead.

optional bool optimize_with_core = 83 [default = false];

Returns

Whether the optimizeWithCore field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasOptimizeWithMaxHs()

boolean hasOptimizeWithMaxHs

(

)

This has no effect if optimize_with_core is false. If true, use a different
core-based algorithm similar to the max-HS algo for max-SAT. This is a
hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT
one. This is also related to the PhD work of tobyodavies@
"Automatic Logic-Based Benders Decomposition with MiniZinc"
http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489

optional bool optimize_with_max_hs = 85 [default = false];

Returns

Whether the optimizeWithMaxHs field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPbCleanupIncrement()

boolean hasPbCleanupIncrement

(

)

Same as for the clauses, but for the learned pseudo-Boolean constraints.

optional int32 pb_cleanup_increment = 46 [default = 200];

Returns

Whether the pbCleanupIncrement field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPbCleanupRatio()

boolean hasPbCleanupRatio

(

)

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns

Whether the pbCleanupRatio field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPermutePresolveConstraintOrder()

boolean hasPermutePresolveConstraintOrder

(

)

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns

Whether the permutePresolveConstraintOrder field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPermuteVariableRandomly()

boolean hasPermuteVariableRandomly

(

)

This is mainly here to test the solver variability. Note that in tests, if
not explicitly set to false, all 3 options will be set to true so that
clients do not rely on the solver returning a specific solution if they are
many equivalent optimal solutions.

optional bool permute_variable_randomly = 178 [default = false];

Returns

Whether the permuteVariableRandomly field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPolarityRephaseIncrement()

boolean hasPolarityRephaseIncrement

(

)

If non-zero, then we change the polarity heuristic after that many number
of conflicts in an arithmetically increasing fashion. So x the first time,
2 * x the second time, etc...

optional int32 polarity_rephase_increment = 168 [default = 1000];

Returns

Whether the polarityRephaseIncrement field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPolishLpSolution()

boolean hasPolishLpSolution

(

)

Whether we try to do a few degenerate iteration at the end of an LP solve
to minimize the fractionality of the integer variable in the basis. This
helps on some problems, but not so much on others. It also cost of bit of
time to do such polish step.

optional bool polish_lp_solution = 175 [default = false];

Returns

Whether the polishLpSolution field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPreferredVariableOrder()

boolean hasPreferredVariableOrder

(

)

optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];

Returns

Whether the preferredVariableOrder field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPresolveBlockedClause()

boolean hasPresolveBlockedClause

(

)

Whether we use an heuristic to detect some basic case of blocked clause
in the SAT presolve.

optional bool presolve_blocked_clause = 88 [default = true];

Returns

Whether the presolveBlockedClause field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPresolveBvaThreshold()

boolean hasPresolveBvaThreshold

(

)

Apply Bounded Variable Addition (BVA) if the number of clauses is reduced
by stricly more than this threshold. The algorithm described in the paper
uses 0, but quick experiments showed that 1 is a good value. It may not be
worth it to add a new variable just to remove one clause.

optional int32 presolve_bva_threshold = 73 [default = 1];

Returns

Whether the presolveBvaThreshold field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPresolveBveClauseWeight()

boolean hasPresolveBveClauseWeight

(

)

During presolve, we apply BVE only if this weight times the number of
clauses plus the number of clause literals is not increased.

optional int32 presolve_bve_clause_weight = 55 [default = 3];

Returns

Whether the presolveBveClauseWeight field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPresolveBveThreshold()

boolean hasPresolveBveThreshold

(

)

During presolve, only try to perform the bounded variable elimination (BVE)
of a variable x if the number of occurrences of x times the number of
occurrences of not(x) is not greater than this parameter.

optional int32 presolve_bve_threshold = 54 [default = 500];

Returns

Whether the presolveBveThreshold field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPresolveExtractIntegerEnforcement()

boolean hasPresolveExtractIntegerEnforcement

(

)

If true, we will extract from linear constraints, enforcement literals of
the form "integer variable at bound => simplified constraint". This should
always be beneficial except that we don't always handle them as efficiently
as we could for now. This causes problem on manna81.mps (LP relaxation not
as tight it seems) and on neos-3354841-apure.mps.gz (too many literals
created this way).

optional bool presolve_extract_integer_enforcement = 174 [default = false];

Returns

Whether the presolveExtractIntegerEnforcement field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPresolveProbingDeterministicTimeLimit()

boolean hasPresolveProbingDeterministicTimeLimit

(

)

The maximum "deterministic" time limit to spend in probing. A value of
zero will disable the probing.

optional double presolve_probing_deterministic_time_limit = 57 [default = 30];

Returns

Whether the presolveProbingDeterministicTimeLimit field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPresolveSubstitutionLevel()

boolean hasPresolveSubstitutionLevel

(

)

How much substitution (also called free variable aggregation in MIP
litterature) should we perform at presolve. This currently only concerns
variable appearing only in linear constraints. For now the value 0 turns it
off and any positive value performs substitution.

optional int32 presolve_substitution_level = 147 [default = 1];

Returns

Whether the presolveSubstitutionLevel field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPresolveUseBva()

boolean hasPresolveUseBva

(

)

Whether or not we use Bounded Variable Addition (BVA) in the presolve.

optional bool presolve_use_bva = 72 [default = true];

Returns

Whether the presolveUseBva field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasProbingPeriodAtRoot()

boolean hasProbingPeriodAtRoot

(

)

If set at zero (the default), it is disabled. Otherwise the solver attempts
probing at every 'probing_period' root node. Period of 1 enables probing at
every root node.

optional int64 probing_period_at_root = 142 [default = 0];

Returns

Whether the probingPeriodAtRoot field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasPseudoCostReliabilityThreshold()

boolean hasPseudoCostReliabilityThreshold

(

)

The solver ignores the pseudo costs of variables with number of recordings
less than this threshold.

optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];

Returns

Whether the pseudoCostReliabilityThreshold field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRandomBranchesRatio()

boolean hasRandomBranchesRatio

(

)

A number between 0 and 1 that indicates the proportion of branching
variables that are selected randomly instead of choosing the first variable
from the given variable_ordering strategy.

optional double random_branches_ratio = 32 [default = 0];

Returns

Whether the randomBranchesRatio field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRandomizeSearch()

boolean hasRandomizeSearch

(

)

Randomize fixed search.

optional bool randomize_search = 103 [default = false];

Returns

Whether the randomizeSearch field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRandomPolarityRatio()

boolean hasRandomPolarityRatio

(

)

The proportion of polarity chosen at random. Note that this take
precedence over the phase saving heuristic. This is different from
initial_polarity:POLARITY_RANDOM because it will select a new random
polarity each time the variable is branched upon instead of selecting one
initially and then always taking this choice.

optional double random_polarity_ratio = 45 [default = 0];

Returns

Whether the randomPolarityRatio field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRandomSeed()

boolean hasRandomSeed

(

)

At the beginning of each solve, the random number generator used in some
part of the solver is reinitialized to this seed. If you change the random
seed, the solver may make different choices during the solving process.
For some problems, the running time may vary a lot depending on small
change in the solving algorithm. Running the solver with different seeds
enables to have more robust benchmarks when evaluating new features.

optional int32 random_seed = 31 [default = 1];

Returns

Whether the randomSeed field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasReduceMemoryUsageInInterleaveMode()

boolean hasReduceMemoryUsageInInterleaveMode

(

)

Temporary parameter until the memory usage is more optimized.

optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];

Returns

Whether the reduceMemoryUsageInInterleaveMode field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRelativeGapLimit()

boolean hasRelativeGapLimit

(

)

optional double relative_gap_limit = 160 [default = 0];

Returns

Whether the relativeGapLimit field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRepairHint()

boolean hasRepairHint

(

)

If true, the solver tries to repair the solution given in the hint. This
search terminates after the 'hint_conflict_limit' is reached and the solver
switches to regular search. If false, then  we do a FIXED_SEARCH using the
hint until the hint_conflict_limit is reached.

optional bool repair_hint = 167 [default = false];

Returns

Whether the repairHint field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRestartDlAverageRatio()

boolean hasRestartDlAverageRatio

(

)

In the moving average restart algorithms, a restart is triggered if the
window average times this ratio is greater that the global average.

optional double restart_dl_average_ratio = 63 [default = 1];

Returns

Whether the restartDlAverageRatio field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRestartLbdAverageRatio()

boolean hasRestartLbdAverageRatio

(

)

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns

Whether the restartLbdAverageRatio field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRestartPeriod()

boolean hasRestartPeriod

(

)

Restart period for the FIXED_RESTART strategy. This is also the multiplier
used by the LUBY_RESTART strategy.

optional int32 restart_period = 30 [default = 50];

Returns

Whether the restartPeriod field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasRestartRunningWindowSize()

boolean hasRestartRunningWindowSize

(

)

Size of the window for the moving average restarts.

optional int32 restart_running_window_size = 62 [default = 50];

Returns

Whether the restartRunningWindowSize field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasSearchBranching()

boolean hasSearchBranching

(

)

optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];

Returns

Whether the searchBranching field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasSearchRandomizationTolerance()

boolean hasSearchRandomizationTolerance

(

)

Search randomization will collect equivalent 'max valued' variables, and
pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST,
all unassigned variables are equivalent. If the variable strategy is
CHOOSE_LOWEST_MIN, and `lm` is the current lowest min of all unassigned
variables, then the set of max valued variables will be all unassigned
variables where
   lm <= variable min <= lm + search_randomization_tolerance

optional int64 search_randomization_tolerance = 104 [default = 0];

Returns

Whether the searchRandomizationTolerance field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasShareLevelZeroBounds()

boolean hasShareLevelZeroBounds

(

)

Allows sharing of the bounds of modified variables at level 0.

optional bool share_level_zero_bounds = 114 [default = true];

Returns

Whether the shareLevelZeroBounds field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasShareObjectiveBounds()

boolean hasShareObjectiveBounds

(

)

Allows objective sharing between workers.

optional bool share_objective_bounds = 113 [default = true];

Returns

Whether the shareObjectiveBounds field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasStopAfterFirstSolution()

boolean hasStopAfterFirstSolution

(

)

For an optimization problem, stop the solver as soon as we have a solution.

optional bool stop_after_first_solution = 98 [default = false];

Returns

Whether the stopAfterFirstSolution field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasStopAfterPresolve()

boolean hasStopAfterPresolve

(

)

Mainly used when improving the presolver. When true, stops the solver after
the presolve is complete.

optional bool stop_after_presolve = 149 [default = false];

Returns

Whether the stopAfterPresolve field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasStrategyChangeIncreaseRatio()

boolean hasStrategyChangeIncreaseRatio

(

)

The parameter num_conflicts_before_strategy_changes is increased by that
much after each strategy change.

optional double strategy_change_increase_ratio = 69 [default = 0];

Returns

Whether the strategyChangeIncreaseRatio field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasSubsumptionDuringConflictAnalysis()

boolean hasSubsumptionDuringConflictAnalysis

(

)

At a really low cost, during the 1-UIP conflict computation, it is easy to
detect if some of the involved reasons are subsumed by the current
conflict. When this is true, such clauses are detached and later removed
from the problem.

optional bool subsumption_during_conflict_analysis = 56 [default = true];

Returns

Whether the subsumptionDuringConflictAnalysis field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasSymmetryLevel()

boolean hasSymmetryLevel

(

)

Whether we try to automatically detect the symmetries in a model and
exploit them. Currently, at level 1 we detect them in presolve and try
to fix Booleans. At level 2, we also do some form of dynamic symmetry
breaking during search.

optional int32 symmetry_level = 183 [default = 2];

Returns

Whether the symmetryLevel field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasTreatBinaryClausesSeparately()

boolean hasTreatBinaryClausesSeparately

(

)

If true, the binary clauses are treated separately from the others. This
should be faster and uses less memory. However it changes the propagation
order.

optional bool treat_binary_clauses_separately = 33 [default = true];

Returns

Whether the treatBinaryClausesSeparately field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseAbslRandom()

boolean hasUseAbslRandom

(

)

optional bool use_absl_random = 180 [default = false];

Returns

Whether the useAbslRandom field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseBlockingRestart()

boolean hasUseBlockingRestart

(

)

Block a moving restart algorithm if the trail size of the current conflict
is greater than the multiplier times the moving average of the trail size
at the previous conflicts.

optional bool use_blocking_restart = 64 [default = false];

Returns

Whether the useBlockingRestart field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseBranchingInLp()

boolean hasUseBranchingInLp

(

)

If true, the solver attemts to generate more info inside lp propagator by
branching on some variables if certain criteria are met during the search
tree exploration.

optional bool use_branching_in_lp = 139 [default = false];

Returns

Whether the useBranchingInLp field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseCombinedNoOverlap()

boolean hasUseCombinedNoOverlap

(

)

This can be beneficial if there is a lot of no-overlap constraints but a
relatively low number of different intervals in the problem. Like 1000
intervals, but 1M intervals in the no-overlap constraints covering them.

optional bool use_combined_no_overlap = 133 [default = false];

Returns

Whether the useCombinedNoOverlap field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseDisjunctiveConstraintInCumulativeConstraint()

boolean hasUseDisjunctiveConstraintInCumulativeConstraint

(

)

When this is true, the cumulative constraint is reinforced with propagators
from the disjunctive constraint to improve the inference on a set of tasks
that are disjunctive at the root of the problem. This additional level
supplements the default level of reasoning.
Propagators of the cumulative constraint will not be used at all if all the
tasks are disjunctive at root node.
This always result in better propagation, but it is usually slow, so
depending on the problem, turning this off may lead to a faster solution.

optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];

Returns

Whether the useDisjunctiveConstraintInCumulativeConstraint field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseErwaHeuristic()

boolean hasUseErwaHeuristic

(

)

Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as
described in "Learning Rate Based Branching Heuristic for SAT solvers",
J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.

optional bool use_erwa_heuristic = 75 [default = false];

Returns

Whether the useErwaHeuristic field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseExactLpReason()

boolean hasUseExactLpReason

(

)

The solver usually exploit the LP relaxation of a model. If this option is
true, then whatever is infered by the LP will be used like an heuristic to
compute EXACT propagation on the IP. So with this option, there is no
numerical imprecision issues.

optional bool use_exact_lp_reason = 109 [default = true];

Returns

Whether the useExactLpReason field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseFeasibilityPump()

boolean hasUseFeasibilityPump

(

)

Adds a feasibility pump subsolver along with lns subsolvers.

optional bool use_feasibility_pump = 164 [default = true];

Returns

Whether the useFeasibilityPump field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseImpliedBounds()

boolean hasUseImpliedBounds

(

)

Stores and exploits "implied-bounds" in the solver. That is, relations of
the form literal => (var >= bound). This is currently used to derive
stronger cuts.

optional bool use_implied_bounds = 144 [default = true];

Returns

Whether the useImpliedBounds field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseLnsOnly()

boolean hasUseLnsOnly

(

)

LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns

Whether the useLnsOnly field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseOptimizationHints()

boolean hasUseOptimizationHints

(

)

For an optimization problem, whether we follow some hints in order to find
a better first solution. For a variable with hint, the solver will always
try to follow the hint. It will revert to the variable_branching default
otherwise.

optional bool use_optimization_hints = 35 [default = true];

Returns

Whether the useOptimizationHints field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseOptionalVariables()

boolean hasUseOptionalVariables

(

)

If true, we automatically detect variables whose constraint are always
enforced by the same literal and we mark them as optional. This allows
to propagate them as if they were present in some situation.

optional bool use_optional_variables = 108 [default = true];

Returns

Whether the useOptionalVariables field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseOverloadCheckerInCumulativeConstraint()

boolean hasUseOverloadCheckerInCumulativeConstraint

(

)

When this is true, the cumulative constraint is reinforced with overload
checking, i.e., an additional level of reasoning based on energy. This
additional level supplements the default level of reasoning as well as
timetable edge finding.
This always result in better propagation, but it is usually slow, so
depending on the problem, turning this off may lead to a faster solution.

optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];

Returns

Whether the useOverloadCheckerInCumulativeConstraint field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUsePbResolution()

boolean hasUsePbResolution

(

)

Whether to use pseudo-Boolean resolution to analyze a conflict. Note that
this option only make sense if your problem is modelized using
pseudo-Boolean constraints. If you only have clauses, this shouldn't change
anything (except slow the solver down).

optional bool use_pb_resolution = 43 [default = false];

Returns

Whether the usePbResolution field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUsePhaseSaving()

boolean hasUsePhaseSaving

(

)

If this is true, then the polarity of a variable will be the last value it
was assigned to, or its default polarity if it was never assigned since the
call to ResetDecisionHeuristic().
Actually, we use a newer version where we follow the last value in the
longest non-conflicting partial assignment in the current phase.
This is called 'literal phase saving'. For details see 'A Lightweight
Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and
A.Darwiche, In 10th International Conference on Theory and Applications of
Satisfiability Testing, 2007.

optional bool use_phase_saving = 44 [default = true];

Returns

Whether the usePhaseSaving field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUsePrecedencesInDisjunctiveConstraint()

boolean hasUsePrecedencesInDisjunctiveConstraint

(

)

When this is true, then a disjunctive constraint will try to use the
precedence relations between time intervals to propagate their bounds
further. For instance if task A and B are both before C and task A and B
are in disjunction, then we can deduce that task C must start after
duration(A) + duration(B) instead of simply max(duration(A), duration(B)),
provided that the start time for all task was currently zero.
This always result in better propagation, but it is usually slow, so
depending on the problem, turning this off may lead to a faster solution.

optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];

Returns

Whether the usePrecedencesInDisjunctiveConstraint field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseProbingSearch()

boolean hasUseProbingSearch

(

)

If true, search will continuously probe Boolean variables, and integer
variable bounds.

optional bool use_probing_search = 176 [default = false];

Returns

Whether the useProbingSearch field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseRelaxationLns()

boolean hasUseRelaxationLns

(

)

Turns on a lns worker which solves relaxed version of the original problem
by removing constraints from the problem in order to get better bounds.

optional bool use_relaxation_lns = 150 [default = false];

Returns

Whether the useRelaxationLns field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseRinsLns()

boolean hasUseRinsLns

(

)

Turns on relaxation induced neighborhood generator.

optional bool use_rins_lns = 129 [default = true];

Returns

Whether the useRinsLns field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseSatInprocessing()

boolean hasUseSatInprocessing

(

)

optional bool use_sat_inprocessing = 163 [default = false];

Returns

Whether the useSatInprocessing field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasUseTimetableEdgeFindingInCumulativeConstraint()

boolean hasUseTimetableEdgeFindingInCumulativeConstraint

(

)

When this is true, the cumulative constraint is reinforced with timetable
edge finding, i.e., an additional level of reasoning based on the
conjunction of energy and mandatory parts. This additional level
supplements the default level of reasoning as well as overload_checker.
This always result in better propagation, but it is usually slow, so
depending on the problem, turning this off may lead to a faster solution.

optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];

Returns

Whether the useTimetableEdgeFindingInCumulativeConstraint field is set.

Implemented in SatParameters.Builder, and SatParameters.

hasVariableActivityDecay()

boolean hasVariableActivityDecay

(

)

Each time a conflict is found, the activities of some variables are
increased by one. Then, the activity of all variables are multiplied by
variable_activity_decay.
To implement this efficiently, the activity of all the variables is not
decayed at each conflict. Instead, the activity increment is multiplied by
1 / decay. When an activity reach max_variable_activity_value, all the
activity are multiplied by 1 / max_variable_activity_value.

optional double variable_activity_decay = 15 [default = 0.8];

Returns

Whether the variableActivityDecay field is set.

Implemented in SatParameters.Builder, and SatParameters.

---

The documentation for this interface was generated from the following file:

• SatParametersOrBuilder.java