Java Reference

Java Reference

Detailed Description

Contains the definitions for all the sat algorithm parameters and their
default values.
NEXT TAG: 186

Protobuf type

operations_research.sat.SatParameters

Definition at line 15 of file SatParameters.java.

Classes

enum  BinaryMinizationAlgorithm
 
class  Builder
 
enum  ClauseOrdering
 
enum  ClauseProtection
 
enum  ConflictMinimizationAlgorithm
 
enum  FPRoundingMethod
 
enum  MaxSatAssumptionOrder
 
enum  MaxSatStratificationAlgorithm
 
enum  Polarity
 
enum  RestartAlgorithm
 
enum  SearchBranching
 
enum  VariableOrder
 

Public Member Functions

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

Static Public Member Functions

static final com.google.protobuf.Descriptors.Descriptor getDescriptor ()
 
static com.google.ortools.sat.SatParameters parseFrom (java.nio.ByteBuffer data) throws com.google.protobuf.InvalidProtocolBufferException
 
static com.google.ortools.sat.SatParameters parseFrom (java.nio.ByteBuffer data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
 
static com.google.ortools.sat.SatParameters parseFrom (com.google.protobuf.ByteString data) throws com.google.protobuf.InvalidProtocolBufferException
 
static com.google.ortools.sat.SatParameters parseFrom (com.google.protobuf.ByteString data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
 
static com.google.ortools.sat.SatParameters parseFrom (byte[] data) throws com.google.protobuf.InvalidProtocolBufferException
 
static com.google.ortools.sat.SatParameters parseFrom (byte[] data, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws com.google.protobuf.InvalidProtocolBufferException
 
static com.google.ortools.sat.SatParameters parseFrom (java.io.InputStream input) throws java.io.IOException
 
static com.google.ortools.sat.SatParameters parseFrom (java.io.InputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
 
static com.google.ortools.sat.SatParameters parseDelimitedFrom (java.io.InputStream input) throws java.io.IOException
 
static com.google.ortools.sat.SatParameters parseDelimitedFrom (java.io.InputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
 
static com.google.ortools.sat.SatParameters parseFrom (com.google.protobuf.CodedInputStream input) throws java.io.IOException
 
static com.google.ortools.sat.SatParameters parseFrom (com.google.protobuf.CodedInputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
 
static Builder newBuilder ()
 
static Builder newBuilder (com.google.ortools.sat.SatParameters prototype)
 
static com.google.ortools.sat.SatParameters getDefaultInstance ()
 
static com.google.protobuf.Parser< SatParametersparser ()
 

Static Public Attributes

static final int NAME_FIELD_NUMBER = 171
 
static final int PREFERRED_VARIABLE_ORDER_FIELD_NUMBER = 1
 
static final int INITIAL_POLARITY_FIELD_NUMBER = 2
 
static final int USE_PHASE_SAVING_FIELD_NUMBER = 44
 
static final int POLARITY_REPHASE_INCREMENT_FIELD_NUMBER = 168
 
static final int RANDOM_POLARITY_RATIO_FIELD_NUMBER = 45
 
static final int RANDOM_BRANCHES_RATIO_FIELD_NUMBER = 32
 
static final int USE_ERWA_HEURISTIC_FIELD_NUMBER = 75
 
static final int INITIAL_VARIABLES_ACTIVITY_FIELD_NUMBER = 76
 
static final int ALSO_BUMP_VARIABLES_IN_CONFLICT_REASONS_FIELD_NUMBER = 77
 
static final int MINIMIZATION_ALGORITHM_FIELD_NUMBER = 4
 
static final int BINARY_MINIMIZATION_ALGORITHM_FIELD_NUMBER = 34
 
static final int SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER = 56
 
static final int CLAUSE_CLEANUP_PERIOD_FIELD_NUMBER = 11
 
static final int CLAUSE_CLEANUP_TARGET_FIELD_NUMBER = 13
 
static final int CLAUSE_CLEANUP_PROTECTION_FIELD_NUMBER = 58
 
static final int CLAUSE_CLEANUP_LBD_BOUND_FIELD_NUMBER = 59
 
static final int CLAUSE_CLEANUP_ORDERING_FIELD_NUMBER = 60
 
static final int PB_CLEANUP_INCREMENT_FIELD_NUMBER = 46
 
static final int PB_CLEANUP_RATIO_FIELD_NUMBER = 47
 
static final int MINIMIZE_WITH_PROPAGATION_RESTART_PERIOD_FIELD_NUMBER = 96
 
static final int MINIMIZE_WITH_PROPAGATION_NUM_DECISIONS_FIELD_NUMBER = 97
 
static final int VARIABLE_ACTIVITY_DECAY_FIELD_NUMBER = 15
 
static final int MAX_VARIABLE_ACTIVITY_VALUE_FIELD_NUMBER = 16
 
static final int GLUCOSE_MAX_DECAY_FIELD_NUMBER = 22
 
static final int GLUCOSE_DECAY_INCREMENT_FIELD_NUMBER = 23
 
static final int GLUCOSE_DECAY_INCREMENT_PERIOD_FIELD_NUMBER = 24
 
static final int CLAUSE_ACTIVITY_DECAY_FIELD_NUMBER = 17
 
static final int MAX_CLAUSE_ACTIVITY_VALUE_FIELD_NUMBER = 18
 
static final int RESTART_ALGORITHMS_FIELD_NUMBER = 61
 
static final int DEFAULT_RESTART_ALGORITHMS_FIELD_NUMBER = 70
 
static final int RESTART_PERIOD_FIELD_NUMBER = 30
 
static final int RESTART_RUNNING_WINDOW_SIZE_FIELD_NUMBER = 62
 
static final int RESTART_DL_AVERAGE_RATIO_FIELD_NUMBER = 63
 
static final int RESTART_LBD_AVERAGE_RATIO_FIELD_NUMBER = 71
 
static final int USE_BLOCKING_RESTART_FIELD_NUMBER = 64
 
static final int BLOCKING_RESTART_WINDOW_SIZE_FIELD_NUMBER = 65
 
static final int BLOCKING_RESTART_MULTIPLIER_FIELD_NUMBER = 66
 
static final int NUM_CONFLICTS_BEFORE_STRATEGY_CHANGES_FIELD_NUMBER = 68
 
static final int STRATEGY_CHANGE_INCREASE_RATIO_FIELD_NUMBER = 69
 
static final int MAX_TIME_IN_SECONDS_FIELD_NUMBER = 36
 
static final int MAX_DETERMINISTIC_TIME_FIELD_NUMBER = 67
 
static final int MAX_NUMBER_OF_CONFLICTS_FIELD_NUMBER = 37
 
static final int MAX_MEMORY_IN_MB_FIELD_NUMBER = 40
 
static final int ABSOLUTE_GAP_LIMIT_FIELD_NUMBER = 159
 
static final int RELATIVE_GAP_LIMIT_FIELD_NUMBER = 160
 
static final int TREAT_BINARY_CLAUSES_SEPARATELY_FIELD_NUMBER = 33
 
static final int RANDOM_SEED_FIELD_NUMBER = 31
 
static final int PERMUTE_VARIABLE_RANDOMLY_FIELD_NUMBER = 178
 
static final int PERMUTE_PRESOLVE_CONSTRAINT_ORDER_FIELD_NUMBER = 179
 
static final int USE_ABSL_RANDOM_FIELD_NUMBER = 180
 
static final int LOG_SEARCH_PROGRESS_FIELD_NUMBER = 41
 
static final int FILL_LOGS_IN_RESPONSE_FIELD_NUMBER = 185
 
static final int USE_PB_RESOLUTION_FIELD_NUMBER = 43
 
static final int MINIMIZE_REDUCTION_DURING_PB_RESOLUTION_FIELD_NUMBER = 48
 
static final int COUNT_ASSUMPTION_LEVELS_IN_LBD_FIELD_NUMBER = 49
 
static final int PRESOLVE_BVE_THRESHOLD_FIELD_NUMBER = 54
 
static final int PRESOLVE_BVE_CLAUSE_WEIGHT_FIELD_NUMBER = 55
 
static final int PRESOLVE_PROBING_DETERMINISTIC_TIME_LIMIT_FIELD_NUMBER = 57
 
static final int PRESOLVE_BLOCKED_CLAUSE_FIELD_NUMBER = 88
 
static final int PRESOLVE_USE_BVA_FIELD_NUMBER = 72
 
static final int PRESOLVE_BVA_THRESHOLD_FIELD_NUMBER = 73
 
static final int MAX_PRESOLVE_ITERATIONS_FIELD_NUMBER = 138
 
static final int CP_MODEL_PRESOLVE_FIELD_NUMBER = 86
 
static final int CP_MODEL_POSTSOLVE_WITH_FULL_SOLVER_FIELD_NUMBER = 162
 
static final int CP_MODEL_MAX_NUM_PRESOLVE_OPERATIONS_FIELD_NUMBER = 151
 
static final int CP_MODEL_PROBING_LEVEL_FIELD_NUMBER = 110
 
static final int CP_MODEL_USE_SAT_PRESOLVE_FIELD_NUMBER = 93
 
static final int USE_SAT_INPROCESSING_FIELD_NUMBER = 163
 
static final int EXPAND_ELEMENT_CONSTRAINTS_FIELD_NUMBER = 140
 
static final int EXPAND_AUTOMATON_CONSTRAINTS_FIELD_NUMBER = 143
 
static final int EXPAND_TABLE_CONSTRAINTS_FIELD_NUMBER = 158
 
static final int EXPAND_ALLDIFF_CONSTRAINTS_FIELD_NUMBER = 170
 
static final int EXPAND_RESERVOIR_CONSTRAINTS_FIELD_NUMBER = 182
 
static final int DISABLE_CONSTRAINT_EXPANSION_FIELD_NUMBER = 181
 
static final int MERGE_NO_OVERLAP_WORK_LIMIT_FIELD_NUMBER = 145
 
static final int MERGE_AT_MOST_ONE_WORK_LIMIT_FIELD_NUMBER = 146
 
static final int PRESOLVE_SUBSTITUTION_LEVEL_FIELD_NUMBER = 147
 
static final int PRESOLVE_EXTRACT_INTEGER_ENFORCEMENT_FIELD_NUMBER = 174
 
static final int USE_OPTIMIZATION_HINTS_FIELD_NUMBER = 35
 
static final int MINIMIZE_CORE_FIELD_NUMBER = 50
 
static final int FIND_MULTIPLE_CORES_FIELD_NUMBER = 84
 
static final int COVER_OPTIMIZATION_FIELD_NUMBER = 89
 
static final int MAX_SAT_ASSUMPTION_ORDER_FIELD_NUMBER = 51
 
static final int MAX_SAT_REVERSE_ASSUMPTION_ORDER_FIELD_NUMBER = 52
 
static final int MAX_SAT_STRATIFICATION_FIELD_NUMBER = 53
 
static final int USE_PRECEDENCES_IN_DISJUNCTIVE_CONSTRAINT_FIELD_NUMBER = 74
 
static final int USE_OVERLOAD_CHECKER_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER = 78
 
static final int USE_TIMETABLE_EDGE_FINDING_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER = 79
 
static final int USE_DISJUNCTIVE_CONSTRAINT_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER = 80
 
static final int LINEARIZATION_LEVEL_FIELD_NUMBER = 90
 
static final int BOOLEAN_ENCODING_LEVEL_FIELD_NUMBER = 107
 
static final int MAX_NUM_CUTS_FIELD_NUMBER = 91
 
static final int ONLY_ADD_CUTS_AT_LEVEL_ZERO_FIELD_NUMBER = 92
 
static final int ADD_KNAPSACK_CUTS_FIELD_NUMBER = 111
 
static final int ADD_CG_CUTS_FIELD_NUMBER = 117
 
static final int ADD_MIR_CUTS_FIELD_NUMBER = 120
 
static final int ADD_ZERO_HALF_CUTS_FIELD_NUMBER = 169
 
static final int ADD_CLIQUE_CUTS_FIELD_NUMBER = 172
 
static final int MAX_ALL_DIFF_CUT_SIZE_FIELD_NUMBER = 148
 
static final int ADD_LIN_MAX_CUTS_FIELD_NUMBER = 152
 
static final int MAX_INTEGER_ROUNDING_SCALING_FIELD_NUMBER = 119
 
static final int ADD_LP_CONSTRAINTS_LAZILY_FIELD_NUMBER = 112
 
static final int MIN_ORTHOGONALITY_FOR_LP_CONSTRAINTS_FIELD_NUMBER = 115
 
static final int MAX_CUT_ROUNDS_AT_LEVEL_ZERO_FIELD_NUMBER = 154
 
static final int MAX_CONSECUTIVE_INACTIVE_COUNT_FIELD_NUMBER = 121
 
static final int CUT_MAX_ACTIVE_COUNT_VALUE_FIELD_NUMBER = 155
 
static final int CUT_ACTIVE_COUNT_DECAY_FIELD_NUMBER = 156
 
static final int CUT_CLEANUP_TARGET_FIELD_NUMBER = 157
 
static final int NEW_CONSTRAINTS_BATCH_SIZE_FIELD_NUMBER = 122
 
static final int SEARCH_BRANCHING_FIELD_NUMBER = 82
 
static final int HINT_CONFLICT_LIMIT_FIELD_NUMBER = 153
 
static final int REPAIR_HINT_FIELD_NUMBER = 167
 
static final int EXPLOIT_INTEGER_LP_SOLUTION_FIELD_NUMBER = 94
 
static final int EXPLOIT_ALL_LP_SOLUTION_FIELD_NUMBER = 116
 
static final int EXPLOIT_BEST_SOLUTION_FIELD_NUMBER = 130
 
static final int EXPLOIT_RELAXATION_SOLUTION_FIELD_NUMBER = 161
 
static final int EXPLOIT_OBJECTIVE_FIELD_NUMBER = 131
 
static final int PROBING_PERIOD_AT_ROOT_FIELD_NUMBER = 142
 
static final int USE_PROBING_SEARCH_FIELD_NUMBER = 176
 
static final int PSEUDO_COST_RELIABILITY_THRESHOLD_FIELD_NUMBER = 123
 
static final int OPTIMIZE_WITH_CORE_FIELD_NUMBER = 83
 
static final int BINARY_SEARCH_NUM_CONFLICTS_FIELD_NUMBER = 99
 
static final int OPTIMIZE_WITH_MAX_HS_FIELD_NUMBER = 85
 
static final int ENUMERATE_ALL_SOLUTIONS_FIELD_NUMBER = 87
 
static final int KEEP_ALL_FEASIBLE_SOLUTIONS_IN_PRESOLVE_FIELD_NUMBER = 173
 
static final int FILL_TIGHTENED_DOMAINS_IN_RESPONSE_FIELD_NUMBER = 132
 
static final int INSTANTIATE_ALL_VARIABLES_FIELD_NUMBER = 106
 
static final int AUTO_DETECT_GREATER_THAN_AT_LEAST_ONE_OF_FIELD_NUMBER = 95
 
static final int STOP_AFTER_FIRST_SOLUTION_FIELD_NUMBER = 98
 
static final int STOP_AFTER_PRESOLVE_FIELD_NUMBER = 149
 
static final int NUM_SEARCH_WORKERS_FIELD_NUMBER = 100
 
static final int INTERLEAVE_SEARCH_FIELD_NUMBER = 136
 
static final int INTERLEAVE_BATCH_SIZE_FIELD_NUMBER = 134
 
static final int REDUCE_MEMORY_USAGE_IN_INTERLEAVE_MODE_FIELD_NUMBER = 141
 
static final int SHARE_OBJECTIVE_BOUNDS_FIELD_NUMBER = 113
 
static final int SHARE_LEVEL_ZERO_BOUNDS_FIELD_NUMBER = 114
 
static final int USE_LNS_ONLY_FIELD_NUMBER = 101
 
static final int LNS_FOCUS_ON_DECISION_VARIABLES_FIELD_NUMBER = 105
 
static final int LNS_EXPAND_INTERVALS_IN_CONSTRAINT_GRAPH_FIELD_NUMBER = 184
 
static final int USE_RINS_LNS_FIELD_NUMBER = 129
 
static final int USE_FEASIBILITY_PUMP_FIELD_NUMBER = 164
 
static final int FP_ROUNDING_FIELD_NUMBER = 165
 
static final int USE_RELAXATION_LNS_FIELD_NUMBER = 150
 
static final int DIVERSIFY_LNS_PARAMS_FIELD_NUMBER = 137
 
static final int RANDOMIZE_SEARCH_FIELD_NUMBER = 103
 
static final int SEARCH_RANDOMIZATION_TOLERANCE_FIELD_NUMBER = 104
 
static final int USE_OPTIONAL_VARIABLES_FIELD_NUMBER = 108
 
static final int USE_EXACT_LP_REASON_FIELD_NUMBER = 109
 
static final int USE_BRANCHING_IN_LP_FIELD_NUMBER = 139
 
static final int USE_COMBINED_NO_OVERLAP_FIELD_NUMBER = 133
 
static final int CATCH_SIGINT_SIGNAL_FIELD_NUMBER = 135
 
static final int USE_IMPLIED_BOUNDS_FIELD_NUMBER = 144
 
static final int POLISH_LP_SOLUTION_FIELD_NUMBER = 175
 
static final int CONVERT_INTERVALS_FIELD_NUMBER = 177
 
static final int SYMMETRY_LEVEL_FIELD_NUMBER = 183
 
static final int MIP_MAX_BOUND_FIELD_NUMBER = 124
 
static final int MIP_VAR_SCALING_FIELD_NUMBER = 125
 
static final int MIP_AUTOMATICALLY_SCALE_VARIABLES_FIELD_NUMBER = 166
 
static final int MIP_WANTED_PRECISION_FIELD_NUMBER = 126
 
static final int MIP_MAX_ACTIVITY_EXPONENT_FIELD_NUMBER = 127
 
static final int MIP_CHECK_PRECISION_FIELD_NUMBER = 128
 
.lang.Deprecated static final com.google.protobuf.Parser< SatParametersPARSER
 

Protected Member Functions

.lang.Override java.lang.Object newInstance (UnusedPrivateParameter unused)
 
.lang.Override com.google.protobuf.GeneratedMessageV3.FieldAccessorTable internalGetFieldAccessorTable ()
 
.lang.Override Builder newBuilderForType (com.google.protobuf.GeneratedMessageV3.BuilderParent parent)
 

Member Function Documentation

◆ equals()

.lang.Override boolean equals ( final java.lang.Object  obj)

Definition at line 8727 of file SatParameters.java.

◆ getAbsoluteGapLimit()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4044 of file SatParameters.java.

◆ getAddCgCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5555 of file SatParameters.java.

◆ getAddCliqueCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5644 of file SatParameters.java.

◆ getAddKnapsackCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5526 of file SatParameters.java.

◆ getAddLinMaxCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5706 of file SatParameters.java.

◆ getAddLpConstraintsLazily()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5778 of file SatParameters.java.

◆ getAddMirCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5584 of file SatParameters.java.

◆ getAddZeroHalfCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5613 of file SatParameters.java.

◆ getAlsoBumpVariablesInConflictReasons()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3035 of file SatParameters.java.

◆ getAutoDetectGreaterThanAtLeastOneOf()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6572 of file SatParameters.java.

◆ getBinaryMinimizationAlgorithm()

.lang.Override com.google.ortools.sat.SatParameters.BinaryMinizationAlgorithm getBinaryMinimizationAlgorithm ( )

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

Returns
The binaryMinimizationAlgorithm.

Implements SatParametersOrBuilder.

Definition at line 3071 of file SatParameters.java.

◆ getBinarySearchNumConflicts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6362 of file SatParameters.java.

◆ getBlockingRestartMultiplier()

.lang.Override double getBlockingRestartMultiplier ( )

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns
The blockingRestartMultiplier.

Implements SatParametersOrBuilder.

Definition at line 3809 of file SatParameters.java.

◆ getBlockingRestartWindowSize()

.lang.Override int getBlockingRestartWindowSize ( )

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns
The blockingRestartWindowSize.

Implements SatParametersOrBuilder.

Definition at line 3790 of file SatParameters.java.

◆ getBooleanEncodingLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5433 of file SatParameters.java.

◆ getCatchSigintSignal()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7217 of file SatParameters.java.

◆ getClauseActivityDecay()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3497 of file SatParameters.java.

◆ getClauseCleanupLbdBound()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3210 of file SatParameters.java.

◆ getClauseCleanupOrdering()

.lang.Override com.google.ortools.sat.SatParameters.ClauseOrdering getClauseCleanupOrdering ( )

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

Returns
The clauseCleanupOrdering.

Implements SatParametersOrBuilder.

Definition at line 3227 of file SatParameters.java.

◆ getClauseCleanupPeriod()

.lang.Override int getClauseCleanupPeriod ( )
Trigger a cleanup when this number of "deletable" clauses is learned.

optional int32 clause_cleanup_period = 11 [default = 10000];

Returns
The clauseCleanupPeriod.

Implements SatParametersOrBuilder.

Definition at line 3133 of file SatParameters.java.

◆ getClauseCleanupProtection()

.lang.Override com.google.ortools.sat.SatParameters.ClauseProtection getClauseCleanupProtection ( )

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

Returns
The clauseCleanupProtection.

Implements SatParametersOrBuilder.

Definition at line 3179 of file SatParameters.java.

◆ getClauseCleanupTarget()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3162 of file SatParameters.java.

◆ getConvertIntervals()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7312 of file SatParameters.java.

◆ getCountAssumptionLevelsInLbd()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4363 of file SatParameters.java.

◆ getCoverOptimization()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5148 of file SatParameters.java.

◆ getCpModelMaxNumPresolveOperations()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4661 of file SatParameters.java.

◆ getCpModelPostsolveWithFullSolver()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4632 of file SatParameters.java.

◆ getCpModelPresolve()

.lang.Override boolean getCpModelPresolve ( )
Whether we presolve the cp_model before solving it.

optional bool cp_model_presolve = 86 [default = true];

Returns
The cpModelPresolve.

Implements SatParametersOrBuilder.

Definition at line 4599 of file SatParameters.java.

◆ getCpModelProbingLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4688 of file SatParameters.java.

◆ getCpModelUseSatPresolve()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4715 of file SatParameters.java.

◆ getCutActiveCountDecay()

.lang.Override double getCutActiveCountDecay ( )

optional double cut_active_count_decay = 156 [default = 0.8];

Returns
The cutActiveCountDecay.

Implements SatParametersOrBuilder.

Definition at line 5921 of file SatParameters.java.

◆ getCutCleanupTarget()

.lang.Override int getCutCleanupTarget ( )
Target number of constraints to remove during cleanup.

optional int32 cut_cleanup_target = 157 [default = 1000];

Returns
The cutCleanupTarget.

Implements SatParametersOrBuilder.

Definition at line 5948 of file SatParameters.java.

◆ getCutMaxActiveCountValue()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5902 of file SatParameters.java.

◆ getDefaultInstance()

static com.google.ortools.sat.SatParameters getDefaultInstance ( )
static

Definition at line 22012 of file SatParameters.java.

◆ getDefaultInstanceForType()

.lang.Override com.google.ortools.sat.SatParameters getDefaultInstanceForType ( )

Definition at line 22037 of file SatParameters.java.

◆ getDefaultRestartAlgorithms()

.lang.Override java.lang.String getDefaultRestartAlgorithms ( )

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

Returns
The defaultRestartAlgorithms.

Implements SatParametersOrBuilder.

Definition at line 3607 of file SatParameters.java.

◆ getDefaultRestartAlgorithmsBytes()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3627 of file SatParameters.java.

◆ getDescriptor()

static final com.google.protobuf.Descriptors.Descriptor getDescriptor ( )
static

Definition at line 1108 of file SatParameters.java.

◆ getDisableConstraintExpansion()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4906 of file SatParameters.java.

◆ getDiversifyLnsParams()

.lang.Override boolean getDiversifyLnsParams ( )
If true, registers more lns subsolvers with different parameters.

optional bool diversify_lns_params = 137 [default = false];

Returns
The diversifyLnsParams.

Implements SatParametersOrBuilder.

Definition at line 6994 of file SatParameters.java.

◆ getEnumerateAllSolutions()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6436 of file SatParameters.java.

◆ getExpandAlldiffConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4848 of file SatParameters.java.

◆ getExpandAutomatonConstraints()

.lang.Override boolean getExpandAutomatonConstraints ( )
If true, the automaton constraints are expanded.

optional bool expand_automaton_constraints = 143 [default = true];

Returns
The expandAutomatonConstraints.

Implements SatParametersOrBuilder.

Definition at line 4790 of file SatParameters.java.

◆ getExpandElementConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4763 of file SatParameters.java.

◆ getExpandReservoirConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4877 of file SatParameters.java.

◆ getExpandTableConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4819 of file SatParameters.java.

◆ getExploitAllLpSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6120 of file SatParameters.java.

◆ getExploitBestSolution()

.lang.Override boolean getExploitBestSolution ( )
When branching on a variable, follow the last best solution value.

optional bool exploit_best_solution = 130 [default = false];

Returns
The exploitBestSolution.

Implements SatParametersOrBuilder.

Definition at line 6147 of file SatParameters.java.

◆ getExploitIntegerLpSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6089 of file SatParameters.java.

◆ getExploitObjective()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6207 of file SatParameters.java.

◆ getExploitRelaxationSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6178 of file SatParameters.java.

◆ getFillLogsInResponse()

.lang.Override boolean getFillLogsInResponse ( )
Whether logs should be stored in the response proto.

optional bool fill_logs_in_response = 185 [default = false];

Returns
The fillLogsInResponse.

Implements SatParametersOrBuilder.

Definition at line 4256 of file SatParameters.java.

◆ getFillTightenedDomainsInResponse()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6510 of file SatParameters.java.

◆ getFindMultipleCores()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5119 of file SatParameters.java.

◆ getFpRounding()

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

Returns
The fpRounding.

Implements SatParametersOrBuilder.

Definition at line 6936 of file SatParameters.java.

◆ getGlucoseDecayIncrement()

.lang.Override double getGlucoseDecayIncrement ( )

optional double glucose_decay_increment = 23 [default = 0.01];

Returns
The glucoseDecayIncrement.

Implements SatParametersOrBuilder.

Definition at line 3451 of file SatParameters.java.

◆ getGlucoseDecayIncrementPeriod()

.lang.Override int getGlucoseDecayIncrementPeriod ( )

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns
The glucoseDecayIncrementPeriod.

Implements SatParametersOrBuilder.

Definition at line 3470 of file SatParameters.java.

◆ getGlucoseMaxDecay()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3432 of file SatParameters.java.

◆ getHintConflictLimit()

.lang.Override int getHintConflictLimit ( )
Conflict limit used in the phase that exploit the solution hint.

optional int32 hint_conflict_limit = 153 [default = 10];

Returns
The hintConflictLimit.

Implements SatParametersOrBuilder.

Definition at line 6023 of file SatParameters.java.

◆ getInitialPolarity()

.lang.Override com.google.ortools.sat.SatParameters.Polarity getInitialPolarity ( )

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

Returns
The initialPolarity.

Implements SatParametersOrBuilder.

Definition at line 2792 of file SatParameters.java.

◆ getInitialVariablesActivity()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3002 of file SatParameters.java.

◆ getInstantiateAllVariables()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6539 of file SatParameters.java.

◆ getInterleaveBatchSize()

.lang.Override int getInterleaveBatchSize ( )

optional int32 interleave_batch_size = 134 [default = 1];

Returns
The interleaveBatchSize.

Implements SatParametersOrBuilder.

Definition at line 6719 of file SatParameters.java.

◆ getInterleaveSearch()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6700 of file SatParameters.java.

◆ getKeepAllFeasibleSolutionsInPresolve()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6475 of file SatParameters.java.

◆ getLinearizationLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5404 of file SatParameters.java.

◆ getLnsExpandIntervalsInConstraintGraph()

.lang.Override boolean getLnsExpandIntervalsInConstraintGraph ( )

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns
The lnsExpandIntervalsInConstraintGraph.

Implements SatParametersOrBuilder.

Definition at line 6865 of file SatParameters.java.

◆ getLnsFocusOnDecisionVariables()

.lang.Override boolean getLnsFocusOnDecisionVariables ( )

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns
The lnsFocusOnDecisionVariables.

Implements SatParametersOrBuilder.

Definition at line 6846 of file SatParameters.java.

◆ getLogSearchProgress()

.lang.Override boolean getLogSearchProgress ( )
Whether the solver should log the search progress to LOG(INFO).

optional bool log_search_progress = 41 [default = false];

Returns
The logSearchProgress.

Implements SatParametersOrBuilder.

Definition at line 4229 of file SatParameters.java.

◆ getMaxAllDiffCutSize()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5675 of file SatParameters.java.

◆ getMaxClauseActivityValue()

.lang.Override double getMaxClauseActivityValue ( )

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

Returns
The maxClauseActivityValue.

Implements SatParametersOrBuilder.

Definition at line 3516 of file SatParameters.java.

◆ getMaxConsecutiveInactiveCount()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5871 of file SatParameters.java.

◆ getMaxCutRoundsAtLevelZero()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5840 of file SatParameters.java.

◆ getMaxDeterministicTime()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3929 of file SatParameters.java.

◆ getMaxIntegerRoundingScaling()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5745 of file SatParameters.java.

◆ getMaxMemoryInMb()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3999 of file SatParameters.java.

◆ getMaxNumberOfConflicts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3966 of file SatParameters.java.

◆ getMaxNumCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5466 of file SatParameters.java.

◆ getMaxPresolveIterations()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4572 of file SatParameters.java.

◆ getMaxSatAssumptionOrder()

.lang.Override com.google.ortools.sat.SatParameters.MaxSatAssumptionOrder getMaxSatAssumptionOrder ( )

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

Returns
The maxSatAssumptionOrder.

Implements SatParametersOrBuilder.

Definition at line 5165 of file SatParameters.java.

◆ getMaxSatReverseAssumptionOrder()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5196 of file SatParameters.java.

◆ getMaxSatStratification()

.lang.Override com.google.ortools.sat.SatParameters.MaxSatStratificationAlgorithm getMaxSatStratification ( )

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

Returns
The maxSatStratification.

Implements SatParametersOrBuilder.

Definition at line 5213 of file SatParameters.java.

◆ getMaxTimeInSeconds()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3898 of file SatParameters.java.

◆ getMaxVariableActivityValue()

.lang.Override double getMaxVariableActivityValue ( )

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

Returns
The maxVariableActivityValue.

Implements SatParametersOrBuilder.

Definition at line 3399 of file SatParameters.java.

◆ getMergeAtMostOneWorkLimit()

.lang.Override double getMergeAtMostOneWorkLimit ( )

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns
The mergeAtMostOneWorkLimit.

Implements SatParametersOrBuilder.

Definition at line 4960 of file SatParameters.java.

◆ getMergeNoOverlapWorkLimit()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4941 of file SatParameters.java.

◆ getMinimizationAlgorithm()

.lang.Override com.google.ortools.sat.SatParameters.ConflictMinimizationAlgorithm getMinimizationAlgorithm ( )

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

Returns
The minimizationAlgorithm.

Implements SatParametersOrBuilder.

Definition at line 3052 of file SatParameters.java.

◆ getMinimizeCore()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5090 of file SatParameters.java.

◆ getMinimizeReductionDuringPbResolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4322 of file SatParameters.java.

◆ getMinimizeWithPropagationNumDecisions()

.lang.Override int getMinimizeWithPropagationNumDecisions ( )

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns
The minimizeWithPropagationNumDecisions.

Implements SatParametersOrBuilder.

Definition at line 3341 of file SatParameters.java.

◆ getMinimizeWithPropagationRestartPeriod()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3322 of file SatParameters.java.

◆ getMinOrthogonalityForLpConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5813 of file SatParameters.java.

◆ getMipAutomaticallyScaleVariables()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7442 of file SatParameters.java.

◆ getMipCheckPrecision()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7557 of file SatParameters.java.

◆ getMipMaxActivityExponent()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7526 of file SatParameters.java.

◆ getMipMaxBound()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7376 of file SatParameters.java.

◆ getMipVarScaling()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7407 of file SatParameters.java.

◆ getMipWantedPrecision()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7487 of file SatParameters.java.

◆ getName()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2722 of file SatParameters.java.

◆ getNameBytes()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2747 of file SatParameters.java.

◆ getNewConstraintsBatchSize()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5977 of file SatParameters.java.

◆ getNumConflictsBeforeStrategyChanges()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3840 of file SatParameters.java.

◆ getNumSearchWorkers()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6665 of file SatParameters.java.

◆ getOnlyAddCutsAtLevelZero()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5495 of file SatParameters.java.

◆ getOptimizeWithCore()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6329 of file SatParameters.java.

◆ getOptimizeWithMaxHs()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6399 of file SatParameters.java.

◆ getParserForType()

.lang.Override com.google.protobuf.Parser<SatParameters> getParserForType ( )

Definition at line 22032 of file SatParameters.java.

◆ getPbCleanupIncrement()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3256 of file SatParameters.java.

◆ getPbCleanupRatio()

.lang.Override double getPbCleanupRatio ( )

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns
The pbCleanupRatio.

Implements SatParametersOrBuilder.

Definition at line 3275 of file SatParameters.java.

◆ getPermutePresolveConstraintOrder()

.lang.Override boolean getPermutePresolveConstraintOrder ( )

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns
The permutePresolveConstraintOrder.

Implements SatParametersOrBuilder.

Definition at line 4183 of file SatParameters.java.

◆ getPermuteVariableRandomly()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4164 of file SatParameters.java.

◆ getPolarityRephaseIncrement()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2868 of file SatParameters.java.

◆ getPolishLpSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7281 of file SatParameters.java.

◆ getPreferredVariableOrder()

.lang.Override com.google.ortools.sat.SatParameters.VariableOrder getPreferredVariableOrder ( )

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

Returns
The preferredVariableOrder.

Implements SatParametersOrBuilder.

Definition at line 2773 of file SatParameters.java.

◆ getPresolveBlockedClause()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4481 of file SatParameters.java.

◆ getPresolveBvaThreshold()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4541 of file SatParameters.java.

◆ getPresolveBveClauseWeight()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4423 of file SatParameters.java.

◆ getPresolveBveThreshold()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4394 of file SatParameters.java.

◆ getPresolveExtractIntegerEnforcement()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5030 of file SatParameters.java.

◆ getPresolveProbingDeterministicTimeLimit()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4452 of file SatParameters.java.

◆ getPresolveSubstitutionLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4993 of file SatParameters.java.

◆ getPresolveUseBva()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4508 of file SatParameters.java.

◆ getProbingPeriodAtRoot()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6238 of file SatParameters.java.

◆ getPseudoCostReliabilityThreshold()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6296 of file SatParameters.java.

◆ getRandomBranchesRatio()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2934 of file SatParameters.java.

◆ getRandomizeSearch()

.lang.Override boolean getRandomizeSearch ( )
Randomize fixed search.

optional bool randomize_search = 103 [default = false];

Returns
The randomizeSearch.

Implements SatParametersOrBuilder.

Definition at line 7021 of file SatParameters.java.

◆ getRandomPolarityRatio()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2903 of file SatParameters.java.

◆ getRandomSeed()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4131 of file SatParameters.java.

◆ getReduceMemoryUsageInInterleaveMode()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6746 of file SatParameters.java.

◆ getRelativeGapLimit()

.lang.Override double getRelativeGapLimit ( )

optional double relative_gap_limit = 160 [default = 0];

Returns
The relativeGapLimit.

Implements SatParametersOrBuilder.

Definition at line 4063 of file SatParameters.java.

◆ getRepairHint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6056 of file SatParameters.java.

◆ getRestartAlgorithms()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3588 of file SatParameters.java.

◆ getRestartAlgorithmsCount()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3568 of file SatParameters.java.

◆ getRestartAlgorithmsList()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3548 of file SatParameters.java.

◆ getRestartDlAverageRatio()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3721 of file SatParameters.java.

◆ getRestartLbdAverageRatio()

.lang.Override double getRestartLbdAverageRatio ( )

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns
The restartLbdAverageRatio.

Implements SatParametersOrBuilder.

Definition at line 3740 of file SatParameters.java.

◆ getRestartPeriod()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3665 of file SatParameters.java.

◆ getRestartRunningWindowSize()

.lang.Override int getRestartRunningWindowSize ( )
Size of the window for the moving average restarts.

optional int32 restart_running_window_size = 62 [default = 50];

Returns
The restartRunningWindowSize.

Implements SatParametersOrBuilder.

Definition at line 3692 of file SatParameters.java.

◆ getSearchBranching()

.lang.Override com.google.ortools.sat.SatParameters.SearchBranching getSearchBranching ( )

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

Returns
The searchBranching.

Implements SatParametersOrBuilder.

Definition at line 5994 of file SatParameters.java.

◆ getSearchRandomizationTolerance()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7060 of file SatParameters.java.

◆ getSerializedSize()

.lang.Override int getSerializedSize ( )

Definition at line 8065 of file SatParameters.java.

◆ getShareLevelZeroBounds()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6800 of file SatParameters.java.

◆ getShareObjectiveBounds()

.lang.Override boolean getShareObjectiveBounds ( )
Allows objective sharing between workers.

optional bool share_objective_bounds = 113 [default = true];

Returns
The shareObjectiveBounds.

Implements SatParametersOrBuilder.

Definition at line 6773 of file SatParameters.java.

◆ getStopAfterFirstSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6599 of file SatParameters.java.

◆ getStopAfterPresolve()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6628 of file SatParameters.java.

◆ getStrategyChangeIncreaseRatio()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3869 of file SatParameters.java.

◆ getSubsumptionDuringConflictAnalysis()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3106 of file SatParameters.java.

◆ getSymmetryLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7345 of file SatParameters.java.

◆ getTreatBinaryClausesSeparately()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4094 of file SatParameters.java.

◆ getUnknownFields()

.lang.Override final com.google.protobuf.UnknownFieldSet getUnknownFields ( )

Definition at line 146 of file SatParameters.java.

◆ getUseAbslRandom()

.lang.Override boolean getUseAbslRandom ( )

optional bool use_absl_random = 180 [default = false];

Returns
The useAbslRandom.

Implements SatParametersOrBuilder.

Definition at line 4202 of file SatParameters.java.

◆ getUseBlockingRestart()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3771 of file SatParameters.java.

◆ getUseBranchingInLp()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7155 of file SatParameters.java.

◆ getUseCombinedNoOverlap()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7186 of file SatParameters.java.

◆ getUseDisjunctiveConstraintInCumulativeConstraint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5371 of file SatParameters.java.

◆ getUseErwaHeuristic()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2965 of file SatParameters.java.

◆ getUseExactLpReason()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7124 of file SatParameters.java.

◆ getUseFeasibilityPump()

.lang.Override boolean getUseFeasibilityPump ( )
Adds a feasibility pump subsolver along with lns subsolvers.

optional bool use_feasibility_pump = 164 [default = true];

Returns
The useFeasibilityPump.

Implements SatParametersOrBuilder.

Definition at line 6919 of file SatParameters.java.

◆ getUseImpliedBounds()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7248 of file SatParameters.java.

◆ getUseLnsOnly()

.lang.Override boolean getUseLnsOnly ( )
LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns
The useLnsOnly.

Implements SatParametersOrBuilder.

Definition at line 6827 of file SatParameters.java.

◆ getUseOptimizationHints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5063 of file SatParameters.java.

◆ getUseOptionalVariables()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7091 of file SatParameters.java.

◆ getUseOverloadCheckerInCumulativeConstraint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5293 of file SatParameters.java.

◆ getUsePbResolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4289 of file SatParameters.java.

◆ getUsePhaseSaving()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2837 of file SatParameters.java.

◆ getUsePrecedencesInDisjunctiveConstraint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5256 of file SatParameters.java.

◆ getUseProbingSearch()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6267 of file SatParameters.java.

◆ getUseRelaxationLns()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6967 of file SatParameters.java.

◆ getUseRinsLns()

.lang.Override boolean getUseRinsLns ( )
Turns on relaxation induced neighborhood generator.

optional bool use_rins_lns = 129 [default = true];

Returns
The useRinsLns.

Implements SatParametersOrBuilder.

Definition at line 6892 of file SatParameters.java.

◆ getUseSatInprocessing()

.lang.Override boolean getUseSatInprocessing ( )

optional bool use_sat_inprocessing = 163 [default = false];

Returns
The useSatInprocessing.

Implements SatParametersOrBuilder.

Definition at line 4734 of file SatParameters.java.

◆ getUseTimetableEdgeFindingInCumulativeConstraint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5330 of file SatParameters.java.

◆ getVariableActivityDecay()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3380 of file SatParameters.java.

◆ hasAbsoluteGapLimit()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4023 of file SatParameters.java.

◆ hasAddCgCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5542 of file SatParameters.java.

◆ hasAddCliqueCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5630 of file SatParameters.java.

◆ hasAddKnapsackCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5512 of file SatParameters.java.

◆ hasAddLinMaxCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5692 of file SatParameters.java.

◆ hasAddLpConstraintsLazily()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5763 of file SatParameters.java.

◆ hasAddMirCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5571 of file SatParameters.java.

◆ hasAddZeroHalfCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5600 of file SatParameters.java.

◆ hasAlsoBumpVariablesInConflictReasons()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3020 of file SatParameters.java.

◆ hasAutoDetectGreaterThanAtLeastOneOf()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6557 of file SatParameters.java.

◆ hasBinaryMinimizationAlgorithm()

.lang.Override boolean hasBinaryMinimizationAlgorithm ( )

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

Returns
Whether the binaryMinimizationAlgorithm field is set.

Implements SatParametersOrBuilder.

Definition at line 3064 of file SatParameters.java.

◆ hasBinarySearchNumConflicts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6347 of file SatParameters.java.

◆ hasBlockingRestartMultiplier()

.lang.Override boolean hasBlockingRestartMultiplier ( )

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns
Whether the blockingRestartMultiplier field is set.

Implements SatParametersOrBuilder.

Definition at line 3801 of file SatParameters.java.

◆ hasBlockingRestartWindowSize()

.lang.Override boolean hasBlockingRestartWindowSize ( )

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns
Whether the blockingRestartWindowSize field is set.

Implements SatParametersOrBuilder.

Definition at line 3782 of file SatParameters.java.

◆ hasBooleanEncodingLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5420 of file SatParameters.java.

◆ hasCatchSigintSignal()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7203 of file SatParameters.java.

◆ hasClauseActivityDecay()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3485 of file SatParameters.java.

◆ hasClauseCleanupLbdBound()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3197 of file SatParameters.java.

◆ hasClauseCleanupOrdering()

.lang.Override boolean hasClauseCleanupOrdering ( )

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

Returns
Whether the clauseCleanupOrdering field is set.

Implements SatParametersOrBuilder.

Definition at line 3220 of file SatParameters.java.

◆ hasClauseCleanupPeriod()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3121 of file SatParameters.java.

◆ hasClauseCleanupProtection()

.lang.Override boolean hasClauseCleanupProtection ( )

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

Returns
Whether the clauseCleanupProtection field is set.

Implements SatParametersOrBuilder.

Definition at line 3172 of file SatParameters.java.

◆ hasClauseCleanupTarget()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3149 of file SatParameters.java.

◆ hasConvertIntervals()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7298 of file SatParameters.java.

◆ hasCountAssumptionLevelsInLbd()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4344 of file SatParameters.java.

◆ hasCoverOptimization()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5135 of file SatParameters.java.

◆ hasCpModelMaxNumPresolveOperations()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4648 of file SatParameters.java.

◆ hasCpModelPostsolveWithFullSolver()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4617 of file SatParameters.java.

◆ hasCpModelPresolve()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4587 of file SatParameters.java.

◆ hasCpModelProbingLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4676 of file SatParameters.java.

◆ hasCpModelUseSatPresolve()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4703 of file SatParameters.java.

◆ hasCutActiveCountDecay()

.lang.Override boolean hasCutActiveCountDecay ( )

optional double cut_active_count_decay = 156 [default = 0.8];

Returns
Whether the cutActiveCountDecay field is set.

Implements SatParametersOrBuilder.

Definition at line 5913 of file SatParameters.java.

◆ hasCutCleanupTarget()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5936 of file SatParameters.java.

◆ hasCutMaxActiveCountValue()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5888 of file SatParameters.java.

◆ hasDefaultRestartAlgorithms()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3599 of file SatParameters.java.

◆ hasDisableConstraintExpansion()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4893 of file SatParameters.java.

◆ hasDiversifyLnsParams()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6982 of file SatParameters.java.

◆ hasEnumerateAllSolutions()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6419 of file SatParameters.java.

◆ hasExpandAlldiffConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4835 of file SatParameters.java.

◆ hasExpandAutomatonConstraints()

.lang.Override boolean hasExpandAutomatonConstraints ( )
If true, the automaton constraints are expanded.

optional bool expand_automaton_constraints = 143 [default = true];

Returns
Whether the expandAutomatonConstraints field is set.

Implements SatParametersOrBuilder.

Definition at line 4778 of file SatParameters.java.

◆ hasExpandElementConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4750 of file SatParameters.java.

◆ hasExpandReservoirConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4864 of file SatParameters.java.

◆ hasExpandTableConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4806 of file SatParameters.java.

◆ hasExploitAllLpSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6106 of file SatParameters.java.

◆ hasExploitBestSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6135 of file SatParameters.java.

◆ hasExploitIntegerLpSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6074 of file SatParameters.java.

◆ hasExploitObjective()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6194 of file SatParameters.java.

◆ hasExploitRelaxationSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6164 of file SatParameters.java.

◆ hasFillLogsInResponse()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4244 of file SatParameters.java.

◆ hasFillTightenedDomainsInResponse()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6494 of file SatParameters.java.

◆ hasFindMultipleCores()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5106 of file SatParameters.java.

◆ hasFpRounding()

.lang.Override boolean hasFpRounding ( )

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

Returns
Whether the fpRounding field is set.

Implements SatParametersOrBuilder.

Definition at line 6929 of file SatParameters.java.

◆ hasGlucoseDecayIncrement()

.lang.Override boolean hasGlucoseDecayIncrement ( )

optional double glucose_decay_increment = 23 [default = 0.01];

Returns
Whether the glucoseDecayIncrement field is set.

Implements SatParametersOrBuilder.

Definition at line 3443 of file SatParameters.java.

◆ hasGlucoseDecayIncrementPeriod()

.lang.Override boolean hasGlucoseDecayIncrementPeriod ( )

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns
Whether the glucoseDecayIncrementPeriod field is set.

Implements SatParametersOrBuilder.

Definition at line 3462 of file SatParameters.java.

◆ hasGlucoseMaxDecay()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3417 of file SatParameters.java.

◆ hashCode()

.lang.Override int hashCode ( )

Definition at line 9565 of file SatParameters.java.

◆ hasHintConflictLimit()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6011 of file SatParameters.java.

◆ hasInitialPolarity()

.lang.Override boolean hasInitialPolarity ( )

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

Returns
Whether the initialPolarity field is set.

Implements SatParametersOrBuilder.

Definition at line 2785 of file SatParameters.java.

◆ hasInitialVariablesActivity()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2985 of file SatParameters.java.

◆ hasInstantiateAllVariables()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6526 of file SatParameters.java.

◆ hasInterleaveBatchSize()

.lang.Override boolean hasInterleaveBatchSize ( )

optional int32 interleave_batch_size = 134 [default = 1];

Returns
Whether the interleaveBatchSize field is set.

Implements SatParametersOrBuilder.

Definition at line 6711 of file SatParameters.java.

◆ hasInterleaveSearch()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6684 of file SatParameters.java.

◆ hasKeepAllFeasibleSolutionsInPresolve()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6457 of file SatParameters.java.

◆ hasLinearizationLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5389 of file SatParameters.java.

◆ hasLnsExpandIntervalsInConstraintGraph()

.lang.Override boolean hasLnsExpandIntervalsInConstraintGraph ( )

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns
Whether the lnsExpandIntervalsInConstraintGraph field is set.

Implements SatParametersOrBuilder.

Definition at line 6857 of file SatParameters.java.

◆ hasLnsFocusOnDecisionVariables()

.lang.Override boolean hasLnsFocusOnDecisionVariables ( )

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns
Whether the lnsFocusOnDecisionVariables field is set.

Implements SatParametersOrBuilder.

Definition at line 6838 of file SatParameters.java.

◆ hasLogSearchProgress()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4217 of file SatParameters.java.

◆ hasMaxAllDiffCutSize()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5661 of file SatParameters.java.

◆ hasMaxClauseActivityValue()

.lang.Override boolean hasMaxClauseActivityValue ( )

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

Returns
Whether the maxClauseActivityValue field is set.

Implements SatParametersOrBuilder.

Definition at line 3508 of file SatParameters.java.

◆ hasMaxConsecutiveInactiveCount()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5857 of file SatParameters.java.

◆ hasMaxCutRoundsAtLevelZero()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5828 of file SatParameters.java.

◆ hasMaxDeterministicTime()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3915 of file SatParameters.java.

◆ hasMaxIntegerRoundingScaling()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5727 of file SatParameters.java.

◆ hasMaxMemoryInMb()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3984 of file SatParameters.java.

◆ hasMaxNumberOfConflicts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3949 of file SatParameters.java.

◆ hasMaxNumCuts()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5451 of file SatParameters.java.

◆ hasMaxPresolveIterations()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4558 of file SatParameters.java.

◆ hasMaxSatAssumptionOrder()

.lang.Override boolean hasMaxSatAssumptionOrder ( )

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

Returns
Whether the maxSatAssumptionOrder field is set.

Implements SatParametersOrBuilder.

Definition at line 5158 of file SatParameters.java.

◆ hasMaxSatReverseAssumptionOrder()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5183 of file SatParameters.java.

◆ hasMaxSatStratification()

.lang.Override boolean hasMaxSatStratification ( )

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

Returns
Whether the maxSatStratification field is set.

Implements SatParametersOrBuilder.

Definition at line 5206 of file SatParameters.java.

◆ hasMaxTimeInSeconds()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3885 of file SatParameters.java.

◆ hasMaxVariableActivityValue()

.lang.Override boolean hasMaxVariableActivityValue ( )

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

Returns
Whether the maxVariableActivityValue field is set.

Implements SatParametersOrBuilder.

Definition at line 3391 of file SatParameters.java.

◆ hasMergeAtMostOneWorkLimit()

.lang.Override boolean hasMergeAtMostOneWorkLimit ( )

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns
Whether the mergeAtMostOneWorkLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 4952 of file SatParameters.java.

◆ hasMergeNoOverlapWorkLimit()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4925 of file SatParameters.java.

◆ hasMinimizationAlgorithm()

.lang.Override boolean hasMinimizationAlgorithm ( )

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

Returns
Whether the minimizationAlgorithm field is set.

Implements SatParametersOrBuilder.

Definition at line 3045 of file SatParameters.java.

◆ hasMinimizeCore()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5078 of file SatParameters.java.

◆ hasMinimizeReductionDuringPbResolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4307 of file SatParameters.java.

◆ hasMinimizeWithPropagationNumDecisions()

.lang.Override boolean hasMinimizeWithPropagationNumDecisions ( )

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns
Whether the minimizeWithPropagationNumDecisions field is set.

Implements SatParametersOrBuilder.

Definition at line 3333 of file SatParameters.java.

◆ hasMinimizeWithPropagationRestartPeriod()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3300 of file SatParameters.java.

◆ hasMinOrthogonalityForLpConstraints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5797 of file SatParameters.java.

◆ hasMipAutomaticallyScaleVariables()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7426 of file SatParameters.java.

◆ hasMipCheckPrecision()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7543 of file SatParameters.java.

◆ hasMipMaxActivityExponent()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7508 of file SatParameters.java.

◆ hasMipMaxBound()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7362 of file SatParameters.java.

◆ hasMipVarScaling()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7393 of file SatParameters.java.

◆ hasMipWantedPrecision()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7466 of file SatParameters.java.

◆ hasName()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2709 of file SatParameters.java.

◆ hasNewConstraintsBatchSize()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5964 of file SatParameters.java.

◆ hasNumConflictsBeforeStrategyChanges()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3826 of file SatParameters.java.

◆ hasNumSearchWorkers()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6648 of file SatParameters.java.

◆ hasOnlyAddCutsAtLevelZero()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5482 of file SatParameters.java.

◆ hasOptimizeWithCore()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6314 of file SatParameters.java.

◆ hasOptimizeWithMaxHs()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6382 of file SatParameters.java.

◆ hasPbCleanupIncrement()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3244 of file SatParameters.java.

◆ hasPbCleanupRatio()

.lang.Override boolean hasPbCleanupRatio ( )

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns
Whether the pbCleanupRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 3267 of file SatParameters.java.

◆ hasPermutePresolveConstraintOrder()

.lang.Override boolean hasPermutePresolveConstraintOrder ( )

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns
Whether the permutePresolveConstraintOrder field is set.

Implements SatParametersOrBuilder.

Definition at line 4175 of file SatParameters.java.

◆ hasPermuteVariableRandomly()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4149 of file SatParameters.java.

◆ hasPolarityRephaseIncrement()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2854 of file SatParameters.java.

◆ hasPolishLpSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7266 of file SatParameters.java.

◆ hasPreferredVariableOrder()

.lang.Override boolean hasPreferredVariableOrder ( )

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

Returns
Whether the preferredVariableOrder field is set.

Implements SatParametersOrBuilder.

Definition at line 2766 of file SatParameters.java.

◆ hasPresolveBlockedClause()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4468 of file SatParameters.java.

◆ hasPresolveBvaThreshold()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4526 of file SatParameters.java.

◆ hasPresolveBveClauseWeight()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4410 of file SatParameters.java.

◆ hasPresolveBveThreshold()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4380 of file SatParameters.java.

◆ hasPresolveExtractIntegerEnforcement()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5013 of file SatParameters.java.

◆ hasPresolveProbingDeterministicTimeLimit()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4439 of file SatParameters.java.

◆ hasPresolveSubstitutionLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4978 of file SatParameters.java.

◆ hasPresolveUseBva()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4496 of file SatParameters.java.

◆ hasProbingPeriodAtRoot()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6224 of file SatParameters.java.

◆ hasPseudoCostReliabilityThreshold()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6283 of file SatParameters.java.

◆ hasRandomBranchesRatio()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2920 of file SatParameters.java.

◆ hasRandomizeSearch()

.lang.Override boolean hasRandomizeSearch ( )
Randomize fixed search.

optional bool randomize_search = 103 [default = false];

Returns
Whether the randomizeSearch field is set.

Implements SatParametersOrBuilder.

Definition at line 7009 of file SatParameters.java.

◆ hasRandomPolarityRatio()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2887 of file SatParameters.java.

◆ hasRandomSeed()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4114 of file SatParameters.java.

◆ hasReduceMemoryUsageInInterleaveMode()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6734 of file SatParameters.java.

◆ hasRelativeGapLimit()

.lang.Override boolean hasRelativeGapLimit ( )

optional double relative_gap_limit = 160 [default = 0];

Returns
Whether the relativeGapLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 4055 of file SatParameters.java.

◆ hasRepairHint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6041 of file SatParameters.java.

◆ hasRestartDlAverageRatio()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3708 of file SatParameters.java.

◆ hasRestartLbdAverageRatio()

.lang.Override boolean hasRestartLbdAverageRatio ( )

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns
Whether the restartLbdAverageRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 3732 of file SatParameters.java.

◆ hasRestartPeriod()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3652 of file SatParameters.java.

◆ hasRestartRunningWindowSize()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3680 of file SatParameters.java.

◆ hasSearchBranching()

.lang.Override boolean hasSearchBranching ( )

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

Returns
Whether the searchBranching field is set.

Implements SatParametersOrBuilder.

Definition at line 5987 of file SatParameters.java.

◆ hasSearchRandomizationTolerance()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7042 of file SatParameters.java.

◆ hasShareLevelZeroBounds()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6788 of file SatParameters.java.

◆ hasShareObjectiveBounds()

.lang.Override boolean hasShareObjectiveBounds ( )
Allows objective sharing between workers.

optional bool share_objective_bounds = 113 [default = true];

Returns
Whether the shareObjectiveBounds field is set.

Implements SatParametersOrBuilder.

Definition at line 6761 of file SatParameters.java.

◆ hasStopAfterFirstSolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6587 of file SatParameters.java.

◆ hasStopAfterPresolve()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6615 of file SatParameters.java.

◆ hasStrategyChangeIncreaseRatio()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3856 of file SatParameters.java.

◆ hasSubsumptionDuringConflictAnalysis()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3091 of file SatParameters.java.

◆ hasSymmetryLevel()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7330 of file SatParameters.java.

◆ hasTreatBinaryClausesSeparately()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4080 of file SatParameters.java.

◆ hasUseAbslRandom()

.lang.Override boolean hasUseAbslRandom ( )

optional bool use_absl_random = 180 [default = false];

Returns
Whether the useAbslRandom field is set.

Implements SatParametersOrBuilder.

Definition at line 4194 of file SatParameters.java.

◆ hasUseBlockingRestart()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3757 of file SatParameters.java.

◆ hasUseBranchingInLp()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7141 of file SatParameters.java.

◆ hasUseCombinedNoOverlap()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7172 of file SatParameters.java.

◆ hasUseDisjunctiveConstraintInCumulativeConstraint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5352 of file SatParameters.java.

◆ hasUseErwaHeuristic()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2951 of file SatParameters.java.

◆ hasUseExactLpReason()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7109 of file SatParameters.java.

◆ hasUseFeasibilityPump()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6907 of file SatParameters.java.

◆ hasUseImpliedBounds()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7234 of file SatParameters.java.

◆ hasUseLnsOnly()

.lang.Override boolean hasUseLnsOnly ( )
LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns
Whether the useLnsOnly field is set.

Implements SatParametersOrBuilder.

Definition at line 6815 of file SatParameters.java.

◆ hasUseOptimizationHints()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5048 of file SatParameters.java.

◆ hasUseOptionalVariables()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 7077 of file SatParameters.java.

◆ hasUseOverloadCheckerInCumulativeConstraint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5276 of file SatParameters.java.

◆ hasUsePbResolution()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 4274 of file SatParameters.java.

◆ hasUsePhaseSaving()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 2817 of file SatParameters.java.

◆ hasUsePrecedencesInDisjunctiveConstraint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5237 of file SatParameters.java.

◆ hasUseProbingSearch()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6254 of file SatParameters.java.

◆ hasUseRelaxationLns()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 6954 of file SatParameters.java.

◆ hasUseRinsLns()

.lang.Override boolean hasUseRinsLns ( )
Turns on relaxation induced neighborhood generator.

optional bool use_rins_lns = 129 [default = true];

Returns
Whether the useRinsLns field is set.

Implements SatParametersOrBuilder.

Definition at line 6880 of file SatParameters.java.

◆ hasUseSatInprocessing()

.lang.Override boolean hasUseSatInprocessing ( )

optional bool use_sat_inprocessing = 163 [default = false];

Returns
Whether the useSatInprocessing field is set.

Implements SatParametersOrBuilder.

Definition at line 4726 of file SatParameters.java.

◆ hasUseTimetableEdgeFindingInCumulativeConstraint()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 5313 of file SatParameters.java.

◆ hasVariableActivityDecay()

.lang.Override 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.

Implements SatParametersOrBuilder.

Definition at line 3362 of file SatParameters.java.

◆ internalGetFieldAccessorTable()

.lang.Override com.google.protobuf.GeneratedMessageV3.FieldAccessorTable internalGetFieldAccessorTable ( )
protected

Definition at line 1114 of file SatParameters.java.

◆ isInitialized()

.lang.Override final boolean isInitialized ( )

Definition at line 7563 of file SatParameters.java.

◆ newBuilder() [1/2]

static Builder newBuilder ( )
static

Definition at line 10410 of file SatParameters.java.

◆ newBuilder() [2/2]

static Builder newBuilder ( com.google.ortools.sat.SatParameters  prototype)
static

Definition at line 10413 of file SatParameters.java.

◆ newBuilderForType() [1/2]

.lang.Override Builder newBuilderForType ( )

Definition at line 10409 of file SatParameters.java.

◆ newBuilderForType() [2/2]

.lang.Override Builder newBuilderForType ( com.google.protobuf.GeneratedMessageV3.BuilderParent  parent)
protected

Definition at line 10423 of file SatParameters.java.

◆ newInstance()

.lang.Override java.lang.Object newInstance ( UnusedPrivateParameter  unused)
protected

Definition at line 139 of file SatParameters.java.

◆ parseDelimitedFrom() [1/2]

static com.google.ortools.sat.SatParameters parseDelimitedFrom ( java.io.InputStream  input) throws java.io.IOException
static

Definition at line 10382 of file SatParameters.java.

◆ parseDelimitedFrom() [2/2]

static com.google.ortools.sat.SatParameters parseDelimitedFrom ( java.io.InputStream  input,
com.google.protobuf.ExtensionRegistryLite  extensionRegistry 
) throws java.io.IOException
static

Definition at line 10387 of file SatParameters.java.

◆ parseFrom() [1/10]

static com.google.ortools.sat.SatParameters parseFrom ( byte[]  data) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 10360 of file SatParameters.java.

◆ parseFrom() [2/10]

static com.google.ortools.sat.SatParameters parseFrom ( byte[]  data,
com.google.protobuf.ExtensionRegistryLite  extensionRegistry 
) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 10364 of file SatParameters.java.

◆ parseFrom() [3/10]

static com.google.ortools.sat.SatParameters parseFrom ( com.google.protobuf.ByteString  data) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 10349 of file SatParameters.java.

◆ parseFrom() [4/10]

static com.google.ortools.sat.SatParameters parseFrom ( com.google.protobuf.ByteString  data,
com.google.protobuf.ExtensionRegistryLite  extensionRegistry 
) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 10354 of file SatParameters.java.

◆ parseFrom() [5/10]

static com.google.ortools.sat.SatParameters parseFrom ( com.google.protobuf.CodedInputStream  input) throws java.io.IOException
static

Definition at line 10394 of file SatParameters.java.

◆ parseFrom() [6/10]

static com.google.ortools.sat.SatParameters parseFrom ( com.google.protobuf.CodedInputStream  input,
com.google.protobuf.ExtensionRegistryLite  extensionRegistry 
) throws java.io.IOException
static

Definition at line 10400 of file SatParameters.java.

◆ parseFrom() [7/10]

static com.google.ortools.sat.SatParameters parseFrom ( java.io.InputStream  input) throws java.io.IOException
static

Definition at line 10370 of file SatParameters.java.

◆ parseFrom() [8/10]

static com.google.ortools.sat.SatParameters parseFrom ( java.io.InputStream  input,
com.google.protobuf.ExtensionRegistryLite  extensionRegistry 
) throws java.io.IOException
static

Definition at line 10375 of file SatParameters.java.

◆ parseFrom() [9/10]

static com.google.ortools.sat.SatParameters parseFrom ( java.nio.ByteBuffer  data) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 10338 of file SatParameters.java.

◆ parseFrom() [10/10]

static com.google.ortools.sat.SatParameters parseFrom ( java.nio.ByteBuffer  data,
com.google.protobuf.ExtensionRegistryLite  extensionRegistry 
) throws com.google.protobuf.InvalidProtocolBufferException
static

Definition at line 10343 of file SatParameters.java.

◆ parser()

static com.google.protobuf.Parser<SatParameters> parser ( )
static

Definition at line 22027 of file SatParameters.java.

◆ toBuilder()

.lang.Override Builder toBuilder ( )

Definition at line 10417 of file SatParameters.java.

◆ writeTo()

.lang.Override void writeTo ( com.google.protobuf.CodedOutputStream  output) throws java.io.IOException

Definition at line 7573 of file SatParameters.java.

Member Data Documentation

◆ ABSOLUTE_GAP_LIMIT_FIELD_NUMBER

final int ABSOLUTE_GAP_LIMIT_FIELD_NUMBER = 159
static

Definition at line 4003 of file SatParameters.java.

◆ ADD_CG_CUTS_FIELD_NUMBER

final int ADD_CG_CUTS_FIELD_NUMBER = 117
static

Definition at line 5530 of file SatParameters.java.

◆ ADD_CLIQUE_CUTS_FIELD_NUMBER

final int ADD_CLIQUE_CUTS_FIELD_NUMBER = 172
static

Definition at line 5617 of file SatParameters.java.

◆ ADD_KNAPSACK_CUTS_FIELD_NUMBER

final int ADD_KNAPSACK_CUTS_FIELD_NUMBER = 111
static

Definition at line 5499 of file SatParameters.java.

◆ ADD_LIN_MAX_CUTS_FIELD_NUMBER

final int ADD_LIN_MAX_CUTS_FIELD_NUMBER = 152
static

Definition at line 5679 of file SatParameters.java.

◆ ADD_LP_CONSTRAINTS_LAZILY_FIELD_NUMBER

final int ADD_LP_CONSTRAINTS_LAZILY_FIELD_NUMBER = 112
static

Definition at line 5749 of file SatParameters.java.

◆ ADD_MIR_CUTS_FIELD_NUMBER

final int ADD_MIR_CUTS_FIELD_NUMBER = 120
static

Definition at line 5559 of file SatParameters.java.

◆ ADD_ZERO_HALF_CUTS_FIELD_NUMBER

final int ADD_ZERO_HALF_CUTS_FIELD_NUMBER = 169
static

Definition at line 5588 of file SatParameters.java.

◆ ALSO_BUMP_VARIABLES_IN_CONFLICT_REASONS_FIELD_NUMBER

final int ALSO_BUMP_VARIABLES_IN_CONFLICT_REASONS_FIELD_NUMBER = 77
static

Definition at line 3006 of file SatParameters.java.

◆ AUTO_DETECT_GREATER_THAN_AT_LEAST_ONE_OF_FIELD_NUMBER

final int AUTO_DETECT_GREATER_THAN_AT_LEAST_ONE_OF_FIELD_NUMBER = 95
static

Definition at line 6543 of file SatParameters.java.

◆ BINARY_MINIMIZATION_ALGORITHM_FIELD_NUMBER

final int BINARY_MINIMIZATION_ALGORITHM_FIELD_NUMBER = 34
static

Definition at line 3058 of file SatParameters.java.

◆ BINARY_SEARCH_NUM_CONFLICTS_FIELD_NUMBER

final int BINARY_SEARCH_NUM_CONFLICTS_FIELD_NUMBER = 99
static

Definition at line 6333 of file SatParameters.java.

◆ BLOCKING_RESTART_MULTIPLIER_FIELD_NUMBER

final int BLOCKING_RESTART_MULTIPLIER_FIELD_NUMBER = 66
static

Definition at line 3794 of file SatParameters.java.

◆ BLOCKING_RESTART_WINDOW_SIZE_FIELD_NUMBER

final int BLOCKING_RESTART_WINDOW_SIZE_FIELD_NUMBER = 65
static

Definition at line 3775 of file SatParameters.java.

◆ BOOLEAN_ENCODING_LEVEL_FIELD_NUMBER

final int BOOLEAN_ENCODING_LEVEL_FIELD_NUMBER = 107
static

Definition at line 5408 of file SatParameters.java.

◆ CATCH_SIGINT_SIGNAL_FIELD_NUMBER

final int CATCH_SIGINT_SIGNAL_FIELD_NUMBER = 135
static

Definition at line 7190 of file SatParameters.java.

◆ CLAUSE_ACTIVITY_DECAY_FIELD_NUMBER

final int CLAUSE_ACTIVITY_DECAY_FIELD_NUMBER = 17
static

Definition at line 3474 of file SatParameters.java.

◆ CLAUSE_CLEANUP_LBD_BOUND_FIELD_NUMBER

final int CLAUSE_CLEANUP_LBD_BOUND_FIELD_NUMBER = 59
static

Definition at line 3185 of file SatParameters.java.

◆ CLAUSE_CLEANUP_ORDERING_FIELD_NUMBER

final int CLAUSE_CLEANUP_ORDERING_FIELD_NUMBER = 60
static

Definition at line 3214 of file SatParameters.java.

◆ CLAUSE_CLEANUP_PERIOD_FIELD_NUMBER

final int CLAUSE_CLEANUP_PERIOD_FIELD_NUMBER = 11
static

Definition at line 3110 of file SatParameters.java.

◆ CLAUSE_CLEANUP_PROTECTION_FIELD_NUMBER

final int CLAUSE_CLEANUP_PROTECTION_FIELD_NUMBER = 58
static

Definition at line 3166 of file SatParameters.java.

◆ CLAUSE_CLEANUP_TARGET_FIELD_NUMBER

final int CLAUSE_CLEANUP_TARGET_FIELD_NUMBER = 13
static

Definition at line 3137 of file SatParameters.java.

◆ CONVERT_INTERVALS_FIELD_NUMBER

final int CONVERT_INTERVALS_FIELD_NUMBER = 177
static

Definition at line 7285 of file SatParameters.java.

◆ COUNT_ASSUMPTION_LEVELS_IN_LBD_FIELD_NUMBER

final int COUNT_ASSUMPTION_LEVELS_IN_LBD_FIELD_NUMBER = 49
static

Definition at line 4326 of file SatParameters.java.

◆ COVER_OPTIMIZATION_FIELD_NUMBER

final int COVER_OPTIMIZATION_FIELD_NUMBER = 89
static

Definition at line 5123 of file SatParameters.java.

◆ CP_MODEL_MAX_NUM_PRESOLVE_OPERATIONS_FIELD_NUMBER

final int CP_MODEL_MAX_NUM_PRESOLVE_OPERATIONS_FIELD_NUMBER = 151
static

Definition at line 4636 of file SatParameters.java.

◆ CP_MODEL_POSTSOLVE_WITH_FULL_SOLVER_FIELD_NUMBER

final int CP_MODEL_POSTSOLVE_WITH_FULL_SOLVER_FIELD_NUMBER = 162
static

Definition at line 4603 of file SatParameters.java.

◆ CP_MODEL_PRESOLVE_FIELD_NUMBER

final int CP_MODEL_PRESOLVE_FIELD_NUMBER = 86
static

Definition at line 4576 of file SatParameters.java.

◆ CP_MODEL_PROBING_LEVEL_FIELD_NUMBER

final int CP_MODEL_PROBING_LEVEL_FIELD_NUMBER = 110
static

Definition at line 4665 of file SatParameters.java.

◆ CP_MODEL_USE_SAT_PRESOLVE_FIELD_NUMBER

final int CP_MODEL_USE_SAT_PRESOLVE_FIELD_NUMBER = 93
static

Definition at line 4692 of file SatParameters.java.

◆ CUT_ACTIVE_COUNT_DECAY_FIELD_NUMBER

final int CUT_ACTIVE_COUNT_DECAY_FIELD_NUMBER = 156
static

Definition at line 5906 of file SatParameters.java.

◆ CUT_CLEANUP_TARGET_FIELD_NUMBER

final int CUT_CLEANUP_TARGET_FIELD_NUMBER = 157
static

Definition at line 5925 of file SatParameters.java.

◆ CUT_MAX_ACTIVE_COUNT_VALUE_FIELD_NUMBER

final int CUT_MAX_ACTIVE_COUNT_VALUE_FIELD_NUMBER = 155
static

Definition at line 5875 of file SatParameters.java.

◆ DEFAULT_RESTART_ALGORITHMS_FIELD_NUMBER

final int DEFAULT_RESTART_ALGORITHMS_FIELD_NUMBER = 70
static

Definition at line 3592 of file SatParameters.java.

◆ DISABLE_CONSTRAINT_EXPANSION_FIELD_NUMBER

final int DISABLE_CONSTRAINT_EXPANSION_FIELD_NUMBER = 181
static

Definition at line 4881 of file SatParameters.java.

◆ DIVERSIFY_LNS_PARAMS_FIELD_NUMBER

final int DIVERSIFY_LNS_PARAMS_FIELD_NUMBER = 137
static

Definition at line 6971 of file SatParameters.java.

◆ ENUMERATE_ALL_SOLUTIONS_FIELD_NUMBER

final int ENUMERATE_ALL_SOLUTIONS_FIELD_NUMBER = 87
static

Definition at line 6403 of file SatParameters.java.

◆ EXPAND_ALLDIFF_CONSTRAINTS_FIELD_NUMBER

final int EXPAND_ALLDIFF_CONSTRAINTS_FIELD_NUMBER = 170
static

Definition at line 4823 of file SatParameters.java.

◆ EXPAND_AUTOMATON_CONSTRAINTS_FIELD_NUMBER

final int EXPAND_AUTOMATON_CONSTRAINTS_FIELD_NUMBER = 143
static

Definition at line 4767 of file SatParameters.java.

◆ EXPAND_ELEMENT_CONSTRAINTS_FIELD_NUMBER

final int EXPAND_ELEMENT_CONSTRAINTS_FIELD_NUMBER = 140
static

Definition at line 4738 of file SatParameters.java.

◆ EXPAND_RESERVOIR_CONSTRAINTS_FIELD_NUMBER

final int EXPAND_RESERVOIR_CONSTRAINTS_FIELD_NUMBER = 182
static

Definition at line 4852 of file SatParameters.java.

◆ EXPAND_TABLE_CONSTRAINTS_FIELD_NUMBER

final int EXPAND_TABLE_CONSTRAINTS_FIELD_NUMBER = 158
static

Definition at line 4794 of file SatParameters.java.

◆ EXPLOIT_ALL_LP_SOLUTION_FIELD_NUMBER

final int EXPLOIT_ALL_LP_SOLUTION_FIELD_NUMBER = 116
static

Definition at line 6093 of file SatParameters.java.

◆ EXPLOIT_BEST_SOLUTION_FIELD_NUMBER

final int EXPLOIT_BEST_SOLUTION_FIELD_NUMBER = 130
static

Definition at line 6124 of file SatParameters.java.

◆ EXPLOIT_INTEGER_LP_SOLUTION_FIELD_NUMBER

final int EXPLOIT_INTEGER_LP_SOLUTION_FIELD_NUMBER = 94
static

Definition at line 6060 of file SatParameters.java.

◆ EXPLOIT_OBJECTIVE_FIELD_NUMBER

final int EXPLOIT_OBJECTIVE_FIELD_NUMBER = 131
static

Definition at line 6182 of file SatParameters.java.

◆ EXPLOIT_RELAXATION_SOLUTION_FIELD_NUMBER

final int EXPLOIT_RELAXATION_SOLUTION_FIELD_NUMBER = 161
static

Definition at line 6151 of file SatParameters.java.

◆ FILL_LOGS_IN_RESPONSE_FIELD_NUMBER

final int FILL_LOGS_IN_RESPONSE_FIELD_NUMBER = 185
static

Definition at line 4233 of file SatParameters.java.

◆ FILL_TIGHTENED_DOMAINS_IN_RESPONSE_FIELD_NUMBER

final int FILL_TIGHTENED_DOMAINS_IN_RESPONSE_FIELD_NUMBER = 132
static

Definition at line 6479 of file SatParameters.java.

◆ FIND_MULTIPLE_CORES_FIELD_NUMBER

final int FIND_MULTIPLE_CORES_FIELD_NUMBER = 84
static

Definition at line 5094 of file SatParameters.java.

◆ FP_ROUNDING_FIELD_NUMBER

final int FP_ROUNDING_FIELD_NUMBER = 165
static

Definition at line 6923 of file SatParameters.java.

◆ GLUCOSE_DECAY_INCREMENT_FIELD_NUMBER

final int GLUCOSE_DECAY_INCREMENT_FIELD_NUMBER = 23
static

Definition at line 3436 of file SatParameters.java.

◆ GLUCOSE_DECAY_INCREMENT_PERIOD_FIELD_NUMBER

final int GLUCOSE_DECAY_INCREMENT_PERIOD_FIELD_NUMBER = 24
static

Definition at line 3455 of file SatParameters.java.

◆ GLUCOSE_MAX_DECAY_FIELD_NUMBER

final int GLUCOSE_MAX_DECAY_FIELD_NUMBER = 22
static

Definition at line 3403 of file SatParameters.java.

◆ HINT_CONFLICT_LIMIT_FIELD_NUMBER

final int HINT_CONFLICT_LIMIT_FIELD_NUMBER = 153
static

Definition at line 6000 of file SatParameters.java.

◆ INITIAL_POLARITY_FIELD_NUMBER

final int INITIAL_POLARITY_FIELD_NUMBER = 2
static

Definition at line 2779 of file SatParameters.java.

◆ INITIAL_VARIABLES_ACTIVITY_FIELD_NUMBER

final int INITIAL_VARIABLES_ACTIVITY_FIELD_NUMBER = 76
static

Definition at line 2969 of file SatParameters.java.

◆ INSTANTIATE_ALL_VARIABLES_FIELD_NUMBER

final int INSTANTIATE_ALL_VARIABLES_FIELD_NUMBER = 106
static

Definition at line 6514 of file SatParameters.java.

◆ INTERLEAVE_BATCH_SIZE_FIELD_NUMBER

final int INTERLEAVE_BATCH_SIZE_FIELD_NUMBER = 134
static

Definition at line 6704 of file SatParameters.java.

◆ INTERLEAVE_SEARCH_FIELD_NUMBER

final int INTERLEAVE_SEARCH_FIELD_NUMBER = 136
static

Definition at line 6669 of file SatParameters.java.

◆ KEEP_ALL_FEASIBLE_SOLUTIONS_IN_PRESOLVE_FIELD_NUMBER

final int KEEP_ALL_FEASIBLE_SOLUTIONS_IN_PRESOLVE_FIELD_NUMBER = 173
static

Definition at line 6440 of file SatParameters.java.

◆ LINEARIZATION_LEVEL_FIELD_NUMBER

final int LINEARIZATION_LEVEL_FIELD_NUMBER = 90
static

Definition at line 5375 of file SatParameters.java.

◆ LNS_EXPAND_INTERVALS_IN_CONSTRAINT_GRAPH_FIELD_NUMBER

final int LNS_EXPAND_INTERVALS_IN_CONSTRAINT_GRAPH_FIELD_NUMBER = 184
static

Definition at line 6850 of file SatParameters.java.

◆ LNS_FOCUS_ON_DECISION_VARIABLES_FIELD_NUMBER

final int LNS_FOCUS_ON_DECISION_VARIABLES_FIELD_NUMBER = 105
static

Definition at line 6831 of file SatParameters.java.

◆ LOG_SEARCH_PROGRESS_FIELD_NUMBER

final int LOG_SEARCH_PROGRESS_FIELD_NUMBER = 41
static

Definition at line 4206 of file SatParameters.java.

◆ MAX_ALL_DIFF_CUT_SIZE_FIELD_NUMBER

final int MAX_ALL_DIFF_CUT_SIZE_FIELD_NUMBER = 148
static

Definition at line 5648 of file SatParameters.java.

◆ MAX_CLAUSE_ACTIVITY_VALUE_FIELD_NUMBER

final int MAX_CLAUSE_ACTIVITY_VALUE_FIELD_NUMBER = 18
static

Definition at line 3501 of file SatParameters.java.

◆ MAX_CONSECUTIVE_INACTIVE_COUNT_FIELD_NUMBER

final int MAX_CONSECUTIVE_INACTIVE_COUNT_FIELD_NUMBER = 121
static

Definition at line 5844 of file SatParameters.java.

◆ MAX_CUT_ROUNDS_AT_LEVEL_ZERO_FIELD_NUMBER

final int MAX_CUT_ROUNDS_AT_LEVEL_ZERO_FIELD_NUMBER = 154
static

Definition at line 5817 of file SatParameters.java.

◆ MAX_DETERMINISTIC_TIME_FIELD_NUMBER

final int MAX_DETERMINISTIC_TIME_FIELD_NUMBER = 67
static

Definition at line 3902 of file SatParameters.java.

◆ MAX_INTEGER_ROUNDING_SCALING_FIELD_NUMBER

final int MAX_INTEGER_ROUNDING_SCALING_FIELD_NUMBER = 119
static

Definition at line 5710 of file SatParameters.java.

◆ MAX_MEMORY_IN_MB_FIELD_NUMBER

final int MAX_MEMORY_IN_MB_FIELD_NUMBER = 40
static

Definition at line 3970 of file SatParameters.java.

◆ MAX_NUM_CUTS_FIELD_NUMBER

final int MAX_NUM_CUTS_FIELD_NUMBER = 91
static

Definition at line 5437 of file SatParameters.java.

◆ MAX_NUMBER_OF_CONFLICTS_FIELD_NUMBER

final int MAX_NUMBER_OF_CONFLICTS_FIELD_NUMBER = 37
static

Definition at line 3933 of file SatParameters.java.

◆ MAX_PRESOLVE_ITERATIONS_FIELD_NUMBER

final int MAX_PRESOLVE_ITERATIONS_FIELD_NUMBER = 138
static

Definition at line 4545 of file SatParameters.java.

◆ MAX_SAT_ASSUMPTION_ORDER_FIELD_NUMBER

final int MAX_SAT_ASSUMPTION_ORDER_FIELD_NUMBER = 51
static

Definition at line 5152 of file SatParameters.java.

◆ MAX_SAT_REVERSE_ASSUMPTION_ORDER_FIELD_NUMBER

final int MAX_SAT_REVERSE_ASSUMPTION_ORDER_FIELD_NUMBER = 52
static

Definition at line 5171 of file SatParameters.java.

◆ MAX_SAT_STRATIFICATION_FIELD_NUMBER

final int MAX_SAT_STRATIFICATION_FIELD_NUMBER = 53
static

Definition at line 5200 of file SatParameters.java.

◆ MAX_TIME_IN_SECONDS_FIELD_NUMBER

final int MAX_TIME_IN_SECONDS_FIELD_NUMBER = 36
static

Definition at line 3873 of file SatParameters.java.

◆ MAX_VARIABLE_ACTIVITY_VALUE_FIELD_NUMBER

final int MAX_VARIABLE_ACTIVITY_VALUE_FIELD_NUMBER = 16
static

Definition at line 3384 of file SatParameters.java.

◆ MERGE_AT_MOST_ONE_WORK_LIMIT_FIELD_NUMBER

final int MERGE_AT_MOST_ONE_WORK_LIMIT_FIELD_NUMBER = 146
static

Definition at line 4945 of file SatParameters.java.

◆ MERGE_NO_OVERLAP_WORK_LIMIT_FIELD_NUMBER

final int MERGE_NO_OVERLAP_WORK_LIMIT_FIELD_NUMBER = 145
static

Definition at line 4910 of file SatParameters.java.

◆ MIN_ORTHOGONALITY_FOR_LP_CONSTRAINTS_FIELD_NUMBER

final int MIN_ORTHOGONALITY_FOR_LP_CONSTRAINTS_FIELD_NUMBER = 115
static

Definition at line 5782 of file SatParameters.java.

◆ MINIMIZATION_ALGORITHM_FIELD_NUMBER

final int MINIMIZATION_ALGORITHM_FIELD_NUMBER = 4
static

Definition at line 3039 of file SatParameters.java.

◆ MINIMIZE_CORE_FIELD_NUMBER

final int MINIMIZE_CORE_FIELD_NUMBER = 50
static

Definition at line 5067 of file SatParameters.java.

◆ MINIMIZE_REDUCTION_DURING_PB_RESOLUTION_FIELD_NUMBER

final int MINIMIZE_REDUCTION_DURING_PB_RESOLUTION_FIELD_NUMBER = 48
static

Definition at line 4293 of file SatParameters.java.

◆ MINIMIZE_WITH_PROPAGATION_NUM_DECISIONS_FIELD_NUMBER

final int MINIMIZE_WITH_PROPAGATION_NUM_DECISIONS_FIELD_NUMBER = 97
static

Definition at line 3326 of file SatParameters.java.

◆ MINIMIZE_WITH_PROPAGATION_RESTART_PERIOD_FIELD_NUMBER

final int MINIMIZE_WITH_PROPAGATION_RESTART_PERIOD_FIELD_NUMBER = 96
static

Definition at line 3279 of file SatParameters.java.

◆ MIP_AUTOMATICALLY_SCALE_VARIABLES_FIELD_NUMBER

final int MIP_AUTOMATICALLY_SCALE_VARIABLES_FIELD_NUMBER = 166
static

Definition at line 7411 of file SatParameters.java.

◆ MIP_CHECK_PRECISION_FIELD_NUMBER

final int MIP_CHECK_PRECISION_FIELD_NUMBER = 128
static

Definition at line 7530 of file SatParameters.java.

◆ MIP_MAX_ACTIVITY_EXPONENT_FIELD_NUMBER

final int MIP_MAX_ACTIVITY_EXPONENT_FIELD_NUMBER = 127
static

Definition at line 7491 of file SatParameters.java.

◆ MIP_MAX_BOUND_FIELD_NUMBER

final int MIP_MAX_BOUND_FIELD_NUMBER = 124
static

Definition at line 7349 of file SatParameters.java.

◆ MIP_VAR_SCALING_FIELD_NUMBER

final int MIP_VAR_SCALING_FIELD_NUMBER = 125
static

Definition at line 7380 of file SatParameters.java.

◆ MIP_WANTED_PRECISION_FIELD_NUMBER

final int MIP_WANTED_PRECISION_FIELD_NUMBER = 126
static

Definition at line 7446 of file SatParameters.java.

◆ NAME_FIELD_NUMBER

final int NAME_FIELD_NUMBER = 171
static

Definition at line 2697 of file SatParameters.java.

◆ NEW_CONSTRAINTS_BATCH_SIZE_FIELD_NUMBER

final int NEW_CONSTRAINTS_BATCH_SIZE_FIELD_NUMBER = 122
static

Definition at line 5952 of file SatParameters.java.

◆ NUM_CONFLICTS_BEFORE_STRATEGY_CHANGES_FIELD_NUMBER

final int NUM_CONFLICTS_BEFORE_STRATEGY_CHANGES_FIELD_NUMBER = 68
static

Definition at line 3813 of file SatParameters.java.

◆ NUM_SEARCH_WORKERS_FIELD_NUMBER

final int NUM_SEARCH_WORKERS_FIELD_NUMBER = 100
static

Definition at line 6632 of file SatParameters.java.

◆ ONLY_ADD_CUTS_AT_LEVEL_ZERO_FIELD_NUMBER

final int ONLY_ADD_CUTS_AT_LEVEL_ZERO_FIELD_NUMBER = 92
static

Definition at line 5470 of file SatParameters.java.

◆ OPTIMIZE_WITH_CORE_FIELD_NUMBER

final int OPTIMIZE_WITH_CORE_FIELD_NUMBER = 83
static

Definition at line 6300 of file SatParameters.java.

◆ OPTIMIZE_WITH_MAX_HS_FIELD_NUMBER

final int OPTIMIZE_WITH_MAX_HS_FIELD_NUMBER = 85
static

Definition at line 6366 of file SatParameters.java.

◆ PARSER

.lang.Deprecated static final com.google.protobuf.Parser<SatParameters> PARSER
static
Initial value:
= new com.google.protobuf.AbstractParser<SatParameters>() {
@java.lang.Override
public SatParameters parsePartialFrom(
com.google.protobuf.CodedInputStream input,
com.google.protobuf.ExtensionRegistryLite extensionRegistry)
throws com.google.protobuf.InvalidProtocolBufferException {
return new SatParameters(input, extensionRegistry);
}
}

Definition at line 22017 of file SatParameters.java.

◆ PB_CLEANUP_INCREMENT_FIELD_NUMBER

final int PB_CLEANUP_INCREMENT_FIELD_NUMBER = 46
static

Definition at line 3233 of file SatParameters.java.

◆ PB_CLEANUP_RATIO_FIELD_NUMBER

final int PB_CLEANUP_RATIO_FIELD_NUMBER = 47
static

Definition at line 3260 of file SatParameters.java.

◆ PERMUTE_PRESOLVE_CONSTRAINT_ORDER_FIELD_NUMBER

final int PERMUTE_PRESOLVE_CONSTRAINT_ORDER_FIELD_NUMBER = 179
static

Definition at line 4168 of file SatParameters.java.

◆ PERMUTE_VARIABLE_RANDOMLY_FIELD_NUMBER

final int PERMUTE_VARIABLE_RANDOMLY_FIELD_NUMBER = 178
static

Definition at line 4135 of file SatParameters.java.

◆ POLARITY_REPHASE_INCREMENT_FIELD_NUMBER

final int POLARITY_REPHASE_INCREMENT_FIELD_NUMBER = 168
static

Definition at line 2841 of file SatParameters.java.

◆ POLISH_LP_SOLUTION_FIELD_NUMBER

final int POLISH_LP_SOLUTION_FIELD_NUMBER = 175
static

Definition at line 7252 of file SatParameters.java.

◆ PREFERRED_VARIABLE_ORDER_FIELD_NUMBER

final int PREFERRED_VARIABLE_ORDER_FIELD_NUMBER = 1
static

Definition at line 2760 of file SatParameters.java.

◆ PRESOLVE_BLOCKED_CLAUSE_FIELD_NUMBER

final int PRESOLVE_BLOCKED_CLAUSE_FIELD_NUMBER = 88
static

Definition at line 4456 of file SatParameters.java.

◆ PRESOLVE_BVA_THRESHOLD_FIELD_NUMBER

final int PRESOLVE_BVA_THRESHOLD_FIELD_NUMBER = 73
static

Definition at line 4512 of file SatParameters.java.

◆ PRESOLVE_BVE_CLAUSE_WEIGHT_FIELD_NUMBER

final int PRESOLVE_BVE_CLAUSE_WEIGHT_FIELD_NUMBER = 55
static

Definition at line 4398 of file SatParameters.java.

◆ PRESOLVE_BVE_THRESHOLD_FIELD_NUMBER

final int PRESOLVE_BVE_THRESHOLD_FIELD_NUMBER = 54
static

Definition at line 4367 of file SatParameters.java.

◆ PRESOLVE_EXTRACT_INTEGER_ENFORCEMENT_FIELD_NUMBER

final int PRESOLVE_EXTRACT_INTEGER_ENFORCEMENT_FIELD_NUMBER = 174
static

Definition at line 4997 of file SatParameters.java.

◆ PRESOLVE_PROBING_DETERMINISTIC_TIME_LIMIT_FIELD_NUMBER

final int PRESOLVE_PROBING_DETERMINISTIC_TIME_LIMIT_FIELD_NUMBER = 57
static

Definition at line 4427 of file SatParameters.java.

◆ PRESOLVE_SUBSTITUTION_LEVEL_FIELD_NUMBER

final int PRESOLVE_SUBSTITUTION_LEVEL_FIELD_NUMBER = 147
static

Definition at line 4964 of file SatParameters.java.

◆ PRESOLVE_USE_BVA_FIELD_NUMBER

final int PRESOLVE_USE_BVA_FIELD_NUMBER = 72
static

Definition at line 4485 of file SatParameters.java.

◆ PROBING_PERIOD_AT_ROOT_FIELD_NUMBER

final int PROBING_PERIOD_AT_ROOT_FIELD_NUMBER = 142
static

Definition at line 6211 of file SatParameters.java.

◆ PSEUDO_COST_RELIABILITY_THRESHOLD_FIELD_NUMBER

final int PSEUDO_COST_RELIABILITY_THRESHOLD_FIELD_NUMBER = 123
static

Definition at line 6271 of file SatParameters.java.

◆ RANDOM_BRANCHES_RATIO_FIELD_NUMBER

final int RANDOM_BRANCHES_RATIO_FIELD_NUMBER = 32
static

Definition at line 2907 of file SatParameters.java.

◆ RANDOM_POLARITY_RATIO_FIELD_NUMBER

final int RANDOM_POLARITY_RATIO_FIELD_NUMBER = 45
static

Definition at line 2872 of file SatParameters.java.

◆ RANDOM_SEED_FIELD_NUMBER

final int RANDOM_SEED_FIELD_NUMBER = 31
static

Definition at line 4098 of file SatParameters.java.

◆ RANDOMIZE_SEARCH_FIELD_NUMBER

final int RANDOMIZE_SEARCH_FIELD_NUMBER = 103
static

Definition at line 6998 of file SatParameters.java.

◆ REDUCE_MEMORY_USAGE_IN_INTERLEAVE_MODE_FIELD_NUMBER

final int REDUCE_MEMORY_USAGE_IN_INTERLEAVE_MODE_FIELD_NUMBER = 141
static

Definition at line 6723 of file SatParameters.java.

◆ RELATIVE_GAP_LIMIT_FIELD_NUMBER

final int RELATIVE_GAP_LIMIT_FIELD_NUMBER = 160
static

Definition at line 4048 of file SatParameters.java.

◆ REPAIR_HINT_FIELD_NUMBER

final int REPAIR_HINT_FIELD_NUMBER = 167
static

Definition at line 6027 of file SatParameters.java.

◆ RESTART_ALGORITHMS_FIELD_NUMBER

final int RESTART_ALGORITHMS_FIELD_NUMBER = 61
static

Definition at line 3520 of file SatParameters.java.

◆ RESTART_DL_AVERAGE_RATIO_FIELD_NUMBER

final int RESTART_DL_AVERAGE_RATIO_FIELD_NUMBER = 63
static

Definition at line 3696 of file SatParameters.java.

◆ RESTART_LBD_AVERAGE_RATIO_FIELD_NUMBER

final int RESTART_LBD_AVERAGE_RATIO_FIELD_NUMBER = 71
static

Definition at line 3725 of file SatParameters.java.

◆ RESTART_PERIOD_FIELD_NUMBER

final int RESTART_PERIOD_FIELD_NUMBER = 30
static

Definition at line 3640 of file SatParameters.java.

◆ RESTART_RUNNING_WINDOW_SIZE_FIELD_NUMBER

final int RESTART_RUNNING_WINDOW_SIZE_FIELD_NUMBER = 62
static

Definition at line 3669 of file SatParameters.java.

◆ SEARCH_BRANCHING_FIELD_NUMBER

final int SEARCH_BRANCHING_FIELD_NUMBER = 82
static

Definition at line 5981 of file SatParameters.java.

◆ SEARCH_RANDOMIZATION_TOLERANCE_FIELD_NUMBER

final int SEARCH_RANDOMIZATION_TOLERANCE_FIELD_NUMBER = 104
static

Definition at line 7025 of file SatParameters.java.

◆ SHARE_LEVEL_ZERO_BOUNDS_FIELD_NUMBER

final int SHARE_LEVEL_ZERO_BOUNDS_FIELD_NUMBER = 114
static

Definition at line 6777 of file SatParameters.java.

◆ SHARE_OBJECTIVE_BOUNDS_FIELD_NUMBER

final int SHARE_OBJECTIVE_BOUNDS_FIELD_NUMBER = 113
static

Definition at line 6750 of file SatParameters.java.

◆ STOP_AFTER_FIRST_SOLUTION_FIELD_NUMBER

final int STOP_AFTER_FIRST_SOLUTION_FIELD_NUMBER = 98
static

Definition at line 6576 of file SatParameters.java.

◆ STOP_AFTER_PRESOLVE_FIELD_NUMBER

final int STOP_AFTER_PRESOLVE_FIELD_NUMBER = 149
static

Definition at line 6603 of file SatParameters.java.

◆ STRATEGY_CHANGE_INCREASE_RATIO_FIELD_NUMBER

final int STRATEGY_CHANGE_INCREASE_RATIO_FIELD_NUMBER = 69
static

Definition at line 3844 of file SatParameters.java.

◆ SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER

final int SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER = 56
static

Definition at line 3077 of file SatParameters.java.

◆ SYMMETRY_LEVEL_FIELD_NUMBER

final int SYMMETRY_LEVEL_FIELD_NUMBER = 183
static

Definition at line 7316 of file SatParameters.java.

◆ TREAT_BINARY_CLAUSES_SEPARATELY_FIELD_NUMBER

final int TREAT_BINARY_CLAUSES_SEPARATELY_FIELD_NUMBER = 33
static

Definition at line 4067 of file SatParameters.java.

◆ USE_ABSL_RANDOM_FIELD_NUMBER

final int USE_ABSL_RANDOM_FIELD_NUMBER = 180
static

Definition at line 4187 of file SatParameters.java.

◆ USE_BLOCKING_RESTART_FIELD_NUMBER

final int USE_BLOCKING_RESTART_FIELD_NUMBER = 64
static

Definition at line 3744 of file SatParameters.java.

◆ USE_BRANCHING_IN_LP_FIELD_NUMBER

final int USE_BRANCHING_IN_LP_FIELD_NUMBER = 139
static

Definition at line 7128 of file SatParameters.java.

◆ USE_COMBINED_NO_OVERLAP_FIELD_NUMBER

final int USE_COMBINED_NO_OVERLAP_FIELD_NUMBER = 133
static

Definition at line 7159 of file SatParameters.java.

◆ USE_DISJUNCTIVE_CONSTRAINT_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER

final int USE_DISJUNCTIVE_CONSTRAINT_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER = 80
static

Definition at line 5334 of file SatParameters.java.

◆ USE_ERWA_HEURISTIC_FIELD_NUMBER

final int USE_ERWA_HEURISTIC_FIELD_NUMBER = 75
static

Definition at line 2938 of file SatParameters.java.

◆ USE_EXACT_LP_REASON_FIELD_NUMBER

final int USE_EXACT_LP_REASON_FIELD_NUMBER = 109
static

Definition at line 7095 of file SatParameters.java.

◆ USE_FEASIBILITY_PUMP_FIELD_NUMBER

final int USE_FEASIBILITY_PUMP_FIELD_NUMBER = 164
static

Definition at line 6896 of file SatParameters.java.

◆ USE_IMPLIED_BOUNDS_FIELD_NUMBER

final int USE_IMPLIED_BOUNDS_FIELD_NUMBER = 144
static

Definition at line 7221 of file SatParameters.java.

◆ USE_LNS_ONLY_FIELD_NUMBER

final int USE_LNS_ONLY_FIELD_NUMBER = 101
static

Definition at line 6804 of file SatParameters.java.

◆ USE_OPTIMIZATION_HINTS_FIELD_NUMBER

final int USE_OPTIMIZATION_HINTS_FIELD_NUMBER = 35
static

Definition at line 5034 of file SatParameters.java.

◆ USE_OPTIONAL_VARIABLES_FIELD_NUMBER

final int USE_OPTIONAL_VARIABLES_FIELD_NUMBER = 108
static

Definition at line 7064 of file SatParameters.java.

◆ USE_OVERLOAD_CHECKER_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER

final int USE_OVERLOAD_CHECKER_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER = 78
static

Definition at line 5260 of file SatParameters.java.

◆ USE_PB_RESOLUTION_FIELD_NUMBER

final int USE_PB_RESOLUTION_FIELD_NUMBER = 43
static

Definition at line 4260 of file SatParameters.java.

◆ USE_PHASE_SAVING_FIELD_NUMBER

final int USE_PHASE_SAVING_FIELD_NUMBER = 44
static

Definition at line 2798 of file SatParameters.java.

◆ USE_PRECEDENCES_IN_DISJUNCTIVE_CONSTRAINT_FIELD_NUMBER

final int USE_PRECEDENCES_IN_DISJUNCTIVE_CONSTRAINT_FIELD_NUMBER = 74
static

Definition at line 5219 of file SatParameters.java.

◆ USE_PROBING_SEARCH_FIELD_NUMBER

final int USE_PROBING_SEARCH_FIELD_NUMBER = 176
static

Definition at line 6242 of file SatParameters.java.

◆ USE_RELAXATION_LNS_FIELD_NUMBER

final int USE_RELAXATION_LNS_FIELD_NUMBER = 150
static

Definition at line 6942 of file SatParameters.java.

◆ USE_RINS_LNS_FIELD_NUMBER

final int USE_RINS_LNS_FIELD_NUMBER = 129
static

Definition at line 6869 of file SatParameters.java.

◆ USE_SAT_INPROCESSING_FIELD_NUMBER

final int USE_SAT_INPROCESSING_FIELD_NUMBER = 163
static

Definition at line 4719 of file SatParameters.java.

◆ USE_TIMETABLE_EDGE_FINDING_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER

final int USE_TIMETABLE_EDGE_FINDING_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER = 79
static

Definition at line 5297 of file SatParameters.java.

◆ VARIABLE_ACTIVITY_DECAY_FIELD_NUMBER

final int VARIABLE_ACTIVITY_DECAY_FIELD_NUMBER = 15
static

Definition at line 3345 of file SatParameters.java.


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