Java Reference

Java Reference

Detailed Description

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

Protobuf type

operations_research.sat.SatParameters

Definition at line 10571 of file SatParameters.java.

Public Member Functions

.lang.Override Builder clear ()
 
.lang.Override com.google.protobuf.Descriptors.Descriptor getDescriptorForType ()
 
.lang.Override com.google.ortools.sat.SatParameters getDefaultInstanceForType ()
 
.lang.Override com.google.ortools.sat.SatParameters build ()
 
.lang.Override com.google.ortools.sat.SatParameters buildPartial ()
 
.lang.Override Builder clone ()
 
.lang.Override Builder setField (com.google.protobuf.Descriptors.FieldDescriptor field, java.lang.Object value)
 
.lang.Override Builder clearField (com.google.protobuf.Descriptors.FieldDescriptor field)
 
.lang.Override Builder clearOneof (com.google.protobuf.Descriptors.OneofDescriptor oneof)
 
.lang.Override Builder setRepeatedField (com.google.protobuf.Descriptors.FieldDescriptor field, int index, java.lang.Object value)
 
.lang.Override Builder addRepeatedField (com.google.protobuf.Descriptors.FieldDescriptor field, java.lang.Object value)
 
.lang.Override Builder mergeFrom (com.google.protobuf.Message other)
 
Builder mergeFrom (com.google.ortools.sat.SatParameters other)
 
.lang.Override final boolean isInitialized ()
 
.lang.Override Builder mergeFrom (com.google.protobuf.CodedInputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) throws java.io.IOException
 
boolean hasName ()
 
java.lang.String getName ()
 
com.google.protobuf.ByteString getNameBytes ()
 
Builder setName (java.lang.String value)
 
Builder clearName ()
 
Builder setNameBytes (com.google.protobuf.ByteString value)
 
.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...
 
Builder setPreferredVariableOrder (com.google.ortools.sat.SatParameters.VariableOrder value)
 optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER]; More...
 
Builder clearPreferredVariableOrder ()
 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...
 
Builder setInitialPolarity (com.google.ortools.sat.SatParameters.Polarity value)
 optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE]; More...
 
Builder clearInitialPolarity ()
 optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE]; More...
 
.lang.Override boolean hasUsePhaseSaving ()
 
.lang.Override boolean getUsePhaseSaving ()
 
Builder setUsePhaseSaving (boolean value)
 
Builder clearUsePhaseSaving ()
 
.lang.Override boolean hasPolarityRephaseIncrement ()
 
.lang.Override int getPolarityRephaseIncrement ()
 
Builder setPolarityRephaseIncrement (int value)
 
Builder clearPolarityRephaseIncrement ()
 
.lang.Override boolean hasRandomPolarityRatio ()
 
.lang.Override double getRandomPolarityRatio ()
 
Builder setRandomPolarityRatio (double value)
 
Builder clearRandomPolarityRatio ()
 
.lang.Override boolean hasRandomBranchesRatio ()
 
.lang.Override double getRandomBranchesRatio ()
 
Builder setRandomBranchesRatio (double value)
 
Builder clearRandomBranchesRatio ()
 
.lang.Override boolean hasUseErwaHeuristic ()
 
.lang.Override boolean getUseErwaHeuristic ()
 
Builder setUseErwaHeuristic (boolean value)
 
Builder clearUseErwaHeuristic ()
 
.lang.Override boolean hasInitialVariablesActivity ()
 
.lang.Override double getInitialVariablesActivity ()
 
Builder setInitialVariablesActivity (double value)
 
Builder clearInitialVariablesActivity ()
 
.lang.Override boolean hasAlsoBumpVariablesInConflictReasons ()
 
.lang.Override boolean getAlsoBumpVariablesInConflictReasons ()
 
Builder setAlsoBumpVariablesInConflictReasons (boolean value)
 
Builder clearAlsoBumpVariablesInConflictReasons ()
 
.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...
 
Builder setMinimizationAlgorithm (com.google.ortools.sat.SatParameters.ConflictMinimizationAlgorithm value)
 optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE]; More...
 
Builder clearMinimizationAlgorithm ()
 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...
 
Builder setBinaryMinimizationAlgorithm (com.google.ortools.sat.SatParameters.BinaryMinizationAlgorithm value)
 optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST]; More...
 
Builder clearBinaryMinimizationAlgorithm ()
 optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST]; More...
 
.lang.Override boolean hasSubsumptionDuringConflictAnalysis ()
 
.lang.Override boolean getSubsumptionDuringConflictAnalysis ()
 
Builder setSubsumptionDuringConflictAnalysis (boolean value)
 
Builder clearSubsumptionDuringConflictAnalysis ()
 
.lang.Override boolean hasClauseCleanupPeriod ()
 
.lang.Override int getClauseCleanupPeriod ()
 
Builder setClauseCleanupPeriod (int value)
 
Builder clearClauseCleanupPeriod ()
 
.lang.Override boolean hasClauseCleanupTarget ()
 
.lang.Override int getClauseCleanupTarget ()
 
Builder setClauseCleanupTarget (int value)
 
Builder clearClauseCleanupTarget ()
 
.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...
 
Builder setClauseCleanupProtection (com.google.ortools.sat.SatParameters.ClauseProtection value)
 optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE]; More...
 
Builder clearClauseCleanupProtection ()
 optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE]; More...
 
.lang.Override boolean hasClauseCleanupLbdBound ()
 
.lang.Override int getClauseCleanupLbdBound ()
 
Builder setClauseCleanupLbdBound (int value)
 
Builder clearClauseCleanupLbdBound ()
 
.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...
 
Builder setClauseCleanupOrdering (com.google.ortools.sat.SatParameters.ClauseOrdering value)
 optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY]; More...
 
Builder clearClauseCleanupOrdering ()
 optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY]; More...
 
.lang.Override boolean hasPbCleanupIncrement ()
 
.lang.Override int getPbCleanupIncrement ()
 
Builder setPbCleanupIncrement (int value)
 
Builder clearPbCleanupIncrement ()
 
.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...
 
Builder setPbCleanupRatio (double value)
 optional double pb_cleanup_ratio = 47 [default = 0.5]; More...
 
Builder clearPbCleanupRatio ()
 optional double pb_cleanup_ratio = 47 [default = 0.5]; More...
 
.lang.Override boolean hasMinimizeWithPropagationRestartPeriod ()
 
.lang.Override int getMinimizeWithPropagationRestartPeriod ()
 
Builder setMinimizeWithPropagationRestartPeriod (int value)
 
Builder clearMinimizeWithPropagationRestartPeriod ()
 
.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...
 
Builder setMinimizeWithPropagationNumDecisions (int value)
 optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000]; More...
 
Builder clearMinimizeWithPropagationNumDecisions ()
 optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000]; More...
 
.lang.Override boolean hasVariableActivityDecay ()
 
.lang.Override double getVariableActivityDecay ()
 
Builder setVariableActivityDecay (double value)
 
Builder clearVariableActivityDecay ()
 
.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...
 
Builder setMaxVariableActivityValue (double value)
 optional double max_variable_activity_value = 16 [default = 1e+100]; More...
 
Builder clearMaxVariableActivityValue ()
 optional double max_variable_activity_value = 16 [default = 1e+100]; More...
 
.lang.Override boolean hasGlucoseMaxDecay ()
 
.lang.Override double getGlucoseMaxDecay ()
 
Builder setGlucoseMaxDecay (double value)
 
Builder clearGlucoseMaxDecay ()
 
.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...
 
Builder setGlucoseDecayIncrement (double value)
 optional double glucose_decay_increment = 23 [default = 0.01]; More...
 
Builder clearGlucoseDecayIncrement ()
 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...
 
Builder setGlucoseDecayIncrementPeriod (int value)
 optional int32 glucose_decay_increment_period = 24 [default = 5000]; More...
 
Builder clearGlucoseDecayIncrementPeriod ()
 optional int32 glucose_decay_increment_period = 24 [default = 5000]; More...
 
.lang.Override boolean hasClauseActivityDecay ()
 
.lang.Override double getClauseActivityDecay ()
 
Builder setClauseActivityDecay (double value)
 
Builder clearClauseActivityDecay ()
 
.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...
 
Builder setMaxClauseActivityValue (double value)
 optional double max_clause_activity_value = 18 [default = 1e+20]; More...
 
Builder clearMaxClauseActivityValue ()
 optional double max_clause_activity_value = 18 [default = 1e+20]; More...
 
java.util.List< com.google.ortools.sat.SatParameters.RestartAlgorithmgetRestartAlgorithmsList ()
 
int getRestartAlgorithmsCount ()
 
com.google.ortools.sat.SatParameters.RestartAlgorithm getRestartAlgorithms (int index)
 
Builder setRestartAlgorithms (int index, com.google.ortools.sat.SatParameters.RestartAlgorithm value)
 
Builder addRestartAlgorithms (com.google.ortools.sat.SatParameters.RestartAlgorithm value)
 
Builder addAllRestartAlgorithms (java.lang.Iterable<? extends com.google.ortools.sat.SatParameters.RestartAlgorithm > values)
 
Builder clearRestartAlgorithms ()
 
boolean hasDefaultRestartAlgorithms ()
 optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"]; More...
 
java.lang.String getDefaultRestartAlgorithms ()
 optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"]; More...
 
com.google.protobuf.ByteString getDefaultRestartAlgorithmsBytes ()
 optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"]; More...
 
Builder setDefaultRestartAlgorithms (java.lang.String value)
 optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"]; More...
 
Builder clearDefaultRestartAlgorithms ()
 optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"]; More...
 
Builder setDefaultRestartAlgorithmsBytes (com.google.protobuf.ByteString value)
 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 ()
 
Builder setRestartPeriod (int value)
 
Builder clearRestartPeriod ()
 
.lang.Override boolean hasRestartRunningWindowSize ()
 
.lang.Override int getRestartRunningWindowSize ()
 
Builder setRestartRunningWindowSize (int value)
 
Builder clearRestartRunningWindowSize ()
 
.lang.Override boolean hasRestartDlAverageRatio ()
 
.lang.Override double getRestartDlAverageRatio ()
 
Builder setRestartDlAverageRatio (double value)
 
Builder clearRestartDlAverageRatio ()
 
.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...
 
Builder setRestartLbdAverageRatio (double value)
 optional double restart_lbd_average_ratio = 71 [default = 1]; More...
 
Builder clearRestartLbdAverageRatio ()
 optional double restart_lbd_average_ratio = 71 [default = 1]; More...
 
.lang.Override boolean hasUseBlockingRestart ()
 
.lang.Override boolean getUseBlockingRestart ()
 
Builder setUseBlockingRestart (boolean value)
 
Builder clearUseBlockingRestart ()
 
.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...
 
Builder setBlockingRestartWindowSize (int value)
 optional int32 blocking_restart_window_size = 65 [default = 5000]; More...
 
Builder clearBlockingRestartWindowSize ()
 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...
 
Builder setBlockingRestartMultiplier (double value)
 optional double blocking_restart_multiplier = 66 [default = 1.4]; More...
 
Builder clearBlockingRestartMultiplier ()
 optional double blocking_restart_multiplier = 66 [default = 1.4]; More...
 
.lang.Override boolean hasNumConflictsBeforeStrategyChanges ()
 
.lang.Override int getNumConflictsBeforeStrategyChanges ()
 
Builder setNumConflictsBeforeStrategyChanges (int value)
 
Builder clearNumConflictsBeforeStrategyChanges ()
 
.lang.Override boolean hasStrategyChangeIncreaseRatio ()
 
.lang.Override double getStrategyChangeIncreaseRatio ()
 
Builder setStrategyChangeIncreaseRatio (double value)
 
Builder clearStrategyChangeIncreaseRatio ()
 
.lang.Override boolean hasMaxTimeInSeconds ()
 
.lang.Override double getMaxTimeInSeconds ()
 
Builder setMaxTimeInSeconds (double value)
 
Builder clearMaxTimeInSeconds ()
 
.lang.Override boolean hasMaxDeterministicTime ()
 
.lang.Override double getMaxDeterministicTime ()
 
Builder setMaxDeterministicTime (double value)
 
Builder clearMaxDeterministicTime ()
 
.lang.Override boolean hasMaxNumberOfConflicts ()
 
.lang.Override long getMaxNumberOfConflicts ()
 
Builder setMaxNumberOfConflicts (long value)
 
Builder clearMaxNumberOfConflicts ()
 
.lang.Override boolean hasMaxMemoryInMb ()
 
.lang.Override long getMaxMemoryInMb ()
 
Builder setMaxMemoryInMb (long value)
 
Builder clearMaxMemoryInMb ()
 
.lang.Override boolean hasAbsoluteGapLimit ()
 
.lang.Override double getAbsoluteGapLimit ()
 
Builder setAbsoluteGapLimit (double value)
 
Builder clearAbsoluteGapLimit ()
 
.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...
 
Builder setRelativeGapLimit (double value)
 optional double relative_gap_limit = 160 [default = 0]; More...
 
Builder clearRelativeGapLimit ()
 optional double relative_gap_limit = 160 [default = 0]; More...
 
.lang.Override boolean hasTreatBinaryClausesSeparately ()
 
.lang.Override boolean getTreatBinaryClausesSeparately ()
 
Builder setTreatBinaryClausesSeparately (boolean value)
 
Builder clearTreatBinaryClausesSeparately ()
 
.lang.Override boolean hasRandomSeed ()
 
.lang.Override int getRandomSeed ()
 
Builder setRandomSeed (int value)
 
Builder clearRandomSeed ()
 
.lang.Override boolean hasPermuteVariableRandomly ()
 
.lang.Override boolean getPermuteVariableRandomly ()
 
Builder setPermuteVariableRandomly (boolean value)
 
Builder clearPermuteVariableRandomly ()
 
.lang.Override boolean hasPermutePresolveConstraintOrder ()
 optional bool permute_presolve_constraint_order = 179 [default = false]; More...
 
.lang.Override boolean getPermutePresolveConstraintOrder ()
 optional bool permute_presolve_constraint_order = 179 [default = false]; More...
 
Builder setPermutePresolveConstraintOrder (boolean value)
 optional bool permute_presolve_constraint_order = 179 [default = false]; More...
 
Builder clearPermutePresolveConstraintOrder ()
 optional bool permute_presolve_constraint_order = 179 [default = false]; More...
 
.lang.Override boolean hasUseAbslRandom ()
 optional bool use_absl_random = 180 [default = false]; More...
 
.lang.Override boolean getUseAbslRandom ()
 optional bool use_absl_random = 180 [default = false]; More...
 
Builder setUseAbslRandom (boolean value)
 optional bool use_absl_random = 180 [default = false]; More...
 
Builder clearUseAbslRandom ()
 optional bool use_absl_random = 180 [default = false]; More...
 
.lang.Override boolean hasLogSearchProgress ()
 
.lang.Override boolean getLogSearchProgress ()
 
Builder setLogSearchProgress (boolean value)
 
Builder clearLogSearchProgress ()
 
boolean hasLogPrefix ()
 
java.lang.String getLogPrefix ()
 
com.google.protobuf.ByteString getLogPrefixBytes ()
 
Builder setLogPrefix (java.lang.String value)
 
Builder clearLogPrefix ()
 
Builder setLogPrefixBytes (com.google.protobuf.ByteString value)
 
.lang.Override boolean hasLogToStdout ()
 
.lang.Override boolean getLogToStdout ()
 
Builder setLogToStdout (boolean value)
 
Builder clearLogToStdout ()
 
.lang.Override boolean hasLogToResponse ()
 
.lang.Override boolean getLogToResponse ()
 
Builder setLogToResponse (boolean value)
 
Builder clearLogToResponse ()
 
.lang.Override boolean hasUsePbResolution ()
 
.lang.Override boolean getUsePbResolution ()
 
Builder setUsePbResolution (boolean value)
 
Builder clearUsePbResolution ()
 
.lang.Override boolean hasMinimizeReductionDuringPbResolution ()
 
.lang.Override boolean getMinimizeReductionDuringPbResolution ()
 
Builder setMinimizeReductionDuringPbResolution (boolean value)
 
Builder clearMinimizeReductionDuringPbResolution ()
 
.lang.Override boolean hasCountAssumptionLevelsInLbd ()
 
.lang.Override boolean getCountAssumptionLevelsInLbd ()
 
Builder setCountAssumptionLevelsInLbd (boolean value)
 
Builder clearCountAssumptionLevelsInLbd ()
 
.lang.Override boolean hasPresolveBveThreshold ()
 
.lang.Override int getPresolveBveThreshold ()
 
Builder setPresolveBveThreshold (int value)
 
Builder clearPresolveBveThreshold ()
 
.lang.Override boolean hasPresolveBveClauseWeight ()
 
.lang.Override int getPresolveBveClauseWeight ()
 
Builder setPresolveBveClauseWeight (int value)
 
Builder clearPresolveBveClauseWeight ()
 
.lang.Override boolean hasPresolveProbingDeterministicTimeLimit ()
 
.lang.Override double getPresolveProbingDeterministicTimeLimit ()
 
Builder setPresolveProbingDeterministicTimeLimit (double value)
 
Builder clearPresolveProbingDeterministicTimeLimit ()
 
.lang.Override boolean hasPresolveBlockedClause ()
 
.lang.Override boolean getPresolveBlockedClause ()
 
Builder setPresolveBlockedClause (boolean value)
 
Builder clearPresolveBlockedClause ()
 
.lang.Override boolean hasPresolveUseBva ()
 
.lang.Override boolean getPresolveUseBva ()
 
Builder setPresolveUseBva (boolean value)
 
Builder clearPresolveUseBva ()
 
.lang.Override boolean hasPresolveBvaThreshold ()
 
.lang.Override int getPresolveBvaThreshold ()
 
Builder setPresolveBvaThreshold (int value)
 
Builder clearPresolveBvaThreshold ()
 
.lang.Override boolean hasMaxPresolveIterations ()
 
.lang.Override int getMaxPresolveIterations ()
 
Builder setMaxPresolveIterations (int value)
 
Builder clearMaxPresolveIterations ()
 
.lang.Override boolean hasCpModelPresolve ()
 
.lang.Override boolean getCpModelPresolve ()
 
Builder setCpModelPresolve (boolean value)
 
Builder clearCpModelPresolve ()
 
.lang.Override boolean hasCpModelPostsolveWithFullSolver ()
 
.lang.Override boolean getCpModelPostsolveWithFullSolver ()
 
Builder setCpModelPostsolveWithFullSolver (boolean value)
 
Builder clearCpModelPostsolveWithFullSolver ()
 
.lang.Override boolean hasCpModelMaxNumPresolveOperations ()
 
.lang.Override int getCpModelMaxNumPresolveOperations ()
 
Builder setCpModelMaxNumPresolveOperations (int value)
 
Builder clearCpModelMaxNumPresolveOperations ()
 
.lang.Override boolean hasCpModelProbingLevel ()
 
.lang.Override int getCpModelProbingLevel ()
 
Builder setCpModelProbingLevel (int value)
 
Builder clearCpModelProbingLevel ()
 
.lang.Override boolean hasCpModelUseSatPresolve ()
 
.lang.Override boolean getCpModelUseSatPresolve ()
 
Builder setCpModelUseSatPresolve (boolean value)
 
Builder clearCpModelUseSatPresolve ()
 
.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...
 
Builder setUseSatInprocessing (boolean value)
 optional bool use_sat_inprocessing = 163 [default = false]; More...
 
Builder clearUseSatInprocessing ()
 optional bool use_sat_inprocessing = 163 [default = false]; More...
 
.lang.Override boolean hasExpandElementConstraints ()
 
.lang.Override boolean getExpandElementConstraints ()
 
Builder setExpandElementConstraints (boolean value)
 
Builder clearExpandElementConstraints ()
 
.lang.Override boolean hasExpandAutomatonConstraints ()
 
.lang.Override boolean getExpandAutomatonConstraints ()
 
Builder setExpandAutomatonConstraints (boolean value)
 
Builder clearExpandAutomatonConstraints ()
 
.lang.Override boolean hasExpandTableConstraints ()
 
.lang.Override boolean getExpandTableConstraints ()
 
Builder setExpandTableConstraints (boolean value)
 
Builder clearExpandTableConstraints ()
 
.lang.Override boolean hasExpandAlldiffConstraints ()
 
.lang.Override boolean getExpandAlldiffConstraints ()
 
Builder setExpandAlldiffConstraints (boolean value)
 
Builder clearExpandAlldiffConstraints ()
 
.lang.Override boolean hasExpandReservoirConstraints ()
 
.lang.Override boolean getExpandReservoirConstraints ()
 
Builder setExpandReservoirConstraints (boolean value)
 
Builder clearExpandReservoirConstraints ()
 
.lang.Override boolean hasDisableConstraintExpansion ()
 
.lang.Override boolean getDisableConstraintExpansion ()
 
Builder setDisableConstraintExpansion (boolean value)
 
Builder clearDisableConstraintExpansion ()
 
.lang.Override boolean hasMergeNoOverlapWorkLimit ()
 
.lang.Override double getMergeNoOverlapWorkLimit ()
 
Builder setMergeNoOverlapWorkLimit (double value)
 
Builder clearMergeNoOverlapWorkLimit ()
 
.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...
 
Builder setMergeAtMostOneWorkLimit (double value)
 optional double merge_at_most_one_work_limit = 146 [default = 100000000]; More...
 
Builder clearMergeAtMostOneWorkLimit ()
 optional double merge_at_most_one_work_limit = 146 [default = 100000000]; More...
 
.lang.Override boolean hasPresolveSubstitutionLevel ()
 
.lang.Override int getPresolveSubstitutionLevel ()
 
Builder setPresolveSubstitutionLevel (int value)
 
Builder clearPresolveSubstitutionLevel ()
 
.lang.Override boolean hasPresolveExtractIntegerEnforcement ()
 
.lang.Override boolean getPresolveExtractIntegerEnforcement ()
 
Builder setPresolveExtractIntegerEnforcement (boolean value)
 
Builder clearPresolveExtractIntegerEnforcement ()
 
.lang.Override boolean hasUseOptimizationHints ()
 
.lang.Override boolean getUseOptimizationHints ()
 
Builder setUseOptimizationHints (boolean value)
 
Builder clearUseOptimizationHints ()
 
.lang.Override boolean hasMinimizeCore ()
 
.lang.Override boolean getMinimizeCore ()
 
Builder setMinimizeCore (boolean value)
 
Builder clearMinimizeCore ()
 
.lang.Override boolean hasFindMultipleCores ()
 
.lang.Override boolean getFindMultipleCores ()
 
Builder setFindMultipleCores (boolean value)
 
Builder clearFindMultipleCores ()
 
.lang.Override boolean hasCoverOptimization ()
 
.lang.Override boolean getCoverOptimization ()
 
Builder setCoverOptimization (boolean value)
 
Builder clearCoverOptimization ()
 
.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...
 
Builder setMaxSatAssumptionOrder (com.google.ortools.sat.SatParameters.MaxSatAssumptionOrder value)
 optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER]; More...
 
Builder clearMaxSatAssumptionOrder ()
 optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER]; More...
 
.lang.Override boolean hasMaxSatReverseAssumptionOrder ()
 
.lang.Override boolean getMaxSatReverseAssumptionOrder ()
 
Builder setMaxSatReverseAssumptionOrder (boolean value)
 
Builder clearMaxSatReverseAssumptionOrder ()
 
.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...
 
Builder setMaxSatStratification (com.google.ortools.sat.SatParameters.MaxSatStratificationAlgorithm value)
 optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT]; More...
 
Builder clearMaxSatStratification ()
 optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT]; More...
 
.lang.Override boolean hasUsePrecedencesInDisjunctiveConstraint ()
 
.lang.Override boolean getUsePrecedencesInDisjunctiveConstraint ()
 
Builder setUsePrecedencesInDisjunctiveConstraint (boolean value)
 
Builder clearUsePrecedencesInDisjunctiveConstraint ()
 
.lang.Override boolean hasUseOverloadCheckerInCumulativeConstraint ()
 
.lang.Override boolean getUseOverloadCheckerInCumulativeConstraint ()
 
Builder setUseOverloadCheckerInCumulativeConstraint (boolean value)
 
Builder clearUseOverloadCheckerInCumulativeConstraint ()
 
.lang.Override boolean hasUseTimetableEdgeFindingInCumulativeConstraint ()
 
.lang.Override boolean getUseTimetableEdgeFindingInCumulativeConstraint ()
 
Builder setUseTimetableEdgeFindingInCumulativeConstraint (boolean value)
 
Builder clearUseTimetableEdgeFindingInCumulativeConstraint ()
 
.lang.Override boolean hasUseDisjunctiveConstraintInCumulativeConstraint ()
 
.lang.Override boolean getUseDisjunctiveConstraintInCumulativeConstraint ()
 
Builder setUseDisjunctiveConstraintInCumulativeConstraint (boolean value)
 
Builder clearUseDisjunctiveConstraintInCumulativeConstraint ()
 
.lang.Override boolean hasLinearizationLevel ()
 
.lang.Override int getLinearizationLevel ()
 
Builder setLinearizationLevel (int value)
 
Builder clearLinearizationLevel ()
 
.lang.Override boolean hasBooleanEncodingLevel ()
 
.lang.Override int getBooleanEncodingLevel ()
 
Builder setBooleanEncodingLevel (int value)
 
Builder clearBooleanEncodingLevel ()
 
.lang.Override boolean hasMaxNumCuts ()
 
.lang.Override int getMaxNumCuts ()
 
Builder setMaxNumCuts (int value)
 
Builder clearMaxNumCuts ()
 
.lang.Override boolean hasOnlyAddCutsAtLevelZero ()
 
.lang.Override boolean getOnlyAddCutsAtLevelZero ()
 
Builder setOnlyAddCutsAtLevelZero (boolean value)
 
Builder clearOnlyAddCutsAtLevelZero ()
 
.lang.Override boolean hasAddKnapsackCuts ()
 
.lang.Override boolean getAddKnapsackCuts ()
 
Builder setAddKnapsackCuts (boolean value)
 
Builder clearAddKnapsackCuts ()
 
.lang.Override boolean hasAddCgCuts ()
 
.lang.Override boolean getAddCgCuts ()
 
Builder setAddCgCuts (boolean value)
 
Builder clearAddCgCuts ()
 
.lang.Override boolean hasAddMirCuts ()
 
.lang.Override boolean getAddMirCuts ()
 
Builder setAddMirCuts (boolean value)
 
Builder clearAddMirCuts ()
 
.lang.Override boolean hasAddZeroHalfCuts ()
 
.lang.Override boolean getAddZeroHalfCuts ()
 
Builder setAddZeroHalfCuts (boolean value)
 
Builder clearAddZeroHalfCuts ()
 
.lang.Override boolean hasAddCliqueCuts ()
 
.lang.Override boolean getAddCliqueCuts ()
 
Builder setAddCliqueCuts (boolean value)
 
Builder clearAddCliqueCuts ()
 
.lang.Override boolean hasMaxAllDiffCutSize ()
 
.lang.Override int getMaxAllDiffCutSize ()
 
Builder setMaxAllDiffCutSize (int value)
 
Builder clearMaxAllDiffCutSize ()
 
.lang.Override boolean hasAddLinMaxCuts ()
 
.lang.Override boolean getAddLinMaxCuts ()
 
Builder setAddLinMaxCuts (boolean value)
 
Builder clearAddLinMaxCuts ()
 
.lang.Override boolean hasMaxIntegerRoundingScaling ()
 
.lang.Override int getMaxIntegerRoundingScaling ()
 
Builder setMaxIntegerRoundingScaling (int value)
 
Builder clearMaxIntegerRoundingScaling ()
 
.lang.Override boolean hasAddLpConstraintsLazily ()
 
.lang.Override boolean getAddLpConstraintsLazily ()
 
Builder setAddLpConstraintsLazily (boolean value)
 
Builder clearAddLpConstraintsLazily ()
 
.lang.Override boolean hasMinOrthogonalityForLpConstraints ()
 
.lang.Override double getMinOrthogonalityForLpConstraints ()
 
Builder setMinOrthogonalityForLpConstraints (double value)
 
Builder clearMinOrthogonalityForLpConstraints ()
 
.lang.Override boolean hasMaxCutRoundsAtLevelZero ()
 
.lang.Override int getMaxCutRoundsAtLevelZero ()
 
Builder setMaxCutRoundsAtLevelZero (int value)
 
Builder clearMaxCutRoundsAtLevelZero ()
 
.lang.Override boolean hasMaxConsecutiveInactiveCount ()
 
.lang.Override int getMaxConsecutiveInactiveCount ()
 
Builder setMaxConsecutiveInactiveCount (int value)
 
Builder clearMaxConsecutiveInactiveCount ()
 
.lang.Override boolean hasCutMaxActiveCountValue ()
 
.lang.Override double getCutMaxActiveCountValue ()
 
Builder setCutMaxActiveCountValue (double value)
 
Builder clearCutMaxActiveCountValue ()
 
.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...
 
Builder setCutActiveCountDecay (double value)
 optional double cut_active_count_decay = 156 [default = 0.8]; More...
 
Builder clearCutActiveCountDecay ()
 optional double cut_active_count_decay = 156 [default = 0.8]; More...
 
.lang.Override boolean hasCutCleanupTarget ()
 
.lang.Override int getCutCleanupTarget ()
 
Builder setCutCleanupTarget (int value)
 
Builder clearCutCleanupTarget ()
 
.lang.Override boolean hasNewConstraintsBatchSize ()
 
.lang.Override int getNewConstraintsBatchSize ()
 
Builder setNewConstraintsBatchSize (int value)
 
Builder clearNewConstraintsBatchSize ()
 
.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...
 
Builder setSearchBranching (com.google.ortools.sat.SatParameters.SearchBranching value)
 optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH]; More...
 
Builder clearSearchBranching ()
 optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH]; More...
 
.lang.Override boolean hasHintConflictLimit ()
 
.lang.Override int getHintConflictLimit ()
 
Builder setHintConflictLimit (int value)
 
Builder clearHintConflictLimit ()
 
.lang.Override boolean hasRepairHint ()
 
.lang.Override boolean getRepairHint ()
 
Builder setRepairHint (boolean value)
 
Builder clearRepairHint ()
 
.lang.Override boolean hasExploitIntegerLpSolution ()
 
.lang.Override boolean getExploitIntegerLpSolution ()
 
Builder setExploitIntegerLpSolution (boolean value)
 
Builder clearExploitIntegerLpSolution ()
 
.lang.Override boolean hasExploitAllLpSolution ()
 
.lang.Override boolean getExploitAllLpSolution ()
 
Builder setExploitAllLpSolution (boolean value)
 
Builder clearExploitAllLpSolution ()
 
.lang.Override boolean hasExploitBestSolution ()
 
.lang.Override boolean getExploitBestSolution ()
 
Builder setExploitBestSolution (boolean value)
 
Builder clearExploitBestSolution ()
 
.lang.Override boolean hasExploitRelaxationSolution ()
 
.lang.Override boolean getExploitRelaxationSolution ()
 
Builder setExploitRelaxationSolution (boolean value)
 
Builder clearExploitRelaxationSolution ()
 
.lang.Override boolean hasExploitObjective ()
 
.lang.Override boolean getExploitObjective ()
 
Builder setExploitObjective (boolean value)
 
Builder clearExploitObjective ()
 
.lang.Override boolean hasProbingPeriodAtRoot ()
 
.lang.Override long getProbingPeriodAtRoot ()
 
Builder setProbingPeriodAtRoot (long value)
 
Builder clearProbingPeriodAtRoot ()
 
.lang.Override boolean hasUseProbingSearch ()
 
.lang.Override boolean getUseProbingSearch ()
 
Builder setUseProbingSearch (boolean value)
 
Builder clearUseProbingSearch ()
 
.lang.Override boolean hasPseudoCostReliabilityThreshold ()
 
.lang.Override long getPseudoCostReliabilityThreshold ()
 
Builder setPseudoCostReliabilityThreshold (long value)
 
Builder clearPseudoCostReliabilityThreshold ()
 
.lang.Override boolean hasOptimizeWithCore ()
 
.lang.Override boolean getOptimizeWithCore ()
 
Builder setOptimizeWithCore (boolean value)
 
Builder clearOptimizeWithCore ()
 
.lang.Override boolean hasBinarySearchNumConflicts ()
 
.lang.Override int getBinarySearchNumConflicts ()
 
Builder setBinarySearchNumConflicts (int value)
 
Builder clearBinarySearchNumConflicts ()
 
.lang.Override boolean hasOptimizeWithMaxHs ()
 
.lang.Override boolean getOptimizeWithMaxHs ()
 
Builder setOptimizeWithMaxHs (boolean value)
 
Builder clearOptimizeWithMaxHs ()
 
.lang.Override boolean hasEnumerateAllSolutions ()
 
.lang.Override boolean getEnumerateAllSolutions ()
 
Builder setEnumerateAllSolutions (boolean value)
 
Builder clearEnumerateAllSolutions ()
 
.lang.Override boolean hasKeepAllFeasibleSolutionsInPresolve ()
 
.lang.Override boolean getKeepAllFeasibleSolutionsInPresolve ()
 
Builder setKeepAllFeasibleSolutionsInPresolve (boolean value)
 
Builder clearKeepAllFeasibleSolutionsInPresolve ()
 
.lang.Override boolean hasFillTightenedDomainsInResponse ()
 
.lang.Override boolean getFillTightenedDomainsInResponse ()
 
Builder setFillTightenedDomainsInResponse (boolean value)
 
Builder clearFillTightenedDomainsInResponse ()
 
.lang.Override boolean hasInstantiateAllVariables ()
 
.lang.Override boolean getInstantiateAllVariables ()
 
Builder setInstantiateAllVariables (boolean value)
 
Builder clearInstantiateAllVariables ()
 
.lang.Override boolean hasAutoDetectGreaterThanAtLeastOneOf ()
 
.lang.Override boolean getAutoDetectGreaterThanAtLeastOneOf ()
 
Builder setAutoDetectGreaterThanAtLeastOneOf (boolean value)
 
Builder clearAutoDetectGreaterThanAtLeastOneOf ()
 
.lang.Override boolean hasStopAfterFirstSolution ()
 
.lang.Override boolean getStopAfterFirstSolution ()
 
Builder setStopAfterFirstSolution (boolean value)
 
Builder clearStopAfterFirstSolution ()
 
.lang.Override boolean hasStopAfterPresolve ()
 
.lang.Override boolean getStopAfterPresolve ()
 
Builder setStopAfterPresolve (boolean value)
 
Builder clearStopAfterPresolve ()
 
.lang.Override boolean hasNumSearchWorkers ()
 
.lang.Override int getNumSearchWorkers ()
 
Builder setNumSearchWorkers (int value)
 
Builder clearNumSearchWorkers ()
 
.lang.Override boolean hasInterleaveSearch ()
 
.lang.Override boolean getInterleaveSearch ()
 
Builder setInterleaveSearch (boolean value)
 
Builder clearInterleaveSearch ()
 
.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...
 
Builder setInterleaveBatchSize (int value)
 optional int32 interleave_batch_size = 134 [default = 1]; More...
 
Builder clearInterleaveBatchSize ()
 optional int32 interleave_batch_size = 134 [default = 1]; More...
 
.lang.Override boolean hasReduceMemoryUsageInInterleaveMode ()
 
.lang.Override boolean getReduceMemoryUsageInInterleaveMode ()
 
Builder setReduceMemoryUsageInInterleaveMode (boolean value)
 
Builder clearReduceMemoryUsageInInterleaveMode ()
 
.lang.Override boolean hasShareObjectiveBounds ()
 
.lang.Override boolean getShareObjectiveBounds ()
 
Builder setShareObjectiveBounds (boolean value)
 
Builder clearShareObjectiveBounds ()
 
.lang.Override boolean hasShareLevelZeroBounds ()
 
.lang.Override boolean getShareLevelZeroBounds ()
 
Builder setShareLevelZeroBounds (boolean value)
 
Builder clearShareLevelZeroBounds ()
 
.lang.Override boolean hasUseLnsOnly ()
 
.lang.Override boolean getUseLnsOnly ()
 
Builder setUseLnsOnly (boolean value)
 
Builder clearUseLnsOnly ()
 
.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...
 
Builder setLnsFocusOnDecisionVariables (boolean value)
 optional bool lns_focus_on_decision_variables = 105 [default = false]; More...
 
Builder clearLnsFocusOnDecisionVariables ()
 optional bool lns_focus_on_decision_variables = 105 [default = false]; More...
 
.lang.Override boolean hasLnsExpandIntervalsInConstraintGraph ()
 optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true]; More...
 
.lang.Override boolean getLnsExpandIntervalsInConstraintGraph ()
 optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true]; More...
 
Builder setLnsExpandIntervalsInConstraintGraph (boolean value)
 optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true]; More...
 
Builder clearLnsExpandIntervalsInConstraintGraph ()
 optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true]; More...
 
.lang.Override boolean hasUseRinsLns ()
 
.lang.Override boolean getUseRinsLns ()
 
Builder setUseRinsLns (boolean value)
 
Builder clearUseRinsLns ()
 
.lang.Override boolean hasUseFeasibilityPump ()
 
.lang.Override boolean getUseFeasibilityPump ()
 
Builder setUseFeasibilityPump (boolean value)
 
Builder clearUseFeasibilityPump ()
 
.lang.Override boolean hasFpRounding ()
 optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED]; More...
 
.lang.Override com.google.ortools.sat.SatParameters.FPRoundingMethod getFpRounding ()
 optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED]; More...
 
Builder setFpRounding (com.google.ortools.sat.SatParameters.FPRoundingMethod value)
 optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED]; More...
 
Builder clearFpRounding ()
 optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED]; More...
 
.lang.Override boolean hasUseRelaxationLns ()
 
.lang.Override boolean getUseRelaxationLns ()
 
Builder setUseRelaxationLns (boolean value)
 
Builder clearUseRelaxationLns ()
 
.lang.Override boolean hasDiversifyLnsParams ()
 
.lang.Override boolean getDiversifyLnsParams ()
 
Builder setDiversifyLnsParams (boolean value)
 
Builder clearDiversifyLnsParams ()
 
.lang.Override boolean hasRandomizeSearch ()
 
.lang.Override boolean getRandomizeSearch ()
 
Builder setRandomizeSearch (boolean value)
 
Builder clearRandomizeSearch ()
 
.lang.Override boolean hasSearchRandomizationTolerance ()
 
.lang.Override long getSearchRandomizationTolerance ()
 
Builder setSearchRandomizationTolerance (long value)
 
Builder clearSearchRandomizationTolerance ()
 
.lang.Override boolean hasUseOptionalVariables ()
 
.lang.Override boolean getUseOptionalVariables ()
 
Builder setUseOptionalVariables (boolean value)
 
Builder clearUseOptionalVariables ()
 
.lang.Override boolean hasUseExactLpReason ()
 
.lang.Override boolean getUseExactLpReason ()
 
Builder setUseExactLpReason (boolean value)
 
Builder clearUseExactLpReason ()
 
.lang.Override boolean hasUseBranchingInLp ()
 
.lang.Override boolean getUseBranchingInLp ()
 
Builder setUseBranchingInLp (boolean value)
 
Builder clearUseBranchingInLp ()
 
.lang.Override boolean hasUseCombinedNoOverlap ()
 
.lang.Override boolean getUseCombinedNoOverlap ()
 
Builder setUseCombinedNoOverlap (boolean value)
 
Builder clearUseCombinedNoOverlap ()
 
.lang.Override boolean hasCatchSigintSignal ()
 
.lang.Override boolean getCatchSigintSignal ()
 
Builder setCatchSigintSignal (boolean value)
 
Builder clearCatchSigintSignal ()
 
.lang.Override boolean hasUseImpliedBounds ()
 
.lang.Override boolean getUseImpliedBounds ()
 
Builder setUseImpliedBounds (boolean value)
 
Builder clearUseImpliedBounds ()
 
.lang.Override boolean hasPolishLpSolution ()
 
.lang.Override boolean getPolishLpSolution ()
 
Builder setPolishLpSolution (boolean value)
 
Builder clearPolishLpSolution ()
 
.lang.Override boolean hasConvertIntervals ()
 
.lang.Override boolean getConvertIntervals ()
 
Builder setConvertIntervals (boolean value)
 
Builder clearConvertIntervals ()
 
.lang.Override boolean hasSymmetryLevel ()
 
.lang.Override int getSymmetryLevel ()
 
Builder setSymmetryLevel (int value)
 
Builder clearSymmetryLevel ()
 
.lang.Override boolean hasMipMaxBound ()
 
.lang.Override double getMipMaxBound ()
 
Builder setMipMaxBound (double value)
 
Builder clearMipMaxBound ()
 
.lang.Override boolean hasMipVarScaling ()
 
.lang.Override double getMipVarScaling ()
 
Builder setMipVarScaling (double value)
 
Builder clearMipVarScaling ()
 
.lang.Override boolean hasMipAutomaticallyScaleVariables ()
 
.lang.Override boolean getMipAutomaticallyScaleVariables ()
 
Builder setMipAutomaticallyScaleVariables (boolean value)
 
Builder clearMipAutomaticallyScaleVariables ()
 
.lang.Override boolean hasMipWantedPrecision ()
 
.lang.Override double getMipWantedPrecision ()
 
Builder setMipWantedPrecision (double value)
 
Builder clearMipWantedPrecision ()
 
.lang.Override boolean hasMipMaxActivityExponent ()
 
.lang.Override int getMipMaxActivityExponent ()
 
Builder setMipMaxActivityExponent (int value)
 
Builder clearMipMaxActivityExponent ()
 
.lang.Override boolean hasMipCheckPrecision ()
 
.lang.Override double getMipCheckPrecision ()
 
Builder setMipCheckPrecision (double value)
 
Builder clearMipCheckPrecision ()
 
.lang.Override final Builder setUnknownFields (final com.google.protobuf.UnknownFieldSet unknownFields)
 
.lang.Override final Builder mergeUnknownFields (final com.google.protobuf.UnknownFieldSet unknownFields)
 

Static Public Member Functions

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

Protected Member Functions

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

Member Function Documentation

◆ addAllRestartAlgorithms()

Builder addAllRestartAlgorithms ( java.lang.Iterable<? extends com.google.ortools.sat.SatParameters.RestartAlgorithm values)
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
valuesThe restartAlgorithms to add.
Returns
This builder for chaining.

Definition at line 14041 of file SatParameters.java.

◆ addRepeatedField()

.lang.Override Builder addRepeatedField ( com.google.protobuf.Descriptors.FieldDescriptor  field,
java.lang.Object  value 
)

Definition at line 11666 of file SatParameters.java.

◆ addRestartAlgorithms()

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
valueThe restartAlgorithms to add.
Returns
This builder for chaining.

Definition at line 14016 of file SatParameters.java.

◆ build()

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

Definition at line 10949 of file SatParameters.java.

◆ buildPartial()

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

Definition at line 10958 of file SatParameters.java.

◆ clear()

.lang.Override Builder clear ( )

Definition at line 10604 of file SatParameters.java.

◆ clearAbsoluteGapLimit()

Builder clearAbsoluteGapLimit ( )
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
This builder for chaining.

Definition at line 14979 of file SatParameters.java.

◆ clearAddCgCuts()

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

optional bool add_cg_cuts = 117 [default = true];

Returns
This builder for chaining.

Definition at line 18227 of file SatParameters.java.

◆ clearAddCliqueCuts()

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

optional bool add_clique_cuts = 172 [default = true];

Returns
This builder for chaining.

Definition at line 18408 of file SatParameters.java.

◆ clearAddKnapsackCuts()

Builder clearAddKnapsackCuts ( )
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
This builder for chaining.

Definition at line 18168 of file SatParameters.java.

◆ clearAddLinMaxCuts()

Builder clearAddLinMaxCuts ( )
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
This builder for chaining.

Definition at line 18534 of file SatParameters.java.

◆ clearAddLpConstraintsLazily()

Builder clearAddLpConstraintsLazily ( )
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
This builder for chaining.

Definition at line 18680 of file SatParameters.java.

◆ clearAddMirCuts()

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

optional bool add_mir_cuts = 120 [default = true];

Returns
This builder for chaining.

Definition at line 18286 of file SatParameters.java.

◆ clearAddZeroHalfCuts()

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

optional bool add_zero_half_cuts = 169 [default = true];

Returns
This builder for chaining.

Definition at line 18345 of file SatParameters.java.

◆ clearAlsoBumpVariablesInConflictReasons()

Builder clearAlsoBumpVariablesInConflictReasons ( )
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
This builder for chaining.

Definition at line 12905 of file SatParameters.java.

◆ clearAutoDetectGreaterThanAtLeastOneOf()

Builder clearAutoDetectGreaterThanAtLeastOneOf ( )
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
This builder for chaining.

Definition at line 20298 of file SatParameters.java.

◆ clearBinaryMinimizationAlgorithm()

Builder clearBinaryMinimizationAlgorithm ( )

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

Returns
This builder for chaining.

Definition at line 12991 of file SatParameters.java.

◆ clearBinarySearchNumConflicts()

Builder clearBinarySearchNumConflicts ( )
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
This builder for chaining.

Definition at line 19872 of file SatParameters.java.

◆ clearBlockingRestartMultiplier()

Builder clearBlockingRestartMultiplier ( )

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns
This builder for chaining.

Definition at line 14502 of file SatParameters.java.

◆ clearBlockingRestartWindowSize()

Builder clearBlockingRestartWindowSize ( )

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns
This builder for chaining.

Definition at line 14463 of file SatParameters.java.

◆ clearBooleanEncodingLevel()

Builder clearBooleanEncodingLevel ( )
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
This builder for chaining.

Definition at line 17979 of file SatParameters.java.

◆ clearCatchSigintSignal()

Builder clearCatchSigintSignal ( )
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
This builder for chaining.

Definition at line 21615 of file SatParameters.java.

◆ clearClauseActivityDecay()

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

optional double clause_activity_decay = 17 [default = 0.999];

Returns
This builder for chaining.

Definition at line 13863 of file SatParameters.java.

◆ clearClauseCleanupLbdBound()

Builder clearClauseCleanupLbdBound ( )
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
This builder for chaining.

Definition at line 13274 of file SatParameters.java.

◆ clearClauseCleanupOrdering()

Builder clearClauseCleanupOrdering ( )

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

Returns
This builder for chaining.

Definition at line 13317 of file SatParameters.java.

◆ clearClauseCleanupPeriod()

Builder clearClauseCleanupPeriod ( )
Trigger a cleanup when this number of "deletable" clauses is learned.

optional int32 clause_cleanup_period = 11 [default = 10000];

Returns
This builder for chaining.

Definition at line 13113 of file SatParameters.java.

◆ clearClauseCleanupProtection()

Builder clearClauseCleanupProtection ( )

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

Returns
This builder for chaining.

Definition at line 13215 of file SatParameters.java.

◆ clearClauseCleanupTarget()

Builder clearClauseCleanupTarget ( )
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
This builder for chaining.

Definition at line 13172 of file SatParameters.java.

◆ clearConvertIntervals()

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

optional bool convert_intervals = 177 [default = false];

Returns
This builder for chaining.

Definition at line 21808 of file SatParameters.java.

◆ clearCountAssumptionLevelsInLbd()

Builder clearCountAssumptionLevelsInLbd ( )
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
This builder for chaining.

Definition at line 15795 of file SatParameters.java.

◆ clearCoverOptimization()

Builder clearCoverOptimization ( )
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
This builder for chaining.

Definition at line 17392 of file SatParameters.java.

◆ clearCpModelMaxNumPresolveOperations()

Builder clearCpModelMaxNumPresolveOperations ( )
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
This builder for chaining.

Definition at line 16401 of file SatParameters.java.

◆ clearCpModelPostsolveWithFullSolver()

Builder clearCpModelPostsolveWithFullSolver ( )
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
This builder for chaining.

Definition at line 16342 of file SatParameters.java.

◆ clearCpModelPresolve()

Builder clearCpModelPresolve ( )
Whether we presolve the cp_model before solving it.

optional bool cp_model_presolve = 86 [default = true];

Returns
This builder for chaining.

Definition at line 16275 of file SatParameters.java.

◆ clearCpModelProbingLevel()

Builder clearCpModelProbingLevel ( )
How much effort do we spend on probing. 0 disables it completely.

optional int32 cp_model_probing_level = 110 [default = 2];

Returns
This builder for chaining.

Definition at line 16456 of file SatParameters.java.

◆ clearCpModelUseSatPresolve()

Builder clearCpModelUseSatPresolve ( )
Whether we also use the sat presolve when cp_model_presolve is true.

optional bool cp_model_use_sat_presolve = 93 [default = true];

Returns
This builder for chaining.

Definition at line 16511 of file SatParameters.java.

◆ clearCutActiveCountDecay()

Builder clearCutActiveCountDecay ( )

optional double cut_active_count_decay = 156 [default = 0.8];

Returns
This builder for chaining.

Definition at line 18971 of file SatParameters.java.

◆ clearCutCleanupTarget()

Builder clearCutCleanupTarget ( )
Target number of constraints to remove during cleanup.

optional int32 cut_cleanup_target = 157 [default = 1000];

Returns
This builder for chaining.

Definition at line 19026 of file SatParameters.java.

◆ clearCutMaxActiveCountValue()

Builder clearCutMaxActiveCountValue ( )
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
This builder for chaining.

Definition at line 18932 of file SatParameters.java.

◆ clearDefaultRestartAlgorithms()

Builder clearDefaultRestartAlgorithms ( )

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

Returns
This builder for chaining.

Definition at line 14134 of file SatParameters.java.

◆ clearDisableConstraintExpansion()

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

optional bool disable_constraint_expansion = 181 [default = false];

Returns
This builder for chaining.

Definition at line 16900 of file SatParameters.java.

◆ clearDiversifyLnsParams()

Builder clearDiversifyLnsParams ( )
If true, registers more lns subsolvers with different parameters.

optional bool diversify_lns_params = 137 [default = false];

Returns
This builder for chaining.

Definition at line 21162 of file SatParameters.java.

◆ clearEnumerateAllSolutions()

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

optional bool enumerate_all_solutions = 87 [default = false];

Returns
This builder for chaining.

Definition at line 20022 of file SatParameters.java.

◆ clearExpandAlldiffConstraints()

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

optional bool expand_alldiff_constraints = 170 [default = false];

Returns
This builder for chaining.

Definition at line 16782 of file SatParameters.java.

◆ clearExpandAutomatonConstraints()

Builder clearExpandAutomatonConstraints ( )
If true, the automaton constraints are expanded.

optional bool expand_automaton_constraints = 143 [default = true];

Returns
This builder for chaining.

Definition at line 16664 of file SatParameters.java.

◆ clearExpandElementConstraints()

Builder clearExpandElementConstraints ( )
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
This builder for chaining.

Definition at line 16609 of file SatParameters.java.

◆ clearExpandReservoirConstraints()

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

optional bool expand_reservoir_constraints = 182 [default = true];

Returns
This builder for chaining.

Definition at line 16841 of file SatParameters.java.

◆ clearExpandTableConstraints()

Builder clearExpandTableConstraints ( )
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
This builder for chaining.

Definition at line 16723 of file SatParameters.java.

◆ clearExploitAllLpSolution()

Builder clearExploitAllLpSolution ( )
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
This builder for chaining.

Definition at line 19380 of file SatParameters.java.

◆ clearExploitBestSolution()

Builder clearExploitBestSolution ( )
When branching on a variable, follow the last best solution value.

optional bool exploit_best_solution = 130 [default = false];

Returns
This builder for chaining.

Definition at line 19435 of file SatParameters.java.

◆ clearExploitIntegerLpSolution()

Builder clearExploitIntegerLpSolution ( )
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
This builder for chaining.

Definition at line 19317 of file SatParameters.java.

◆ clearExploitObjective()

Builder clearExploitObjective ( )
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
This builder for chaining.

Definition at line 19557 of file SatParameters.java.

◆ clearExploitRelaxationSolution()

Builder clearExploitRelaxationSolution ( )
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
This builder for chaining.

Definition at line 19498 of file SatParameters.java.

◆ clearField()

.lang.Override Builder clearField ( com.google.protobuf.Descriptors.FieldDescriptor  field)

Definition at line 11650 of file SatParameters.java.

◆ clearFillTightenedDomainsInResponse()

Builder clearFillTightenedDomainsInResponse ( )
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
This builder for chaining.

Definition at line 20172 of file SatParameters.java.

◆ clearFindMultipleCores()

Builder clearFindMultipleCores ( )
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
This builder for chaining.

Definition at line 17333 of file SatParameters.java.

◆ clearFpRounding()

Builder clearFpRounding ( )

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

Returns
This builder for chaining.

Definition at line 21048 of file SatParameters.java.

◆ clearGlucoseDecayIncrement()

Builder clearGlucoseDecayIncrement ( )

optional double glucose_decay_increment = 23 [default = 0.01];

Returns
This builder for chaining.

Definition at line 13769 of file SatParameters.java.

◆ clearGlucoseDecayIncrementPeriod()

Builder clearGlucoseDecayIncrementPeriod ( )

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns
This builder for chaining.

Definition at line 13808 of file SatParameters.java.

◆ clearGlucoseMaxDecay()

Builder clearGlucoseMaxDecay ( )
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
This builder for chaining.

Definition at line 13730 of file SatParameters.java.

◆ clearHintConflictLimit()

Builder clearHintConflictLimit ( )
Conflict limit used in the phase that exploit the solution hint.

optional int32 hint_conflict_limit = 153 [default = 10];

Returns
This builder for chaining.

Definition at line 19183 of file SatParameters.java.

◆ clearInitialPolarity()

Builder clearInitialPolarity ( )

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

Returns
This builder for chaining.

Definition at line 12416 of file SatParameters.java.

◆ clearInitialVariablesActivity()

Builder clearInitialVariablesActivity ( )
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
This builder for chaining.

Definition at line 12838 of file SatParameters.java.

◆ clearInstantiateAllVariables()

Builder clearInstantiateAllVariables ( )
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
This builder for chaining.

Definition at line 20231 of file SatParameters.java.

◆ clearInterleaveBatchSize()

Builder clearInterleaveBatchSize ( )

optional int32 interleave_batch_size = 134 [default = 1];

Returns
This builder for chaining.

Definition at line 20597 of file SatParameters.java.

◆ clearInterleaveSearch()

Builder clearInterleaveSearch ( )
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
This builder for chaining.

Definition at line 20558 of file SatParameters.java.

◆ clearKeepAllFeasibleSolutionsInPresolve()

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

optional bool keep_all_feasible_solutions_in_presolve = 173 [default = false];

Returns
This builder for chaining.

Definition at line 20101 of file SatParameters.java.

◆ clearLinearizationLevel()

Builder clearLinearizationLevel ( )
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
This builder for chaining.

Definition at line 17920 of file SatParameters.java.

◆ clearLnsExpandIntervalsInConstraintGraph()

Builder clearLnsExpandIntervalsInConstraintGraph ( )

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns
This builder for chaining.

Definition at line 20895 of file SatParameters.java.

◆ clearLnsFocusOnDecisionVariables()

Builder clearLnsFocusOnDecisionVariables ( )

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns
This builder for chaining.

Definition at line 20856 of file SatParameters.java.

◆ clearLogPrefix()

Builder clearLogPrefix ( )
Add a prefix to all logs.

optional string log_prefix = 185 [default = ""];

Returns
This builder for chaining.

Definition at line 15449 of file SatParameters.java.

◆ clearLogSearchProgress()

Builder clearLogSearchProgress ( )
Whether the solver should log the search progress. By default, it logs to
LOG(INFO). This can be overwritten by the log_destination parameter.

optional bool log_search_progress = 41 [default = false];

Returns
This builder for chaining.

Definition at line 15360 of file SatParameters.java.

◆ clearLogToResponse()

Builder clearLogToResponse ( )
Log to response proto.

optional bool log_to_response = 187 [default = false];

Returns
This builder for chaining.

Definition at line 15578 of file SatParameters.java.

◆ clearLogToStdout()

Builder clearLogToStdout ( )
Log to stdout.

optional bool log_to_stdout = 186 [default = true];

Returns
This builder for chaining.

Definition at line 15523 of file SatParameters.java.

◆ clearMaxAllDiffCutSize()

Builder clearMaxAllDiffCutSize ( )
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
This builder for chaining.

Definition at line 18471 of file SatParameters.java.

◆ clearMaxClauseActivityValue()

Builder clearMaxClauseActivityValue ( )

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

Returns
This builder for chaining.

Definition at line 13902 of file SatParameters.java.

◆ clearMaxConsecutiveInactiveCount()

Builder clearMaxConsecutiveInactiveCount ( )
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
This builder for chaining.

Definition at line 18869 of file SatParameters.java.

◆ clearMaxCutRoundsAtLevelZero()

Builder clearMaxCutRoundsAtLevelZero ( )
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
This builder for chaining.

Definition at line 18806 of file SatParameters.java.

◆ clearMaxDeterministicTime()

Builder clearMaxDeterministicTime ( )
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
This builder for chaining.

Definition at line 14746 of file SatParameters.java.

◆ clearMaxIntegerRoundingScaling()

Builder clearMaxIntegerRoundingScaling ( )
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
This builder for chaining.

Definition at line 18613 of file SatParameters.java.

◆ clearMaxMemoryInMb()

Builder clearMaxMemoryInMb ( )
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
This builder for chaining.

Definition at line 14888 of file SatParameters.java.

◆ clearMaxNumberOfConflicts()

Builder clearMaxNumberOfConflicts ( )
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
This builder for chaining.

Definition at line 14821 of file SatParameters.java.

◆ clearMaxNumCuts()

Builder clearMaxNumCuts ( )
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
This builder for chaining.

Definition at line 18046 of file SatParameters.java.

◆ clearMaxPresolveIterations()

Builder clearMaxPresolveIterations ( )
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
This builder for chaining.

Definition at line 16220 of file SatParameters.java.

◆ clearMaxSatAssumptionOrder()

Builder clearMaxSatAssumptionOrder ( )

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

Returns
This builder for chaining.

Definition at line 17435 of file SatParameters.java.

◆ clearMaxSatReverseAssumptionOrder()

Builder clearMaxSatReverseAssumptionOrder ( )
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
This builder for chaining.

Definition at line 17494 of file SatParameters.java.

◆ clearMaxSatStratification()

Builder clearMaxSatStratification ( )

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

Returns
This builder for chaining.

Definition at line 17537 of file SatParameters.java.

◆ clearMaxTimeInSeconds()

Builder clearMaxTimeInSeconds ( )
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
This builder for chaining.

Definition at line 14683 of file SatParameters.java.

◆ clearMaxVariableActivityValue()

Builder clearMaxVariableActivityValue ( )

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

Returns
This builder for chaining.

Definition at line 13663 of file SatParameters.java.

◆ clearMergeAtMostOneWorkLimit()

Builder clearMergeAtMostOneWorkLimit ( )

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns
This builder for chaining.

Definition at line 17010 of file SatParameters.java.

◆ clearMergeNoOverlapWorkLimit()

Builder clearMergeNoOverlapWorkLimit ( )
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
This builder for chaining.

Definition at line 16971 of file SatParameters.java.

◆ clearMinimizationAlgorithm()

Builder clearMinimizationAlgorithm ( )

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

Returns
This builder for chaining.

Definition at line 12948 of file SatParameters.java.

◆ clearMinimizeCore()

Builder clearMinimizeCore ( )
Whether we use a simple heuristic to try to minimize an UNSAT core.

optional bool minimize_core = 50 [default = true];

Returns
This builder for chaining.

Definition at line 17274 of file SatParameters.java.

◆ clearMinimizeReductionDuringPbResolution()

Builder clearMinimizeReductionDuringPbResolution ( )
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
This builder for chaining.

Definition at line 15712 of file SatParameters.java.

◆ clearMinimizeWithPropagationNumDecisions()

Builder clearMinimizeWithPropagationNumDecisions ( )

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns
This builder for chaining.

Definition at line 13545 of file SatParameters.java.

◆ clearMinimizeWithPropagationRestartPeriod()

Builder clearMinimizeWithPropagationRestartPeriod ( )
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
This builder for chaining.

Definition at line 13506 of file SatParameters.java.

◆ clearMinOrthogonalityForLpConstraints()

Builder clearMinOrthogonalityForLpConstraints ( )
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
This builder for chaining.

Definition at line 18751 of file SatParameters.java.

◆ clearMipAutomaticallyScaleVariables()

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

optional bool mip_automatically_scale_variables = 166 [default = true];

Returns
This builder for chaining.

Definition at line 22072 of file SatParameters.java.

◆ clearMipCheckPrecision()

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

optional double mip_check_precision = 128 [default = 0.0001];

Returns
This builder for chaining.

Definition at line 22305 of file SatParameters.java.

◆ clearMipMaxActivityExponent()

Builder clearMipMaxActivityExponent ( )
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
This builder for chaining.

Definition at line 22242 of file SatParameters.java.

◆ clearMipMaxBound()

Builder clearMipMaxBound ( )
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
This builder for chaining.

Definition at line 21938 of file SatParameters.java.

◆ clearMipVarScaling()

Builder clearMipVarScaling ( )
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
This builder for chaining.

Definition at line 22001 of file SatParameters.java.

◆ clearMipWantedPrecision()

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

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

Returns
This builder for chaining.

Definition at line 22163 of file SatParameters.java.

◆ clearName()

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

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

Returns
This builder for chaining.

Definition at line 12310 of file SatParameters.java.

◆ clearNewConstraintsBatchSize()

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

optional int32 new_constraints_batch_size = 122 [default = 50];

Returns
This builder for chaining.

Definition at line 19085 of file SatParameters.java.

◆ clearNumConflictsBeforeStrategyChanges()

Builder clearNumConflictsBeforeStrategyChanges ( )
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
This builder for chaining.

Definition at line 14565 of file SatParameters.java.

◆ clearNumSearchWorkers()

Builder clearNumSearchWorkers ( )
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
This builder for chaining.

Definition at line 20487 of file SatParameters.java.

◆ clearOneof()

.lang.Override Builder clearOneof ( com.google.protobuf.Descriptors.OneofDescriptor  oneof)

Definition at line 11655 of file SatParameters.java.

◆ clearOnlyAddCutsAtLevelZero()

Builder clearOnlyAddCutsAtLevelZero ( )
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
This builder for chaining.

Definition at line 18105 of file SatParameters.java.

◆ clearOptimizeWithCore()

Builder clearOptimizeWithCore ( )
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
This builder for chaining.

Definition at line 19805 of file SatParameters.java.

◆ clearOptimizeWithMaxHs()

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

optional bool optimize_with_max_hs = 85 [default = false];

Returns
This builder for chaining.

Definition at line 19947 of file SatParameters.java.

◆ clearPbCleanupIncrement()

Builder clearPbCleanupIncrement ( )
Same as for the clauses, but for the learned pseudo-Boolean constraints.

optional int32 pb_cleanup_increment = 46 [default = 200];

Returns
This builder for chaining.

Definition at line 13372 of file SatParameters.java.

◆ clearPbCleanupRatio()

Builder clearPbCleanupRatio ( )

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns
This builder for chaining.

Definition at line 13411 of file SatParameters.java.

◆ clearPermutePresolveConstraintOrder()

Builder clearPermutePresolveConstraintOrder ( )

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns
This builder for chaining.

Definition at line 15262 of file SatParameters.java.

◆ clearPermuteVariableRandomly()

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

optional bool permute_variable_randomly = 178 [default = false];

Returns
This builder for chaining.

Definition at line 15223 of file SatParameters.java.

◆ clearPolarityRephaseIncrement()

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

optional int32 polarity_rephase_increment = 168 [default = 1000];

Returns
This builder for chaining.

Definition at line 12566 of file SatParameters.java.

◆ clearPolishLpSolution()

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

optional bool polish_lp_solution = 175 [default = false];

Returns
This builder for chaining.

Definition at line 21745 of file SatParameters.java.

◆ clearPreferredVariableOrder()

Builder clearPreferredVariableOrder ( )

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

Returns
This builder for chaining.

Definition at line 12373 of file SatParameters.java.

◆ clearPresolveBlockedClause()

Builder clearPresolveBlockedClause ( )
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
This builder for chaining.

Definition at line 16035 of file SatParameters.java.

◆ clearPresolveBvaThreshold()

Builder clearPresolveBvaThreshold ( )
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
This builder for chaining.

Definition at line 16157 of file SatParameters.java.

◆ clearPresolveBveClauseWeight()

Builder clearPresolveBveClauseWeight ( )
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
This builder for chaining.

Definition at line 15917 of file SatParameters.java.

◆ clearPresolveBveThreshold()

Builder clearPresolveBveThreshold ( )
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
This builder for chaining.

Definition at line 15858 of file SatParameters.java.

◆ clearPresolveExtractIntegerEnforcement()

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

optional bool presolve_extract_integer_enforcement = 174 [default = false];

Returns
This builder for chaining.

Definition at line 17152 of file SatParameters.java.

◆ clearPresolveProbingDeterministicTimeLimit()

Builder clearPresolveProbingDeterministicTimeLimit ( )
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
This builder for chaining.

Definition at line 15976 of file SatParameters.java.

◆ clearPresolveSubstitutionLevel()

Builder clearPresolveSubstitutionLevel ( )
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
This builder for chaining.

Definition at line 17077 of file SatParameters.java.

◆ clearPresolveUseBva()

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

optional bool presolve_use_bva = 72 [default = true];

Returns
This builder for chaining.

Definition at line 16090 of file SatParameters.java.

◆ clearProbingPeriodAtRoot()

Builder clearProbingPeriodAtRoot ( )
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
This builder for chaining.

Definition at line 19620 of file SatParameters.java.

◆ clearPseudoCostReliabilityThreshold()

Builder clearPseudoCostReliabilityThreshold ( )
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
This builder for chaining.

Definition at line 19738 of file SatParameters.java.

◆ clearRandomBranchesRatio()

Builder clearRandomBranchesRatio ( )
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
This builder for chaining.

Definition at line 12700 of file SatParameters.java.

◆ clearRandomizeSearch()

Builder clearRandomizeSearch ( )
Randomize fixed search.

optional bool randomize_search = 103 [default = false];

Returns
This builder for chaining.

Definition at line 21217 of file SatParameters.java.

◆ clearRandomPolarityRatio()

Builder clearRandomPolarityRatio ( )
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
This builder for chaining.

Definition at line 12637 of file SatParameters.java.

◆ clearRandomSeed()

Builder clearRandomSeed ( )
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
This builder for chaining.

Definition at line 15156 of file SatParameters.java.

◆ clearReduceMemoryUsageInInterleaveMode()

Builder clearReduceMemoryUsageInInterleaveMode ( )
Temporary parameter until the memory usage is more optimized.

optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];

Returns
This builder for chaining.

Definition at line 20652 of file SatParameters.java.

◆ clearRelativeGapLimit()

Builder clearRelativeGapLimit ( )

optional double relative_gap_limit = 160 [default = 0];

Returns
This builder for chaining.

Definition at line 15018 of file SatParameters.java.

◆ clearRepairHint()

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

optional bool repair_hint = 167 [default = false];

Returns
This builder for chaining.

Definition at line 19250 of file SatParameters.java.

◆ clearRestartAlgorithms()

Builder clearRestartAlgorithms ( )
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
This builder for chaining.

Definition at line 14065 of file SatParameters.java.

◆ clearRestartDlAverageRatio()

Builder clearRestartDlAverageRatio ( )
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
This builder for chaining.

Definition at line 14322 of file SatParameters.java.

◆ clearRestartLbdAverageRatio()

Builder clearRestartLbdAverageRatio ( )

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns
This builder for chaining.

Definition at line 14361 of file SatParameters.java.

◆ clearRestartPeriod()

Builder clearRestartPeriod ( )
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
This builder for chaining.

Definition at line 14208 of file SatParameters.java.

◆ clearRestartRunningWindowSize()

Builder clearRestartRunningWindowSize ( )
Size of the window for the moving average restarts.

optional int32 restart_running_window_size = 62 [default = 50];

Returns
This builder for chaining.

Definition at line 14263 of file SatParameters.java.

◆ clearSearchBranching()

Builder clearSearchBranching ( )

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

Returns
This builder for chaining.

Definition at line 19128 of file SatParameters.java.

◆ clearSearchRandomizationTolerance()

Builder clearSearchRandomizationTolerance ( )
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
This builder for chaining.

Definition at line 21296 of file SatParameters.java.

◆ clearShareLevelZeroBounds()

Builder clearShareLevelZeroBounds ( )
Allows sharing of the bounds of modified variables at level 0.

optional bool share_level_zero_bounds = 114 [default = true];

Returns
This builder for chaining.

Definition at line 20762 of file SatParameters.java.

◆ clearShareObjectiveBounds()

Builder clearShareObjectiveBounds ( )
Allows objective sharing between workers.

optional bool share_objective_bounds = 113 [default = true];

Returns
This builder for chaining.

Definition at line 20707 of file SatParameters.java.

◆ clearStopAfterFirstSolution()

Builder clearStopAfterFirstSolution ( )
For an optimization problem, stop the solver as soon as we have a solution.

optional bool stop_after_first_solution = 98 [default = false];

Returns
This builder for chaining.

Definition at line 20353 of file SatParameters.java.

◆ clearStopAfterPresolve()

Builder clearStopAfterPresolve ( )
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
This builder for chaining.

Definition at line 20412 of file SatParameters.java.

◆ clearStrategyChangeIncreaseRatio()

Builder clearStrategyChangeIncreaseRatio ( )
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
This builder for chaining.

Definition at line 14624 of file SatParameters.java.

◆ clearSubsumptionDuringConflictAnalysis()

Builder clearSubsumptionDuringConflictAnalysis ( )
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
This builder for chaining.

Definition at line 13058 of file SatParameters.java.

◆ clearSymmetryLevel()

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

optional int32 symmetry_level = 183 [default = 2];

Returns
This builder for chaining.

Definition at line 21875 of file SatParameters.java.

◆ clearTreatBinaryClausesSeparately()

Builder clearTreatBinaryClausesSeparately ( )
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
This builder for chaining.

Definition at line 15081 of file SatParameters.java.

◆ clearUseAbslRandom()

Builder clearUseAbslRandom ( )

optional bool use_absl_random = 180 [default = false];

Returns
This builder for chaining.

Definition at line 15301 of file SatParameters.java.

◆ clearUseBlockingRestart()

Builder clearUseBlockingRestart ( )
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
This builder for chaining.

Definition at line 14424 of file SatParameters.java.

◆ clearUseBranchingInLp()

Builder clearUseBranchingInLp ( )
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
This builder for chaining.

Definition at line 21489 of file SatParameters.java.

◆ clearUseCombinedNoOverlap()

Builder clearUseCombinedNoOverlap ( )
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
This builder for chaining.

Definition at line 21552 of file SatParameters.java.

◆ clearUseDisjunctiveConstraintInCumulativeConstraint()

Builder clearUseDisjunctiveConstraintInCumulativeConstraint ( )
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
This builder for chaining.

Definition at line 17853 of file SatParameters.java.

◆ clearUseErwaHeuristic()

Builder clearUseErwaHeuristic ( )
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
This builder for chaining.

Definition at line 12763 of file SatParameters.java.

◆ clearUseExactLpReason()

Builder clearUseExactLpReason ( )
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
This builder for chaining.

Definition at line 21426 of file SatParameters.java.

◆ clearUseFeasibilityPump()

Builder clearUseFeasibilityPump ( )
Adds a feasibility pump subsolver along with lns subsolvers.

optional bool use_feasibility_pump = 164 [default = true];

Returns
This builder for chaining.

Definition at line 21005 of file SatParameters.java.

◆ clearUseImpliedBounds()

Builder clearUseImpliedBounds ( )
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
This builder for chaining.

Definition at line 21678 of file SatParameters.java.

◆ clearUseLnsOnly()

Builder clearUseLnsOnly ( )
LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns
This builder for chaining.

Definition at line 20817 of file SatParameters.java.

◆ clearUseOptimizationHints()

Builder clearUseOptimizationHints ( )
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
This builder for chaining.

Definition at line 17219 of file SatParameters.java.

◆ clearUseOptionalVariables()

Builder clearUseOptionalVariables ( )
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
This builder for chaining.

Definition at line 21359 of file SatParameters.java.

◆ clearUseOverloadCheckerInCumulativeConstraint()

Builder clearUseOverloadCheckerInCumulativeConstraint ( )
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
This builder for chaining.

Definition at line 17695 of file SatParameters.java.

◆ clearUsePbResolution()

Builder clearUsePbResolution ( )
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
This builder for chaining.

Definition at line 15645 of file SatParameters.java.

◆ clearUsePhaseSaving()

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

optional bool use_phase_saving = 44 [default = true];

Returns
This builder for chaining.

Definition at line 12503 of file SatParameters.java.

◆ clearUsePrecedencesInDisjunctiveConstraint()

Builder clearUsePrecedencesInDisjunctiveConstraint ( )
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
This builder for chaining.

Definition at line 17620 of file SatParameters.java.

◆ clearUseProbingSearch()

Builder clearUseProbingSearch ( )
If true, search will continuously probe Boolean variables, and integer
variable bounds.

optional bool use_probing_search = 176 [default = false];

Returns
This builder for chaining.

Definition at line 19679 of file SatParameters.java.

◆ clearUseRelaxationLns()

Builder clearUseRelaxationLns ( )
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
This builder for chaining.

Definition at line 21107 of file SatParameters.java.

◆ clearUseRinsLns()

Builder clearUseRinsLns ( )
Turns on relaxation induced neighborhood generator.

optional bool use_rins_lns = 129 [default = true];

Returns
This builder for chaining.

Definition at line 20950 of file SatParameters.java.

◆ clearUseSatInprocessing()

Builder clearUseSatInprocessing ( )

optional bool use_sat_inprocessing = 163 [default = false];

Returns
This builder for chaining.

Definition at line 16550 of file SatParameters.java.

◆ clearUseTimetableEdgeFindingInCumulativeConstraint()

Builder clearUseTimetableEdgeFindingInCumulativeConstraint ( )
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
This builder for chaining.

Definition at line 17770 of file SatParameters.java.

◆ clearVariableActivityDecay()

Builder clearVariableActivityDecay ( )
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
This builder for chaining.

Definition at line 13624 of file SatParameters.java.

◆ clone()

.lang.Override Builder clone ( )

Definition at line 11640 of file SatParameters.java.

◆ getAbsoluteGapLimit()

.lang.Override double getAbsoluteGapLimit ( )
Stop the search when the gap between the best feasible objective (O) and
our best objective bound (B) is smaller than a limit.
The exact definition is:
  • Absolute: abs(O - B)
  • Relative: abs(O - B) / max(1, abs(O)). Important: The relative gap depends on the objective offset! If you artificially shift the objective, you will get widely different value of the relative gap. Note that if the gap is reached, the search status will be OPTIMAL. But one can check the best objective bound to see the actual gap.
optional double absolute_gap_limit = 159 [default = 0];
Returns
The absoluteGapLimit.

Implements SatParametersOrBuilder.

Definition at line 14935 of file SatParameters.java.

◆ getAddCgCuts()

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

optional bool add_cg_cuts = 117 [default = true];

Returns
The addCgCuts.

Implements SatParametersOrBuilder.

Definition at line 18199 of file SatParameters.java.

◆ getAddCliqueCuts()

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

optional bool add_clique_cuts = 172 [default = true];

Returns
The addCliqueCuts.

Implements SatParametersOrBuilder.

Definition at line 18378 of file SatParameters.java.

◆ getAddKnapsackCuts()

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

optional bool add_knapsack_cuts = 111 [default = false];

Returns
The addKnapsackCuts.

Implements SatParametersOrBuilder.

Definition at line 18138 of file SatParameters.java.

◆ getAddLinMaxCuts()

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

optional bool add_lin_max_cuts = 152 [default = true];

Returns
The addLinMaxCuts.

Implements SatParametersOrBuilder.

Definition at line 18504 of file SatParameters.java.

◆ getAddLpConstraintsLazily()

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

optional bool add_lp_constraints_lazily = 112 [default = true];

Returns
The addLpConstraintsLazily.

Implements SatParametersOrBuilder.

Definition at line 18648 of file SatParameters.java.

◆ getAddMirCuts()

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

optional bool add_mir_cuts = 120 [default = true];

Returns
The addMirCuts.

Implements SatParametersOrBuilder.

Definition at line 18258 of file SatParameters.java.

◆ getAddZeroHalfCuts()

.lang.Override boolean getAddZeroHalfCuts ( )
Whether we generate Zero-Half cuts at root node.
Note that for now, this is not heavily tuned.

optional bool add_zero_half_cuts = 169 [default = true];

Returns
The addZeroHalfCuts.

Implements SatParametersOrBuilder.

Definition at line 18317 of file SatParameters.java.

◆ getAlsoBumpVariablesInConflictReasons()

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

optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];

Returns
The alsoBumpVariablesInConflictReasons.

Implements SatParametersOrBuilder.

Definition at line 12873 of file SatParameters.java.

◆ getAutoDetectGreaterThanAtLeastOneOf()

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

optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];

Returns
The autoDetectGreaterThanAtLeastOneOf.

Implements SatParametersOrBuilder.

Definition at line 20266 of file SatParameters.java.

◆ getBinaryMinimizationAlgorithm()

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

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

Returns
The binaryMinimizationAlgorithm.

Implements SatParametersOrBuilder.

Definition at line 12968 of file SatParameters.java.

◆ getBinarySearchNumConflicts()

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

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

Returns
The binarySearchNumConflicts.

Implements SatParametersOrBuilder.

Definition at line 19840 of file SatParameters.java.

◆ getBlockingRestartMultiplier()

.lang.Override double getBlockingRestartMultiplier ( )

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns
The blockingRestartMultiplier.

Implements SatParametersOrBuilder.

Definition at line 14484 of file SatParameters.java.

◆ getBlockingRestartWindowSize()

.lang.Override int getBlockingRestartWindowSize ( )

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns
The blockingRestartWindowSize.

Implements SatParametersOrBuilder.

Definition at line 14445 of file SatParameters.java.

◆ getBooleanEncodingLevel()

.lang.Override int getBooleanEncodingLevel ( )
A non-negative level indicating how much we should try to fully encode
Integer variables as Boolean.

optional int32 boolean_encoding_level = 107 [default = 1];

Returns
The booleanEncodingLevel.

Implements SatParametersOrBuilder.

Definition at line 17951 of file SatParameters.java.

◆ getCatchSigintSignal()

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

optional bool catch_sigint_signal = 135 [default = true];

Returns
The catchSigintSignal.

Implements SatParametersOrBuilder.

Definition at line 21585 of file SatParameters.java.

◆ getClauseActivityDecay()

.lang.Override double getClauseActivityDecay ( )
Clause activity parameters (same effect as the one on the variables).

optional double clause_activity_decay = 17 [default = 0.999];

Returns
The clauseActivityDecay.

Implements SatParametersOrBuilder.

Definition at line 13837 of file SatParameters.java.

◆ getClauseCleanupLbdBound()

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

optional int32 clause_cleanup_lbd_bound = 59 [default = 5];

Returns
The clauseCleanupLbdBound.

Implements SatParametersOrBuilder.

Definition at line 13246 of file SatParameters.java.

◆ getClauseCleanupOrdering()

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

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

Returns
The clauseCleanupOrdering.

Implements SatParametersOrBuilder.

Definition at line 13294 of file SatParameters.java.

◆ getClauseCleanupPeriod()

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

optional int32 clause_cleanup_period = 11 [default = 10000];

Returns
The clauseCleanupPeriod.

Implements SatParametersOrBuilder.

Definition at line 13087 of file SatParameters.java.

◆ getClauseCleanupProtection()

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

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

Returns
The clauseCleanupProtection.

Implements SatParametersOrBuilder.

Definition at line 13192 of file SatParameters.java.

◆ getClauseCleanupTarget()

.lang.Override int getClauseCleanupTarget ( )
During a cleanup, we will always keep that number of "deletable" clauses.
Note that this doesn't include the "protected" clauses.

optional int32 clause_cleanup_target = 13 [default = 10000];

Returns
The clauseCleanupTarget.

Implements SatParametersOrBuilder.

Definition at line 13144 of file SatParameters.java.

◆ getConvertIntervals()

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

optional bool convert_intervals = 177 [default = false];

Returns
The convertIntervals.

Implements SatParametersOrBuilder.

Definition at line 21778 of file SatParameters.java.

◆ getCountAssumptionLevelsInLbd()

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

optional bool count_assumption_levels_in_lbd = 49 [default = true];

Returns
The countAssumptionLevelsInLbd.

Implements SatParametersOrBuilder.

Definition at line 15755 of file SatParameters.java.

◆ getCoverOptimization()

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

optional bool cover_optimization = 89 [default = true];

Returns
The coverOptimization.

Implements SatParametersOrBuilder.

Definition at line 17364 of file SatParameters.java.

◆ getCpModelMaxNumPresolveOperations()

.lang.Override int getCpModelMaxNumPresolveOperations ( )
If positive, try to stop just after that many presolve rules have been
applied. This is mainly useful for debugging presolve.

optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];

Returns
The cpModelMaxNumPresolveOperations.

Implements SatParametersOrBuilder.

Definition at line 16373 of file SatParameters.java.

◆ getCpModelPostsolveWithFullSolver()

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

optional bool cp_model_postsolve_with_full_solver = 162 [default = false];

Returns
The cpModelPostsolveWithFullSolver.

Implements SatParametersOrBuilder.

Definition at line 16310 of file SatParameters.java.

◆ getCpModelPresolve()

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

optional bool cp_model_presolve = 86 [default = true];

Returns
The cpModelPresolve.

Implements SatParametersOrBuilder.

Definition at line 16249 of file SatParameters.java.

◆ getCpModelProbingLevel()

.lang.Override int getCpModelProbingLevel ( )
How much effort do we spend on probing. 0 disables it completely.

optional int32 cp_model_probing_level = 110 [default = 2];

Returns
The cpModelProbingLevel.

Implements SatParametersOrBuilder.

Definition at line 16430 of file SatParameters.java.

◆ getCpModelUseSatPresolve()

.lang.Override boolean getCpModelUseSatPresolve ( )
Whether we also use the sat presolve when cp_model_presolve is true.

optional bool cp_model_use_sat_presolve = 93 [default = true];

Returns
The cpModelUseSatPresolve.

Implements SatParametersOrBuilder.

Definition at line 16485 of file SatParameters.java.

◆ getCutActiveCountDecay()

.lang.Override double getCutActiveCountDecay ( )

optional double cut_active_count_decay = 156 [default = 0.8];

Returns
The cutActiveCountDecay.

Implements SatParametersOrBuilder.

Definition at line 18953 of file SatParameters.java.

◆ getCutCleanupTarget()

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

optional int32 cut_cleanup_target = 157 [default = 1000];

Returns
The cutCleanupTarget.

Implements SatParametersOrBuilder.

Definition at line 19000 of file SatParameters.java.

◆ getCutMaxActiveCountValue()

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

optional double cut_max_active_count_value = 155 [default = 10000000000];

Returns
The cutMaxActiveCountValue.

Implements SatParametersOrBuilder.

Definition at line 18902 of file SatParameters.java.

◆ getDefaultInstanceForType()

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

Definition at line 10944 of file SatParameters.java.

◆ getDefaultRestartAlgorithms()

java.lang.String getDefaultRestartAlgorithms ( )

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

Returns
The defaultRestartAlgorithms.

Implements SatParametersOrBuilder.

Definition at line 14084 of file SatParameters.java.

◆ getDefaultRestartAlgorithmsBytes()

com.google.protobuf.ByteString getDefaultRestartAlgorithmsBytes ( )

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

Returns
The bytes for defaultRestartAlgorithms.

Implements SatParametersOrBuilder.

Definition at line 14103 of file SatParameters.java.

◆ getDescriptor()

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

Definition at line 10576 of file SatParameters.java.

◆ getDescriptorForType()

.lang.Override com.google.protobuf.Descriptors.Descriptor getDescriptorForType ( )

Definition at line 10939 of file SatParameters.java.

◆ getDisableConstraintExpansion()

.lang.Override boolean getDisableConstraintExpansion ( )
If true, it disable all constraint expansion.
This should only be used to test the presolve of expanded constraints.

optional bool disable_constraint_expansion = 181 [default = false];

Returns
The disableConstraintExpansion.

Implements SatParametersOrBuilder.

Definition at line 16872 of file SatParameters.java.

◆ getDiversifyLnsParams()

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

optional bool diversify_lns_params = 137 [default = false];

Returns
The diversifyLnsParams.

Implements SatParametersOrBuilder.

Definition at line 21136 of file SatParameters.java.

◆ getEnumerateAllSolutions()

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

optional bool enumerate_all_solutions = 87 [default = false];

Returns
The enumerateAllSolutions.

Implements SatParametersOrBuilder.

Definition at line 19986 of file SatParameters.java.

◆ getExpandAlldiffConstraints()

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

optional bool expand_alldiff_constraints = 170 [default = false];

Returns
The expandAlldiffConstraints.

Implements SatParametersOrBuilder.

Definition at line 16754 of file SatParameters.java.

◆ getExpandAutomatonConstraints()

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

optional bool expand_automaton_constraints = 143 [default = true];

Returns
The expandAutomatonConstraints.

Implements SatParametersOrBuilder.

Definition at line 16638 of file SatParameters.java.

◆ getExpandElementConstraints()

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

optional bool expand_element_constraints = 140 [default = true];

Returns
The expandElementConstraints.

Implements SatParametersOrBuilder.

Definition at line 16581 of file SatParameters.java.

◆ getExpandReservoirConstraints()

.lang.Override boolean getExpandReservoirConstraints ( )
If true, expand the reservoir constraints by creating booleans for all
possible precedences between event and encoding the constraint.

optional bool expand_reservoir_constraints = 182 [default = true];

Returns
The expandReservoirConstraints.

Implements SatParametersOrBuilder.

Definition at line 16813 of file SatParameters.java.

◆ getExpandTableConstraints()

.lang.Override boolean getExpandTableConstraints ( )
If true, the positive table constraints are expanded.
Note that currently, negative table constraints are always expanded.

optional bool expand_table_constraints = 158 [default = true];

Returns
The expandTableConstraints.

Implements SatParametersOrBuilder.

Definition at line 16695 of file SatParameters.java.

◆ getExploitAllLpSolution()

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

optional bool exploit_all_lp_solution = 116 [default = true];

Returns
The exploitAllLpSolution.

Implements SatParametersOrBuilder.

Definition at line 19350 of file SatParameters.java.

◆ getExploitBestSolution()

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

optional bool exploit_best_solution = 130 [default = false];

Returns
The exploitBestSolution.

Implements SatParametersOrBuilder.

Definition at line 19409 of file SatParameters.java.

◆ getExploitIntegerLpSolution()

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

optional bool exploit_integer_lp_solution = 94 [default = true];

Returns
The exploitIntegerLpSolution.

Implements SatParametersOrBuilder.

Definition at line 19285 of file SatParameters.java.

◆ getExploitObjective()

.lang.Override boolean getExploitObjective ( )
When branching an a variable that directly affect the objective,
branch on the value that lead to the best objective first.

optional bool exploit_objective = 131 [default = true];

Returns
The exploitObjective.

Implements SatParametersOrBuilder.

Definition at line 19529 of file SatParameters.java.

◆ getExploitRelaxationSolution()

.lang.Override boolean getExploitRelaxationSolution ( )
When branching on a variable, follow the last best relaxation solution
value. We use the relaxation with the tightest bound on the objective as
the best relaxation solution.

optional bool exploit_relaxation_solution = 161 [default = false];

Returns
The exploitRelaxationSolution.

Implements SatParametersOrBuilder.

Definition at line 19468 of file SatParameters.java.

◆ getFillTightenedDomainsInResponse()

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

optional bool fill_tightened_domains_in_response = 132 [default = false];

Returns
The fillTightenedDomainsInResponse.

Implements SatParametersOrBuilder.

Definition at line 20138 of file SatParameters.java.

◆ getFindMultipleCores()

.lang.Override boolean getFindMultipleCores ( )
Whether we try to find more independent cores for a given set of
assumptions in the core based max-SAT algorithms.

optional bool find_multiple_cores = 84 [default = true];

Returns
The findMultipleCores.

Implements SatParametersOrBuilder.

Definition at line 17305 of file SatParameters.java.

◆ getFpRounding()

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

Returns
The fpRounding.

Implements SatParametersOrBuilder.

Definition at line 21025 of file SatParameters.java.

◆ getGlucoseDecayIncrement()

.lang.Override double getGlucoseDecayIncrement ( )

optional double glucose_decay_increment = 23 [default = 0.01];

Returns
The glucoseDecayIncrement.

Implements SatParametersOrBuilder.

Definition at line 13751 of file SatParameters.java.

◆ getGlucoseDecayIncrementPeriod()

.lang.Override int getGlucoseDecayIncrementPeriod ( )

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns
The glucoseDecayIncrementPeriod.

Implements SatParametersOrBuilder.

Definition at line 13790 of file SatParameters.java.

◆ getGlucoseMaxDecay()

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

optional double glucose_max_decay = 22 [default = 0.95];

Returns
The glucoseMaxDecay.

Implements SatParametersOrBuilder.

Definition at line 13698 of file SatParameters.java.

◆ getHintConflictLimit()

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

optional int32 hint_conflict_limit = 153 [default = 10];

Returns
The hintConflictLimit.

Implements SatParametersOrBuilder.

Definition at line 19157 of file SatParameters.java.

◆ getInitialPolarity()

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

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

Returns
The initialPolarity.

Implements SatParametersOrBuilder.

Definition at line 12393 of file SatParameters.java.

◆ getInitialVariablesActivity()

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

optional double initial_variables_activity = 76 [default = 0];

Returns
The initialVariablesActivity.

Implements SatParametersOrBuilder.

Definition at line 12802 of file SatParameters.java.

◆ getInstantiateAllVariables()

.lang.Override boolean getInstantiateAllVariables ( )
If true, the solver will add a default integer branching strategy to the
already defined search strategy.

optional bool instantiate_all_variables = 106 [default = true];

Returns
The instantiateAllVariables.

Implements SatParametersOrBuilder.

Definition at line 20203 of file SatParameters.java.

◆ getInterleaveBatchSize()

.lang.Override int getInterleaveBatchSize ( )

optional int32 interleave_batch_size = 134 [default = 1];

Returns
The interleaveBatchSize.

Implements SatParametersOrBuilder.

Definition at line 20579 of file SatParameters.java.

◆ getInterleaveSearch()

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

optional bool interleave_search = 136 [default = false];

Returns
The interleaveSearch.

Implements SatParametersOrBuilder.

Definition at line 20524 of file SatParameters.java.

◆ getKeepAllFeasibleSolutionsInPresolve()

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

optional bool keep_all_feasible_solutions_in_presolve = 173 [default = false];

Returns
The keepAllFeasibleSolutionsInPresolve.

Implements SatParametersOrBuilder.

Definition at line 20063 of file SatParameters.java.

◆ getLinearizationLevel()

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

optional int32 linearization_level = 90 [default = 1];

Returns
The linearizationLevel.

Implements SatParametersOrBuilder.

Definition at line 17888 of file SatParameters.java.

◆ getLnsExpandIntervalsInConstraintGraph()

.lang.Override boolean getLnsExpandIntervalsInConstraintGraph ( )

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns
The lnsExpandIntervalsInConstraintGraph.

Implements SatParametersOrBuilder.

Definition at line 20877 of file SatParameters.java.

◆ getLnsFocusOnDecisionVariables()

.lang.Override boolean getLnsFocusOnDecisionVariables ( )

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns
The lnsFocusOnDecisionVariables.

Implements SatParametersOrBuilder.

Definition at line 20838 of file SatParameters.java.

◆ getLogPrefix()

java.lang.String getLogPrefix ( )
Add a prefix to all logs.

optional string log_prefix = 185 [default = ""];

Returns
The logPrefix.

Implements SatParametersOrBuilder.

Definition at line 15387 of file SatParameters.java.

◆ getLogPrefixBytes()

com.google.protobuf.ByteString getLogPrefixBytes ( )
Add a prefix to all logs.

optional string log_prefix = 185 [default = ""];

Returns
The bytes for logPrefix.

Implements SatParametersOrBuilder.

Definition at line 15410 of file SatParameters.java.

◆ getLogSearchProgress()

.lang.Override boolean getLogSearchProgress ( )
Whether the solver should log the search progress. By default, it logs to
LOG(INFO). This can be overwritten by the log_destination parameter.

optional bool log_search_progress = 41 [default = false];

Returns
The logSearchProgress.

Implements SatParametersOrBuilder.

Definition at line 15332 of file SatParameters.java.

◆ getLogToResponse()

.lang.Override boolean getLogToResponse ( )
Log to response proto.

optional bool log_to_response = 187 [default = false];

Returns
The logToResponse.

Implements SatParametersOrBuilder.

Definition at line 15552 of file SatParameters.java.

◆ getLogToStdout()

.lang.Override boolean getLogToStdout ( )
Log to stdout.

optional bool log_to_stdout = 186 [default = true];

Returns
The logToStdout.

Implements SatParametersOrBuilder.

Definition at line 15497 of file SatParameters.java.

◆ getMaxAllDiffCutSize()

.lang.Override int getMaxAllDiffCutSize ( )
Cut generator for all diffs can add too many cuts for large all_diff
constraints. This parameter restricts the large all_diff constraints to
have a cut generator.

optional int32 max_all_diff_cut_size = 148 [default = 7];

Returns
The maxAllDiffCutSize.

Implements SatParametersOrBuilder.

Definition at line 18441 of file SatParameters.java.

◆ getMaxClauseActivityValue()

.lang.Override double getMaxClauseActivityValue ( )

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

Returns
The maxClauseActivityValue.

Implements SatParametersOrBuilder.

Definition at line 13884 of file SatParameters.java.

◆ getMaxConsecutiveInactiveCount()

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

optional int32 max_consecutive_inactive_count = 121 [default = 100];

Returns
The maxConsecutiveInactiveCount.

Implements SatParametersOrBuilder.

Definition at line 18839 of file SatParameters.java.

◆ getMaxCutRoundsAtLevelZero()

.lang.Override int getMaxCutRoundsAtLevelZero ( )
Max number of time we perform cut generation and resolve the LP at level 0.

optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];

Returns
The maxCutRoundsAtLevelZero.

Implements SatParametersOrBuilder.

Definition at line 18780 of file SatParameters.java.

◆ getMaxDeterministicTime()

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

optional double max_deterministic_time = 67 [default = inf];

Returns
The maxDeterministicTime.

Implements SatParametersOrBuilder.

Definition at line 14716 of file SatParameters.java.

◆ getMaxIntegerRoundingScaling()

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

optional int32 max_integer_rounding_scaling = 119 [default = 600];

Returns
The maxIntegerRoundingScaling.

Implements SatParametersOrBuilder.

Definition at line 18575 of file SatParameters.java.

◆ getMaxMemoryInMb()

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

optional int64 max_memory_in_mb = 40 [default = 10000];

Returns
The maxMemoryInMb.

Implements SatParametersOrBuilder.

Definition at line 14856 of file SatParameters.java.

◆ getMaxNumberOfConflicts()

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

optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];

Returns
The maxNumberOfConflicts.

Implements SatParametersOrBuilder.

Definition at line 14785 of file SatParameters.java.

◆ getMaxNumCuts()

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

optional int32 max_num_cuts = 91 [default = 10000];

Returns
The maxNumCuts.

Implements SatParametersOrBuilder.

Definition at line 18014 of file SatParameters.java.

◆ getMaxPresolveIterations()

.lang.Override int getMaxPresolveIterations ( )
In case of large reduction in a presolve iteration, we perform multiple
presolve iterations. This parameter controls the maximum number of such
presolve iterations.

optional int32 max_presolve_iterations = 138 [default = 3];

Returns
The maxPresolveIterations.

Implements SatParametersOrBuilder.

Definition at line 16190 of file SatParameters.java.

◆ getMaxSatAssumptionOrder()

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

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

Returns
The maxSatAssumptionOrder.

Implements SatParametersOrBuilder.

Definition at line 17412 of file SatParameters.java.

◆ getMaxSatReverseAssumptionOrder()

.lang.Override boolean getMaxSatReverseAssumptionOrder ( )
If true, adds the assumption in the reverse order of the one defined by
max_sat_assumption_order.

optional bool max_sat_reverse_assumption_order = 52 [default = false];

Returns
The maxSatReverseAssumptionOrder.

Implements SatParametersOrBuilder.

Definition at line 17466 of file SatParameters.java.

◆ getMaxSatStratification()

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

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

Returns
The maxSatStratification.

Implements SatParametersOrBuilder.

Definition at line 17514 of file SatParameters.java.

◆ getMaxTimeInSeconds()

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

optional double max_time_in_seconds = 36 [default = inf];

Returns
The maxTimeInSeconds.

Implements SatParametersOrBuilder.

Definition at line 14655 of file SatParameters.java.

◆ getMaxVariableActivityValue()

.lang.Override double getMaxVariableActivityValue ( )

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

Returns
The maxVariableActivityValue.

Implements SatParametersOrBuilder.

Definition at line 13645 of file SatParameters.java.

◆ getMergeAtMostOneWorkLimit()

.lang.Override double getMergeAtMostOneWorkLimit ( )

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns
The mergeAtMostOneWorkLimit.

Implements SatParametersOrBuilder.

Definition at line 16992 of file SatParameters.java.

◆ getMergeNoOverlapWorkLimit()

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

optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];

Returns
The mergeNoOverlapWorkLimit.

Implements SatParametersOrBuilder.

Definition at line 16937 of file SatParameters.java.

◆ getMinimizationAlgorithm()

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

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

Returns
The minimizationAlgorithm.

Implements SatParametersOrBuilder.

Definition at line 12925 of file SatParameters.java.

◆ getMinimizeCore()

.lang.Override boolean getMinimizeCore ( )
Whether we use a simple heuristic to try to minimize an UNSAT core.

optional bool minimize_core = 50 [default = true];

Returns
The minimizeCore.

Implements SatParametersOrBuilder.

Definition at line 17248 of file SatParameters.java.

◆ getMinimizeReductionDuringPbResolution()

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

optional bool minimize_reduction_during_pb_resolution = 48 [default = false];

Returns
The minimizeReductionDuringPbResolution.

Implements SatParametersOrBuilder.

Definition at line 15680 of file SatParameters.java.

◆ getMinimizeWithPropagationNumDecisions()

.lang.Override int getMinimizeWithPropagationNumDecisions ( )

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns
The minimizeWithPropagationNumDecisions.

Implements SatParametersOrBuilder.

Definition at line 13527 of file SatParameters.java.

◆ getMinimizeWithPropagationRestartPeriod()

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

optional int32 minimize_with_propagation_restart_period = 96 [default = 10];

Returns
The minimizeWithPropagationRestartPeriod.

Implements SatParametersOrBuilder.

Definition at line 13460 of file SatParameters.java.

◆ getMinOrthogonalityForLpConstraints()

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

optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];

Returns
The minOrthogonalityForLpConstraints.

Implements SatParametersOrBuilder.

Definition at line 18717 of file SatParameters.java.

◆ getMipAutomaticallyScaleVariables()

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

optional bool mip_automatically_scale_variables = 166 [default = true];

Returns
The mipAutomaticallyScaleVariables.

Implements SatParametersOrBuilder.

Definition at line 22038 of file SatParameters.java.

◆ getMipCheckPrecision()

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

optional double mip_check_precision = 128 [default = 0.0001];

Returns
The mipCheckPrecision.

Implements SatParametersOrBuilder.

Definition at line 22275 of file SatParameters.java.

◆ getMipMaxActivityExponent()

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

optional int32 mip_max_activity_exponent = 127 [default = 53];

Returns
The mipMaxActivityExponent.

Implements SatParametersOrBuilder.

Definition at line 22204 of file SatParameters.java.

◆ getMipMaxBound()

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

optional double mip_max_bound = 124 [default = 10000000];

Returns
The mipMaxBound.

Implements SatParametersOrBuilder.

Definition at line 21908 of file SatParameters.java.

◆ getMipVarScaling()

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

optional double mip_var_scaling = 125 [default = 1];

Returns
The mipVarScaling.

Implements SatParametersOrBuilder.

Definition at line 21971 of file SatParameters.java.

◆ getMipWantedPrecision()

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

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

Returns
The mipWantedPrecision.

Implements SatParametersOrBuilder.

Definition at line 22119 of file SatParameters.java.

◆ getName()

java.lang.String getName ( )
In some context, like in a portfolio of search, it makes sense to name a
given parameters set for logging purpose.

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

Returns
The name.

Implements SatParametersOrBuilder.

Definition at line 12245 of file SatParameters.java.

◆ getNameBytes()

com.google.protobuf.ByteString getNameBytes ( )
In some context, like in a portfolio of search, it makes sense to name a
given parameters set for logging purpose.

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

Returns
The bytes for name.

Implements SatParametersOrBuilder.

Definition at line 12269 of file SatParameters.java.

◆ getNewConstraintsBatchSize()

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

optional int32 new_constraints_batch_size = 122 [default = 50];

Returns
The newConstraintsBatchSize.

Implements SatParametersOrBuilder.

Definition at line 19057 of file SatParameters.java.

◆ getNumConflictsBeforeStrategyChanges()

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

optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];

Returns
The numConflictsBeforeStrategyChanges.

Implements SatParametersOrBuilder.

Definition at line 14535 of file SatParameters.java.

◆ getNumSearchWorkers()

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

optional int32 num_search_workers = 100 [default = 1];

Returns
The numSearchWorkers.

Implements SatParametersOrBuilder.

Definition at line 20451 of file SatParameters.java.

◆ getOnlyAddCutsAtLevelZero()

.lang.Override boolean getOnlyAddCutsAtLevelZero ( )
For the cut that can be generated at any level, this control if we only
try to generate them at the root node.

optional bool only_add_cuts_at_level_zero = 92 [default = false];

Returns
The onlyAddCutsAtLevelZero.

Implements SatParametersOrBuilder.

Definition at line 18077 of file SatParameters.java.

◆ getOptimizeWithCore()

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

optional bool optimize_with_core = 83 [default = false];

Returns
The optimizeWithCore.

Implements SatParametersOrBuilder.

Definition at line 19773 of file SatParameters.java.

◆ getOptimizeWithMaxHs()

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

optional bool optimize_with_max_hs = 85 [default = false];

Returns
The optimizeWithMaxHs.

Implements SatParametersOrBuilder.

Definition at line 19911 of file SatParameters.java.

◆ getPbCleanupIncrement()

.lang.Override int getPbCleanupIncrement ( )
Same as for the clauses, but for the learned pseudo-Boolean constraints.

optional int32 pb_cleanup_increment = 46 [default = 200];

Returns
The pbCleanupIncrement.

Implements SatParametersOrBuilder.

Definition at line 13346 of file SatParameters.java.

◆ getPbCleanupRatio()

.lang.Override double getPbCleanupRatio ( )

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns
The pbCleanupRatio.

Implements SatParametersOrBuilder.

Definition at line 13393 of file SatParameters.java.

◆ getPermutePresolveConstraintOrder()

.lang.Override boolean getPermutePresolveConstraintOrder ( )

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns
The permutePresolveConstraintOrder.

Implements SatParametersOrBuilder.

Definition at line 15244 of file SatParameters.java.

◆ getPermuteVariableRandomly()

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

optional bool permute_variable_randomly = 178 [default = false];

Returns
The permuteVariableRandomly.

Implements SatParametersOrBuilder.

Definition at line 15191 of file SatParameters.java.

◆ getPolarityRephaseIncrement()

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

optional int32 polarity_rephase_increment = 168 [default = 1000];

Returns
The polarityRephaseIncrement.

Implements SatParametersOrBuilder.

Definition at line 12536 of file SatParameters.java.

◆ getPolishLpSolution()

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

optional bool polish_lp_solution = 175 [default = false];

Returns
The polishLpSolution.

Implements SatParametersOrBuilder.

Definition at line 21713 of file SatParameters.java.

◆ getPreferredVariableOrder()

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

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

Returns
The preferredVariableOrder.

Implements SatParametersOrBuilder.

Definition at line 12350 of file SatParameters.java.

◆ getPresolveBlockedClause()

.lang.Override boolean getPresolveBlockedClause ( )
Whether we use an heuristic to detect some basic case of blocked clause
in the SAT presolve.

optional bool presolve_blocked_clause = 88 [default = true];

Returns
The presolveBlockedClause.

Implements SatParametersOrBuilder.

Definition at line 16007 of file SatParameters.java.

◆ getPresolveBvaThreshold()

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

optional int32 presolve_bva_threshold = 73 [default = 1];

Returns
The presolveBvaThreshold.

Implements SatParametersOrBuilder.

Definition at line 16125 of file SatParameters.java.

◆ getPresolveBveClauseWeight()

.lang.Override int getPresolveBveClauseWeight ( )
During presolve, we apply BVE only if this weight times the number of
clauses plus the number of clause literals is not increased.

optional int32 presolve_bve_clause_weight = 55 [default = 3];

Returns
The presolveBveClauseWeight.

Implements SatParametersOrBuilder.

Definition at line 15889 of file SatParameters.java.

◆ getPresolveBveThreshold()

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

optional int32 presolve_bve_threshold = 54 [default = 500];

Returns
The presolveBveThreshold.

Implements SatParametersOrBuilder.

Definition at line 15828 of file SatParameters.java.

◆ getPresolveExtractIntegerEnforcement()

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

optional bool presolve_extract_integer_enforcement = 174 [default = false];

Returns
The presolveExtractIntegerEnforcement.

Implements SatParametersOrBuilder.

Definition at line 17116 of file SatParameters.java.

◆ getPresolveProbingDeterministicTimeLimit()

.lang.Override double getPresolveProbingDeterministicTimeLimit ( )
The maximum "deterministic" time limit to spend in probing. A value of
zero will disable the probing.

optional double presolve_probing_deterministic_time_limit = 57 [default = 30];

Returns
The presolveProbingDeterministicTimeLimit.

Implements SatParametersOrBuilder.

Definition at line 15948 of file SatParameters.java.

◆ getPresolveSubstitutionLevel()

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

optional int32 presolve_substitution_level = 147 [default = 1];

Returns
The presolveSubstitutionLevel.

Implements SatParametersOrBuilder.

Definition at line 17045 of file SatParameters.java.

◆ getPresolveUseBva()

.lang.Override boolean getPresolveUseBva ( )
Whether or not we use Bounded Variable Addition (BVA) in the presolve.

optional bool presolve_use_bva = 72 [default = true];

Returns
The presolveUseBva.

Implements SatParametersOrBuilder.

Definition at line 16064 of file SatParameters.java.

◆ getProbingPeriodAtRoot()

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

optional int64 probing_period_at_root = 142 [default = 0];

Returns
The probingPeriodAtRoot.

Implements SatParametersOrBuilder.

Definition at line 19590 of file SatParameters.java.

◆ getPseudoCostReliabilityThreshold()

.lang.Override long getPseudoCostReliabilityThreshold ( )
The solver ignores the pseudo costs of variables with number of recordings
less than this threshold.

optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];

Returns
The pseudoCostReliabilityThreshold.

Implements SatParametersOrBuilder.

Definition at line 19710 of file SatParameters.java.

◆ getRandomBranchesRatio()

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

optional double random_branches_ratio = 32 [default = 0];

Returns
The randomBranchesRatio.

Implements SatParametersOrBuilder.

Definition at line 12670 of file SatParameters.java.

◆ getRandomizeSearch()

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

optional bool randomize_search = 103 [default = false];

Returns
The randomizeSearch.

Implements SatParametersOrBuilder.

Definition at line 21191 of file SatParameters.java.

◆ getRandomPolarityRatio()

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

optional double random_polarity_ratio = 45 [default = 0];

Returns
The randomPolarityRatio.

Implements SatParametersOrBuilder.

Definition at line 12603 of file SatParameters.java.

◆ getRandomSeed()

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

optional int32 random_seed = 31 [default = 1];

Returns
The randomSeed.

Implements SatParametersOrBuilder.

Definition at line 15120 of file SatParameters.java.

◆ getReduceMemoryUsageInInterleaveMode()

.lang.Override boolean getReduceMemoryUsageInInterleaveMode ( )
Temporary parameter until the memory usage is more optimized.

optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];

Returns
The reduceMemoryUsageInInterleaveMode.

Implements SatParametersOrBuilder.

Definition at line 20626 of file SatParameters.java.

◆ getRelativeGapLimit()

.lang.Override double getRelativeGapLimit ( )

optional double relative_gap_limit = 160 [default = 0];

Returns
The relativeGapLimit.

Implements SatParametersOrBuilder.

Definition at line 15000 of file SatParameters.java.

◆ getRepairHint()

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

optional bool repair_hint = 167 [default = false];

Returns
The repairHint.

Implements SatParametersOrBuilder.

Definition at line 19218 of file SatParameters.java.

◆ getRestartAlgorithms()

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

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

Parameters
indexThe index of the element to return.
Returns
The restartAlgorithms at the given index.

Implements SatParametersOrBuilder.

Definition at line 13970 of file SatParameters.java.

◆ getRestartAlgorithmsCount()

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

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

Returns
The count of restartAlgorithms.

Implements SatParametersOrBuilder.

Definition at line 13951 of file SatParameters.java.

◆ getRestartAlgorithmsList()

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

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

Returns
A list containing the restartAlgorithms.

Implements SatParametersOrBuilder.

Definition at line 13932 of file SatParameters.java.

◆ getRestartDlAverageRatio()

.lang.Override double getRestartDlAverageRatio ( )
In the moving average restart algorithms, a restart is triggered if the
window average times this ratio is greater that the global average.

optional double restart_dl_average_ratio = 63 [default = 1];

Returns
The restartDlAverageRatio.

Implements SatParametersOrBuilder.

Definition at line 14294 of file SatParameters.java.

◆ getRestartLbdAverageRatio()

.lang.Override double getRestartLbdAverageRatio ( )

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns
The restartLbdAverageRatio.

Implements SatParametersOrBuilder.

Definition at line 14343 of file SatParameters.java.

◆ getRestartPeriod()

.lang.Override int getRestartPeriod ( )
Restart period for the FIXED_RESTART strategy. This is also the multiplier
used by the LUBY_RESTART strategy.

optional int32 restart_period = 30 [default = 50];

Returns
The restartPeriod.

Implements SatParametersOrBuilder.

Definition at line 14180 of file SatParameters.java.

◆ getRestartRunningWindowSize()

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

optional int32 restart_running_window_size = 62 [default = 50];

Returns
The restartRunningWindowSize.

Implements SatParametersOrBuilder.

Definition at line 14237 of file SatParameters.java.

◆ getSearchBranching()

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

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

Returns
The searchBranching.

Implements SatParametersOrBuilder.

Definition at line 19105 of file SatParameters.java.

◆ getSearchRandomizationTolerance()

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

optional int64 search_randomization_tolerance = 104 [default = 0];

Returns
The searchRandomizationTolerance.

Implements SatParametersOrBuilder.

Definition at line 21258 of file SatParameters.java.

◆ getShareLevelZeroBounds()

.lang.Override boolean getShareLevelZeroBounds ( )
Allows sharing of the bounds of modified variables at level 0.

optional bool share_level_zero_bounds = 114 [default = true];

Returns
The shareLevelZeroBounds.

Implements SatParametersOrBuilder.

Definition at line 20736 of file SatParameters.java.

◆ getShareObjectiveBounds()

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

optional bool share_objective_bounds = 113 [default = true];

Returns
The shareObjectiveBounds.

Implements SatParametersOrBuilder.

Definition at line 20681 of file SatParameters.java.

◆ getStopAfterFirstSolution()

.lang.Override boolean getStopAfterFirstSolution ( )
For an optimization problem, stop the solver as soon as we have a solution.

optional bool stop_after_first_solution = 98 [default = false];

Returns
The stopAfterFirstSolution.

Implements SatParametersOrBuilder.

Definition at line 20327 of file SatParameters.java.

◆ getStopAfterPresolve()

.lang.Override boolean getStopAfterPresolve ( )
Mainly used when improving the presolver. When true, stops the solver after
the presolve is complete.

optional bool stop_after_presolve = 149 [default = false];

Returns
The stopAfterPresolve.

Implements SatParametersOrBuilder.

Definition at line 20384 of file SatParameters.java.

◆ getStrategyChangeIncreaseRatio()

.lang.Override double getStrategyChangeIncreaseRatio ( )
The parameter num_conflicts_before_strategy_changes is increased by that
much after each strategy change.

optional double strategy_change_increase_ratio = 69 [default = 0];

Returns
The strategyChangeIncreaseRatio.

Implements SatParametersOrBuilder.

Definition at line 14596 of file SatParameters.java.

◆ getSubsumptionDuringConflictAnalysis()

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

optional bool subsumption_during_conflict_analysis = 56 [default = true];

Returns
The subsumptionDuringConflictAnalysis.

Implements SatParametersOrBuilder.

Definition at line 13026 of file SatParameters.java.

◆ getSymmetryLevel()

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

optional int32 symmetry_level = 183 [default = 2];

Returns
The symmetryLevel.

Implements SatParametersOrBuilder.

Definition at line 21843 of file SatParameters.java.

◆ getTreatBinaryClausesSeparately()

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

optional bool treat_binary_clauses_separately = 33 [default = true];

Returns
The treatBinaryClausesSeparately.

Implements SatParametersOrBuilder.

Definition at line 15051 of file SatParameters.java.

◆ getUseAbslRandom()

.lang.Override boolean getUseAbslRandom ( )

optional bool use_absl_random = 180 [default = false];

Returns
The useAbslRandom.

Implements SatParametersOrBuilder.

Definition at line 15283 of file SatParameters.java.

◆ getUseBlockingRestart()

.lang.Override boolean getUseBlockingRestart ( )
Block a moving restart algorithm if the trail size of the current conflict
is greater than the multiplier times the moving average of the trail size
at the previous conflicts.

optional bool use_blocking_restart = 64 [default = false];

Returns
The useBlockingRestart.

Implements SatParametersOrBuilder.

Definition at line 14394 of file SatParameters.java.

◆ getUseBranchingInLp()

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

optional bool use_branching_in_lp = 139 [default = false];

Returns
The useBranchingInLp.

Implements SatParametersOrBuilder.

Definition at line 21459 of file SatParameters.java.

◆ getUseCombinedNoOverlap()

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

optional bool use_combined_no_overlap = 133 [default = false];

Returns
The useCombinedNoOverlap.

Implements SatParametersOrBuilder.

Definition at line 21522 of file SatParameters.java.

◆ getUseDisjunctiveConstraintInCumulativeConstraint()

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

optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];

Returns
The useDisjunctiveConstraintInCumulativeConstraint.

Implements SatParametersOrBuilder.

Definition at line 17813 of file SatParameters.java.

◆ getUseErwaHeuristic()

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

optional bool use_erwa_heuristic = 75 [default = false];

Returns
The useErwaHeuristic.

Implements SatParametersOrBuilder.

Definition at line 12733 of file SatParameters.java.

◆ getUseExactLpReason()

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

optional bool use_exact_lp_reason = 109 [default = true];

Returns
The useExactLpReason.

Implements SatParametersOrBuilder.

Definition at line 21394 of file SatParameters.java.

◆ getUseFeasibilityPump()

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

optional bool use_feasibility_pump = 164 [default = true];

Returns
The useFeasibilityPump.

Implements SatParametersOrBuilder.

Definition at line 20979 of file SatParameters.java.

◆ getUseImpliedBounds()

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

optional bool use_implied_bounds = 144 [default = true];

Returns
The useImpliedBounds.

Implements SatParametersOrBuilder.

Definition at line 21648 of file SatParameters.java.

◆ getUseLnsOnly()

.lang.Override boolean getUseLnsOnly ( )
LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns
The useLnsOnly.

Implements SatParametersOrBuilder.

Definition at line 20791 of file SatParameters.java.

◆ getUseOptimizationHints()

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

optional bool use_optimization_hints = 35 [default = true];

Returns
The useOptimizationHints.

Implements SatParametersOrBuilder.

Definition at line 17187 of file SatParameters.java.

◆ getUseOptionalVariables()

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

optional bool use_optional_variables = 108 [default = true];

Returns
The useOptionalVariables.

Implements SatParametersOrBuilder.

Definition at line 21329 of file SatParameters.java.

◆ getUseOverloadCheckerInCumulativeConstraint()

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

optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];

Returns
The useOverloadCheckerInCumulativeConstraint.

Implements SatParametersOrBuilder.

Definition at line 17659 of file SatParameters.java.

◆ getUsePbResolution()

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

optional bool use_pb_resolution = 43 [default = false];

Returns
The usePbResolution.

Implements SatParametersOrBuilder.

Definition at line 15613 of file SatParameters.java.

◆ getUsePhaseSaving()

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

optional bool use_phase_saving = 44 [default = true];

Returns
The usePhaseSaving.

Implements SatParametersOrBuilder.

Definition at line 12461 of file SatParameters.java.

◆ getUsePrecedencesInDisjunctiveConstraint()

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

optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];

Returns
The usePrecedencesInDisjunctiveConstraint.

Implements SatParametersOrBuilder.

Definition at line 17580 of file SatParameters.java.

◆ getUseProbingSearch()

.lang.Override boolean getUseProbingSearch ( )
If true, search will continuously probe Boolean variables, and integer
variable bounds.

optional bool use_probing_search = 176 [default = false];

Returns
The useProbingSearch.

Implements SatParametersOrBuilder.

Definition at line 19651 of file SatParameters.java.

◆ getUseRelaxationLns()

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

optional bool use_relaxation_lns = 150 [default = false];

Returns
The useRelaxationLns.

Implements SatParametersOrBuilder.

Definition at line 21079 of file SatParameters.java.

◆ getUseRinsLns()

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

optional bool use_rins_lns = 129 [default = true];

Returns
The useRinsLns.

Implements SatParametersOrBuilder.

Definition at line 20924 of file SatParameters.java.

◆ getUseSatInprocessing()

.lang.Override boolean getUseSatInprocessing ( )

optional bool use_sat_inprocessing = 163 [default = false];

Returns
The useSatInprocessing.

Implements SatParametersOrBuilder.

Definition at line 16532 of file SatParameters.java.

◆ getUseTimetableEdgeFindingInCumulativeConstraint()

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

optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];

Returns
The useTimetableEdgeFindingInCumulativeConstraint.

Implements SatParametersOrBuilder.

Definition at line 17734 of file SatParameters.java.

◆ getVariableActivityDecay()

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

optional double variable_activity_decay = 15 [default = 0.8];

Returns
The variableActivityDecay.

Implements SatParametersOrBuilder.

Definition at line 13586 of file SatParameters.java.

◆ hasAbsoluteGapLimit()

.lang.Override boolean hasAbsoluteGapLimit ( )
Stop the search when the gap between the best feasible objective (O) and
our best objective bound (B) is smaller than a limit.
The exact definition is:
  • Absolute: abs(O - B)
  • Relative: abs(O - B) / max(1, abs(O)). Important: The relative gap depends on the objective offset! If you artificially shift the objective, you will get widely different value of the relative gap. Note that if the gap is reached, the search status will be OPTIMAL. But one can check the best objective bound to see the actual gap.
optional double absolute_gap_limit = 159 [default = 0];
Returns
Whether the absoluteGapLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 14914 of file SatParameters.java.

◆ hasAddCgCuts()

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

optional bool add_cg_cuts = 117 [default = true];

Returns
Whether the addCgCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 18186 of file SatParameters.java.

◆ hasAddCliqueCuts()

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

optional bool add_clique_cuts = 172 [default = true];

Returns
Whether the addCliqueCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 18364 of file SatParameters.java.

◆ hasAddKnapsackCuts()

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

optional bool add_knapsack_cuts = 111 [default = false];

Returns
Whether the addKnapsackCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 18124 of file SatParameters.java.

◆ hasAddLinMaxCuts()

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

optional bool add_lin_max_cuts = 152 [default = true];

Returns
Whether the addLinMaxCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 18490 of file SatParameters.java.

◆ hasAddLpConstraintsLazily()

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

optional bool add_lp_constraints_lazily = 112 [default = true];

Returns
Whether the addLpConstraintsLazily field is set.

Implements SatParametersOrBuilder.

Definition at line 18633 of file SatParameters.java.

◆ hasAddMirCuts()

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

optional bool add_mir_cuts = 120 [default = true];

Returns
Whether the addMirCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 18245 of file SatParameters.java.

◆ hasAddZeroHalfCuts()

.lang.Override boolean hasAddZeroHalfCuts ( )
Whether we generate Zero-Half cuts at root node.
Note that for now, this is not heavily tuned.

optional bool add_zero_half_cuts = 169 [default = true];

Returns
Whether the addZeroHalfCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 18304 of file SatParameters.java.

◆ hasAlsoBumpVariablesInConflictReasons()

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

optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];

Returns
Whether the alsoBumpVariablesInConflictReasons field is set.

Implements SatParametersOrBuilder.

Definition at line 12858 of file SatParameters.java.

◆ hasAutoDetectGreaterThanAtLeastOneOf()

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

optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];

Returns
Whether the autoDetectGreaterThanAtLeastOneOf field is set.

Implements SatParametersOrBuilder.

Definition at line 20251 of file SatParameters.java.

◆ hasBinaryMinimizationAlgorithm()

.lang.Override boolean hasBinaryMinimizationAlgorithm ( )

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

Returns
Whether the binaryMinimizationAlgorithm field is set.

Implements SatParametersOrBuilder.

Definition at line 12960 of file SatParameters.java.

◆ hasBinarySearchNumConflicts()

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

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

Returns
Whether the binarySearchNumConflicts field is set.

Implements SatParametersOrBuilder.

Definition at line 19825 of file SatParameters.java.

◆ hasBlockingRestartMultiplier()

.lang.Override boolean hasBlockingRestartMultiplier ( )

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns
Whether the blockingRestartMultiplier field is set.

Implements SatParametersOrBuilder.

Definition at line 14476 of file SatParameters.java.

◆ hasBlockingRestartWindowSize()

.lang.Override boolean hasBlockingRestartWindowSize ( )

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns
Whether the blockingRestartWindowSize field is set.

Implements SatParametersOrBuilder.

Definition at line 14437 of file SatParameters.java.

◆ hasBooleanEncodingLevel()

.lang.Override boolean hasBooleanEncodingLevel ( )
A non-negative level indicating how much we should try to fully encode
Integer variables as Boolean.

optional int32 boolean_encoding_level = 107 [default = 1];

Returns
Whether the booleanEncodingLevel field is set.

Implements SatParametersOrBuilder.

Definition at line 17938 of file SatParameters.java.

◆ hasCatchSigintSignal()

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

optional bool catch_sigint_signal = 135 [default = true];

Returns
Whether the catchSigintSignal field is set.

Implements SatParametersOrBuilder.

Definition at line 21571 of file SatParameters.java.

◆ hasClauseActivityDecay()

.lang.Override boolean hasClauseActivityDecay ( )
Clause activity parameters (same effect as the one on the variables).

optional double clause_activity_decay = 17 [default = 0.999];

Returns
Whether the clauseActivityDecay field is set.

Implements SatParametersOrBuilder.

Definition at line 13825 of file SatParameters.java.

◆ hasClauseCleanupLbdBound()

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

optional int32 clause_cleanup_lbd_bound = 59 [default = 5];

Returns
Whether the clauseCleanupLbdBound field is set.

Implements SatParametersOrBuilder.

Definition at line 13233 of file SatParameters.java.

◆ hasClauseCleanupOrdering()

.lang.Override boolean hasClauseCleanupOrdering ( )

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

Returns
Whether the clauseCleanupOrdering field is set.

Implements SatParametersOrBuilder.

Definition at line 13286 of file SatParameters.java.

◆ hasClauseCleanupPeriod()

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

optional int32 clause_cleanup_period = 11 [default = 10000];

Returns
Whether the clauseCleanupPeriod field is set.

Implements SatParametersOrBuilder.

Definition at line 13075 of file SatParameters.java.

◆ hasClauseCleanupProtection()

.lang.Override boolean hasClauseCleanupProtection ( )

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

Returns
Whether the clauseCleanupProtection field is set.

Implements SatParametersOrBuilder.

Definition at line 13184 of file SatParameters.java.

◆ hasClauseCleanupTarget()

.lang.Override boolean hasClauseCleanupTarget ( )
During a cleanup, we will always keep that number of "deletable" clauses.
Note that this doesn't include the "protected" clauses.

optional int32 clause_cleanup_target = 13 [default = 10000];

Returns
Whether the clauseCleanupTarget field is set.

Implements SatParametersOrBuilder.

Definition at line 13131 of file SatParameters.java.

◆ hasConvertIntervals()

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

optional bool convert_intervals = 177 [default = false];

Returns
Whether the convertIntervals field is set.

Implements SatParametersOrBuilder.

Definition at line 21764 of file SatParameters.java.

◆ hasCountAssumptionLevelsInLbd()

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

optional bool count_assumption_levels_in_lbd = 49 [default = true];

Returns
Whether the countAssumptionLevelsInLbd field is set.

Implements SatParametersOrBuilder.

Definition at line 15736 of file SatParameters.java.

◆ hasCoverOptimization()

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

optional bool cover_optimization = 89 [default = true];

Returns
Whether the coverOptimization field is set.

Implements SatParametersOrBuilder.

Definition at line 17351 of file SatParameters.java.

◆ hasCpModelMaxNumPresolveOperations()

.lang.Override boolean hasCpModelMaxNumPresolveOperations ( )
If positive, try to stop just after that many presolve rules have been
applied. This is mainly useful for debugging presolve.

optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];

Returns
Whether the cpModelMaxNumPresolveOperations field is set.

Implements SatParametersOrBuilder.

Definition at line 16360 of file SatParameters.java.

◆ hasCpModelPostsolveWithFullSolver()

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

optional bool cp_model_postsolve_with_full_solver = 162 [default = false];

Returns
Whether the cpModelPostsolveWithFullSolver field is set.

Implements SatParametersOrBuilder.

Definition at line 16295 of file SatParameters.java.

◆ hasCpModelPresolve()

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

optional bool cp_model_presolve = 86 [default = true];

Returns
Whether the cpModelPresolve field is set.

Implements SatParametersOrBuilder.

Definition at line 16237 of file SatParameters.java.

◆ hasCpModelProbingLevel()

.lang.Override boolean hasCpModelProbingLevel ( )
How much effort do we spend on probing. 0 disables it completely.

optional int32 cp_model_probing_level = 110 [default = 2];

Returns
Whether the cpModelProbingLevel field is set.

Implements SatParametersOrBuilder.

Definition at line 16418 of file SatParameters.java.

◆ hasCpModelUseSatPresolve()

.lang.Override boolean hasCpModelUseSatPresolve ( )
Whether we also use the sat presolve when cp_model_presolve is true.

optional bool cp_model_use_sat_presolve = 93 [default = true];

Returns
Whether the cpModelUseSatPresolve field is set.

Implements SatParametersOrBuilder.

Definition at line 16473 of file SatParameters.java.

◆ hasCutActiveCountDecay()

.lang.Override boolean hasCutActiveCountDecay ( )

optional double cut_active_count_decay = 156 [default = 0.8];

Returns
Whether the cutActiveCountDecay field is set.

Implements SatParametersOrBuilder.

Definition at line 18945 of file SatParameters.java.

◆ hasCutCleanupTarget()

.lang.Override boolean hasCutCleanupTarget ( )
Target number of constraints to remove during cleanup.

optional int32 cut_cleanup_target = 157 [default = 1000];

Returns
Whether the cutCleanupTarget field is set.

Implements SatParametersOrBuilder.

Definition at line 18988 of file SatParameters.java.

◆ hasCutMaxActiveCountValue()

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

optional double cut_max_active_count_value = 155 [default = 10000000000];

Returns
Whether the cutMaxActiveCountValue field is set.

Implements SatParametersOrBuilder.

Definition at line 18888 of file SatParameters.java.

◆ hasDefaultRestartAlgorithms()

boolean hasDefaultRestartAlgorithms ( )

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

Returns
Whether the defaultRestartAlgorithms field is set.

Implements SatParametersOrBuilder.

Definition at line 14077 of file SatParameters.java.

◆ hasDisableConstraintExpansion()

.lang.Override boolean hasDisableConstraintExpansion ( )
If true, it disable all constraint expansion.
This should only be used to test the presolve of expanded constraints.

optional bool disable_constraint_expansion = 181 [default = false];

Returns
Whether the disableConstraintExpansion field is set.

Implements SatParametersOrBuilder.

Definition at line 16859 of file SatParameters.java.

◆ hasDiversifyLnsParams()

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

optional bool diversify_lns_params = 137 [default = false];

Returns
Whether the diversifyLnsParams field is set.

Implements SatParametersOrBuilder.

Definition at line 21124 of file SatParameters.java.

◆ hasEnumerateAllSolutions()

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

optional bool enumerate_all_solutions = 87 [default = false];

Returns
Whether the enumerateAllSolutions field is set.

Implements SatParametersOrBuilder.

Definition at line 19969 of file SatParameters.java.

◆ hasExpandAlldiffConstraints()

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

optional bool expand_alldiff_constraints = 170 [default = false];

Returns
Whether the expandAlldiffConstraints field is set.

Implements SatParametersOrBuilder.

Definition at line 16741 of file SatParameters.java.

◆ hasExpandAutomatonConstraints()

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

optional bool expand_automaton_constraints = 143 [default = true];

Returns
Whether the expandAutomatonConstraints field is set.

Implements SatParametersOrBuilder.

Definition at line 16626 of file SatParameters.java.

◆ hasExpandElementConstraints()

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

optional bool expand_element_constraints = 140 [default = true];

Returns
Whether the expandElementConstraints field is set.

Implements SatParametersOrBuilder.

Definition at line 16568 of file SatParameters.java.

◆ hasExpandReservoirConstraints()

.lang.Override boolean hasExpandReservoirConstraints ( )
If true, expand the reservoir constraints by creating booleans for all
possible precedences between event and encoding the constraint.

optional bool expand_reservoir_constraints = 182 [default = true];

Returns
Whether the expandReservoirConstraints field is set.

Implements SatParametersOrBuilder.

Definition at line 16800 of file SatParameters.java.

◆ hasExpandTableConstraints()

.lang.Override boolean hasExpandTableConstraints ( )
If true, the positive table constraints are expanded.
Note that currently, negative table constraints are always expanded.

optional bool expand_table_constraints = 158 [default = true];

Returns
Whether the expandTableConstraints field is set.

Implements SatParametersOrBuilder.

Definition at line 16682 of file SatParameters.java.

◆ hasExploitAllLpSolution()

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

optional bool exploit_all_lp_solution = 116 [default = true];

Returns
Whether the exploitAllLpSolution field is set.

Implements SatParametersOrBuilder.

Definition at line 19336 of file SatParameters.java.

◆ hasExploitBestSolution()

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

optional bool exploit_best_solution = 130 [default = false];

Returns
Whether the exploitBestSolution field is set.

Implements SatParametersOrBuilder.

Definition at line 19397 of file SatParameters.java.

◆ hasExploitIntegerLpSolution()

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

optional bool exploit_integer_lp_solution = 94 [default = true];

Returns
Whether the exploitIntegerLpSolution field is set.

Implements SatParametersOrBuilder.

Definition at line 19270 of file SatParameters.java.

◆ hasExploitObjective()

.lang.Override boolean hasExploitObjective ( )
When branching an a variable that directly affect the objective,
branch on the value that lead to the best objective first.

optional bool exploit_objective = 131 [default = true];

Returns
Whether the exploitObjective field is set.

Implements SatParametersOrBuilder.

Definition at line 19516 of file SatParameters.java.

◆ hasExploitRelaxationSolution()

.lang.Override boolean hasExploitRelaxationSolution ( )
When branching on a variable, follow the last best relaxation solution
value. We use the relaxation with the tightest bound on the objective as
the best relaxation solution.

optional bool exploit_relaxation_solution = 161 [default = false];

Returns
Whether the exploitRelaxationSolution field is set.

Implements SatParametersOrBuilder.

Definition at line 19454 of file SatParameters.java.

◆ hasFillTightenedDomainsInResponse()

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

optional bool fill_tightened_domains_in_response = 132 [default = false];

Returns
Whether the fillTightenedDomainsInResponse field is set.

Implements SatParametersOrBuilder.

Definition at line 20122 of file SatParameters.java.

◆ hasFindMultipleCores()

.lang.Override boolean hasFindMultipleCores ( )
Whether we try to find more independent cores for a given set of
assumptions in the core based max-SAT algorithms.

optional bool find_multiple_cores = 84 [default = true];

Returns
Whether the findMultipleCores field is set.

Implements SatParametersOrBuilder.

Definition at line 17292 of file SatParameters.java.

◆ hasFpRounding()

.lang.Override boolean hasFpRounding ( )

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

Returns
Whether the fpRounding field is set.

Implements SatParametersOrBuilder.

Definition at line 21017 of file SatParameters.java.

◆ hasGlucoseDecayIncrement()

.lang.Override boolean hasGlucoseDecayIncrement ( )

optional double glucose_decay_increment = 23 [default = 0.01];

Returns
Whether the glucoseDecayIncrement field is set.

Implements SatParametersOrBuilder.

Definition at line 13743 of file SatParameters.java.

◆ hasGlucoseDecayIncrementPeriod()

.lang.Override boolean hasGlucoseDecayIncrementPeriod ( )

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns
Whether the glucoseDecayIncrementPeriod field is set.

Implements SatParametersOrBuilder.

Definition at line 13782 of file SatParameters.java.

◆ hasGlucoseMaxDecay()

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

optional double glucose_max_decay = 22 [default = 0.95];

Returns
Whether the glucoseMaxDecay field is set.

Implements SatParametersOrBuilder.

Definition at line 13683 of file SatParameters.java.

◆ hasHintConflictLimit()

.lang.Override boolean hasHintConflictLimit ( )
Conflict limit used in the phase that exploit the solution hint.

optional int32 hint_conflict_limit = 153 [default = 10];

Returns
Whether the hintConflictLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 19145 of file SatParameters.java.

◆ hasInitialPolarity()

.lang.Override boolean hasInitialPolarity ( )

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

Returns
Whether the initialPolarity field is set.

Implements SatParametersOrBuilder.

Definition at line 12385 of file SatParameters.java.

◆ hasInitialVariablesActivity()

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

optional double initial_variables_activity = 76 [default = 0];

Returns
Whether the initialVariablesActivity field is set.

Implements SatParametersOrBuilder.

Definition at line 12785 of file SatParameters.java.

◆ hasInstantiateAllVariables()

.lang.Override boolean hasInstantiateAllVariables ( )
If true, the solver will add a default integer branching strategy to the
already defined search strategy.

optional bool instantiate_all_variables = 106 [default = true];

Returns
Whether the instantiateAllVariables field is set.

Implements SatParametersOrBuilder.

Definition at line 20190 of file SatParameters.java.

◆ hasInterleaveBatchSize()

.lang.Override boolean hasInterleaveBatchSize ( )

optional int32 interleave_batch_size = 134 [default = 1];

Returns
Whether the interleaveBatchSize field is set.

Implements SatParametersOrBuilder.

Definition at line 20571 of file SatParameters.java.

◆ hasInterleaveSearch()

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

optional bool interleave_search = 136 [default = false];

Returns
Whether the interleaveSearch field is set.

Implements SatParametersOrBuilder.

Definition at line 20508 of file SatParameters.java.

◆ hasKeepAllFeasibleSolutionsInPresolve()

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

optional bool keep_all_feasible_solutions_in_presolve = 173 [default = false];

Returns
Whether the keepAllFeasibleSolutionsInPresolve field is set.

Implements SatParametersOrBuilder.

Definition at line 20045 of file SatParameters.java.

◆ hasLinearizationLevel()

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

optional int32 linearization_level = 90 [default = 1];

Returns
Whether the linearizationLevel field is set.

Implements SatParametersOrBuilder.

Definition at line 17873 of file SatParameters.java.

◆ hasLnsExpandIntervalsInConstraintGraph()

.lang.Override boolean hasLnsExpandIntervalsInConstraintGraph ( )

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns
Whether the lnsExpandIntervalsInConstraintGraph field is set.

Implements SatParametersOrBuilder.

Definition at line 20869 of file SatParameters.java.

◆ hasLnsFocusOnDecisionVariables()

.lang.Override boolean hasLnsFocusOnDecisionVariables ( )

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns
Whether the lnsFocusOnDecisionVariables field is set.

Implements SatParametersOrBuilder.

Definition at line 20830 of file SatParameters.java.

◆ hasLogPrefix()

boolean hasLogPrefix ( )
Add a prefix to all logs.

optional string log_prefix = 185 [default = ""];

Returns
Whether the logPrefix field is set.

Implements SatParametersOrBuilder.

Definition at line 15376 of file SatParameters.java.

◆ hasLogSearchProgress()

.lang.Override boolean hasLogSearchProgress ( )
Whether the solver should log the search progress. By default, it logs to
LOG(INFO). This can be overwritten by the log_destination parameter.

optional bool log_search_progress = 41 [default = false];

Returns
Whether the logSearchProgress field is set.

Implements SatParametersOrBuilder.

Definition at line 15319 of file SatParameters.java.

◆ hasLogToResponse()

.lang.Override boolean hasLogToResponse ( )
Log to response proto.

optional bool log_to_response = 187 [default = false];

Returns
Whether the logToResponse field is set.

Implements SatParametersOrBuilder.

Definition at line 15540 of file SatParameters.java.

◆ hasLogToStdout()

.lang.Override boolean hasLogToStdout ( )
Log to stdout.

optional bool log_to_stdout = 186 [default = true];

Returns
Whether the logToStdout field is set.

Implements SatParametersOrBuilder.

Definition at line 15485 of file SatParameters.java.

◆ hasMaxAllDiffCutSize()

.lang.Override boolean hasMaxAllDiffCutSize ( )
Cut generator for all diffs can add too many cuts for large all_diff
constraints. This parameter restricts the large all_diff constraints to
have a cut generator.

optional int32 max_all_diff_cut_size = 148 [default = 7];

Returns
Whether the maxAllDiffCutSize field is set.

Implements SatParametersOrBuilder.

Definition at line 18427 of file SatParameters.java.

◆ hasMaxClauseActivityValue()

.lang.Override boolean hasMaxClauseActivityValue ( )

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

Returns
Whether the maxClauseActivityValue field is set.

Implements SatParametersOrBuilder.

Definition at line 13876 of file SatParameters.java.

◆ hasMaxConsecutiveInactiveCount()

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

optional int32 max_consecutive_inactive_count = 121 [default = 100];

Returns
Whether the maxConsecutiveInactiveCount field is set.

Implements SatParametersOrBuilder.

Definition at line 18825 of file SatParameters.java.

◆ hasMaxCutRoundsAtLevelZero()

.lang.Override boolean hasMaxCutRoundsAtLevelZero ( )
Max number of time we perform cut generation and resolve the LP at level 0.

optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];

Returns
Whether the maxCutRoundsAtLevelZero field is set.

Implements SatParametersOrBuilder.

Definition at line 18768 of file SatParameters.java.

◆ hasMaxDeterministicTime()

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

optional double max_deterministic_time = 67 [default = inf];

Returns
Whether the maxDeterministicTime field is set.

Implements SatParametersOrBuilder.

Definition at line 14702 of file SatParameters.java.

◆ hasMaxIntegerRoundingScaling()

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

optional int32 max_integer_rounding_scaling = 119 [default = 600];

Returns
Whether the maxIntegerRoundingScaling field is set.

Implements SatParametersOrBuilder.

Definition at line 18557 of file SatParameters.java.

◆ hasMaxMemoryInMb()

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

optional int64 max_memory_in_mb = 40 [default = 10000];

Returns
Whether the maxMemoryInMb field is set.

Implements SatParametersOrBuilder.

Definition at line 14841 of file SatParameters.java.

◆ hasMaxNumberOfConflicts()

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

optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];

Returns
Whether the maxNumberOfConflicts field is set.

Implements SatParametersOrBuilder.

Definition at line 14768 of file SatParameters.java.

◆ hasMaxNumCuts()

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

optional int32 max_num_cuts = 91 [default = 10000];

Returns
Whether the maxNumCuts field is set.

Implements SatParametersOrBuilder.

Definition at line 17999 of file SatParameters.java.

◆ hasMaxPresolveIterations()

.lang.Override boolean hasMaxPresolveIterations ( )
In case of large reduction in a presolve iteration, we perform multiple
presolve iterations. This parameter controls the maximum number of such
presolve iterations.

optional int32 max_presolve_iterations = 138 [default = 3];

Returns
Whether the maxPresolveIterations field is set.

Implements SatParametersOrBuilder.

Definition at line 16176 of file SatParameters.java.

◆ hasMaxSatAssumptionOrder()

.lang.Override boolean hasMaxSatAssumptionOrder ( )

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

Returns
Whether the maxSatAssumptionOrder field is set.

Implements SatParametersOrBuilder.

Definition at line 17404 of file SatParameters.java.

◆ hasMaxSatReverseAssumptionOrder()

.lang.Override boolean hasMaxSatReverseAssumptionOrder ( )
If true, adds the assumption in the reverse order of the one defined by
max_sat_assumption_order.

optional bool max_sat_reverse_assumption_order = 52 [default = false];

Returns
Whether the maxSatReverseAssumptionOrder field is set.

Implements SatParametersOrBuilder.

Definition at line 17453 of file SatParameters.java.

◆ hasMaxSatStratification()

.lang.Override boolean hasMaxSatStratification ( )

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

Returns
Whether the maxSatStratification field is set.

Implements SatParametersOrBuilder.

Definition at line 17506 of file SatParameters.java.

◆ hasMaxTimeInSeconds()

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

optional double max_time_in_seconds = 36 [default = inf];

Returns
Whether the maxTimeInSeconds field is set.

Implements SatParametersOrBuilder.

Definition at line 14642 of file SatParameters.java.

◆ hasMaxVariableActivityValue()

.lang.Override boolean hasMaxVariableActivityValue ( )

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

Returns
Whether the maxVariableActivityValue field is set.

Implements SatParametersOrBuilder.

Definition at line 13637 of file SatParameters.java.

◆ hasMergeAtMostOneWorkLimit()

.lang.Override boolean hasMergeAtMostOneWorkLimit ( )

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns
Whether the mergeAtMostOneWorkLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 16984 of file SatParameters.java.

◆ hasMergeNoOverlapWorkLimit()

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

optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];

Returns
Whether the mergeNoOverlapWorkLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 16921 of file SatParameters.java.

◆ hasMinimizationAlgorithm()

.lang.Override boolean hasMinimizationAlgorithm ( )

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

Returns
Whether the minimizationAlgorithm field is set.

Implements SatParametersOrBuilder.

Definition at line 12917 of file SatParameters.java.

◆ hasMinimizeCore()

.lang.Override boolean hasMinimizeCore ( )
Whether we use a simple heuristic to try to minimize an UNSAT core.

optional bool minimize_core = 50 [default = true];

Returns
Whether the minimizeCore field is set.

Implements SatParametersOrBuilder.

Definition at line 17236 of file SatParameters.java.

◆ hasMinimizeReductionDuringPbResolution()

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

optional bool minimize_reduction_during_pb_resolution = 48 [default = false];

Returns
Whether the minimizeReductionDuringPbResolution field is set.

Implements SatParametersOrBuilder.

Definition at line 15665 of file SatParameters.java.

◆ hasMinimizeWithPropagationNumDecisions()

.lang.Override boolean hasMinimizeWithPropagationNumDecisions ( )

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns
Whether the minimizeWithPropagationNumDecisions field is set.

Implements SatParametersOrBuilder.

Definition at line 13519 of file SatParameters.java.

◆ hasMinimizeWithPropagationRestartPeriod()

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

optional int32 minimize_with_propagation_restart_period = 96 [default = 10];

Returns
Whether the minimizeWithPropagationRestartPeriod field is set.

Implements SatParametersOrBuilder.

Definition at line 13438 of file SatParameters.java.

◆ hasMinOrthogonalityForLpConstraints()

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

optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];

Returns
Whether the minOrthogonalityForLpConstraints field is set.

Implements SatParametersOrBuilder.

Definition at line 18701 of file SatParameters.java.

◆ hasMipAutomaticallyScaleVariables()

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

optional bool mip_automatically_scale_variables = 166 [default = true];

Returns
Whether the mipAutomaticallyScaleVariables field is set.

Implements SatParametersOrBuilder.

Definition at line 22022 of file SatParameters.java.

◆ hasMipCheckPrecision()

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

optional double mip_check_precision = 128 [default = 0.0001];

Returns
Whether the mipCheckPrecision field is set.

Implements SatParametersOrBuilder.

Definition at line 22261 of file SatParameters.java.

◆ hasMipMaxActivityExponent()

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

optional int32 mip_max_activity_exponent = 127 [default = 53];

Returns
Whether the mipMaxActivityExponent field is set.

Implements SatParametersOrBuilder.

Definition at line 22186 of file SatParameters.java.

◆ hasMipMaxBound()

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

optional double mip_max_bound = 124 [default = 10000000];

Returns
Whether the mipMaxBound field is set.

Implements SatParametersOrBuilder.

Definition at line 21894 of file SatParameters.java.

◆ hasMipVarScaling()

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

optional double mip_var_scaling = 125 [default = 1];

Returns
Whether the mipVarScaling field is set.

Implements SatParametersOrBuilder.

Definition at line 21957 of file SatParameters.java.

◆ hasMipWantedPrecision()

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

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

Returns
Whether the mipWantedPrecision field is set.

Implements SatParametersOrBuilder.

Definition at line 22098 of file SatParameters.java.

◆ hasName()

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

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

Returns
Whether the name field is set.

Implements SatParametersOrBuilder.

Definition at line 12233 of file SatParameters.java.

◆ hasNewConstraintsBatchSize()

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

optional int32 new_constraints_batch_size = 122 [default = 50];

Returns
Whether the newConstraintsBatchSize field is set.

Implements SatParametersOrBuilder.

Definition at line 19044 of file SatParameters.java.

◆ hasNumConflictsBeforeStrategyChanges()

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

optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];

Returns
Whether the numConflictsBeforeStrategyChanges field is set.

Implements SatParametersOrBuilder.

Definition at line 14521 of file SatParameters.java.

◆ hasNumSearchWorkers()

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

optional int32 num_search_workers = 100 [default = 1];

Returns
Whether the numSearchWorkers field is set.

Implements SatParametersOrBuilder.

Definition at line 20434 of file SatParameters.java.

◆ hasOnlyAddCutsAtLevelZero()

.lang.Override boolean hasOnlyAddCutsAtLevelZero ( )
For the cut that can be generated at any level, this control if we only
try to generate them at the root node.

optional bool only_add_cuts_at_level_zero = 92 [default = false];

Returns
Whether the onlyAddCutsAtLevelZero field is set.

Implements SatParametersOrBuilder.

Definition at line 18064 of file SatParameters.java.

◆ hasOptimizeWithCore()

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

optional bool optimize_with_core = 83 [default = false];

Returns
Whether the optimizeWithCore field is set.

Implements SatParametersOrBuilder.

Definition at line 19758 of file SatParameters.java.

◆ hasOptimizeWithMaxHs()

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

optional bool optimize_with_max_hs = 85 [default = false];

Returns
Whether the optimizeWithMaxHs field is set.

Implements SatParametersOrBuilder.

Definition at line 19894 of file SatParameters.java.

◆ hasPbCleanupIncrement()

.lang.Override boolean hasPbCleanupIncrement ( )
Same as for the clauses, but for the learned pseudo-Boolean constraints.

optional int32 pb_cleanup_increment = 46 [default = 200];

Returns
Whether the pbCleanupIncrement field is set.

Implements SatParametersOrBuilder.

Definition at line 13334 of file SatParameters.java.

◆ hasPbCleanupRatio()

.lang.Override boolean hasPbCleanupRatio ( )

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns
Whether the pbCleanupRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 13385 of file SatParameters.java.

◆ hasPermutePresolveConstraintOrder()

.lang.Override boolean hasPermutePresolveConstraintOrder ( )

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns
Whether the permutePresolveConstraintOrder field is set.

Implements SatParametersOrBuilder.

Definition at line 15236 of file SatParameters.java.

◆ hasPermuteVariableRandomly()

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

optional bool permute_variable_randomly = 178 [default = false];

Returns
Whether the permuteVariableRandomly field is set.

Implements SatParametersOrBuilder.

Definition at line 15176 of file SatParameters.java.

◆ hasPolarityRephaseIncrement()

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

optional int32 polarity_rephase_increment = 168 [default = 1000];

Returns
Whether the polarityRephaseIncrement field is set.

Implements SatParametersOrBuilder.

Definition at line 12522 of file SatParameters.java.

◆ hasPolishLpSolution()

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

optional bool polish_lp_solution = 175 [default = false];

Returns
Whether the polishLpSolution field is set.

Implements SatParametersOrBuilder.

Definition at line 21698 of file SatParameters.java.

◆ hasPreferredVariableOrder()

.lang.Override boolean hasPreferredVariableOrder ( )

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

Returns
Whether the preferredVariableOrder field is set.

Implements SatParametersOrBuilder.

Definition at line 12342 of file SatParameters.java.

◆ hasPresolveBlockedClause()

.lang.Override boolean hasPresolveBlockedClause ( )
Whether we use an heuristic to detect some basic case of blocked clause
in the SAT presolve.

optional bool presolve_blocked_clause = 88 [default = true];

Returns
Whether the presolveBlockedClause field is set.

Implements SatParametersOrBuilder.

Definition at line 15994 of file SatParameters.java.

◆ hasPresolveBvaThreshold()

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

optional int32 presolve_bva_threshold = 73 [default = 1];

Returns
Whether the presolveBvaThreshold field is set.

Implements SatParametersOrBuilder.

Definition at line 16110 of file SatParameters.java.

◆ hasPresolveBveClauseWeight()

.lang.Override boolean hasPresolveBveClauseWeight ( )
During presolve, we apply BVE only if this weight times the number of
clauses plus the number of clause literals is not increased.

optional int32 presolve_bve_clause_weight = 55 [default = 3];

Returns
Whether the presolveBveClauseWeight field is set.

Implements SatParametersOrBuilder.

Definition at line 15876 of file SatParameters.java.

◆ hasPresolveBveThreshold()

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

optional int32 presolve_bve_threshold = 54 [default = 500];

Returns
Whether the presolveBveThreshold field is set.

Implements SatParametersOrBuilder.

Definition at line 15814 of file SatParameters.java.

◆ hasPresolveExtractIntegerEnforcement()

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

optional bool presolve_extract_integer_enforcement = 174 [default = false];

Returns
Whether the presolveExtractIntegerEnforcement field is set.

Implements SatParametersOrBuilder.

Definition at line 17099 of file SatParameters.java.

◆ hasPresolveProbingDeterministicTimeLimit()

.lang.Override boolean hasPresolveProbingDeterministicTimeLimit ( )
The maximum "deterministic" time limit to spend in probing. A value of
zero will disable the probing.

optional double presolve_probing_deterministic_time_limit = 57 [default = 30];

Returns
Whether the presolveProbingDeterministicTimeLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 15935 of file SatParameters.java.

◆ hasPresolveSubstitutionLevel()

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

optional int32 presolve_substitution_level = 147 [default = 1];

Returns
Whether the presolveSubstitutionLevel field is set.

Implements SatParametersOrBuilder.

Definition at line 17030 of file SatParameters.java.

◆ hasPresolveUseBva()

.lang.Override boolean hasPresolveUseBva ( )
Whether or not we use Bounded Variable Addition (BVA) in the presolve.

optional bool presolve_use_bva = 72 [default = true];

Returns
Whether the presolveUseBva field is set.

Implements SatParametersOrBuilder.

Definition at line 16052 of file SatParameters.java.

◆ hasProbingPeriodAtRoot()

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

optional int64 probing_period_at_root = 142 [default = 0];

Returns
Whether the probingPeriodAtRoot field is set.

Implements SatParametersOrBuilder.

Definition at line 19576 of file SatParameters.java.

◆ hasPseudoCostReliabilityThreshold()

.lang.Override boolean hasPseudoCostReliabilityThreshold ( )
The solver ignores the pseudo costs of variables with number of recordings
less than this threshold.

optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];

Returns
Whether the pseudoCostReliabilityThreshold field is set.

Implements SatParametersOrBuilder.

Definition at line 19697 of file SatParameters.java.

◆ hasRandomBranchesRatio()

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

optional double random_branches_ratio = 32 [default = 0];

Returns
Whether the randomBranchesRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 12656 of file SatParameters.java.

◆ hasRandomizeSearch()

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

optional bool randomize_search = 103 [default = false];

Returns
Whether the randomizeSearch field is set.

Implements SatParametersOrBuilder.

Definition at line 21179 of file SatParameters.java.

◆ hasRandomPolarityRatio()

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

optional double random_polarity_ratio = 45 [default = 0];

Returns
Whether the randomPolarityRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 12587 of file SatParameters.java.

◆ hasRandomSeed()

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

optional int32 random_seed = 31 [default = 1];

Returns
Whether the randomSeed field is set.

Implements SatParametersOrBuilder.

Definition at line 15103 of file SatParameters.java.

◆ hasReduceMemoryUsageInInterleaveMode()

.lang.Override boolean hasReduceMemoryUsageInInterleaveMode ( )
Temporary parameter until the memory usage is more optimized.

optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];

Returns
Whether the reduceMemoryUsageInInterleaveMode field is set.

Implements SatParametersOrBuilder.

Definition at line 20614 of file SatParameters.java.

◆ hasRelativeGapLimit()

.lang.Override boolean hasRelativeGapLimit ( )

optional double relative_gap_limit = 160 [default = 0];

Returns
Whether the relativeGapLimit field is set.

Implements SatParametersOrBuilder.

Definition at line 14992 of file SatParameters.java.

◆ hasRepairHint()

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

optional bool repair_hint = 167 [default = false];

Returns
Whether the repairHint field is set.

Implements SatParametersOrBuilder.

Definition at line 19203 of file SatParameters.java.

◆ hasRestartDlAverageRatio()

.lang.Override boolean hasRestartDlAverageRatio ( )
In the moving average restart algorithms, a restart is triggered if the
window average times this ratio is greater that the global average.

optional double restart_dl_average_ratio = 63 [default = 1];

Returns
Whether the restartDlAverageRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 14281 of file SatParameters.java.

◆ hasRestartLbdAverageRatio()

.lang.Override boolean hasRestartLbdAverageRatio ( )

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns
Whether the restartLbdAverageRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 14335 of file SatParameters.java.

◆ hasRestartPeriod()

.lang.Override boolean hasRestartPeriod ( )
Restart period for the FIXED_RESTART strategy. This is also the multiplier
used by the LUBY_RESTART strategy.

optional int32 restart_period = 30 [default = 50];

Returns
Whether the restartPeriod field is set.

Implements SatParametersOrBuilder.

Definition at line 14167 of file SatParameters.java.

◆ hasRestartRunningWindowSize()

.lang.Override boolean hasRestartRunningWindowSize ( )
Size of the window for the moving average restarts.

optional int32 restart_running_window_size = 62 [default = 50];

Returns
Whether the restartRunningWindowSize field is set.

Implements SatParametersOrBuilder.

Definition at line 14225 of file SatParameters.java.

◆ hasSearchBranching()

.lang.Override boolean hasSearchBranching ( )

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

Returns
Whether the searchBranching field is set.

Implements SatParametersOrBuilder.

Definition at line 19097 of file SatParameters.java.

◆ hasSearchRandomizationTolerance()

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

optional int64 search_randomization_tolerance = 104 [default = 0];

Returns
Whether the searchRandomizationTolerance field is set.

Implements SatParametersOrBuilder.

Definition at line 21240 of file SatParameters.java.

◆ hasShareLevelZeroBounds()

.lang.Override boolean hasShareLevelZeroBounds ( )
Allows sharing of the bounds of modified variables at level 0.

optional bool share_level_zero_bounds = 114 [default = true];

Returns
Whether the shareLevelZeroBounds field is set.

Implements SatParametersOrBuilder.

Definition at line 20724 of file SatParameters.java.

◆ hasShareObjectiveBounds()

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

optional bool share_objective_bounds = 113 [default = true];

Returns
Whether the shareObjectiveBounds field is set.

Implements SatParametersOrBuilder.

Definition at line 20669 of file SatParameters.java.

◆ hasStopAfterFirstSolution()

.lang.Override boolean hasStopAfterFirstSolution ( )
For an optimization problem, stop the solver as soon as we have a solution.

optional bool stop_after_first_solution = 98 [default = false];

Returns
Whether the stopAfterFirstSolution field is set.

Implements SatParametersOrBuilder.

Definition at line 20315 of file SatParameters.java.

◆ hasStopAfterPresolve()

.lang.Override boolean hasStopAfterPresolve ( )
Mainly used when improving the presolver. When true, stops the solver after
the presolve is complete.

optional bool stop_after_presolve = 149 [default = false];

Returns
Whether the stopAfterPresolve field is set.

Implements SatParametersOrBuilder.

Definition at line 20371 of file SatParameters.java.

◆ hasStrategyChangeIncreaseRatio()

.lang.Override boolean hasStrategyChangeIncreaseRatio ( )
The parameter num_conflicts_before_strategy_changes is increased by that
much after each strategy change.

optional double strategy_change_increase_ratio = 69 [default = 0];

Returns
Whether the strategyChangeIncreaseRatio field is set.

Implements SatParametersOrBuilder.

Definition at line 14583 of file SatParameters.java.

◆ hasSubsumptionDuringConflictAnalysis()

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

optional bool subsumption_during_conflict_analysis = 56 [default = true];

Returns
Whether the subsumptionDuringConflictAnalysis field is set.

Implements SatParametersOrBuilder.

Definition at line 13011 of file SatParameters.java.

◆ hasSymmetryLevel()

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

optional int32 symmetry_level = 183 [default = 2];

Returns
Whether the symmetryLevel field is set.

Implements SatParametersOrBuilder.

Definition at line 21828 of file SatParameters.java.

◆ hasTreatBinaryClausesSeparately()

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

optional bool treat_binary_clauses_separately = 33 [default = true];

Returns
Whether the treatBinaryClausesSeparately field is set.

Implements SatParametersOrBuilder.

Definition at line 15037 of file SatParameters.java.

◆ hasUseAbslRandom()

.lang.Override boolean hasUseAbslRandom ( )

optional bool use_absl_random = 180 [default = false];

Returns
Whether the useAbslRandom field is set.

Implements SatParametersOrBuilder.

Definition at line 15275 of file SatParameters.java.

◆ hasUseBlockingRestart()

.lang.Override boolean hasUseBlockingRestart ( )
Block a moving restart algorithm if the trail size of the current conflict
is greater than the multiplier times the moving average of the trail size
at the previous conflicts.

optional bool use_blocking_restart = 64 [default = false];

Returns
Whether the useBlockingRestart field is set.

Implements SatParametersOrBuilder.

Definition at line 14380 of file SatParameters.java.

◆ hasUseBranchingInLp()

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

optional bool use_branching_in_lp = 139 [default = false];

Returns
Whether the useBranchingInLp field is set.

Implements SatParametersOrBuilder.

Definition at line 21445 of file SatParameters.java.

◆ hasUseCombinedNoOverlap()

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

optional bool use_combined_no_overlap = 133 [default = false];

Returns
Whether the useCombinedNoOverlap field is set.

Implements SatParametersOrBuilder.

Definition at line 21508 of file SatParameters.java.

◆ hasUseDisjunctiveConstraintInCumulativeConstraint()

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

optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];

Returns
Whether the useDisjunctiveConstraintInCumulativeConstraint field is set.

Implements SatParametersOrBuilder.

Definition at line 17794 of file SatParameters.java.

◆ hasUseErwaHeuristic()

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

optional bool use_erwa_heuristic = 75 [default = false];

Returns
Whether the useErwaHeuristic field is set.

Implements SatParametersOrBuilder.

Definition at line 12719 of file SatParameters.java.

◆ hasUseExactLpReason()

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

optional bool use_exact_lp_reason = 109 [default = true];

Returns
Whether the useExactLpReason field is set.

Implements SatParametersOrBuilder.

Definition at line 21379 of file SatParameters.java.

◆ hasUseFeasibilityPump()

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

optional bool use_feasibility_pump = 164 [default = true];

Returns
Whether the useFeasibilityPump field is set.

Implements SatParametersOrBuilder.

Definition at line 20967 of file SatParameters.java.

◆ hasUseImpliedBounds()

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

optional bool use_implied_bounds = 144 [default = true];

Returns
Whether the useImpliedBounds field is set.

Implements SatParametersOrBuilder.

Definition at line 21634 of file SatParameters.java.

◆ hasUseLnsOnly()

.lang.Override boolean hasUseLnsOnly ( )
LNS parameters.

optional bool use_lns_only = 101 [default = false];

Returns
Whether the useLnsOnly field is set.

Implements SatParametersOrBuilder.

Definition at line 20779 of file SatParameters.java.

◆ hasUseOptimizationHints()

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

optional bool use_optimization_hints = 35 [default = true];

Returns
Whether the useOptimizationHints field is set.

Implements SatParametersOrBuilder.

Definition at line 17172 of file SatParameters.java.

◆ hasUseOptionalVariables()

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

optional bool use_optional_variables = 108 [default = true];

Returns
Whether the useOptionalVariables field is set.

Implements SatParametersOrBuilder.

Definition at line 21315 of file SatParameters.java.

◆ hasUseOverloadCheckerInCumulativeConstraint()

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

optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];

Returns
Whether the useOverloadCheckerInCumulativeConstraint field is set.

Implements SatParametersOrBuilder.

Definition at line 17642 of file SatParameters.java.

◆ hasUsePbResolution()

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

optional bool use_pb_resolution = 43 [default = false];

Returns
Whether the usePbResolution field is set.

Implements SatParametersOrBuilder.

Definition at line 15598 of file SatParameters.java.

◆ hasUsePhaseSaving()

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

optional bool use_phase_saving = 44 [default = true];

Returns
Whether the usePhaseSaving field is set.

Implements SatParametersOrBuilder.

Definition at line 12441 of file SatParameters.java.

◆ hasUsePrecedencesInDisjunctiveConstraint()

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

optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];

Returns
Whether the usePrecedencesInDisjunctiveConstraint field is set.

Implements SatParametersOrBuilder.

Definition at line 17561 of file SatParameters.java.

◆ hasUseProbingSearch()

.lang.Override boolean hasUseProbingSearch ( )
If true, search will continuously probe Boolean variables, and integer
variable bounds.

optional bool use_probing_search = 176 [default = false];

Returns
Whether the useProbingSearch field is set.

Implements SatParametersOrBuilder.

Definition at line 19638 of file SatParameters.java.

◆ hasUseRelaxationLns()

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

optional bool use_relaxation_lns = 150 [default = false];

Returns
Whether the useRelaxationLns field is set.

Implements SatParametersOrBuilder.

Definition at line 21066 of file SatParameters.java.

◆ hasUseRinsLns()

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

optional bool use_rins_lns = 129 [default = true];

Returns
Whether the useRinsLns field is set.

Implements SatParametersOrBuilder.

Definition at line 20912 of file SatParameters.java.

◆ hasUseSatInprocessing()

.lang.Override boolean hasUseSatInprocessing ( )

optional bool use_sat_inprocessing = 163 [default = false];

Returns
Whether the useSatInprocessing field is set.

Implements SatParametersOrBuilder.

Definition at line 16524 of file SatParameters.java.

◆ hasUseTimetableEdgeFindingInCumulativeConstraint()

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

optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];

Returns
Whether the useTimetableEdgeFindingInCumulativeConstraint field is set.

Implements SatParametersOrBuilder.

Definition at line 17717 of file SatParameters.java.

◆ hasVariableActivityDecay()

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

optional double variable_activity_decay = 15 [default = 0.8];

Returns
Whether the variableActivityDecay field is set.

Implements SatParametersOrBuilder.

Definition at line 13568 of file SatParameters.java.

◆ internalGetFieldAccessorTable()

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

Definition at line 10582 of file SatParameters.java.

◆ isInitialized()

.lang.Override final boolean isInitialized ( )

Definition at line 12194 of file SatParameters.java.

◆ mergeFrom() [1/3]

Definition at line 11681 of file SatParameters.java.

◆ mergeFrom() [2/3]

.lang.Override Builder mergeFrom ( com.google.protobuf.CodedInputStream  input,
com.google.protobuf.ExtensionRegistryLite  extensionRegistry 
) throws java.io.IOException

Definition at line 12199 of file SatParameters.java.

◆ mergeFrom() [3/3]

.lang.Override Builder mergeFrom ( com.google.protobuf.Message  other)

Definition at line 11672 of file SatParameters.java.

◆ mergeUnknownFields()

.lang.Override final Builder mergeUnknownFields ( final com.google.protobuf.UnknownFieldSet  unknownFields)

Definition at line 22318 of file SatParameters.java.

◆ setAbsoluteGapLimit()

Builder setAbsoluteGapLimit ( double  value)
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];
Parameters
valueThe absoluteGapLimit to set.
Returns
This builder for chaining.

Definition at line 14956 of file SatParameters.java.

◆ setAddCgCuts()

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

optional bool add_cg_cuts = 117 [default = true];

Parameters
valueThe addCgCuts to set.
Returns
This builder for chaining.

Definition at line 18212 of file SatParameters.java.

◆ setAddCliqueCuts()

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

optional bool add_clique_cuts = 172 [default = true];

Parameters
valueThe addCliqueCuts to set.
Returns
This builder for chaining.

Definition at line 18392 of file SatParameters.java.

◆ setAddKnapsackCuts()

Builder setAddKnapsackCuts ( boolean  value)
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];

Parameters
valueThe addKnapsackCuts to set.
Returns
This builder for chaining.

Definition at line 18152 of file SatParameters.java.

◆ setAddLinMaxCuts()

Builder setAddLinMaxCuts ( boolean  value)
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];

Parameters
valueThe addLinMaxCuts to set.
Returns
This builder for chaining.

Definition at line 18518 of file SatParameters.java.

◆ setAddLpConstraintsLazily()

Builder setAddLpConstraintsLazily ( boolean  value)
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];

Parameters
valueThe addLpConstraintsLazily to set.
Returns
This builder for chaining.

Definition at line 18663 of file SatParameters.java.

◆ setAddMirCuts()

Builder setAddMirCuts ( boolean  value)
Whether we generate MIR cuts at root node.
Note that for now, this is not heavily tuned.

optional bool add_mir_cuts = 120 [default = true];

Parameters
valueThe addMirCuts to set.
Returns
This builder for chaining.

Definition at line 18271 of file SatParameters.java.

◆ setAddZeroHalfCuts()

Builder setAddZeroHalfCuts ( boolean  value)
Whether we generate Zero-Half cuts at root node.
Note that for now, this is not heavily tuned.

optional bool add_zero_half_cuts = 169 [default = true];

Parameters
valueThe addZeroHalfCuts to set.
Returns
This builder for chaining.

Definition at line 18330 of file SatParameters.java.

◆ setAlsoBumpVariablesInConflictReasons()

Builder setAlsoBumpVariablesInConflictReasons ( boolean  value)
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];

Parameters
valueThe alsoBumpVariablesInConflictReasons to set.
Returns
This builder for chaining.

Definition at line 12888 of file SatParameters.java.

◆ setAutoDetectGreaterThanAtLeastOneOf()

Builder setAutoDetectGreaterThanAtLeastOneOf ( boolean  value)
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];

Parameters
valueThe autoDetectGreaterThanAtLeastOneOf to set.
Returns
This builder for chaining.

Definition at line 20281 of file SatParameters.java.

◆ setBinaryMinimizationAlgorithm()

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

Parameters
valueThe binaryMinimizationAlgorithm to set.
Returns
This builder for chaining.

Definition at line 12978 of file SatParameters.java.

◆ setBinarySearchNumConflicts()

Builder setBinarySearchNumConflicts ( int  value)
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];

Parameters
valueThe binarySearchNumConflicts to set.
Returns
This builder for chaining.

Definition at line 19855 of file SatParameters.java.

◆ setBlockingRestartMultiplier()

Builder setBlockingRestartMultiplier ( double  value)

optional double blocking_restart_multiplier = 66 [default = 1.4];

Parameters
valueThe blockingRestartMultiplier to set.
Returns
This builder for chaining.

Definition at line 14492 of file SatParameters.java.

◆ setBlockingRestartWindowSize()

Builder setBlockingRestartWindowSize ( int  value)

optional int32 blocking_restart_window_size = 65 [default = 5000];

Parameters
valueThe blockingRestartWindowSize to set.
Returns
This builder for chaining.

Definition at line 14453 of file SatParameters.java.

◆ setBooleanEncodingLevel()

Builder setBooleanEncodingLevel ( int  value)
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];

Parameters
valueThe booleanEncodingLevel to set.
Returns
This builder for chaining.

Definition at line 17964 of file SatParameters.java.

◆ setCatchSigintSignal()

Builder setCatchSigintSignal ( boolean  value)
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];

Parameters
valueThe catchSigintSignal to set.
Returns
This builder for chain