Java Reference
Java Reference
Detailed Description
Contains the definitions for all the sat algorithm parameters and their default values. NEXT TAG: 165
Protobuf type
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.RestartAlgorithm > | getRestartAlgorithmsList () |
| .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< SatParameters > | getParserForType () |
| .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< SatParameters > | parser () |
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()
|
inline |
Definition at line 7641 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inline |
optional double blocking_restart_multiplier = 66 [default = 1.4];
- Returns
- The blockingRestartMultiplier.
Implements SatParametersOrBuilder.
Definition at line 3420 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inlinestatic |
Definition at line 19216 of file SatParameters.java.
◆ getDefaultInstanceForType()
|
inline |
Definition at line 19241 of file SatParameters.java.
◆ 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()
|
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()
|
inlinestatic |
Definition at line 984 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inline |
optional double glucose_decay_increment = 23 [default = 0.01];
- Returns
- The glucoseDecayIncrement.
Implements SatParametersOrBuilder.
Definition at line 3062 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inline |
optional int32 interleave_batch_size = 134 [default = 1];
- Returns
- The interleaveBatchSize.
Implements SatParametersOrBuilder.
Definition at line 5949 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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@ "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()
|
inline |
Definition at line 19236 of file SatParameters.java.
◆ 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()
|
inline |
optional double pb_cleanup_ratio = 47 [default = 0.5];
- Returns
- The pbCleanupRatio.
Implements SatParametersOrBuilder.
Definition at line 2886 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inline |
optional double relative_gap_limit = 160 [default = 0];
- Returns
- The relativeGapLimit.
Implements SatParametersOrBuilder.
Definition at line 3674 of file SatParameters.java.
◆ getRestartAlgorithms()
|
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
-
index The index of the element to return.
- Returns
- The restartAlgorithms at the given index.
Implements SatParametersOrBuilder.
Definition at line 3199 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
inline |
optional double restart_lbd_average_ratio = 71 [default = 1];
- Returns
- The restartLbdAverageRatio.
Implements SatParametersOrBuilder.
Definition at line 3351 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
inline |
Definition at line 7062 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inline |
Definition at line 136 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inline |
optional bool use_sat_inprocessing = 163 [default = false];
- Returns
- The useSatInprocessing.
Implements SatParametersOrBuilder.
Definition at line 4247 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inline |
Definition at line 8375 of file SatParameters.java.
◆ 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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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@ "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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
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()
|
inlineprotected |
Definition at line 990 of file SatParameters.java.
◆ isInitialized()
|
inline |
Definition at line 6623 of file SatParameters.java.
◆ newBuilder() [1/2]
|
inlinestatic |
Definition at line 9119 of file SatParameters.java.
◆ newBuilder() [2/2]
|
inlinestatic |
Definition at line 9122 of file SatParameters.java.
◆ newBuilderForType() [1/2]
|
inline |
Definition at line 9118 of file SatParameters.java.
◆ newBuilderForType() [2/2]
|
inlineprotected |
Definition at line 9132 of file SatParameters.java.
◆ newInstance()
|
inlineprotected |
Definition at line 129 of file SatParameters.java.
◆ parseDelimitedFrom() [1/2]
|
inlinestatic |
Definition at line 9091 of file SatParameters.java.
◆ parseDelimitedFrom() [2/2]
|
inlinestatic |
Definition at line 9096 of file SatParameters.java.
◆ parseFrom() [1/10]
|
inlinestatic |
Definition at line 9069 of file SatParameters.java.
◆ parseFrom() [2/10]
|
inlinestatic |
Definition at line 9073 of file SatParameters.java.
◆ parseFrom() [3/10]
|
inlinestatic |
Definition at line 9058 of file SatParameters.java.
◆ parseFrom() [4/10]
|
inlinestatic |
Definition at line 9063 of file SatParameters.java.
◆ parseFrom() [5/10]
|
inlinestatic |
Definition at line 9103 of file SatParameters.java.
◆ parseFrom() [6/10]
|
inlinestatic |
Definition at line 9109 of file SatParameters.java.
◆ parseFrom() [7/10]
|
inlinestatic |
Definition at line 9079 of file SatParameters.java.
◆ parseFrom() [8/10]
|
inlinestatic |
Definition at line 9084 of file SatParameters.java.
◆ parseFrom() [9/10]
|
inlinestatic |
Definition at line 9047 of file SatParameters.java.
◆ parseFrom() [10/10]
|
inlinestatic |
Definition at line 9052 of file SatParameters.java.
◆ parser()
|
inlinestatic |
Definition at line 19231 of file SatParameters.java.
◆ toBuilder()
|
inline |
Definition at line 9126 of file SatParameters.java.
◆ writeTo()
|
inline |
Definition at line 6633 of file SatParameters.java.
Member Data Documentation
◆ ABSOLUTE_GAP_LIMIT_FIELD_NUMBER
|
static |
Definition at line 3614 of file SatParameters.java.
◆ ADD_CG_CUTS_FIELD_NUMBER
|
static |
Definition at line 4919 of file SatParameters.java.
◆ ADD_KNAPSACK_CUTS_FIELD_NUMBER
|
static |
Definition at line 4888 of file SatParameters.java.
◆ ADD_LIN_MAX_CUTS_FIELD_NUMBER
|
static |
Definition at line 5008 of file SatParameters.java.
◆ ADD_LP_CONSTRAINTS_LAZILY_FIELD_NUMBER
|
static |
Definition at line 5078 of file SatParameters.java.
◆ ADD_MIR_CUTS_FIELD_NUMBER
|
static |
Definition at line 4948 of file SatParameters.java.
◆ ALSO_BUMP_VARIABLES_IN_CONFLICT_REASONS_FIELD_NUMBER
|
static |
Definition at line 2617 of file SatParameters.java.
◆ AUTO_DETECT_GREATER_THAN_AT_LEAST_ONE_OF_FIELD_NUMBER
|
static |
Definition at line 5773 of file SatParameters.java.
◆ BINARY_MINIMIZATION_ALGORITHM_FIELD_NUMBER
|
static |
Definition at line 2669 of file SatParameters.java.
◆ BINARY_SEARCH_NUM_CONFLICTS_FIELD_NUMBER
|
static |
Definition at line 5602 of file SatParameters.java.
◆ BLOCKING_RESTART_MULTIPLIER_FIELD_NUMBER
|
static |
Definition at line 3405 of file SatParameters.java.
◆ BLOCKING_RESTART_WINDOW_SIZE_FIELD_NUMBER
|
static |
Definition at line 3386 of file SatParameters.java.
◆ BOOLEAN_ENCODING_LEVEL_FIELD_NUMBER
|
static |
Definition at line 4797 of file SatParameters.java.
◆ CATCH_SIGINT_SIGNAL_FIELD_NUMBER
|
static |
Definition at line 6382 of file SatParameters.java.
◆ CLAUSE_ACTIVITY_DECAY_FIELD_NUMBER
|
static |
Definition at line 3085 of file SatParameters.java.
◆ CLAUSE_CLEANUP_LBD_BOUND_FIELD_NUMBER
|
static |
Definition at line 2796 of file SatParameters.java.
◆ CLAUSE_CLEANUP_ORDERING_FIELD_NUMBER
|
static |
Definition at line 2825 of file SatParameters.java.
◆ CLAUSE_CLEANUP_PERIOD_FIELD_NUMBER
|
static |
Definition at line 2721 of file SatParameters.java.
◆ CLAUSE_CLEANUP_PROTECTION_FIELD_NUMBER
|
static |
Definition at line 2777 of file SatParameters.java.
◆ CLAUSE_CLEANUP_TARGET_FIELD_NUMBER
|
static |
Definition at line 2748 of file SatParameters.java.
◆ COUNT_ASSUMPTION_LEVELS_IN_LBD_FIELD_NUMBER
|
static |
Definition at line 3839 of file SatParameters.java.
◆ COVER_OPTIMIZATION_FIELD_NUMBER
|
static |
Definition at line 4512 of file SatParameters.java.
◆ CP_MODEL_MAX_NUM_PRESOLVE_OPERATIONS_FIELD_NUMBER
|
static |
Definition at line 4149 of file SatParameters.java.
◆ CP_MODEL_POSTSOLVE_WITH_FULL_SOLVER_FIELD_NUMBER
|
static |
Definition at line 4116 of file SatParameters.java.
◆ CP_MODEL_PRESOLVE_FIELD_NUMBER
|
static |
Definition at line 4089 of file SatParameters.java.
◆ CP_MODEL_PROBING_LEVEL_FIELD_NUMBER
|
static |
Definition at line 4178 of file SatParameters.java.
◆ CP_MODEL_USE_SAT_PRESOLVE_FIELD_NUMBER
|
static |
Definition at line 4205 of file SatParameters.java.
◆ CUT_ACTIVE_COUNT_DECAY_FIELD_NUMBER
|
static |
Definition at line 5235 of file SatParameters.java.
◆ CUT_CLEANUP_TARGET_FIELD_NUMBER
|
static |
Definition at line 5254 of file SatParameters.java.
◆ CUT_MAX_ACTIVE_COUNT_VALUE_FIELD_NUMBER
|
static |
Definition at line 5204 of file SatParameters.java.
◆ DEFAULT_RESTART_ALGORITHMS_FIELD_NUMBER
|
static |
Definition at line 3203 of file SatParameters.java.
◆ DIVERSIFY_LNS_PARAMS_FIELD_NUMBER
|
static |
Definition at line 6163 of file SatParameters.java.
◆ ENUMERATE_ALL_SOLUTIONS_FIELD_NUMBER
|
static |
Definition at line 5672 of file SatParameters.java.
◆ EXPAND_AUTOMATON_CONSTRAINTS_FIELD_NUMBER
|
static |
Definition at line 4280 of file SatParameters.java.
◆ EXPAND_ELEMENT_CONSTRAINTS_FIELD_NUMBER
|
static |
Definition at line 4251 of file SatParameters.java.
◆ EXPAND_TABLE_CONSTRAINTS_FIELD_NUMBER
|
static |
Definition at line 4307 of file SatParameters.java.
◆ EXPLOIT_ALL_LP_SOLUTION_FIELD_NUMBER
|
static |
Definition at line 5391 of file SatParameters.java.
◆ EXPLOIT_BEST_SOLUTION_FIELD_NUMBER
|
static |
Definition at line 5422 of file SatParameters.java.
◆ EXPLOIT_INTEGER_LP_SOLUTION_FIELD_NUMBER
|
static |
Definition at line 5358 of file SatParameters.java.
◆ EXPLOIT_OBJECTIVE_FIELD_NUMBER
|
static |
Definition at line 5480 of file SatParameters.java.
◆ EXPLOIT_RELAXATION_SOLUTION_FIELD_NUMBER
|
static |
Definition at line 5449 of file SatParameters.java.
◆ FILL_TIGHTENED_DOMAINS_IN_RESPONSE_FIELD_NUMBER
|
static |
Definition at line 5709 of file SatParameters.java.
◆ FIND_MULTIPLE_CORES_FIELD_NUMBER
|
static |
Definition at line 4483 of file SatParameters.java.
◆ GLUCOSE_DECAY_INCREMENT_FIELD_NUMBER
|
static |
Definition at line 3047 of file SatParameters.java.
◆ GLUCOSE_DECAY_INCREMENT_PERIOD_FIELD_NUMBER
|
static |
Definition at line 3066 of file SatParameters.java.
◆ GLUCOSE_MAX_DECAY_FIELD_NUMBER
|
static |
Definition at line 3014 of file SatParameters.java.
◆ HINT_CONFLICT_LIMIT_FIELD_NUMBER
|
static |
Definition at line 5329 of file SatParameters.java.
◆ INITIAL_POLARITY_FIELD_NUMBER
|
static |
Definition at line 2425 of file SatParameters.java.
◆ INITIAL_VARIABLES_ACTIVITY_FIELD_NUMBER
|
static |
Definition at line 2580 of file SatParameters.java.
◆ INSTANTIATE_ALL_VARIABLES_FIELD_NUMBER
|
static |
Definition at line 5744 of file SatParameters.java.
◆ INTERLEAVE_BATCH_SIZE_FIELD_NUMBER
|
static |
Definition at line 5934 of file SatParameters.java.
◆ INTERLEAVE_SEARCH_FIELD_NUMBER
|
static |
Definition at line 5899 of file SatParameters.java.
◆ LINEARIZATION_LEVEL_FIELD_NUMBER
|
static |
Definition at line 4764 of file SatParameters.java.
◆ LNS_FOCUS_ON_DECISION_VARIABLES_FIELD_NUMBER
|
static |
Definition at line 6061 of file SatParameters.java.
◆ LOG_SEARCH_PROGRESS_FIELD_NUMBER
|
static |
Definition at line 3746 of file SatParameters.java.
◆ MAX_ALL_DIFF_CUT_SIZE_FIELD_NUMBER
|
static |
Definition at line 4977 of file SatParameters.java.
◆ MAX_CLAUSE_ACTIVITY_VALUE_FIELD_NUMBER
|
static |
Definition at line 3112 of file SatParameters.java.
◆ MAX_CONSECUTIVE_INACTIVE_COUNT_FIELD_NUMBER
|
static |
Definition at line 5173 of file SatParameters.java.
◆ MAX_CUT_ROUNDS_AT_LEVEL_ZERO_FIELD_NUMBER
|
static |
Definition at line 5146 of file SatParameters.java.
◆ MAX_DETERMINISTIC_TIME_FIELD_NUMBER
|
static |
Definition at line 3513 of file SatParameters.java.
◆ MAX_INTEGER_ROUNDING_SCALING_FIELD_NUMBER
|
static |
Definition at line 5039 of file SatParameters.java.
◆ MAX_MEMORY_IN_MB_FIELD_NUMBER
|
static |
Definition at line 3581 of file SatParameters.java.
◆ MAX_NUM_CUTS_FIELD_NUMBER
|
static |
Definition at line 4826 of file SatParameters.java.
◆ MAX_NUMBER_OF_CONFLICTS_FIELD_NUMBER
|
static |
Definition at line 3544 of file SatParameters.java.
◆ MAX_PRESOLVE_ITERATIONS_FIELD_NUMBER
|
static |
Definition at line 4058 of file SatParameters.java.
◆ MAX_SAT_ASSUMPTION_ORDER_FIELD_NUMBER
|
static |
Definition at line 4541 of file SatParameters.java.
◆ MAX_SAT_REVERSE_ASSUMPTION_ORDER_FIELD_NUMBER
|
static |
Definition at line 4560 of file SatParameters.java.
◆ MAX_SAT_STRATIFICATION_FIELD_NUMBER
|
static |
Definition at line 4589 of file SatParameters.java.
◆ MAX_TIME_IN_SECONDS_FIELD_NUMBER
|
static |
Definition at line 3484 of file SatParameters.java.
◆ MAX_VARIABLE_ACTIVITY_VALUE_FIELD_NUMBER
|
static |
Definition at line 2995 of file SatParameters.java.
◆ MERGE_AT_MOST_ONE_WORK_LIMIT_FIELD_NUMBER
|
static |
Definition at line 4371 of file SatParameters.java.
◆ MERGE_NO_OVERLAP_WORK_LIMIT_FIELD_NUMBER
|
static |
Definition at line 4336 of file SatParameters.java.
◆ MIN_ORTHOGONALITY_FOR_LP_CONSTRAINTS_FIELD_NUMBER
|
static |
Definition at line 5111 of file SatParameters.java.
◆ MINIMIZATION_ALGORITHM_FIELD_NUMBER
|
static |
Definition at line 2650 of file SatParameters.java.
◆ MINIMIZE_CORE_FIELD_NUMBER
|
static |
Definition at line 4456 of file SatParameters.java.
◆ MINIMIZE_REDUCTION_DURING_PB_RESOLUTION_FIELD_NUMBER
|
static |
Definition at line 3806 of file SatParameters.java.
◆ MINIMIZE_WITH_PROPAGATION_NUM_DECISIONS_FIELD_NUMBER
|
static |
Definition at line 2937 of file SatParameters.java.
◆ MINIMIZE_WITH_PROPAGATION_RESTART_PERIOD_FIELD_NUMBER
|
static |
Definition at line 2890 of file SatParameters.java.
◆ MIP_CHECK_PRECISION_FIELD_NUMBER
|
static |
Definition at line 6588 of file SatParameters.java.
◆ MIP_MAX_ACTIVITY_EXPONENT_FIELD_NUMBER
|
static |
Definition at line 6549 of file SatParameters.java.
◆ MIP_MAX_BOUND_FIELD_NUMBER
|
static |
Definition at line 6444 of file SatParameters.java.
◆ MIP_VAR_SCALING_FIELD_NUMBER
|
static |
Definition at line 6475 of file SatParameters.java.
◆ MIP_WANTED_PRECISION_FIELD_NUMBER
|
static |
Definition at line 6506 of file SatParameters.java.
◆ NEW_CONSTRAINTS_BATCH_SIZE_FIELD_NUMBER
|
static |
Definition at line 5281 of file SatParameters.java.
◆ NUM_CONFLICTS_BEFORE_STRATEGY_CHANGES_FIELD_NUMBER
|
static |
Definition at line 3424 of file SatParameters.java.
◆ NUM_SEARCH_WORKERS_FIELD_NUMBER
|
static |
Definition at line 5862 of file SatParameters.java.
◆ ONLY_ADD_CUTS_AT_LEVEL_ZERO_FIELD_NUMBER
|
static |
Definition at line 4859 of file SatParameters.java.
◆ OPTIMIZE_WITH_CORE_FIELD_NUMBER
|
static |
Definition at line 5569 of file SatParameters.java.
◆ OPTIMIZE_WITH_MAX_HS_FIELD_NUMBER
|
static |
Definition at line 5635 of file SatParameters.java.
◆ PARSER
|
static |
Definition at line 19221 of file SatParameters.java.
◆ PB_CLEANUP_INCREMENT_FIELD_NUMBER
|
static |
Definition at line 2844 of file SatParameters.java.
◆ PB_CLEANUP_RATIO_FIELD_NUMBER
|
static |
Definition at line 2871 of file SatParameters.java.
◆ PREFERRED_VARIABLE_ORDER_FIELD_NUMBER
|
static |
Definition at line 2406 of file SatParameters.java.
◆ PRESOLVE_BLOCKED_CLAUSE_FIELD_NUMBER
|
static |
Definition at line 3969 of file SatParameters.java.
◆ PRESOLVE_BVA_THRESHOLD_FIELD_NUMBER
|
static |
Definition at line 4025 of file SatParameters.java.
◆ PRESOLVE_BVE_CLAUSE_WEIGHT_FIELD_NUMBER
|
static |
Definition at line 3911 of file SatParameters.java.
◆ PRESOLVE_BVE_THRESHOLD_FIELD_NUMBER
|
static |
Definition at line 3880 of file SatParameters.java.
◆ PRESOLVE_PROBING_DETERMINISTIC_TIME_LIMIT_FIELD_NUMBER
|
static |
Definition at line 3940 of file SatParameters.java.
◆ PRESOLVE_SUBSTITUTION_LEVEL_FIELD_NUMBER
|
static |
Definition at line 4390 of file SatParameters.java.
◆ PRESOLVE_USE_BVA_FIELD_NUMBER
|
static |
Definition at line 3998 of file SatParameters.java.
◆ PROBING_PERIOD_AT_ROOT_FIELD_NUMBER
|
static |
Definition at line 5509 of file SatParameters.java.
◆ PSEUDO_COST_RELIABILITY_THRESHOLD_FIELD_NUMBER
|
static |
Definition at line 5540 of file SatParameters.java.
◆ RANDOM_BRANCHES_RATIO_FIELD_NUMBER
|
static |
Definition at line 2518 of file SatParameters.java.
◆ RANDOM_POLARITY_RATIO_FIELD_NUMBER
|
static |
Definition at line 2483 of file SatParameters.java.
◆ RANDOM_SEED_FIELD_NUMBER
|
static |
Definition at line 3709 of file SatParameters.java.
◆ RANDOMIZE_SEARCH_FIELD_NUMBER
|
static |
Definition at line 6190 of file SatParameters.java.
◆ REDUCE_MEMORY_USAGE_IN_INTERLEAVE_MODE_FIELD_NUMBER
|
static |
Definition at line 5953 of file SatParameters.java.
◆ RELATIVE_GAP_LIMIT_FIELD_NUMBER
|
static |
Definition at line 3659 of file SatParameters.java.
◆ RESTART_ALGORITHMS_FIELD_NUMBER
|
static |
Definition at line 3131 of file SatParameters.java.
◆ RESTART_DL_AVERAGE_RATIO_FIELD_NUMBER
|
static |
Definition at line 3307 of file SatParameters.java.
◆ RESTART_LBD_AVERAGE_RATIO_FIELD_NUMBER
|
static |
Definition at line 3336 of file SatParameters.java.
◆ RESTART_PERIOD_FIELD_NUMBER
|
static |
Definition at line 3251 of file SatParameters.java.
◆ RESTART_RUNNING_WINDOW_SIZE_FIELD_NUMBER
|
static |
Definition at line 3280 of file SatParameters.java.
◆ SEARCH_BRANCHING_FIELD_NUMBER
|
static |
Definition at line 5310 of file SatParameters.java.
◆ SEARCH_RANDOMIZATION_TOLERANCE_FIELD_NUMBER
|
static |
Definition at line 6217 of file SatParameters.java.
◆ SHARE_LEVEL_ZERO_BOUNDS_FIELD_NUMBER
|
static |
Definition at line 6007 of file SatParameters.java.
◆ SHARE_OBJECTIVE_BOUNDS_FIELD_NUMBER
|
static |
Definition at line 5980 of file SatParameters.java.
◆ STOP_AFTER_FIRST_SOLUTION_FIELD_NUMBER
|
static |
Definition at line 5806 of file SatParameters.java.
◆ STOP_AFTER_PRESOLVE_FIELD_NUMBER
|
static |
Definition at line 5833 of file SatParameters.java.
◆ STRATEGY_CHANGE_INCREASE_RATIO_FIELD_NUMBER
|
static |
Definition at line 3455 of file SatParameters.java.
◆ SUBSUMPTION_DURING_CONFLICT_ANALYSIS_FIELD_NUMBER
|
static |
Definition at line 2688 of file SatParameters.java.
◆ TREAT_BINARY_CLAUSES_SEPARATELY_FIELD_NUMBER
|
static |
Definition at line 3678 of file SatParameters.java.
◆ USE_BLOCKING_RESTART_FIELD_NUMBER
|
static |
Definition at line 3355 of file SatParameters.java.
◆ USE_BRANCHING_IN_LP_FIELD_NUMBER
|
static |
Definition at line 6320 of file SatParameters.java.
◆ USE_COMBINED_NO_OVERLAP_FIELD_NUMBER
|
static |
Definition at line 6351 of file SatParameters.java.
◆ USE_DISJUNCTIVE_CONSTRAINT_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER
|
static |
Definition at line 4723 of file SatParameters.java.
◆ USE_ERWA_HEURISTIC_FIELD_NUMBER
|
static |
Definition at line 2549 of file SatParameters.java.
◆ USE_EXACT_LP_REASON_FIELD_NUMBER
|
static |
Definition at line 6287 of file SatParameters.java.
◆ USE_FEASIBILITY_PUMP_FIELD_NUMBER
|
static |
Definition at line 6107 of file SatParameters.java.
◆ USE_IMPLIED_BOUNDS_FIELD_NUMBER
|
static |
Definition at line 6413 of file SatParameters.java.
◆ USE_LNS_ONLY_FIELD_NUMBER
|
static |
Definition at line 6034 of file SatParameters.java.
◆ USE_OPTIMIZATION_HINTS_FIELD_NUMBER
|
static |
Definition at line 4423 of file SatParameters.java.
◆ USE_OPTIONAL_VARIABLES_FIELD_NUMBER
|
static |
Definition at line 6256 of file SatParameters.java.
◆ USE_OVERLOAD_CHECKER_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER
|
static |
Definition at line 4649 of file SatParameters.java.
◆ USE_PB_RESOLUTION_FIELD_NUMBER
|
static |
Definition at line 3773 of file SatParameters.java.
◆ USE_PHASE_SAVING_FIELD_NUMBER
|
static |
Definition at line 2444 of file SatParameters.java.
◆ USE_PRECEDENCES_IN_DISJUNCTIVE_CONSTRAINT_FIELD_NUMBER
|
static |
Definition at line 4608 of file SatParameters.java.
◆ USE_RELAXATION_LNS_FIELD_NUMBER
|
static |
Definition at line 6134 of file SatParameters.java.
◆ USE_RINS_LNS_FIELD_NUMBER
|
static |
Definition at line 6080 of file SatParameters.java.
◆ USE_SAT_INPROCESSING_FIELD_NUMBER
|
static |
Definition at line 4232 of file SatParameters.java.
◆ USE_TIMETABLE_EDGE_FINDING_IN_CUMULATIVE_CONSTRAINT_FIELD_NUMBER
|
static |
Definition at line 4686 of file SatParameters.java.
◆ VARIABLE_ACTIVITY_DECAY_FIELD_NUMBER
|
static |
Definition at line 2956 of file SatParameters.java.
The documentation for this class was generated from the following file: