Java Reference

Java Reference

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.RestartAlgorithmgetRestartAlgorithmsList ()
 
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()

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()

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()

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()

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()

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()

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()

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()

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&#64;
"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()

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 =&gt; 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
indexThe 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()

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&#64;
"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 =&gt; 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: