Java Reference

Java Reference

SatParameters

Detailed Description

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

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  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 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 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 hasLogSearchProgress ()
 
.lang.Override boolean getLogSearchProgress ()
 
.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 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 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 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 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 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 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 hasUseRinsLns ()
 
.lang.Override boolean getUseRinsLns ()
 
.lang.Override boolean hasUseFeasibilityPump ()
 
.lang.Override boolean getUseFeasibilityPump ()
 
.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 hasMipMaxBound ()
 
.lang.Override double getMipMaxBound ()
 
.lang.Override boolean hasMipVarScaling ()
 
.lang.Override double getMipVarScaling ()
 
.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 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 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 LOG_SEARCH_PROGRESS_FIELD_NUMBER = 41
 
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 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 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 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 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 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 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 USE_RINS_LNS_FIELD_NUMBER = 129
 
static final int USE_FEASIBILITY_PUMP_FIELD_NUMBER = 164
 
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 MIP_MAX_BOUND_FIELD_NUMBER = 124
 
static final int MIP_VAR_SCALING_FIELD_NUMBER = 125
 
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)
inline

Definition at line 7641 of file SatParameters.java.

◆ getAbsoluteGapLimit()

.lang.Override double getAbsoluteGapLimit ( )
inline
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 3655 of file SatParameters.java.

◆ getAddCgCuts()

.lang.Override boolean getAddCgCuts ( )
inline
Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
Note that for now, this is not heavily tunned.

optional bool add_cg_cuts = 117 [default = true];

Returns
The addCgCuts.

Implements SatParametersOrBuilder.

Definition at line 4944 of file SatParameters.java.

◆ getAddKnapsackCuts()

.lang.Override boolean getAddKnapsackCuts ( )
inline
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 4915 of file SatParameters.java.

◆ getAddLinMaxCuts()

.lang.Override boolean getAddLinMaxCuts ( )
inline
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 5035 of file SatParameters.java.

◆ getAddLpConstraintsLazily()

.lang.Override boolean getAddLpConstraintsLazily ( )
inline
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 5107 of file SatParameters.java.

◆ getAddMirCuts()

.lang.Override boolean getAddMirCuts ( )
inline
Whether we generate MIR cuts at root node.
Note that for now, this is not heavily tunned.

optional bool add_mir_cuts = 120 [default = true];

Returns
The addMirCuts.

Implements SatParametersOrBuilder.

Definition at line 4973 of file SatParameters.java.

◆ getAlsoBumpVariablesInConflictReasons()

.lang.Override boolean getAlsoBumpVariablesInConflictReasons ( )
inline
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 2646 of file SatParameters.java.

◆ getAutoDetectGreaterThanAtLeastOneOf()

.lang.Override boolean getAutoDetectGreaterThanAtLeastOneOf ( )
inline
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 5802 of file SatParameters.java.

◆ getBinaryMinimizationAlgorithm()

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

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

Returns
The binaryMinimizationAlgorithm.

Implements SatParametersOrBuilder.

Definition at line 2682 of file SatParameters.java.

◆ getBinarySearchNumConflicts()

.lang.Override int getBinarySearchNumConflicts ( )
inline
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 5631 of file SatParameters.java.

◆ getBlockingRestartMultiplier()

.lang.Override double getBlockingRestartMultiplier ( )
inline

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns
The blockingRestartMultiplier.

Implements SatParametersOrBuilder.

Definition at line 3420 of file SatParameters.java.

◆ getBlockingRestartWindowSize()

.lang.Override int getBlockingRestartWindowSize ( )
inline

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns
The blockingRestartWindowSize.

Implements SatParametersOrBuilder.

Definition at line 3401 of file SatParameters.java.

◆ getBooleanEncodingLevel()

.lang.Override int getBooleanEncodingLevel ( )
inline
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 4822 of file SatParameters.java.

◆ getCatchSigintSignal()

.lang.Override boolean getCatchSigintSignal ( )
inline
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 6409 of file SatParameters.java.

◆ getClauseActivityDecay()

.lang.Override double getClauseActivityDecay ( )
inline
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 3108 of file SatParameters.java.

◆ getClauseCleanupLbdBound()

.lang.Override int getClauseCleanupLbdBound ( )
inline
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 2821 of file SatParameters.java.

◆ getClauseCleanupOrdering()

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

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

Returns
The clauseCleanupOrdering.

Implements SatParametersOrBuilder.

Definition at line 2838 of file SatParameters.java.

◆ getClauseCleanupPeriod()

.lang.Override int getClauseCleanupPeriod ( )
inline
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 2744 of file SatParameters.java.

◆ getClauseCleanupProtection()

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

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

Returns
The clauseCleanupProtection.

Implements SatParametersOrBuilder.

Definition at line 2790 of file SatParameters.java.

◆ getClauseCleanupTarget()

.lang.Override int getClauseCleanupTarget ( )
inline
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 2773 of file SatParameters.java.

◆ getCountAssumptionLevelsInLbd()

.lang.Override boolean getCountAssumptionLevelsInLbd ( )
inline
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 3876 of file SatParameters.java.

◆ getCoverOptimization()

.lang.Override boolean getCoverOptimization ( )
inline
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 4537 of file SatParameters.java.

◆ getCpModelMaxNumPresolveOperations()

.lang.Override int getCpModelMaxNumPresolveOperations ( )
inline
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 4174 of file SatParameters.java.

◆ getCpModelPostsolveWithFullSolver()

.lang.Override boolean getCpModelPostsolveWithFullSolver ( )
inline
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 4145 of file SatParameters.java.

◆ getCpModelPresolve()

.lang.Override boolean getCpModelPresolve ( )
inline
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 4112 of file SatParameters.java.

◆ getCpModelProbingLevel()

.lang.Override int getCpModelProbingLevel ( )
inline
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 4201 of file SatParameters.java.

◆ getCpModelUseSatPresolve()

.lang.Override boolean getCpModelUseSatPresolve ( )
inline
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 4228 of file SatParameters.java.

◆ getCutActiveCountDecay()

.lang.Override double getCutActiveCountDecay ( )
inline

optional double cut_active_count_decay = 156 [default = 0.8];

Returns
The cutActiveCountDecay.

Implements SatParametersOrBuilder.

Definition at line 5250 of file SatParameters.java.

◆ getCutCleanupTarget()

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

optional int32 cut_cleanup_target = 157 [default = 1000];

Returns
The cutCleanupTarget.

Implements SatParametersOrBuilder.

Definition at line 5277 of file SatParameters.java.

◆ getCutMaxActiveCountValue()

.lang.Override double getCutMaxActiveCountValue ( )
inline
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 5231 of file SatParameters.java.

◆ getDefaultInstance()

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

Definition at line 19216 of file SatParameters.java.

◆ getDefaultInstanceForType()

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

Definition at line 19241 of file SatParameters.java.

◆ getDefaultRestartAlgorithms()

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

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 3218 of file SatParameters.java.

◆ getDefaultRestartAlgorithmsBytes()

.lang.Override com.google.protobuf.ByteString getDefaultRestartAlgorithmsBytes ( )
inline

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 3238 of file SatParameters.java.

◆ getDescriptor()

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

Definition at line 984 of file SatParameters.java.

◆ getDiversifyLnsParams()

.lang.Override boolean getDiversifyLnsParams ( )
inline
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 6186 of file SatParameters.java.

◆ getEnumerateAllSolutions()

.lang.Override boolean getEnumerateAllSolutions ( )
inline
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): Activate the presolve but with just the rules that do not
change the set of feasible solutions.

optional bool enumerate_all_solutions = 87 [default = false];

Returns
The enumerateAllSolutions.

Implements SatParametersOrBuilder.

Definition at line 5705 of file SatParameters.java.

◆ getExpandAutomatonConstraints()

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

optional bool expand_automaton_constraints = 143 [default = true];

Returns
The expandAutomatonConstraints.

Implements SatParametersOrBuilder.

Definition at line 4303 of file SatParameters.java.

◆ getExpandElementConstraints()

.lang.Override boolean getExpandElementConstraints ( )
inline
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 4276 of file SatParameters.java.

◆ getExpandTableConstraints()

.lang.Override boolean getExpandTableConstraints ( )
inline
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 4332 of file SatParameters.java.

◆ getExploitAllLpSolution()

.lang.Override boolean getExploitAllLpSolution ( )
inline
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 5418 of file SatParameters.java.

◆ getExploitBestSolution()

.lang.Override boolean getExploitBestSolution ( )
inline
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 5445 of file SatParameters.java.

◆ getExploitIntegerLpSolution()

.lang.Override boolean getExploitIntegerLpSolution ( )
inline
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 5387 of file SatParameters.java.

◆ getExploitObjective()

.lang.Override boolean getExploitObjective ( )
inline
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 5505 of file SatParameters.java.

◆ getExploitRelaxationSolution()

.lang.Override boolean getExploitRelaxationSolution ( )
inline
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 5476 of file SatParameters.java.

◆ getFillTightenedDomainsInResponse()

.lang.Override boolean getFillTightenedDomainsInResponse ( )
inline
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 5740 of file SatParameters.java.

◆ getFindMultipleCores()

.lang.Override boolean getFindMultipleCores ( )
inline
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 4508 of file SatParameters.java.

◆ getGlucoseDecayIncrement()

.lang.Override double getGlucoseDecayIncrement ( )
inline

optional double glucose_decay_increment = 23 [default = 0.01];

Returns
The glucoseDecayIncrement.

Implements SatParametersOrBuilder.

Definition at line 3062 of file SatParameters.java.

◆ getGlucoseDecayIncrementPeriod()

.lang.Override int getGlucoseDecayIncrementPeriod ( )
inline

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns
The glucoseDecayIncrementPeriod.

Implements SatParametersOrBuilder.

Definition at line 3081 of file SatParameters.java.

◆ getGlucoseMaxDecay()

.lang.Override double getGlucoseMaxDecay ( )
inline
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 3043 of file SatParameters.java.

◆ getHintConflictLimit()

.lang.Override int getHintConflictLimit ( )
inline
When we try to follow the hint, we do a FIXED_SEARCH using the hint until
this number of conflict is reached.

optional int32 hint_conflict_limit = 153 [default = 10];

Returns
The hintConflictLimit.

Implements SatParametersOrBuilder.

Definition at line 5354 of file SatParameters.java.

◆ getInitialPolarity()

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

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

Returns
The initialPolarity.

Implements SatParametersOrBuilder.

Definition at line 2438 of file SatParameters.java.

◆ getInitialVariablesActivity()

.lang.Override double getInitialVariablesActivity ( )
inline
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 2613 of file SatParameters.java.

◆ getInstantiateAllVariables()

.lang.Override boolean getInstantiateAllVariables ( )
inline
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 5769 of file SatParameters.java.

◆ getInterleaveBatchSize()

.lang.Override int getInterleaveBatchSize ( )
inline

optional int32 interleave_batch_size = 134 [default = 1];

Returns
The interleaveBatchSize.

Implements SatParametersOrBuilder.

Definition at line 5949 of file SatParameters.java.

◆ getInterleaveSearch()

.lang.Override boolean getInterleaveSearch ( )
inline
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 5930 of file SatParameters.java.

◆ getLinearizationLevel()

.lang.Override int getLinearizationLevel ( )
inline
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 4793 of file SatParameters.java.

◆ getLnsFocusOnDecisionVariables()

.lang.Override boolean getLnsFocusOnDecisionVariables ( )
inline

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns
The lnsFocusOnDecisionVariables.

Implements SatParametersOrBuilder.

Definition at line 6076 of file SatParameters.java.

◆ getLogSearchProgress()

.lang.Override boolean getLogSearchProgress ( )
inline
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 3769 of file SatParameters.java.

◆ getMaxAllDiffCutSize()

.lang.Override int getMaxAllDiffCutSize ( )
inline
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 5004 of file SatParameters.java.

◆ getMaxClauseActivityValue()

.lang.Override double getMaxClauseActivityValue ( )
inline

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

Returns
The maxClauseActivityValue.

Implements SatParametersOrBuilder.

Definition at line 3127 of file SatParameters.java.

◆ getMaxConsecutiveInactiveCount()

.lang.Override int getMaxConsecutiveInactiveCount ( )
inline
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 5200 of file SatParameters.java.

◆ getMaxCutRoundsAtLevelZero()

.lang.Override int getMaxCutRoundsAtLevelZero ( )
inline
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 5169 of file SatParameters.java.

◆ getMaxDeterministicTime()

.lang.Override double getMaxDeterministicTime ( )
inline
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 3540 of file SatParameters.java.

◆ getMaxIntegerRoundingScaling()

.lang.Override int getMaxIntegerRoundingScaling ( )
inline
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 5074 of file SatParameters.java.

◆ getMaxMemoryInMb()

.lang.Override long getMaxMemoryInMb ( )
inline
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 3610 of file SatParameters.java.

◆ getMaxNumberOfConflicts()

.lang.Override long getMaxNumberOfConflicts ( )
inline
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 3577 of file SatParameters.java.

◆ getMaxNumCuts()

.lang.Override int getMaxNumCuts ( )
inline
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 4855 of file SatParameters.java.

◆ getMaxPresolveIterations()

.lang.Override int getMaxPresolveIterations ( )
inline
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 4085 of file SatParameters.java.

◆ getMaxSatAssumptionOrder()

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

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

Returns
The maxSatAssumptionOrder.

Implements SatParametersOrBuilder.

Definition at line 4554 of file SatParameters.java.

◆ getMaxSatReverseAssumptionOrder()

.lang.Override boolean getMaxSatReverseAssumptionOrder ( )
inline
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 4585 of file SatParameters.java.

◆ getMaxSatStratification()

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

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

Returns
The maxSatStratification.

Implements SatParametersOrBuilder.

Definition at line 4602 of file SatParameters.java.

◆ getMaxTimeInSeconds()

.lang.Override double getMaxTimeInSeconds ( )
inline
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 3509 of file SatParameters.java.

◆ getMaxVariableActivityValue()

.lang.Override double getMaxVariableActivityValue ( )
inline

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

Returns
The maxVariableActivityValue.

Implements SatParametersOrBuilder.

Definition at line 3010 of file SatParameters.java.

◆ getMergeAtMostOneWorkLimit()

.lang.Override double getMergeAtMostOneWorkLimit ( )
inline

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns
The mergeAtMostOneWorkLimit.

Implements SatParametersOrBuilder.

Definition at line 4386 of file SatParameters.java.

◆ getMergeNoOverlapWorkLimit()

.lang.Override double getMergeNoOverlapWorkLimit ( )
inline
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 4367 of file SatParameters.java.

◆ getMinimizationAlgorithm()

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

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

Returns
The minimizationAlgorithm.

Implements SatParametersOrBuilder.

Definition at line 2663 of file SatParameters.java.

◆ getMinimizeCore()

.lang.Override boolean getMinimizeCore ( )
inline
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 4479 of file SatParameters.java.

◆ getMinimizeReductionDuringPbResolution()

.lang.Override boolean getMinimizeReductionDuringPbResolution ( )
inline
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 3835 of file SatParameters.java.

◆ getMinimizeWithPropagationNumDecisions()

.lang.Override int getMinimizeWithPropagationNumDecisions ( )
inline

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns
The minimizeWithPropagationNumDecisions.

Implements SatParametersOrBuilder.

Definition at line 2952 of file SatParameters.java.

◆ getMinimizeWithPropagationRestartPeriod()

.lang.Override int getMinimizeWithPropagationRestartPeriod ( )
inline
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 2933 of file SatParameters.java.

◆ getMinOrthogonalityForLpConstraints()

.lang.Override double getMinOrthogonalityForLpConstraints ( )
inline
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 5142 of file SatParameters.java.

◆ getMipCheckPrecision()

.lang.Override double getMipCheckPrecision ( )
inline
As explained in mip_precision and mip_max_activity_exponent, we cannot
always reach the wanted coefficient precision during scaling. When we
cannot, we will report MODEL_INVALID if the relative preicision is larger
than this parameter.

optional double mip_check_precision = 128 [default = 0.0001];

Returns
The mipCheckPrecision.

Implements SatParametersOrBuilder.

Definition at line 6617 of file SatParameters.java.

◆ getMipMaxActivityExponent()

.lang.Override int getMipMaxActivityExponent ( )
inline
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 6584 of file SatParameters.java.

◆ getMipMaxBound()

.lang.Override double getMipMaxBound ( )
inline
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 6471 of file SatParameters.java.

◆ getMipVarScaling()

.lang.Override double getMipVarScaling ( )
inline
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 6502 of file SatParameters.java.

◆ getMipWantedPrecision()

.lang.Override double getMipWantedPrecision ( )
inline
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 this relative precision on each of the
constraint (resp. objective) coefficient.
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 6545 of file SatParameters.java.

◆ getNewConstraintsBatchSize()

.lang.Override int getNewConstraintsBatchSize ( )
inline
Add that many lazy contraints (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 5306 of file SatParameters.java.

◆ getNumConflictsBeforeStrategyChanges()

.lang.Override int getNumConflictsBeforeStrategyChanges ( )
inline
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 3451 of file SatParameters.java.

◆ getNumSearchWorkers()

.lang.Override int getNumSearchWorkers ( )
inline
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 5895 of file SatParameters.java.

◆ getOnlyAddCutsAtLevelZero()

.lang.Override boolean getOnlyAddCutsAtLevelZero ( )
inline
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 4884 of file SatParameters.java.

◆ getOptimizeWithCore()

.lang.Override boolean getOptimizeWithCore ( )
inline
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 5598 of file SatParameters.java.

◆ getOptimizeWithMaxHs()

.lang.Override boolean getOptimizeWithMaxHs ( )
inline
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 5668 of file SatParameters.java.

◆ getParserForType()

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

Definition at line 19236 of file SatParameters.java.

◆ getPbCleanupIncrement()

.lang.Override int getPbCleanupIncrement ( )
inline
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 2867 of file SatParameters.java.

◆ getPbCleanupRatio()

.lang.Override double getPbCleanupRatio ( )
inline

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns
The pbCleanupRatio.

Implements SatParametersOrBuilder.

Definition at line 2886 of file SatParameters.java.

◆ getPreferredVariableOrder()

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

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

Returns
The preferredVariableOrder.

Implements SatParametersOrBuilder.

Definition at line 2419 of file SatParameters.java.

◆ getPresolveBlockedClause()

.lang.Override boolean getPresolveBlockedClause ( )
inline
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 3994 of file SatParameters.java.

◆ getPresolveBvaThreshold()

.lang.Override int getPresolveBvaThreshold ( )
inline
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 4054 of file SatParameters.java.

◆ getPresolveBveClauseWeight()

.lang.Override int getPresolveBveClauseWeight ( )
inline
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 3936 of file SatParameters.java.

◆ getPresolveBveThreshold()

.lang.Override int getPresolveBveThreshold ( )
inline
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 3907 of file SatParameters.java.

◆ getPresolveProbingDeterministicTimeLimit()

.lang.Override double getPresolveProbingDeterministicTimeLimit ( )
inline
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 3965 of file SatParameters.java.

◆ getPresolveSubstitutionLevel()

.lang.Override int getPresolveSubstitutionLevel ( )
inline
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 4419 of file SatParameters.java.

◆ getPresolveUseBva()

.lang.Override boolean getPresolveUseBva ( )
inline
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 4021 of file SatParameters.java.

◆ getProbingPeriodAtRoot()

.lang.Override long getProbingPeriodAtRoot ( )
inline
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 5536 of file SatParameters.java.

◆ getPseudoCostReliabilityThreshold()

.lang.Override long getPseudoCostReliabilityThreshold ( )
inline
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 5565 of file SatParameters.java.

◆ getRandomBranchesRatio()

.lang.Override double getRandomBranchesRatio ( )
inline
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 2545 of file SatParameters.java.

◆ getRandomizeSearch()

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

optional bool randomize_search = 103 [default = false];

Returns
The randomizeSearch.

Implements SatParametersOrBuilder.

Definition at line 6213 of file SatParameters.java.

◆ getRandomPolarityRatio()

.lang.Override double getRandomPolarityRatio ( )
inline
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 2514 of file SatParameters.java.

◆ getRandomSeed()

.lang.Override int getRandomSeed ( )
inline
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 3742 of file SatParameters.java.

◆ getReduceMemoryUsageInInterleaveMode()

.lang.Override boolean getReduceMemoryUsageInInterleaveMode ( )
inline
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 5976 of file SatParameters.java.

◆ getRelativeGapLimit()

.lang.Override double getRelativeGapLimit ( )
inline

optional double relative_gap_limit = 160 [default = 0];

Returns
The relativeGapLimit.

Implements SatParametersOrBuilder.

Definition at line 3674 of file SatParameters.java.

◆ getRestartAlgorithms()

.lang.Override com.google.ortools.sat.SatParameters.RestartAlgorithm getRestartAlgorithms ( int  index)
inline
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 3199 of file SatParameters.java.

◆ getRestartAlgorithmsCount()

.lang.Override int getRestartAlgorithmsCount ( )
inline
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 3179 of file SatParameters.java.

◆ getRestartAlgorithmsList()

.lang.Override java.util.List<com.google.ortools.sat.SatParameters.RestartAlgorithm> getRestartAlgorithmsList ( )
inline
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 3159 of file SatParameters.java.

◆ getRestartDlAverageRatio()

.lang.Override double getRestartDlAverageRatio ( )
inline
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 3332 of file SatParameters.java.

◆ getRestartLbdAverageRatio()

.lang.Override double getRestartLbdAverageRatio ( )
inline

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns
The restartLbdAverageRatio.

Implements SatParametersOrBuilder.

Definition at line 3351 of file SatParameters.java.

◆ getRestartPeriod()

.lang.Override int getRestartPeriod ( )
inline
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 3276 of file SatParameters.java.

◆ getRestartRunningWindowSize()

.lang.Override int getRestartRunningWindowSize ( )
inline
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 3303 of file SatParameters.java.

◆ getSearchBranching()

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

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

Returns
The searchBranching.

Implements SatParametersOrBuilder.

Definition at line 5323 of file SatParameters.java.

◆ getSearchRandomizationTolerance()

.lang.Override long getSearchRandomizationTolerance ( )
inline
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 6252 of file SatParameters.java.

◆ getSerializedSize()

.lang.Override int getSerializedSize ( )
inline

Definition at line 7062 of file SatParameters.java.

◆ getShareLevelZeroBounds()

.lang.Override boolean getShareLevelZeroBounds ( )
inline
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 6030 of file SatParameters.java.

◆ getShareObjectiveBounds()

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

optional bool share_objective_bounds = 113 [default = true];

Returns
The shareObjectiveBounds.

Implements SatParametersOrBuilder.

Definition at line 6003 of file SatParameters.java.

◆ getStopAfterFirstSolution()

.lang.Override boolean getStopAfterFirstSolution ( )
inline
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 5829 of file SatParameters.java.

◆ getStopAfterPresolve()

.lang.Override boolean getStopAfterPresolve ( )
inline
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 5858 of file SatParameters.java.

◆ getStrategyChangeIncreaseRatio()

.lang.Override double getStrategyChangeIncreaseRatio ( )
inline
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 3480 of file SatParameters.java.

◆ getSubsumptionDuringConflictAnalysis()

.lang.Override boolean getSubsumptionDuringConflictAnalysis ( )
inline
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 2717 of file SatParameters.java.

◆ getTreatBinaryClausesSeparately()

.lang.Override boolean getTreatBinaryClausesSeparately ( )
inline
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 3705 of file SatParameters.java.

◆ getUnknownFields()

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

Definition at line 136 of file SatParameters.java.

◆ getUseBlockingRestart()

.lang.Override boolean getUseBlockingRestart ( )
inline
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 3382 of file SatParameters.java.

◆ getUseBranchingInLp()

.lang.Override boolean getUseBranchingInLp ( )
inline
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 6347 of file SatParameters.java.

◆ getUseCombinedNoOverlap()

.lang.Override boolean getUseCombinedNoOverlap ( )
inline
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 6378 of file SatParameters.java.

◆ getUseDisjunctiveConstraintInCumulativeConstraint()

.lang.Override boolean getUseDisjunctiveConstraintInCumulativeConstraint ( )
inline
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 4760 of file SatParameters.java.

◆ getUseErwaHeuristic()

.lang.Override boolean getUseErwaHeuristic ( )
inline
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 2576 of file SatParameters.java.

◆ getUseExactLpReason()

.lang.Override boolean getUseExactLpReason ( )
inline
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 6316 of file SatParameters.java.

◆ getUseFeasibilityPump()

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

optional bool use_feasibility_pump = 164 [default = false];

Returns
The useFeasibilityPump.

Implements SatParametersOrBuilder.

Definition at line 6130 of file SatParameters.java.

◆ getUseImpliedBounds()

.lang.Override boolean getUseImpliedBounds ( )
inline
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 6440 of file SatParameters.java.

◆ getUseLnsOnly()

.lang.Override boolean getUseLnsOnly ( )
inline
LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns
The useLnsOnly.

Implements SatParametersOrBuilder.

Definition at line 6057 of file SatParameters.java.

◆ getUseOptimizationHints()

.lang.Override boolean getUseOptimizationHints ( )
inline
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 4452 of file SatParameters.java.

◆ getUseOptionalVariables()

.lang.Override boolean getUseOptionalVariables ( )
inline
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 6283 of file SatParameters.java.

◆ getUseOverloadCheckerInCumulativeConstraint()

.lang.Override boolean getUseOverloadCheckerInCumulativeConstraint ( )
inline
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 4682 of file SatParameters.java.

◆ getUsePbResolution()

.lang.Override boolean getUsePbResolution ( )
inline
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 3802 of file SatParameters.java.

◆ getUsePhaseSaving()

.lang.Override boolean getUsePhaseSaving ( )
inline
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().
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 2479 of file SatParameters.java.

◆ getUsePrecedencesInDisjunctiveConstraint()

.lang.Override boolean getUsePrecedencesInDisjunctiveConstraint ( )
inline
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 4645 of file SatParameters.java.

◆ getUseRelaxationLns()

.lang.Override boolean getUseRelaxationLns ( )
inline
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 6159 of file SatParameters.java.

◆ getUseRinsLns()

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

optional bool use_rins_lns = 129 [default = true];

Returns
The useRinsLns.

Implements SatParametersOrBuilder.

Definition at line 6103 of file SatParameters.java.

◆ getUseSatInprocessing()

.lang.Override boolean getUseSatInprocessing ( )
inline

optional bool use_sat_inprocessing = 163 [default = false];

Returns
The useSatInprocessing.

Implements SatParametersOrBuilder.

Definition at line 4247 of file SatParameters.java.

◆ getUseTimetableEdgeFindingInCumulativeConstraint()

.lang.Override boolean getUseTimetableEdgeFindingInCumulativeConstraint ( )
inline
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 4719 of file SatParameters.java.

◆ getVariableActivityDecay()

.lang.Override double getVariableActivityDecay ( )
inline
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 2991 of file SatParameters.java.

◆ hasAbsoluteGapLimit()

.lang.Override boolean hasAbsoluteGapLimit ( )
inline
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 3634 of file SatParameters.java.

◆ hasAddCgCuts()

.lang.Override boolean hasAddCgCuts ( )
inline
Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
Note that for now, this is not heavily tunned.

optional bool add_cg_cuts = 117 [default = true];

Returns
Whether the addCgCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 4931 of file SatParameters.java.

◆ hasAddKnapsackCuts()

.lang.Override boolean hasAddKnapsackCuts ( )
inline
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 4901 of file SatParameters.java.

◆ hasAddLinMaxCuts()

.lang.Override boolean hasAddLinMaxCuts ( )
inline
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 5021 of file SatParameters.java.

◆ hasAddLpConstraintsLazily()

.lang.Override boolean hasAddLpConstraintsLazily ( )
inline
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 5092 of file SatParameters.java.

◆ hasAddMirCuts()

.lang.Override boolean hasAddMirCuts ( )
inline
Whether we generate MIR cuts at root node.
Note that for now, this is not heavily tunned.

optional bool add_mir_cuts = 120 [default = true];

Returns
Whether the addMirCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 4960 of file SatParameters.java.

◆ hasAlsoBumpVariablesInConflictReasons()

.lang.Override boolean hasAlsoBumpVariablesInConflictReasons ( )
inline
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 2631 of file SatParameters.java.

◆ hasAutoDetectGreaterThanAtLeastOneOf()

.lang.Override boolean hasAutoDetectGreaterThanAtLeastOneOf ( )
inline
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 5787 of file SatParameters.java.

◆ hasBinaryMinimizationAlgorithm()

.lang.Override boolean hasBinaryMinimizationAlgorithm ( )
inline

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 2675 of file SatParameters.java.

◆ hasBinarySearchNumConflicts()

.lang.Override boolean hasBinarySearchNumConflicts ( )
inline
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 5616 of file SatParameters.java.

◆ hasBlockingRestartMultiplier()

.lang.Override boolean hasBlockingRestartMultiplier ( )
inline

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns
Whether the blockingRestartMultiplier field is set.

Implements SatParametersOrBuilder.

Definition at line 3412 of file SatParameters.java.

◆ hasBlockingRestartWindowSize()

.lang.Override boolean hasBlockingRestartWindowSize ( )
inline

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns
Whether the blockingRestartWindowSize field is set.

Implements SatParametersOrBuilder.

Definition at line 3393 of file SatParameters.java.

◆ hasBooleanEncodingLevel()

.lang.Override boolean hasBooleanEncodingLevel ( )
inline
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 4809 of file SatParameters.java.

◆ hasCatchSigintSignal()

.lang.Override boolean hasCatchSigintSignal ( )
inline
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 6395 of file SatParameters.java.

◆ hasClauseActivityDecay()

.lang.Override boolean hasClauseActivityDecay ( )
inline
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 3096 of file SatParameters.java.

◆ hasClauseCleanupLbdBound()

.lang.Override boolean hasClauseCleanupLbdBound ( )
inline
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 2808 of file SatParameters.java.

◆ hasClauseCleanupOrdering()

.lang.Override boolean hasClauseCleanupOrdering ( )
inline

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 2831 of file SatParameters.java.

◆ hasClauseCleanupPeriod()

.lang.Override boolean hasClauseCleanupPeriod ( )
inline
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 2732 of file SatParameters.java.

◆ hasClauseCleanupProtection()

.lang.Override boolean hasClauseCleanupProtection ( )
inline

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 2783 of file SatParameters.java.

◆ hasClauseCleanupTarget()

.lang.Override boolean hasClauseCleanupTarget ( )
inline
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 2760 of file SatParameters.java.

◆ hasCountAssumptionLevelsInLbd()

.lang.Override boolean hasCountAssumptionLevelsInLbd ( )
inline
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 3857 of file SatParameters.java.

◆ hasCoverOptimization()

.lang.Override boolean hasCoverOptimization ( )
inline
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 4524 of file SatParameters.java.

◆ hasCpModelMaxNumPresolveOperations()

.lang.Override boolean hasCpModelMaxNumPresolveOperations ( )
inline
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 4161 of file SatParameters.java.

◆ hasCpModelPostsolveWithFullSolver()

.lang.Override boolean hasCpModelPostsolveWithFullSolver ( )
inline
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 4130 of file SatParameters.java.

◆ hasCpModelPresolve()

.lang.Override boolean hasCpModelPresolve ( )
inline
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 4100 of file SatParameters.java.

◆ hasCpModelProbingLevel()

.lang.Override boolean hasCpModelProbingLevel ( )
inline
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 4189 of file SatParameters.java.

◆ hasCpModelUseSatPresolve()

.lang.Override boolean hasCpModelUseSatPresolve ( )
inline
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 4216 of file SatParameters.java.

◆ hasCutActiveCountDecay()

.lang.Override boolean hasCutActiveCountDecay ( )
inline

optional double cut_active_count_decay = 156 [default = 0.8];

Returns
Whether the cutActiveCountDecay field is set.

Implements SatParametersOrBuilder.

Definition at line 5242 of file SatParameters.java.

◆ hasCutCleanupTarget()

.lang.Override boolean hasCutCleanupTarget ( )
inline
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 5265 of file SatParameters.java.

◆ hasCutMaxActiveCountValue()

.lang.Override boolean hasCutMaxActiveCountValue ( )
inline
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 5217 of file SatParameters.java.

◆ hasDefaultRestartAlgorithms()

.lang.Override boolean hasDefaultRestartAlgorithms ( )
inline

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 3210 of file SatParameters.java.

◆ hasDiversifyLnsParams()

.lang.Override boolean hasDiversifyLnsParams ( )
inline
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 6174 of file SatParameters.java.

◆ hasEnumerateAllSolutions()

.lang.Override boolean hasEnumerateAllSolutions ( )
inline
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): Activate the presolve but with just the rules that do not
change the set of feasible solutions.

optional bool enumerate_all_solutions = 87 [default = false];

Returns
Whether the enumerateAllSolutions field is set.

Implements SatParametersOrBuilder.

Definition at line 5688 of file SatParameters.java.

◆ hasExpandAutomatonConstraints()

.lang.Override boolean hasExpandAutomatonConstraints ( )
inline
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 4291 of file SatParameters.java.

◆ hasExpandElementConstraints()

.lang.Override boolean hasExpandElementConstraints ( )
inline
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 4263 of file SatParameters.java.

◆ hasExpandTableConstraints()

.lang.Override boolean hasExpandTableConstraints ( )
inline
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 4319 of file SatParameters.java.

◆ hasExploitAllLpSolution()

.lang.Override boolean hasExploitAllLpSolution ( )
inline
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 5404 of file SatParameters.java.

◆ hasExploitBestSolution()

.lang.Override boolean hasExploitBestSolution ( )
inline
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 5433 of file SatParameters.java.

◆ hasExploitIntegerLpSolution()

.lang.Override boolean hasExploitIntegerLpSolution ( )
inline
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 5372 of file SatParameters.java.

◆ hasExploitObjective()

.lang.Override boolean hasExploitObjective ( )
inline
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 5492 of file SatParameters.java.

◆ hasExploitRelaxationSolution()

.lang.Override boolean hasExploitRelaxationSolution ( )
inline
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 5462 of file SatParameters.java.

◆ hasFillTightenedDomainsInResponse()

.lang.Override boolean hasFillTightenedDomainsInResponse ( )
inline
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 5724 of file SatParameters.java.

◆ hasFindMultipleCores()

.lang.Override boolean hasFindMultipleCores ( )
inline
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 4495 of file SatParameters.java.

◆ hasGlucoseDecayIncrement()

.lang.Override boolean hasGlucoseDecayIncrement ( )
inline

optional double glucose_decay_increment = 23 [default = 0.01];

Returns
Whether the glucoseDecayIncrement field is set.

Implements SatParametersOrBuilder.

Definition at line 3054 of file SatParameters.java.

◆ hasGlucoseDecayIncrementPeriod()

.lang.Override boolean hasGlucoseDecayIncrementPeriod ( )
inline

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns
Whether the glucoseDecayIncrementPeriod field is set.

Implements SatParametersOrBuilder.

Definition at line 3073 of file SatParameters.java.

◆ hasGlucoseMaxDecay()

.lang.Override boolean hasGlucoseMaxDecay ( )
inline
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 3028 of file SatParameters.java.

◆ hashCode()

.lang.Override int hashCode ( )
inline

Definition at line 8375 of file SatParameters.java.

◆ hasHintConflictLimit()

.lang.Override boolean hasHintConflictLimit ( )
inline
When we try to follow the hint, we do a FIXED_SEARCH using the hint until
this number of conflict is reached.

optional int32 hint_conflict_limit = 153 [default = 10];

Returns
Whether the hintConflictLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 5341 of file SatParameters.java.

◆ hasInitialPolarity()

.lang.Override boolean hasInitialPolarity ( )
inline

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

Returns
Whether the initialPolarity field is set.

Implements SatParametersOrBuilder.

Definition at line 2431 of file SatParameters.java.

◆ hasInitialVariablesActivity()

.lang.Override boolean hasInitialVariablesActivity ( )
inline
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 2596 of file SatParameters.java.

◆ hasInstantiateAllVariables()

.lang.Override boolean hasInstantiateAllVariables ( )
inline
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 5756 of file SatParameters.java.

◆ hasInterleaveBatchSize()

.lang.Override boolean hasInterleaveBatchSize ( )
inline

optional int32 interleave_batch_size = 134 [default = 1];

Returns
Whether the interleaveBatchSize field is set.

Implements SatParametersOrBuilder.

Definition at line 5941 of file SatParameters.java.

◆ hasInterleaveSearch()

.lang.Override boolean hasInterleaveSearch ( )
inline
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 5914 of file SatParameters.java.

◆ hasLinearizationLevel()

.lang.Override boolean hasLinearizationLevel ( )
inline
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 4778 of file SatParameters.java.

◆ hasLnsFocusOnDecisionVariables()

.lang.Override boolean hasLnsFocusOnDecisionVariables ( )
inline

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns
Whether the lnsFocusOnDecisionVariables field is set.

Implements SatParametersOrBuilder.

Definition at line 6068 of file SatParameters.java.

◆ hasLogSearchProgress()

.lang.Override boolean hasLogSearchProgress ( )
inline
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 3757 of file SatParameters.java.

◆ hasMaxAllDiffCutSize()

.lang.Override boolean hasMaxAllDiffCutSize ( )
inline
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 4990 of file SatParameters.java.

◆ hasMaxClauseActivityValue()

.lang.Override boolean hasMaxClauseActivityValue ( )
inline

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

Returns
Whether the maxClauseActivityValue field is set.

Implements SatParametersOrBuilder.

Definition at line 3119 of file SatParameters.java.

◆ hasMaxConsecutiveInactiveCount()

.lang.Override boolean hasMaxConsecutiveInactiveCount ( )
inline
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 5186 of file SatParameters.java.

◆ hasMaxCutRoundsAtLevelZero()

.lang.Override boolean hasMaxCutRoundsAtLevelZero ( )
inline
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 5157 of file SatParameters.java.

◆ hasMaxDeterministicTime()

.lang.Override boolean hasMaxDeterministicTime ( )
inline
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 3526 of file SatParameters.java.

◆ hasMaxIntegerRoundingScaling()

.lang.Override boolean hasMaxIntegerRoundingScaling ( )
inline
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 5056 of file SatParameters.java.

◆ hasMaxMemoryInMb()

.lang.Override boolean hasMaxMemoryInMb ( )
inline
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 3595 of file SatParameters.java.

◆ hasMaxNumberOfConflicts()

.lang.Override boolean hasMaxNumberOfConflicts ( )
inline
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 3560 of file SatParameters.java.

◆ hasMaxNumCuts()

.lang.Override boolean hasMaxNumCuts ( )
inline
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 4840 of file SatParameters.java.

◆ hasMaxPresolveIterations()

.lang.Override boolean hasMaxPresolveIterations ( )
inline
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 4071 of file SatParameters.java.

◆ hasMaxSatAssumptionOrder()

.lang.Override boolean hasMaxSatAssumptionOrder ( )
inline

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 4547 of file SatParameters.java.

◆ hasMaxSatReverseAssumptionOrder()

.lang.Override boolean hasMaxSatReverseAssumptionOrder ( )
inline
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 4572 of file SatParameters.java.

◆ hasMaxSatStratification()

.lang.Override boolean hasMaxSatStratification ( )
inline

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 4595 of file SatParameters.java.

◆ hasMaxTimeInSeconds()

.lang.Override boolean hasMaxTimeInSeconds ( )
inline
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 3496 of file SatParameters.java.

◆ hasMaxVariableActivityValue()

.lang.Override boolean hasMaxVariableActivityValue ( )
inline

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

Returns
Whether the maxVariableActivityValue field is set.

Implements SatParametersOrBuilder.

Definition at line 3002 of file SatParameters.java.

◆ hasMergeAtMostOneWorkLimit()

.lang.Override boolean hasMergeAtMostOneWorkLimit ( )
inline

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns
Whether the mergeAtMostOneWorkLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 4378 of file SatParameters.java.

◆ hasMergeNoOverlapWorkLimit()

.lang.Override boolean hasMergeNoOverlapWorkLimit ( )
inline
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 4351 of file SatParameters.java.

◆ hasMinimizationAlgorithm()

.lang.Override boolean hasMinimizationAlgorithm ( )
inline

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

Returns
Whether the minimizationAlgorithm field is set.

Implements SatParametersOrBuilder.

Definition at line 2656 of file SatParameters.java.

◆ hasMinimizeCore()

.lang.Override boolean hasMinimizeCore ( )
inline
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 4467 of file SatParameters.java.

◆ hasMinimizeReductionDuringPbResolution()

.lang.Override boolean hasMinimizeReductionDuringPbResolution ( )
inline
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 3820 of file SatParameters.java.

◆ hasMinimizeWithPropagationNumDecisions()

.lang.Override boolean hasMinimizeWithPropagationNumDecisions ( )
inline

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns
Whether the minimizeWithPropagationNumDecisions field is set.

Implements SatParametersOrBuilder.

Definition at line 2944 of file SatParameters.java.

◆ hasMinimizeWithPropagationRestartPeriod()

.lang.Override boolean hasMinimizeWithPropagationRestartPeriod ( )
inline
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 2911 of file SatParameters.java.

◆ hasMinOrthogonalityForLpConstraints()

.lang.Override boolean hasMinOrthogonalityForLpConstraints ( )
inline
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 5126 of file SatParameters.java.

◆ hasMipCheckPrecision()

.lang.Override boolean hasMipCheckPrecision ( )
inline
As explained in mip_precision and mip_max_activity_exponent, we cannot
always reach the wanted coefficient precision during scaling. When we
cannot, we will report MODEL_INVALID if the relative preicision is larger
than this parameter.

optional double mip_check_precision = 128 [default = 0.0001];

Returns
Whether the mipCheckPrecision field is set.

Implements SatParametersOrBuilder.

Definition at line 6602 of file SatParameters.java.

◆ hasMipMaxActivityExponent()

.lang.Override boolean hasMipMaxActivityExponent ( )
inline
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 6566 of file SatParameters.java.

◆ hasMipMaxBound()

.lang.Override boolean hasMipMaxBound ( )
inline
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 6457 of file SatParameters.java.

◆ hasMipVarScaling()

.lang.Override boolean hasMipVarScaling ( )
inline
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 6488 of file SatParameters.java.

◆ hasMipWantedPrecision()

.lang.Override boolean hasMipWantedPrecision ( )
inline
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 this relative precision on each of the
constraint (resp. objective) coefficient.
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 6525 of file SatParameters.java.

◆ hasNewConstraintsBatchSize()

.lang.Override boolean hasNewConstraintsBatchSize ( )
inline
Add that many lazy contraints (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 5293 of file SatParameters.java.

◆ hasNumConflictsBeforeStrategyChanges()

.lang.Override boolean hasNumConflictsBeforeStrategyChanges ( )
inline
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 3437 of file SatParameters.java.

◆ hasNumSearchWorkers()

.lang.Override boolean hasNumSearchWorkers ( )
inline
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 5878 of file SatParameters.java.

◆ hasOnlyAddCutsAtLevelZero()

.lang.Override boolean hasOnlyAddCutsAtLevelZero ( )
inline
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 4871 of file SatParameters.java.

◆ hasOptimizeWithCore()

.lang.Override boolean hasOptimizeWithCore ( )
inline
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 5583 of file SatParameters.java.

◆ hasOptimizeWithMaxHs()

.lang.Override boolean hasOptimizeWithMaxHs ( )
inline
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 5651 of file SatParameters.java.

◆ hasPbCleanupIncrement()

.lang.Override boolean hasPbCleanupIncrement ( )
inline
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 2855 of file SatParameters.java.

◆ hasPbCleanupRatio()

.lang.Override boolean hasPbCleanupRatio ( )
inline

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns
Whether the pbCleanupRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 2878 of file SatParameters.java.

◆ hasPreferredVariableOrder()

.lang.Override boolean hasPreferredVariableOrder ( )
inline

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 2412 of file SatParameters.java.

◆ hasPresolveBlockedClause()

.lang.Override boolean hasPresolveBlockedClause ( )
inline
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 3981 of file SatParameters.java.

◆ hasPresolveBvaThreshold()

.lang.Override boolean hasPresolveBvaThreshold ( )
inline
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 4039 of file SatParameters.java.

◆ hasPresolveBveClauseWeight()

.lang.Override boolean hasPresolveBveClauseWeight ( )
inline
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 3923 of file SatParameters.java.

◆ hasPresolveBveThreshold()

.lang.Override boolean hasPresolveBveThreshold ( )
inline
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 3893 of file SatParameters.java.

◆ hasPresolveProbingDeterministicTimeLimit()

.lang.Override boolean hasPresolveProbingDeterministicTimeLimit ( )
inline
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 3952 of file SatParameters.java.

◆ hasPresolveSubstitutionLevel()

.lang.Override boolean hasPresolveSubstitutionLevel ( )
inline
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 4404 of file SatParameters.java.

◆ hasPresolveUseBva()

.lang.Override boolean hasPresolveUseBva ( )
inline
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 4009 of file SatParameters.java.

◆ hasProbingPeriodAtRoot()

.lang.Override boolean hasProbingPeriodAtRoot ( )
inline
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 5522 of file SatParameters.java.

◆ hasPseudoCostReliabilityThreshold()

.lang.Override boolean hasPseudoCostReliabilityThreshold ( )
inline
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 5552 of file SatParameters.java.

◆ hasRandomBranchesRatio()

.lang.Override boolean hasRandomBranchesRatio ( )
inline
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 2531 of file SatParameters.java.

◆ hasRandomizeSearch()

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

optional bool randomize_search = 103 [default = false];

Returns
Whether the randomizeSearch field is set.

Implements SatParametersOrBuilder.

Definition at line 6201 of file SatParameters.java.

◆ hasRandomPolarityRatio()

.lang.Override boolean hasRandomPolarityRatio ( )
inline
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 2498 of file SatParameters.java.

◆ hasRandomSeed()

.lang.Override boolean hasRandomSeed ( )
inline
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 3725 of file SatParameters.java.

◆ hasReduceMemoryUsageInInterleaveMode()

.lang.Override boolean hasReduceMemoryUsageInInterleaveMode ( )
inline
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 5964 of file SatParameters.java.

◆ hasRelativeGapLimit()

.lang.Override boolean hasRelativeGapLimit ( )
inline

optional double relative_gap_limit = 160 [default = 0];

Returns
Whether the relativeGapLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 3666 of file SatParameters.java.

◆ hasRestartDlAverageRatio()

.lang.Override boolean hasRestartDlAverageRatio ( )
inline
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 3319 of file SatParameters.java.

◆ hasRestartLbdAverageRatio()

.lang.Override boolean hasRestartLbdAverageRatio ( )
inline

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns
Whether the restartLbdAverageRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 3343 of file SatParameters.java.

◆ hasRestartPeriod()

.lang.Override boolean hasRestartPeriod ( )
inline
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 3263 of file SatParameters.java.

◆ hasRestartRunningWindowSize()

.lang.Override boolean hasRestartRunningWindowSize ( )
inline
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 3291 of file SatParameters.java.

◆ hasSearchBranching()

.lang.Override boolean hasSearchBranching ( )
inline

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

Returns
Whether the searchBranching field is set.

Implements SatParametersOrBuilder.

Definition at line 5316 of file SatParameters.java.

◆ hasSearchRandomizationTolerance()

.lang.Override boolean hasSearchRandomizationTolerance ( )
inline
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 6234 of file SatParameters.java.

◆ hasShareLevelZeroBounds()

.lang.Override boolean hasShareLevelZeroBounds ( )
inline
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 6018 of file SatParameters.java.

◆ hasShareObjectiveBounds()

.lang.Override boolean hasShareObjectiveBounds ( )
inline
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 5991 of file SatParameters.java.

◆ hasStopAfterFirstSolution()

.lang.Override boolean hasStopAfterFirstSolution ( )
inline
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 5817 of file SatParameters.java.

◆ hasStopAfterPresolve()

.lang.Override boolean hasStopAfterPresolve ( )
inline
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 5845 of file SatParameters.java.

◆ hasStrategyChangeIncreaseRatio()

.lang.Override boolean hasStrategyChangeIncreaseRatio ( )
inline
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 3467 of file SatParameters.java.

◆ hasSubsumptionDuringConflictAnalysis()

.lang.Override boolean hasSubsumptionDuringConflictAnalysis ( )
inline
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 2702 of file SatParameters.java.

◆ hasTreatBinaryClausesSeparately()

.lang.Override boolean hasTreatBinaryClausesSeparately ( )
inline
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 3691 of file SatParameters.java.

◆ hasUseBlockingRestart()

.lang.Override boolean hasUseBlockingRestart ( )
inline
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 3368 of file SatParameters.java.

◆ hasUseBranchingInLp()

.lang.Override boolean hasUseBranchingInLp ( )
inline
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 6333 of file SatParameters.java.

◆ hasUseCombinedNoOverlap()

.lang.Override boolean hasUseCombinedNoOverlap ( )
inline
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 6364 of file SatParameters.java.

◆ hasUseDisjunctiveConstraintInCumulativeConstraint()

.lang.Override boolean hasUseDisjunctiveConstraintInCumulativeConstraint ( )
inline
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 4741 of file SatParameters.java.

◆ hasUseErwaHeuristic()

.lang.Override boolean hasUseErwaHeuristic ( )
inline
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 2562 of file SatParameters.java.

◆ hasUseExactLpReason()

.lang.Override boolean hasUseExactLpReason ( )
inline
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 6301 of file SatParameters.java.

◆ hasUseFeasibilityPump()

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

optional bool use_feasibility_pump = 164 [default = false];

Returns
Whether the useFeasibilityPump field is set.

Implements SatParametersOrBuilder.

Definition at line 6118 of file SatParameters.java.

◆ hasUseImpliedBounds()

.lang.Override boolean hasUseImpliedBounds ( )
inline
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 6426 of file SatParameters.java.

◆ hasUseLnsOnly()

.lang.Override boolean hasUseLnsOnly ( )
inline
LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns
Whether the useLnsOnly field is set.

Implements SatParametersOrBuilder.

Definition at line 6045 of file SatParameters.java.

◆ hasUseOptimizationHints()

.lang.Override boolean hasUseOptimizationHints ( )
inline
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 4437 of file SatParameters.java.

◆ hasUseOptionalVariables()

.lang.Override boolean hasUseOptionalVariables ( )
inline
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 6269 of file SatParameters.java.

◆ hasUseOverloadCheckerInCumulativeConstraint()

.lang.Override boolean hasUseOverloadCheckerInCumulativeConstraint ( )
inline
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 4665 of file SatParameters.java.

◆ hasUsePbResolution()

.lang.Override boolean hasUsePbResolution ( )
inline
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 3787 of file SatParameters.java.

◆ hasUsePhaseSaving()

.lang.Override boolean hasUsePhaseSaving ( )
inline
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().
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 2461 of file SatParameters.java.

◆ hasUsePrecedencesInDisjunctiveConstraint()

.lang.Override boolean hasUsePrecedencesInDisjunctiveConstraint ( )
inline
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 4626 of file SatParameters.java.

◆ hasUseRelaxationLns()

.lang.Override boolean hasUseRelaxationLns ( )
inline
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 6146 of file SatParameters.java.

◆ hasUseRinsLns()

.lang.Override boolean hasUseRinsLns ( )
inline
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 6091 of file SatParameters.java.

◆ hasUseSatInprocessing()

.lang.Override boolean hasUseSatInprocessing ( )
inline

optional bool use_sat_inprocessing = 163 [default = false];

Returns
Whether the useSatInprocessing field is set.

Implements SatParametersOrBuilder.

Definition at line 4239 of file SatParameters.java.

◆ hasUseTimetableEdgeFindingInCumulativeConstraint()

.lang.Override boolean hasUseTimetableEdgeFindingInCumulativeConstraint ( )
inline
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 4702 of file SatParameters.java.

◆ hasVariableActivityDecay()

.lang.Override boolean hasVariableActivityDecay ( )
inline
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 2973 of file SatParameters.java.

◆ internalGetFieldAccessorTable()

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

Definition at line 990 of file SatParameters.java.

◆ isInitialized()

.lang.Override final boolean isInitialized ( )
inline

Definition at line 6623 of file SatParameters.java.

◆ newBuilder() [1/2]

static Builder newBuilder ( )
inlinestatic

Definition at line 9119 of file SatParameters.java.

◆ newBuilder() [2/2]

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

Definition at line 9122 of file SatParameters.java.

◆ newBuilderForType() [1/2]

.lang.Override Builder newBuilderForType ( )
inline

Definition at line 9118 of file SatParameters.java.

◆ newBuilderForType() [2/2]

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

Definition at line 9132 of file SatParameters.java.

◆ newInstance()

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

Definition at line 129 of file SatParameters.java.

◆ parseDelimitedFrom() [1/2]

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

Definition at line 9091 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
inlinestatic

Definition at line 9096 of file SatParameters.java.

◆ parseFrom() [1/10]

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

Definition at line 9069 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
inlinestatic

Definition at line 9073 of file SatParameters.java.

◆ parseFrom() [3/10]

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

Definition at line 9058 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
inlinestatic

Definition at line 9063 of file SatParameters.java.

◆ parseFrom() [5/10]

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

Definition at line 9103 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
inlinestatic

Definition at line 9109 of file SatParameters.java.

◆ parseFrom() [7/10]

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

Definition at line 9079 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
inlinestatic

Definition at line 9084 of file SatParameters.java.

◆ parseFrom() [9/10]

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

Definition at line 9047 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
inlinestatic

Definition at line 9052 of file SatParameters.java.

◆ parser()

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

Definition at line 19231 of file SatParameters.java.

◆ toBuilder()

.lang.Override Builder toBuilder ( )
inline

Definition at line 9126 of file SatParameters.java.

◆ writeTo()

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

Definition at line 6633 of file SatParameters.java.

Member Data Documentation

◆ ABSOLUTE_GAP_LIMIT_FIELD_NUMBER

final int ABSOLUTE_GAP_LIMIT_FIELD_NUMBER = 159
static

Definition at line 3614 of file SatParameters.java.

◆ ADD_CG_CUTS_FIELD_NUMBER

final int ADD_CG_CUTS_FIELD_NUMBER = 117
static

Definition at line 4919 of file SatParameters.java.

◆ ADD_KNAPSACK_CUTS_FIELD_NUMBER

final int ADD_KNAPSACK_CUTS_FIELD_NUMBER = 111
static

Definition at line 4888 of file SatParameters.java.

◆ ADD_LIN_MAX_CUTS_FIELD_NUMBER

final int ADD_LIN_MAX_CUTS_FIELD_NUMBER = 152
static

Definition at line 5008 of file SatParameters.java.

◆ ADD_LP_CONSTRAINTS_LAZILY_FIELD_NUMBER

final int ADD_LP_CONSTRAINTS_LAZILY_FIELD_NUMBER = 112
static

Definition at line 5078 of file SatParameters.java.

◆ ADD_MIR_CUTS_FIELD_NUMBER

final int ADD_MIR_CUTS_FIELD_NUMBER = 120
static

Definition at line 4948 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 2617 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 5773 of file SatParameters.java.

◆ BINARY_MINIMIZATION_ALGORITHM_FIELD_NUMBER

final int BINARY_MINIMIZATION_ALGORITHM_FIELD_NUMBER = 34
static

Definition at line 2669 of file SatParameters.java.

◆ BINARY_SEARCH_NUM_CONFLICTS_FIELD_NUMBER

final int BINARY_SEARCH_NUM_CONFLICTS_FIELD_NUMBER = 99
static

Definition at line 5602 of file SatParameters.java.

◆ BLOCKING_RESTART_MULTIPLIER_FIELD_NUMBER

final int BLOCKING_RESTART_MULTIPLIER_FIELD_NUMBER = 66
static

Definition at line 3405 of file SatParameters.java.

◆ BLOCKING_RESTART_WINDOW_SIZE_FIELD_NUMBER

final int BLOCKING_RESTART_WINDOW_SIZE_FIELD_NUMBER = 65
static

Definition at line 3386 of file SatParameters.java.

◆ BOOLEAN_ENCODING_LEVEL_FIELD_NUMBER

final int BOOLEAN_ENCODING_LEVEL_FIELD_NUMBER = 107
static

Definition at line 4797 of file SatParameters.java.

◆ CATCH_SIGINT_SIGNAL_FIELD_NUMBER

final int CATCH_SIGINT_SIGNAL_FIELD_NUMBER = 135
static

Definition at line 6382 of file SatParameters.java.

◆ CLAUSE_ACTIVITY_DECAY_FIELD_NUMBER

final int CLAUSE_ACTIVITY_DECAY_FIELD_NUMBER = 17
static

Definition at line 3085 of file SatParameters.java.

◆ CLAUSE_CLEANUP_LBD_BOUND_FIELD_NUMBER

final int CLAUSE_CLEANUP_LBD_BOUND_FIELD_NUMBER = 59
static

Definition at line 2796 of file SatParameters.java.

◆ CLAUSE_CLEANUP_ORDERING_FIELD_NUMBER

final int CLAUSE_CLEANUP_ORDERING_FIELD_NUMBER = 60
static

Definition at line 2825 of file SatParameters.java.

◆ CLAUSE_CLEANUP_PERIOD_FIELD_NUMBER

final int CLAUSE_CLEANUP_PERIOD_FIELD_NUMBER = 11
static

Definition at line 2721 of file SatParameters.java.

◆ CLAUSE_CLEANUP_PROTECTION_FIELD_NUMBER

final int CLAUSE_CLEANUP_PROTECTION_FIELD_NUMBER = 58
static

Definition at line 2777 of file SatParameters.java.

◆ CLAUSE_CLEANUP_TARGET_FIELD_NUMBER

final int CLAUSE_CLEANUP_TARGET_FIELD_NUMBER = 13
static

Definition at line 2748 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 3839 of file SatParameters.java.

◆ COVER_OPTIMIZATION_FIELD_NUMBER

final int COVER_OPTIMIZATION_FIELD_NUMBER = 89
static

Definition at line 4512 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 4149 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 4116 of file SatParameters.java.

◆ CP_MODEL_PRESOLVE_FIELD_NUMBER

final int CP_MODEL_PRESOLVE_FIELD_NUMBER = 86
static

Definition at line 4089 of file SatParameters.java.

◆ CP_MODEL_PROBING_LEVEL_FIELD_NUMBER

final int CP_MODEL_PROBING_LEVEL_FIELD_NUMBER = 110
static

Definition at line 4178 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 4205 of file SatParameters.java.

◆ CUT_ACTIVE_COUNT_DECAY_FIELD_NUMBER

final int CUT_ACTIVE_COUNT_DECAY_FIELD_NUMBER = 156
static

Definition at line 5235 of file SatParameters.java.

◆ CUT_CLEANUP_TARGET_FIELD_NUMBER

final int CUT_CLEANUP_TARGET_FIELD_NUMBER = 157
static

Definition at line 5254 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 5204 of file SatParameters.java.

◆ DEFAULT_RESTART_ALGORITHMS_FIELD_NUMBER

final int DEFAULT_RESTART_ALGORITHMS_FIELD_NUMBER = 70
static

Definition at line 3203 of file SatParameters.java.

◆ DIVERSIFY_LNS_PARAMS_FIELD_NUMBER

final int DIVERSIFY_LNS_PARAMS_FIELD_NUMBER = 137
static

Definition at line 6163 of file SatParameters.java.

◆ ENUMERATE_ALL_SOLUTIONS_FIELD_NUMBER

final int ENUMERATE_ALL_SOLUTIONS_FIELD_NUMBER = 87
static

Definition at line 5672 of file SatParameters.java.

◆ EXPAND_AUTOMATON_CONSTRAINTS_FIELD_NUMBER

final int EXPAND_AUTOMATON_CONSTRAINTS_FIELD_NUMBER = 143
static

Definition at line 4280 of file SatParameters.java.

◆ EXPAND_ELEMENT_CONSTRAINTS_FIELD_NUMBER

final int EXPAND_ELEMENT_CONSTRAINTS_FIELD_NUMBER = 140
static

Definition at line 4251 of file SatParameters.java.

◆ EXPAND_TABLE_CONSTRAINTS_FIELD_NUMBER

final int EXPAND_TABLE_CONSTRAINTS_FIELD_NUMBER = 158
static

Definition at line 4307 of file SatParameters.java.

◆ EXPLOIT_ALL_LP_SOLUTION_FIELD_NUMBER

final int EXPLOIT_ALL_LP_SOLUTION_FIELD_NUMBER = 116
static

Definition at line 5391 of file SatParameters.java.

◆ EXPLOIT_BEST_SOLUTION_FIELD_NUMBER

final int EXPLOIT_BEST_SOLUTION_FIELD_NUMBER = 130
static

Definition at line 5422 of file SatParameters.java.

◆ EXPLOIT_INTEGER_LP_SOLUTION_FIELD_NUMBER

final int EXPLOIT_INTEGER_LP_SOLUTION_FIELD_NUMBER = 94
static

Definition at line 5358 of file SatParameters.java.

◆ EXPLOIT_OBJECTIVE_FIELD_NUMBER

final int EXPLOIT_OBJECTIVE_FIELD_NUMBER = 131
static

Definition at line 5480 of file SatParameters.java.

◆ EXPLOIT_RELAXATION_SOLUTION_FIELD_NUMBER

final int EXPLOIT_RELAXATION_SOLUTION_FIELD_NUMBER = 161
static

Definition at line 5449 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 5709 of file SatParameters.java.

◆ FIND_MULTIPLE_CORES_FIELD_NUMBER

final int FIND_MULTIPLE_CORES_FIELD_NUMBER = 84
static

Definition at line 4483 of file SatParameters.java.

◆ GLUCOSE_DECAY_INCREMENT_FIELD_NUMBER

final int GLUCOSE_DECAY_INCREMENT_FIELD_NUMBER = 23
static

Definition at line 3047 of file SatParameters.java.

◆ GLUCOSE_DECAY_INCREMENT_PERIOD_FIELD_NUMBER

final int GLUCOSE_DECAY_INCREMENT_PERIOD_FIELD_NUMBER = 24
static

Definition at line 3066 of file SatParameters.java.

◆ GLUCOSE_MAX_DECAY_FIELD_NUMBER

final int GLUCOSE_MAX_DECAY_FIELD_NUMBER = 22
static

Definition at line 3014 of file SatParameters.java.

◆ HINT_CONFLICT_LIMIT_FIELD_NUMBER

final int HINT_CONFLICT_LIMIT_FIELD_NUMBER = 153
static

Definition at line 5329 of file SatParameters.java.

◆ INITIAL_POLARITY_FIELD_NUMBER

final int INITIAL_POLARITY_FIELD_NUMBER = 2
static

Definition at line 2425 of file SatParameters.java.

◆ INITIAL_VARIABLES_ACTIVITY_FIELD_NUMBER

final int INITIAL_VARIABLES_ACTIVITY_FIELD_NUMBER = 76
static

Definition at line 2580 of file SatParameters.java.

◆ INSTANTIATE_ALL_VARIABLES_FIELD_NUMBER

final int INSTANTIATE_ALL_VARIABLES_FIELD_NUMBER = 106
static

Definition at line 5744 of file SatParameters.java.

◆ INTERLEAVE_BATCH_SIZE_FIELD_NUMBER

final int INTERLEAVE_BATCH_SIZE_FIELD_NUMBER = 134
static

Definition at line 5934 of file SatParameters.java.

◆ INTERLEAVE_SEARCH_FIELD_NUMBER

final int INTERLEAVE_SEARCH_FIELD_NUMBER = 136
static

Definition at line 5899 of file SatParameters.java.

◆ LINEARIZATION_LEVEL_FIELD_NUMBER

final int LINEARIZATION_LEVEL_FIELD_NUMBER = 90
static

Definition at line 4764 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 6061 of file SatParameters.java.

◆ LOG_SEARCH_PROGRESS_FIELD_NUMBER

final int LOG_SEARCH_PROGRESS_FIELD_NUMBER = 41
static

Definition at line 3746 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 4977 of file SatParameters.java.

◆ MAX_CLAUSE_ACTIVITY_VALUE_FIELD_NUMBER

final int MAX_CLAUSE_ACTIVITY_VALUE_FIELD_NUMBER = 18
static

Definition at line 3112 of file SatParameters.java.

◆ MAX_CONSECUTIVE_INACTIVE_COUNT_FIELD_NUMBER

final int MAX_CONSECUTIVE_INACTIVE_COUNT_FIELD_NUMBER = 121
static

Definition at line 5173 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 5146 of file SatParameters.java.

◆ MAX_DETERMINISTIC_TIME_FIELD_NUMBER

final int MAX_DETERMINISTIC_TIME_FIELD_NUMBER = 67
static

Definition at line 3513 of file SatParameters.java.

◆ MAX_INTEGER_ROUNDING_SCALING_FIELD_NUMBER

final int MAX_INTEGER_ROUNDING_SCALING_FIELD_NUMBER = 119
static

Definition at line 5039 of file SatParameters.java.

◆ MAX_MEMORY_IN_MB_FIELD_NUMBER

final int MAX_MEMORY_IN_MB_FIELD_NUMBER = 40
static

Definition at line 3581 of file SatParameters.java.

◆ MAX_NUM_CUTS_FIELD_NUMBER

final int MAX_NUM_CUTS_FIELD_NUMBER = 91
static

Definition at line 4826 of file SatParameters.java.

◆ MAX_NUMBER_OF_CONFLICTS_FIELD_NUMBER

final int MAX_NUMBER_OF_CONFLICTS_FIELD_NUMBER = 37
static

Definition at line 3544 of file SatParameters.java.

◆ MAX_PRESOLVE_ITERATIONS_FIELD_NUMBER

final int MAX_PRESOLVE_ITERATIONS_FIELD_NUMBER = 138
static

Definition at line 4058 of file SatParameters.java.

◆ MAX_SAT_ASSUMPTION_ORDER_FIELD_NUMBER

final int MAX_SAT_ASSUMPTION_ORDER_FIELD_NUMBER = 51
static

Definition at line 4541 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 4560 of file SatParameters.java.

◆ MAX_SAT_STRATIFICATION_FIELD_NUMBER

final int MAX_SAT_STRATIFICATION_FIELD_NUMBER = 53
static

Definition at line 4589 of file SatParameters.java.

◆ MAX_TIME_IN_SECONDS_FIELD_NUMBER

final int MAX_TIME_IN_SECONDS_FIELD_NUMBER = 36
static

Definition at line 3484 of file SatParameters.java.

◆ MAX_VARIABLE_ACTIVITY_VALUE_FIELD_NUMBER

final int MAX_VARIABLE_ACTIVITY_VALUE_FIELD_NUMBER = 16
static

Definition at line 2995 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 4371 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 4336 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 5111 of file SatParameters.java.

◆ MINIMIZATION_ALGORITHM_FIELD_NUMBER

final int MINIMIZATION_ALGORITHM_FIELD_NUMBER = 4
static

Definition at line 2650 of file SatParameters.java.

◆ MINIMIZE_CORE_FIELD_NUMBER

final int MINIMIZE_CORE_FIELD_NUMBER = 50
static

Definition at line 4456 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 3806 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 2937 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 2890 of file SatParameters.java.

◆ MIP_CHECK_PRECISION_FIELD_NUMBER

final int MIP_CHECK_PRECISION_FIELD_NUMBER = 128
static

Definition at line 6588 of file SatParameters.java.

◆ MIP_MAX_ACTIVITY_EXPONENT_FIELD_NUMBER

final int MIP_MAX_ACTIVITY_EXPONENT_FIELD_NUMBER = 127
static

Definition at line 6549 of file SatParameters.java.

◆ MIP_MAX_BOUND_FIELD_NUMBER

final int MIP_MAX_BOUND_FIELD_NUMBER = 124
static

Definition at line 6444 of file SatParameters.java.

◆ MIP_VAR_SCALING_FIELD_NUMBER

final int MIP_VAR_SCALING_FIELD_NUMBER = 125
static

Definition at line 6475 of file SatParameters.java.

◆ MIP_WANTED_PRECISION_FIELD_NUMBER

final int MIP_WANTED_PRECISION_FIELD_NUMBER = 126
static

Definition at line 6506 of file SatParameters.java.

◆ NEW_CONSTRAINTS_BATCH_SIZE_FIELD_NUMBER

final int NEW_CONSTRAINTS_BATCH_SIZE_FIELD_NUMBER = 122
static

Definition at line 5281 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 3424 of file SatParameters.java.

◆ NUM_SEARCH_WORKERS_FIELD_NUMBER

final int NUM_SEARCH_WORKERS_FIELD_NUMBER = 100
static

Definition at line 5862 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 4859 of file SatParameters.java.

◆ OPTIMIZE_WITH_CORE_FIELD_NUMBER

final int OPTIMIZE_WITH_CORE_FIELD_NUMBER = 83
static

Definition at line 5569 of file SatParameters.java.

◆ OPTIMIZE_WITH_MAX_HS_FIELD_NUMBER

final int OPTIMIZE_WITH_MAX_HS_FIELD_NUMBER = 85
static

Definition at line 5635 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 19221 of file SatParameters.java.

◆ PB_CLEANUP_INCREMENT_FIELD_NUMBER

final int PB_CLEANUP_INCREMENT_FIELD_NUMBER = 46
static

Definition at line 2844 of file SatParameters.java.

◆ PB_CLEANUP_RATIO_FIELD_NUMBER

final int PB_CLEANUP_RATIO_FIELD_NUMBER = 47
static

Definition at line 2871 of file SatParameters.java.

◆ PREFERRED_VARIABLE_ORDER_FIELD_NUMBER

final int PREFERRED_VARIABLE_ORDER_FIELD_NUMBER = 1
static

Definition at line 2406 of file SatParameters.java.

◆ PRESOLVE_BLOCKED_CLAUSE_FIELD_NUMBER

final int PRESOLVE_BLOCKED_CLAUSE_FIELD_NUMBER = 88
static

Definition at line 3969 of file SatParameters.java.

◆ PRESOLVE_BVA_THRESHOLD_FIELD_NUMBER

final int PRESOLVE_BVA_THRESHOLD_FIELD_NUMBER = 73
static

Definition at line 4025 of file SatParameters.java.

◆ PRESOLVE_BVE_CLAUSE_WEIGHT_FIELD_NUMBER

final int PRESOLVE_BVE_CLAUSE_WEIGHT_FIELD_NUMBER = 55
static

Definition at line 3911 of file SatParameters.java.

◆ PRESOLVE_BVE_THRESHOLD_FIELD_NUMBER

final int PRESOLVE_BVE_THRESHOLD_FIELD_NUMBER = 54
static

Definition at line 3880 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 3940 of file SatParameters.java.

◆ PRESOLVE_SUBSTITUTION_LEVEL_FIELD_NUMBER

final int PRESOLVE_SUBSTITUTION_LEVEL_FIELD_NUMBER = 147
static

Definition at line 4390 of file SatParameters.java.

◆ PRESOLVE_USE_BVA_FIELD_NUMBER

final int PRESOLVE_USE_BVA_FIELD_NUMBER = 72
static

Definition at line 3998 of file SatParameters.java.

◆ PROBING_PERIOD_AT_ROOT_FIELD_NUMBER

final int PROBING_PERIOD_AT_ROOT_FIELD_NUMBER = 142
static

Definition at line 5509 of file SatParameters.java.

◆ PSEUDO_COST_RELIABILITY_THRESHOLD_FIELD_NUMBER

final int PSEUDO_COST_RELIABILITY_THRESHOLD_FIELD_NUMBER = 123
static

Definition at line 5540 of file SatParameters.java.

◆ RANDOM_BRANCHES_RATIO_FIELD_NUMBER

final int RANDOM_BRANCHES_RATIO_FIELD_NUMBER = 32
static

Definition at line 2518 of file SatParameters.java.

◆ RANDOM_POLARITY_RATIO_FIELD_NUMBER

final int RANDOM_POLARITY_RATIO_FIELD_NUMBER = 45
static

Definition at line 2483 of file SatParameters.java.

◆ RANDOM_SEED_FIELD_NUMBER

final int RANDOM_SEED_FIELD_NUMBER = 31
static

Definition at line 3709 of file SatParameters.java.

◆ RANDOMIZE_SEARCH_FIELD_NUMBER

final int RANDOMIZE_SEARCH_FIELD_NUMBER = 103
static

Definition at line 6190 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 5953 of file SatParameters.java.

◆ RELATIVE_GAP_LIMIT_FIELD_NUMBER

final int RELATIVE_GAP_LIMIT_FIELD_NUMBER = 160
static

Definition at line 3659 of file SatParameters.java.

◆ RESTART_ALGORITHMS_FIELD_NUMBER

final int RESTART_ALGORITHMS_FIELD_NUMBER = 61
static

Definition at line 3131 of file SatParameters.java.

◆ RESTART_DL_AVERAGE_RATIO_FIELD_NUMBER

final int RESTART_DL_AVERAGE_RATIO_FIELD_NUMBER = 63
static

Definition at line 3307 of file SatParameters.java.

◆ RESTART_LBD_AVERAGE_RATIO_FIELD_NUMBER

final int RESTART_LBD_AVERAGE_RATIO_FIELD_NUMBER = 71
static

Definition at line 3336 of file SatParameters.java.

◆ RESTART_PERIOD_FIELD_NUMBER

final int RESTART_PERIOD_FIELD_NUMBER = 30
static

Definition at line 3251 of file SatParameters.java.

◆ RESTART_RUNNING_WINDOW_SIZE_FIELD_NUMBER

final int RESTART_RUNNING_WINDOW_SIZE_FIELD_NUMBER = 62
static

Definition at line 3280 of file SatParameters.java.

◆ SEARCH_BRANCHING_FIELD_NUMBER

final int SEARCH_BRANCHING_FIELD_NUMBER = 82
static

Definition at line 5310 of file SatParameters.java.

◆ SEARCH_RANDOMIZATION_TOLERANCE_FIELD_NUMBER

final int SEARCH_RANDOMIZATION_TOLERANCE_FIELD_NUMBER = 104
static

Definition at line 6217 of file SatParameters.java.

◆ SHARE_LEVEL_ZERO_BOUNDS_FIELD_NUMBER

final int SHARE_LEVEL_ZERO_BOUNDS_FIELD_NUMBER = 114
static

Definition at line 6007 of file SatParameters.java.

◆ SHARE_OBJECTIVE_BOUNDS_FIELD_NUMBER

final int SHARE_OBJECTIVE_BOUNDS_FIELD_NUMBER = 113
static

Definition at line 5980 of file SatParameters.java.

◆ STOP_AFTER_FIRST_SOLUTION_FIELD_NUMBER

final int STOP_AFTER_FIRST_SOLUTION_FIELD_NUMBER = 98
static

Definition at line 5806 of file SatParameters.java.

◆ STOP_AFTER_PRESOLVE_FIELD_NUMBER

final int STOP_AFTER_PRESOLVE_FIELD_NUMBER = 149
static

Definition at line 5833 of file SatParameters.java.

◆ STRATEGY_CHANGE_INCREASE_RATIO_FIELD_NUMBER

final int STRATEGY_CHANGE_INCREASE_RATIO_FIELD_NUMBER = 69
static

Definition at line 3455 of file SatParameters.java.

◆ SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER

final int SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER = 56
static

Definition at line 2688 of file SatParameters.java.

◆ TREAT_BINARY_CLAUSES_SEPARATELY_FIELD_NUMBER

final int TREAT_BINARY_CLAUSES_SEPARATELY_FIELD_NUMBER = 33
static

Definition at line 3678 of file SatParameters.java.

◆ USE_BLOCKING_RESTART_FIELD_NUMBER

final int USE_BLOCKING_RESTART_FIELD_NUMBER = 64
static

Definition at line 3355 of file SatParameters.java.

◆ USE_BRANCHING_IN_LP_FIELD_NUMBER

final int USE_BRANCHING_IN_LP_FIELD_NUMBER = 139
static

Definition at line 6320 of file SatParameters.java.

◆ USE_COMBINED_NO_OVERLAP_FIELD_NUMBER

final int USE_COMBINED_NO_OVERLAP_FIELD_NUMBER = 133
static

Definition at line 6351 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 4723 of file SatParameters.java.

◆ USE_ERWA_HEURISTIC_FIELD_NUMBER

final int USE_ERWA_HEURISTIC_FIELD_NUMBER = 75
static

Definition at line 2549 of file SatParameters.java.

◆ USE_EXACT_LP_REASON_FIELD_NUMBER

final int USE_EXACT_LP_REASON_FIELD_NUMBER = 109
static

Definition at line 6287 of file SatParameters.java.

◆ USE_FEASIBILITY_PUMP_FIELD_NUMBER

final int USE_FEASIBILITY_PUMP_FIELD_NUMBER = 164
static

Definition at line 6107 of file SatParameters.java.

◆ USE_IMPLIED_BOUNDS_FIELD_NUMBER

final int USE_IMPLIED_BOUNDS_FIELD_NUMBER = 144
static

Definition at line 6413 of file SatParameters.java.

◆ USE_LNS_ONLY_FIELD_NUMBER

final int USE_LNS_ONLY_FIELD_NUMBER = 101
static

Definition at line 6034 of file SatParameters.java.

◆ USE_OPTIMIZATION_HINTS_FIELD_NUMBER

final int USE_OPTIMIZATION_HINTS_FIELD_NUMBER = 35
static

Definition at line 4423 of file SatParameters.java.

◆ USE_OPTIONAL_VARIABLES_FIELD_NUMBER

final int USE_OPTIONAL_VARIABLES_FIELD_NUMBER = 108
static

Definition at line 6256 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 4649 of file SatParameters.java.

◆ USE_PB_RESOLUTION_FIELD_NUMBER

final int USE_PB_RESOLUTION_FIELD_NUMBER = 43
static

Definition at line 3773 of file SatParameters.java.

◆ USE_PHASE_SAVING_FIELD_NUMBER

final int USE_PHASE_SAVING_FIELD_NUMBER = 44
static

Definition at line 2444 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 4608 of file SatParameters.java.

◆ USE_RELAXATION_LNS_FIELD_NUMBER

final int USE_RELAXATION_LNS_FIELD_NUMBER = 150
static

Definition at line 6134 of file SatParameters.java.

◆ USE_RINS_LNS_FIELD_NUMBER

final int USE_RINS_LNS_FIELD_NUMBER = 129
static

Definition at line 6080 of file SatParameters.java.

◆ USE_SAT_INPROCESSING_FIELD_NUMBER

final int USE_SAT_INPROCESSING_FIELD_NUMBER = 163
static

Definition at line 4232 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 4686 of file SatParameters.java.

◆ VARIABLE_ACTIVITY_DECAY_FIELD_NUMBER

final int VARIABLE_ACTIVITY_DECAY_FIELD_NUMBER = 15
static

Definition at line 2956 of file SatParameters.java.


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