Java Reference
Java Reference
Detailed Description
Contains the definitions for all the sat algorithm parameters and their default values. NEXT TAG: 165
Protobuf type
Definition at line 9146 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 |
| .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 | 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.RestartAlgorithm > | getRestartAlgorithmsList () |
| 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 | hasLogSearchProgress () |
| .lang.Override boolean | getLogSearchProgress () |
| Builder | setLogSearchProgress (boolean value) |
| Builder | clearLogSearchProgress () |
| .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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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()
|
inline |
The restart strategies will change each time the strategy_counter is increased. The current strategy will simply be the one at index strategy_counter modulo the number of strategy. Note that if this list includes a NO_RESTART, nothing will change when it is reached because the strategy_counter will only increment after a restart. The idea of switching of search strategy tailored for SAT/UNSAT comes from Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/. But more generally, it seems REALLY beneficial to try different strategy.
repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;
- Parameters
-
values The restartAlgorithms to add.
- Returns
- This builder for chaining.
Definition at line 12216 of file SatParameters.java.
◆ addRepeatedField()
|
inline |
Definition at line 10100 of file SatParameters.java.
◆ addRestartAlgorithms()
|
inline |
The restart strategies will change each time the strategy_counter is increased. The current strategy will simply be the one at index strategy_counter modulo the number of strategy. Note that if this list includes a NO_RESTART, nothing will change when it is reached because the strategy_counter will only increment after a restart. The idea of switching of search strategy tailored for SAT/UNSAT comes from Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/. But more generally, it seems REALLY beneficial to try different strategy.
repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;
- Parameters
-
value The restartAlgorithms to add.
- Returns
- This builder for chaining.
Definition at line 12191 of file SatParameters.java.
◆ build()
|
inline |
Definition at line 9478 of file SatParameters.java.
◆ buildPartial()
|
inline |
Definition at line 9487 of file SatParameters.java.
◆ clear()
|
inline |
Definition at line 9179 of file SatParameters.java.
◆ clearAbsoluteGapLimit()
|
inline |
Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit. The exact definition is:
- Absolute: abs(O - B)
- Relative: abs(O - B) / max(1, abs(O)). Important: The relative gap depends on the objective offset! If you artificially shift the objective, you will get widely different value of the relative gap. Note that if the gap is reached, the search status will be OPTIMAL. But one can check the best objective bound to see the actual gap.
optional double absolute_gap_limit = 159 [default = 0];
- Returns
- This builder for chaining.
Definition at line 13154 of file SatParameters.java.
◆ clearAddCgCuts()
|
inline |
Whether we generate and add Chvatal-Gomory cuts to the LP at root node. Note that for now, this is not heavily tunned.
optional bool add_cg_cuts = 117 [default = true];
- Returns
- This builder for chaining.
Definition at line 15783 of file SatParameters.java.
◆ clearAddKnapsackCuts()
|
inline |
Whether we generate knapsack cuts. Note that in our setting where all variables are integer and bounded on both side, such a cut could be applied to any constraint.
optional bool add_knapsack_cuts = 111 [default = false];
- Returns
- This builder for chaining.
Definition at line 15724 of file SatParameters.java.
◆ clearAddLinMaxCuts()
|
inline |
For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)
optional bool add_lin_max_cuts = 152 [default = true];
- Returns
- This builder for chaining.
Definition at line 15968 of file SatParameters.java.
◆ clearAddLpConstraintsLazily()
|
inline |
If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch. A constraint that is only added like this is known as a "lazy" constraint in the literature, except that we currently consider all constraints as lazy here.
optional bool add_lp_constraints_lazily = 112 [default = true];
- Returns
- This builder for chaining.
Definition at line 16114 of file SatParameters.java.
◆ clearAddMirCuts()
|
inline |
Whether we generate MIR cuts at root node. Note that for now, this is not heavily tunned.
optional bool add_mir_cuts = 120 [default = true];
- Returns
- This builder for chaining.
Definition at line 15842 of file SatParameters.java.
◆ clearAlsoBumpVariablesInConflictReasons()
|
inline |
When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped. This is addition to the variables in the conflict, and the one that were used during conflict resolution.
optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];
- Returns
- This builder for chaining.
Definition at line 11080 of file SatParameters.java.
◆ clearAutoDetectGreaterThanAtLeastOneOf()
|
inline |
If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present. This is usually useful to have but can be slow on model with a lot of precedence.
optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];
- Returns
- This builder for chaining.
Definition at line 17531 of file SatParameters.java.
◆ clearBinaryMinimizationAlgorithm()
|
inline |
optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];
- Returns
- This builder for chaining.
Definition at line 11166 of file SatParameters.java.
◆ clearBinarySearchNumConflicts()
|
inline |
If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict. This can quickly reduce the objective domain on some problems.
optional int32 binary_search_num_conflicts = 99 [default = -1];
- Returns
- This builder for chaining.
Definition at line 17184 of file SatParameters.java.
◆ clearBlockingRestartMultiplier()
|
inline |
optional double blocking_restart_multiplier = 66 [default = 1.4];
- Returns
- This builder for chaining.
Definition at line 12677 of file SatParameters.java.
◆ clearBlockingRestartWindowSize()
|
inline |
optional int32 blocking_restart_window_size = 65 [default = 5000];
- Returns
- This builder for chaining.
Definition at line 12638 of file SatParameters.java.
◆ clearBooleanEncodingLevel()
|
inline |
A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.
optional int32 boolean_encoding_level = 107 [default = 1];
- Returns
- This builder for chaining.
Definition at line 15535 of file SatParameters.java.
◆ clearCatchSigintSignal()
|
inline |
Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve. If set, catching the SIGINT signal will terminate the search gracefully, as if a time limit was reached.
optional bool catch_sigint_signal = 135 [default = true];
- Returns
- This builder for chaining.
Definition at line 18766 of file SatParameters.java.
◆ clearClauseActivityDecay()
|
inline |
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 12038 of file SatParameters.java.
◆ clearClauseCleanupLbdBound()
|
inline |
All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.
optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
- Returns
- This builder for chaining.
Definition at line 11449 of file SatParameters.java.
◆ clearClauseCleanupOrdering()
|
inline |
optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];
- Returns
- This builder for chaining.
Definition at line 11492 of file SatParameters.java.
◆ clearClauseCleanupPeriod()
|
inline |
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 11288 of file SatParameters.java.
◆ clearClauseCleanupProtection()
|
inline |
optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];
- Returns
- This builder for chaining.
Definition at line 11390 of file SatParameters.java.
◆ clearClauseCleanupTarget()
|
inline |
During a cleanup, we will always keep that number of "deletable" clauses. Note that this doesn't include the "protected" clauses.
optional int32 clause_cleanup_target = 13 [default = 10000];
- Returns
- This builder for chaining.
Definition at line 11347 of file SatParameters.java.
◆ clearCountAssumptionLevelsInLbd()
|
inline |
Whether or not the assumption levels are taken into account during the LBD computation. According to the reference below, not counting them improves the solver in some situation. Note that this only impact solves under assumptions. Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction" Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes in Computer Science Volume 7962, 2013, pp 309-317.
optional bool count_assumption_levels_in_lbd = 49 [default = true];
- Returns
- This builder for chaining.
Definition at line 13603 of file SatParameters.java.
◆ clearCoverOptimization()
|
inline |
If true, when the max-sat algo find a core, we compute the minimal number of literals in the core that needs to be true to have a feasible solution.
optional bool cover_optimization = 89 [default = true];
- Returns
- This builder for chaining.
Definition at line 14948 of file SatParameters.java.
◆ clearCpModelMaxNumPresolveOperations()
|
inline |
If positive, try to stop just after that many presolve rules have been applied. This is mainly useful for debugging presolve.
optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];
- Returns
- This builder for chaining.
Definition at line 14209 of file SatParameters.java.
◆ clearCpModelPostsolveWithFullSolver()
|
inline |
Advanced usage. We have two different postsolve code. The default one should be better and it allows for a more powerful presolve, but some rarely used features like not fully assigning all variables require the other one.
optional bool cp_model_postsolve_with_full_solver = 162 [default = false];
- Returns
- This builder for chaining.
Definition at line 14150 of file SatParameters.java.
◆ clearCpModelPresolve()
|
inline |
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 14083 of file SatParameters.java.
◆ clearCpModelProbingLevel()
|
inline |
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 14264 of file SatParameters.java.
◆ clearCpModelUseSatPresolve()
|
inline |
Whether we also use the sat presolve when cp_model_presolve is true.
optional bool cp_model_use_sat_presolve = 93 [default = true];
- Returns
- This builder for chaining.
Definition at line 14319 of file SatParameters.java.
◆ clearCutActiveCountDecay()
|
inline |
optional double cut_active_count_decay = 156 [default = 0.8];
- Returns
- This builder for chaining.
Definition at line 16405 of file SatParameters.java.
◆ clearCutCleanupTarget()
|
inline |
Target number of constraints to remove during cleanup.
optional int32 cut_cleanup_target = 157 [default = 1000];
- Returns
- This builder for chaining.
Definition at line 16460 of file SatParameters.java.
◆ clearCutMaxActiveCountValue()
|
inline |
These parameters are similar to sat clause management activity parameters. They are effective only if the number of generated cuts exceed the storage limit. Default values are based on a few experiments on miplib instances.
optional double cut_max_active_count_value = 155 [default = 10000000000];
- Returns
- This builder for chaining.
Definition at line 16366 of file SatParameters.java.
◆ clearDefaultRestartAlgorithms()
|
inline |
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 12309 of file SatParameters.java.
◆ clearDiversifyLnsParams()
|
inline |
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 18313 of file SatParameters.java.
◆ clearEnumerateAllSolutions()
|
inline |
Whether we enumerate all solutions of a problem without objective. Note that setting this to true automatically disable the presolve. This is because the presolve rules only guarantee the existence of one feasible solution to the presolved problem. TODO(user): Activate the presolve but with just the rules that do not change the set of feasible solutions.
optional bool enumerate_all_solutions = 87 [default = false];
- Returns
- This builder for chaining.
Definition at line 17334 of file SatParameters.java.
◆ clearExpandAutomatonConstraints()
|
inline |
If true, the automaton constraints are expanded.
optional bool expand_automaton_constraints = 143 [default = true];
- Returns
- This builder for chaining.
Definition at line 14472 of file SatParameters.java.
◆ clearExpandElementConstraints()
|
inline |
If true, the element constraints are expanded into many linear constraints of the form (index == i) => (element[i] == target).
optional bool expand_element_constraints = 140 [default = true];
- Returns
- This builder for chaining.
Definition at line 14417 of file SatParameters.java.
◆ clearExpandTableConstraints()
|
inline |
If true, the positive table constraints are expanded. Note that currently, negative table constraints are always expanded.
optional bool expand_table_constraints = 158 [default = true];
- Returns
- This builder for chaining.
Definition at line 14531 of file SatParameters.java.
◆ clearExploitAllLpSolution()
|
inline |
If true and the Lp relaxation of the problem has a solution, try to exploit it. This is same as above except in this case the lp solution might not be an integer solution.
optional bool exploit_all_lp_solution = 116 [default = true];
- Returns
- This builder for chaining.
Definition at line 16751 of file SatParameters.java.
◆ clearExploitBestSolution()
|
inline |
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 16806 of file SatParameters.java.
◆ clearExploitIntegerLpSolution()
|
inline |
If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it. Note that since the LP relaxation may not contain all the constraints, such a solution is not necessarily a solution of the full problem.
optional bool exploit_integer_lp_solution = 94 [default = true];
- Returns
- This builder for chaining.
Definition at line 16688 of file SatParameters.java.
◆ clearExploitObjective()
|
inline |
When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.
optional bool exploit_objective = 131 [default = true];
- Returns
- This builder for chaining.
Definition at line 16928 of file SatParameters.java.
◆ clearExploitRelaxationSolution()
|
inline |
When branching on a variable, follow the last best relaxation solution value. We use the relaxation with the tightest bound on the objective as the best relaxation solution.
optional bool exploit_relaxation_solution = 161 [default = false];
- Returns
- This builder for chaining.
Definition at line 16869 of file SatParameters.java.
◆ clearField()
|
inline |
Definition at line 10084 of file SatParameters.java.
◆ clearFillTightenedDomainsInResponse()
|
inline |
If true, add information about the derived variable domains to the CpSolverResponse. It is an option because it makes the response slighly bigger and there is a bit more work involved during the postsolve to construct it, but it should still have a low overhead. See the tightened_variables field in CpSolverResponse for more details.
optional bool fill_tightened_domains_in_response = 132 [default = false];
- Returns
- This builder for chaining.
Definition at line 17405 of file SatParameters.java.
◆ clearFindMultipleCores()
|
inline |
Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.
optional bool find_multiple_cores = 84 [default = true];
- Returns
- This builder for chaining.
Definition at line 14889 of file SatParameters.java.
◆ clearGlucoseDecayIncrement()
|
inline |
optional double glucose_decay_increment = 23 [default = 0.01];
- Returns
- This builder for chaining.
Definition at line 11944 of file SatParameters.java.
◆ clearGlucoseDecayIncrementPeriod()
|
inline |
optional int32 glucose_decay_increment_period = 24 [default = 5000];
- Returns
- This builder for chaining.
Definition at line 11983 of file SatParameters.java.
◆ clearGlucoseMaxDecay()
|
inline |
The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95. This "hack" seems to work well and comes from: Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013 http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136
optional double glucose_max_decay = 22 [default = 0.95];
- Returns
- This builder for chaining.
Definition at line 11905 of file SatParameters.java.
◆ clearHintConflictLimit()
|
inline |
When we try to follow the hint, we do a FIXED_SEARCH using the hint until this number of conflict is reached.
optional int32 hint_conflict_limit = 153 [default = 10];
- Returns
- This builder for chaining.
Definition at line 16621 of file SatParameters.java.
◆ clearInitialPolarity()
|
inline |
optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];
- Returns
- This builder for chaining.
Definition at line 10662 of file SatParameters.java.
◆ clearInitialVariablesActivity()
|
inline |
The initial value of the variables activity. A non-zero value only make sense when use_erwa_heuristic is true. Experiments with a value of 1e-2 together with the ERWA heuristic showed slighthly better result than simply using zero. The idea is that when the "learning rate" of a variable becomes lower than this value, then we prefer to branch on never explored before variables. This is not in the ERWA paper.
optional double initial_variables_activity = 76 [default = 0];
- Returns
- This builder for chaining.
Definition at line 11013 of file SatParameters.java.
◆ clearInstantiateAllVariables()
|
inline |
If true, the solver will add a default integer branching strategy to the already defined search strategy.
optional bool instantiate_all_variables = 106 [default = true];
- Returns
- This builder for chaining.
Definition at line 17464 of file SatParameters.java.
◆ clearInterleaveBatchSize()
|
inline |
optional int32 interleave_batch_size = 134 [default = 1];
- Returns
- This builder for chaining.
Definition at line 17830 of file SatParameters.java.
◆ clearInterleaveSearch()
|
inline |
Experimental. If this is true, then we interleave all our major search strategy and distribute the work amongst num_search_workers. The search is deterministic (independently of num_search_workers!), and we schedule and wait for interleave_batch_size task to be completed before synchronizing and scheduling the next batch of tasks.
optional bool interleave_search = 136 [default = false];
- Returns
- This builder for chaining.
Definition at line 17791 of file SatParameters.java.
◆ clearLinearizationLevel()
|
inline |
A non-negative level indicating the type of constraints we consider in the LP relaxation. At level zero, no LP relaxation is used. At level 1, only the linear constraint and full encoding are added. At level 2, we also add all the Boolean constraints.
optional int32 linearization_level = 90 [default = 1];
- Returns
- This builder for chaining.
Definition at line 15476 of file SatParameters.java.
◆ clearLnsFocusOnDecisionVariables()
|
inline |
optional bool lns_focus_on_decision_variables = 105 [default = false];
- Returns
- This builder for chaining.
Definition at line 18089 of file SatParameters.java.
◆ clearLogSearchProgress()
|
inline |
Whether the solver should log the search progress to LOG(INFO).
optional bool log_search_progress = 41 [default = false];
- Returns
- This builder for chaining.
Definition at line 13386 of file SatParameters.java.
◆ clearMaxAllDiffCutSize()
|
inline |
Cut generator for all diffs can add too many cuts for large all_diff constraints. This parameter restricts the large all_diff constraints to have a cut generator.
optional int32 max_all_diff_cut_size = 148 [default = 7];
- Returns
- This builder for chaining.
Definition at line 15905 of file SatParameters.java.
◆ clearMaxClauseActivityValue()
|
inline |
optional double max_clause_activity_value = 18 [default = 1e+20];
- Returns
- This builder for chaining.
Definition at line 12077 of file SatParameters.java.
◆ clearMaxConsecutiveInactiveCount()
|
inline |
If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP. Note that it might be added again later if it become violated by the current LP solution.
optional int32 max_consecutive_inactive_count = 121 [default = 100];
- Returns
- This builder for chaining.
Definition at line 16303 of file SatParameters.java.
◆ clearMaxCutRoundsAtLevelZero()
|
inline |
Max number of time we perform cut generation and resolve the LP at level 0.
optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];
- Returns
- This builder for chaining.
Definition at line 16240 of file SatParameters.java.
◆ clearMaxDeterministicTime()
|
inline |
Maximum time allowed in deterministic time to solve a problem. The deterministic time should be correlated with the real time used by the solver, the time unit being as close as possible to a second.
optional double max_deterministic_time = 67 [default = inf];
- Returns
- This builder for chaining.
Definition at line 12921 of file SatParameters.java.
◆ clearMaxIntegerRoundingScaling()
|
inline |
In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive). The lower this is, the lower the integer coefficients of the cut will be. Note that cut generated by lower values are not necessarily worse than cut generated by larger value. There is no strict dominance relationship. Setting this to 2 result in the "strong fractional rouding" of Letchford and Lodi.
optional int32 max_integer_rounding_scaling = 119 [default = 600];
- Returns
- This builder for chaining.
Definition at line 16047 of file SatParameters.java.
◆ clearMaxMemoryInMb()
|
inline |
Maximum memory allowed for the whole thread containing the solver. The solver will abort as soon as it detects that this limit is crossed. As a result, this limit is approximative, but usually the solver will not go too much over.
optional int64 max_memory_in_mb = 40 [default = 10000];
- Returns
- This builder for chaining.
Definition at line 13063 of file SatParameters.java.
◆ clearMaxNumberOfConflicts()
|
inline |
Maximum number of conflicts allowed to solve a problem. TODO(user,user): Maybe change the way the conflict limit is enforced? currently it is enforced on each independent internal SAT solve, rather than on the overall number of conflicts across all solves. So in the context of an optimization problem, this is not really usable directly by a client.
optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];
- Returns
- This builder for chaining.
Definition at line 12996 of file SatParameters.java.
◆ clearMaxNumCuts()
|
inline |
The limit on the number of cuts in our cut pool. When this is reached we do not generate cuts anymore. TODO(user): We should probably remove this parameters, and just always generate cuts but only keep the best n or something.
optional int32 max_num_cuts = 91 [default = 10000];
- Returns
- This builder for chaining.
Definition at line 15602 of file SatParameters.java.
◆ clearMaxPresolveIterations()
|
inline |
In case of large reduction in a presolve iteration, we perform multiple presolve iterations. This parameter controls the maximum number of such presolve iterations.
optional int32 max_presolve_iterations = 138 [default = 3];
- Returns
- This builder for chaining.
Definition at line 14028 of file SatParameters.java.
◆ clearMaxSatAssumptionOrder()
|
inline |
optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];
- Returns
- This builder for chaining.
Definition at line 14991 of file SatParameters.java.
◆ clearMaxSatReverseAssumptionOrder()
|
inline |
If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.
optional bool max_sat_reverse_assumption_order = 52 [default = false];
- Returns
- This builder for chaining.
Definition at line 15050 of file SatParameters.java.
◆ clearMaxSatStratification()
|
inline |
optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];
- Returns
- This builder for chaining.
Definition at line 15093 of file SatParameters.java.
◆ clearMaxTimeInSeconds()
|
inline |
Maximum time allowed in seconds to solve a problem. The counter will starts at the beginning of the Solve() call.
optional double max_time_in_seconds = 36 [default = inf];
- Returns
- This builder for chaining.
Definition at line 12858 of file SatParameters.java.
◆ clearMaxVariableActivityValue()
|
inline |
optional double max_variable_activity_value = 16 [default = 1e+100];
- Returns
- This builder for chaining.
Definition at line 11838 of file SatParameters.java.
◆ clearMergeAtMostOneWorkLimit()
|
inline |
optional double merge_at_most_one_work_limit = 146 [default = 100000000];
- Returns
- This builder for chaining.
Definition at line 14641 of file SatParameters.java.
◆ clearMergeNoOverlapWorkLimit()
|
inline |
During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints. This code can be slow, so we have a limit in place on the number of explored nodes in the underlying graph. The internal limit is an int64, but we use double here to simplify manual input.
optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];
- Returns
- This builder for chaining.
Definition at line 14602 of file SatParameters.java.
◆ clearMinimizationAlgorithm()
|
inline |
optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];
- Returns
- This builder for chaining.
Definition at line 11123 of file SatParameters.java.
◆ clearMinimizeCore()
|
inline |
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 14830 of file SatParameters.java.
◆ clearMinimizeReductionDuringPbResolution()
|
inline |
A different algorithm during PB resolution. It minimizes the number of calls to ReduceCoefficients() which can be time consuming. However, the search space will be different and if the coefficients are large, this may lead to integer overflows that could otherwise be prevented.
optional bool minimize_reduction_during_pb_resolution = 48 [default = false];
- Returns
- This builder for chaining.
Definition at line 13520 of file SatParameters.java.
◆ clearMinimizeWithPropagationNumDecisions()
|
inline |
optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];
- Returns
- This builder for chaining.
Definition at line 11720 of file SatParameters.java.
◆ clearMinimizeWithPropagationRestartPeriod()
|
inline |
Parameters for an heuristic similar to the one descibed in "An effective learnt clause minimization approach for CDCL Sat Solvers", https://www.ijcai.org/proceedings/2017/0098.pdf For now, we have a somewhat simpler implementation where every x restart we spend y decisions on clause minimization. The minimization technique is the same as the one used to minimize core in max-sat. We also minimize problem clauses and not just the learned clause that we keep forever like in the paper. Changing these parameters or the kind of clause we minimize seems to have a big impact on the overall perf on our benchmarks. So this technique seems definitely useful, but it is hard to tune properly.
optional int32 minimize_with_propagation_restart_period = 96 [default = 10];
- Returns
- This builder for chaining.
Definition at line 11681 of file SatParameters.java.
◆ clearMinOrthogonalityForLpConstraints()
|
inline |
While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call. Orthogonality is defined as 1 - cosine(vector angle between constraints). A value of zero disable this feature.
optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];
- Returns
- This builder for chaining.
Definition at line 16185 of file SatParameters.java.
◆ clearMipCheckPrecision()
|
inline |
As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted coefficient precision during scaling. When we cannot, we will report MODEL_INVALID if the relative preicision is larger than this parameter.
optional double mip_check_precision = 128 [default = 0.0001];
- Returns
- This builder for chaining.
Definition at line 19188 of file SatParameters.java.
◆ clearMipMaxActivityExponent()
|
inline |
To avoid integer overflow, we always force the maximum possible constraint activity (and objective value) according to the initial variable domain to be smaller than 2 to this given power. Because of this, we cannot always reach the "mip_wanted_precision" parameter above. This can go as high as 62, but some internal algo currently abort early if they might run into integer overflow, so it is better to keep it a bit lower than this.
optional int32 mip_max_activity_exponent = 127 [default = 53];
- Returns
- This builder for chaining.
Definition at line 19121 of file SatParameters.java.
◆ clearMipMaxBound()
|
inline |
We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use. If the MIP model expect larger variable value in the solution, then the converted model will likely not be relevant.
optional double mip_max_bound = 124 [default = 10000000];
- Returns
- This builder for chaining.
Definition at line 18892 of file SatParameters.java.
◆ clearMipVarScaling()
|
inline |
All continuous variable of the problem will be multiplied by this factor. By default, we don't do any variable scaling and rely on the MIP model to specify continuous variable domain with the wanted precision.
optional double mip_var_scaling = 125 [default = 1];
- Returns
- This builder for chaining.
Definition at line 18955 of file SatParameters.java.
◆ clearMipWantedPrecision()
|
inline |
When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients. We will choose the lowest power such that we have this relative precision on each of the constraint (resp. objective) coefficient. We also use this to decide by how much we relax the constraint bounds so that we can have a feasible integer solution of constraints involving continuous variable. This is required for instance when you have an == rhs constraint as in many situation you cannot have a perfect equality with integer variables and coefficients.
optional double mip_wanted_precision = 126 [default = 1e-06];
- Returns
- This builder for chaining.
Definition at line 19042 of file SatParameters.java.
◆ clearNewConstraintsBatchSize()
|
inline |
Add that many lazy contraints (or cuts) at once in the LP. Note that at the beginning of the solve, we do add more than this.
optional int32 new_constraints_batch_size = 122 [default = 50];
- Returns
- This builder for chaining.
Definition at line 16519 of file SatParameters.java.
◆ clearNumConflictsBeforeStrategyChanges()
|
inline |
After each restart, if the number of conflict since the last strategy change is greater that this, then we increment a "strategy_counter" that can be use to change the search strategy used by the following restarts.
optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];
- Returns
- This builder for chaining.
Definition at line 12740 of file SatParameters.java.
◆ clearNumSearchWorkers()
|
inline |
Specify the number of parallel workers to use during search. A number <= 1 means no parallelism. As of 2020-04-10, if you're using SAT via MPSolver (to solve integer programs) this field is overridden with a value of 8, if the field is not set *explicitly*. Thus, always set this field explicitly or via MPSolver::SetNumThreads().
optional int32 num_search_workers = 100 [default = 1];
- Returns
- This builder for chaining.
Definition at line 17720 of file SatParameters.java.
◆ clearOneof()
|
inline |
Definition at line 10089 of file SatParameters.java.
◆ clearOnlyAddCutsAtLevelZero()
|
inline |
For the cut that can be generated at any level, this control if we only try to generate them at the root node.
optional bool only_add_cuts_at_level_zero = 92 [default = false];
- Returns
- This builder for chaining.
Definition at line 15661 of file SatParameters.java.
◆ clearOptimizeWithCore()
|
inline |
The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one. If this is true, then we use a core-based approach (like in max-SAT) when we try to increase the lower bound instead.
optional bool optimize_with_core = 83 [default = false];
- Returns
- This builder for chaining.
Definition at line 17117 of file SatParameters.java.
◆ clearOptimizeWithMaxHs()
|
inline |
This has no effect if optimize_with_core is false. If true, use a different core-based algorithm similar to the max-HS algo for max-SAT. This is a hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT one. This is also related to the PhD work of tobyodavies@ "Automatic Logic-Based Benders Decomposition with MiniZinc" http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489
optional bool optimize_with_max_hs = 85 [default = false];
- Returns
- This builder for chaining.
Definition at line 17259 of file SatParameters.java.
◆ clearPbCleanupIncrement()
|
inline |
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 11547 of file SatParameters.java.
◆ clearPbCleanupRatio()
|
inline |
optional double pb_cleanup_ratio = 47 [default = 0.5];
- Returns
- This builder for chaining.
Definition at line 11586 of file SatParameters.java.
◆ clearPreferredVariableOrder()
|
inline |
optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
- Returns
- This builder for chaining.
Definition at line 10619 of file SatParameters.java.
◆ clearPresolveBlockedClause()
|
inline |
Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.
optional bool presolve_blocked_clause = 88 [default = true];
- Returns
- This builder for chaining.
Definition at line 13843 of file SatParameters.java.
◆ clearPresolveBvaThreshold()
|
inline |
Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold. The algorithm described in the paper uses 0, but quick experiments showed that 1 is a good value. It may not be worth it to add a new variable just to remove one clause.
optional int32 presolve_bva_threshold = 73 [default = 1];
- Returns
- This builder for chaining.
Definition at line 13965 of file SatParameters.java.
◆ clearPresolveBveClauseWeight()
|
inline |
During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.
optional int32 presolve_bve_clause_weight = 55 [default = 3];
- Returns
- This builder for chaining.
Definition at line 13725 of file SatParameters.java.
◆ clearPresolveBveThreshold()
|
inline |
During presolve, only try to perform the bounded variable elimination (BVE) of a variable x if the number of occurrences of x times the number of occurrences of not(x) is not greater than this parameter.
optional int32 presolve_bve_threshold = 54 [default = 500];
- Returns
- This builder for chaining.
Definition at line 13666 of file SatParameters.java.
◆ clearPresolveProbingDeterministicTimeLimit()
|
inline |
The maximum "deterministic" time limit to spend in probing. A value of zero will disable the probing.
optional double presolve_probing_deterministic_time_limit = 57 [default = 30];
- Returns
- This builder for chaining.
Definition at line 13784 of file SatParameters.java.
◆ clearPresolveSubstitutionLevel()
|
inline |
How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve. This currently only concerns variable appearing only in linear constraints. For now the value 0 turns it off and any positive value performs substitution.
optional int32 presolve_substitution_level = 147 [default = 1];
- Returns
- This builder for chaining.
Definition at line 14708 of file SatParameters.java.
◆ clearPresolveUseBva()
|
inline |
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 13898 of file SatParameters.java.
◆ clearProbingPeriodAtRoot()
|
inline |
If set at zero (the default), it is disabled. Otherwise the solver attempts probing at every 'probing_period' root node. Period of 1 enables probing at every root node.
optional int64 probing_period_at_root = 142 [default = 0];
- Returns
- This builder for chaining.
Definition at line 16991 of file SatParameters.java.
◆ clearPseudoCostReliabilityThreshold()
|
inline |
The solver ignores the pseudo costs of variables with number of recordings less than this threshold.
optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
- Returns
- This builder for chaining.
Definition at line 17050 of file SatParameters.java.
◆ clearRandomBranchesRatio()
|
inline |
A number between 0 and 1 that indicates the proportion of branching variables that are selected randomly instead of choosing the first variable from the given variable_ordering strategy.
optional double random_branches_ratio = 32 [default = 0];
- Returns
- This builder for chaining.
Definition at line 10875 of file SatParameters.java.
◆ clearRandomizeSearch()
|
inline |
Randomize fixed search.
optional bool randomize_search = 103 [default = false];
- Returns
- This builder for chaining.
Definition at line 18368 of file SatParameters.java.
◆ clearRandomPolarityRatio()
|
inline |
The proportion of polarity chosen at random. Note that this take precedence over the phase saving heuristic. This is different from initial_polarity:POLARITY_RANDOM because it will select a new random polarity each time the variable is branched upon instead of selecting one initially and then always taking this choice.
optional double random_polarity_ratio = 45 [default = 0];
- Returns
- This builder for chaining.
Definition at line 10812 of file SatParameters.java.
◆ clearRandomSeed()
|
inline |
At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed. If you change the random seed, the solver may make different choices during the solving process. For some problems, the running time may vary a lot depending on small change in the solving algorithm. Running the solver with different seeds enables to have more robust benchmarks when evaluating new features.
optional int32 random_seed = 31 [default = 1];
- Returns
- This builder for chaining.
Definition at line 13331 of file SatParameters.java.
◆ clearReduceMemoryUsageInInterleaveMode()
|
inline |
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 17885 of file SatParameters.java.
◆ clearRelativeGapLimit()
|
inline |
optional double relative_gap_limit = 160 [default = 0];
- Returns
- This builder for chaining.
Definition at line 13193 of file SatParameters.java.
◆ clearRestartAlgorithms()
|
inline |
The restart strategies will change each time the strategy_counter is increased. The current strategy will simply be the one at index strategy_counter modulo the number of strategy. Note that if this list includes a NO_RESTART, nothing will change when it is reached because the strategy_counter will only increment after a restart. The idea of switching of search strategy tailored for SAT/UNSAT comes from Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/. But more generally, it seems REALLY beneficial to try different strategy.
repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;
- Returns
- This builder for chaining.
Definition at line 12240 of file SatParameters.java.
◆ clearRestartDlAverageRatio()
|
inline |
In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.
optional double restart_dl_average_ratio = 63 [default = 1];
- Returns
- This builder for chaining.
Definition at line 12497 of file SatParameters.java.
◆ clearRestartLbdAverageRatio()
|
inline |
optional double restart_lbd_average_ratio = 71 [default = 1];
- Returns
- This builder for chaining.
Definition at line 12536 of file SatParameters.java.
◆ clearRestartPeriod()
|
inline |
Restart period for the FIXED_RESTART strategy. This is also the multiplier used by the LUBY_RESTART strategy.
optional int32 restart_period = 30 [default = 50];
- Returns
- This builder for chaining.
Definition at line 12383 of file SatParameters.java.
◆ clearRestartRunningWindowSize()
|
inline |
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 12438 of file SatParameters.java.
◆ clearSearchBranching()
|
inline |
optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
- Returns
- This builder for chaining.
Definition at line 16562 of file SatParameters.java.
◆ clearSearchRandomizationTolerance()
|
inline |
Search randomization will collect equivalent 'max valued' variables, and pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST, all unassigned variables are equivalent. If the variable strategy is CHOOSE_LOWEST_MIN, and `lm` is the current lowest min of all unassigned variables, then the set of max valued variables will be all unassigned variables where lm <= variable min <= lm + search_randomization_tolerance
optional int64 search_randomization_tolerance = 104 [default = 0];
- Returns
- This builder for chaining.
Definition at line 18447 of file SatParameters.java.
◆ clearShareLevelZeroBounds()
|
inline |
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 17995 of file SatParameters.java.
◆ clearShareObjectiveBounds()
|
inline |
Allows objective sharing between workers.
optional bool share_objective_bounds = 113 [default = true];
- Returns
- This builder for chaining.
Definition at line 17940 of file SatParameters.java.
◆ clearStopAfterFirstSolution()
|
inline |
For an optimization problem, stop the solver as soon as we have a solution.
optional bool stop_after_first_solution = 98 [default = false];
- Returns
- This builder for chaining.
Definition at line 17586 of file SatParameters.java.
◆ clearStopAfterPresolve()
|
inline |
Mainly used when improving the presolver. When true, stops the solver after the presolve is complete.
optional bool stop_after_presolve = 149 [default = false];
- Returns
- This builder for chaining.
Definition at line 17645 of file SatParameters.java.
◆ clearStrategyChangeIncreaseRatio()
|
inline |
The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.
optional double strategy_change_increase_ratio = 69 [default = 0];
- Returns
- This builder for chaining.
Definition at line 12799 of file SatParameters.java.
◆ clearSubsumptionDuringConflictAnalysis()
|
inline |
At a really low cost, during the 1-UIP conflict computation, it is easy to detect if some of the involved reasons are subsumed by the current conflict. When this is true, such clauses are detached and later removed from the problem.
optional bool subsumption_during_conflict_analysis = 56 [default = true];
- Returns
- This builder for chaining.
Definition at line 11233 of file SatParameters.java.
◆ clearTreatBinaryClausesSeparately()
|
inline |
If true, the binary clauses are treated separately from the others. This should be faster and uses less memory. However it changes the propagation order.
optional bool treat_binary_clauses_separately = 33 [default = true];
- Returns
- This builder for chaining.
Definition at line 13256 of file SatParameters.java.
◆ clearUseBlockingRestart()
|
inline |
Block a moving restart algorithm if the trail size of the current conflict is greater than the multiplier times the moving average of the trail size at the previous conflicts.
optional bool use_blocking_restart = 64 [default = false];
- Returns
- This builder for chaining.
Definition at line 12599 of file SatParameters.java.
◆ clearUseBranchingInLp()
|
inline |
If true, the solver attemts to generate more info inside lp propagator by branching on some variables if certain criteria are met during the search tree exploration.
optional bool use_branching_in_lp = 139 [default = false];
- Returns
- This builder for chaining.
Definition at line 18640 of file SatParameters.java.
◆ clearUseCombinedNoOverlap()
|
inline |
This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem. Like 1000 intervals, but 1M intervals in the no-overlap constraints covering them.
optional bool use_combined_no_overlap = 133 [default = false];
- Returns
- This builder for chaining.
Definition at line 18703 of file SatParameters.java.
◆ clearUseDisjunctiveConstraintInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with propagators from the disjunctive constraint to improve the inference on a set of tasks that are disjunctive at the root of the problem. This additional level supplements the default level of reasoning. Propagators of the cumulative constraint will not be used at all if all the tasks are disjunctive at root node. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];
- Returns
- This builder for chaining.
Definition at line 15409 of file SatParameters.java.
◆ clearUseErwaHeuristic()
|
inline |
Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as described in "Learning Rate Based Branching Heuristic for SAT solvers", J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.
optional bool use_erwa_heuristic = 75 [default = false];
- Returns
- This builder for chaining.
Definition at line 10938 of file SatParameters.java.
◆ clearUseExactLpReason()
|
inline |
The solver usually exploit the LP relaxation of a model. If this option is true, then whatever is infered by the LP will be used like an heuristic to compute EXACT propagation on the IP. So with this option, there is no numerical imprecision issues.
optional bool use_exact_lp_reason = 109 [default = true];
- Returns
- This builder for chaining.
Definition at line 18577 of file SatParameters.java.
◆ clearUseFeasibilityPump()
|
inline |
Adds a feasibility pump subsolver along with lns subsolvers.
optional bool use_feasibility_pump = 164 [default = false];
- Returns
- This builder for chaining.
Definition at line 18199 of file SatParameters.java.
◆ clearUseImpliedBounds()
|
inline |
Stores and exploits "implied-bounds" in the solver. That is, relations of the form literal => (var >= bound). This is currently used to derive stronger cuts.
optional bool use_implied_bounds = 144 [default = true];
- Returns
- This builder for chaining.
Definition at line 18829 of file SatParameters.java.
◆ clearUseLnsOnly()
|
inline |
LNS parameters.
optional bool use_lns_only = 101 [default = false];
- Returns
- This builder for chaining.
Definition at line 18050 of file SatParameters.java.
◆ clearUseOptimizationHints()
|
inline |
For an optimization problem, whether we follow some hints in order to find a better first solution. For a variable with hint, the solver will always try to follow the hint. It will revert to the variable_branching default otherwise.
optional bool use_optimization_hints = 35 [default = true];
- Returns
- This builder for chaining.
Definition at line 14775 of file SatParameters.java.
◆ clearUseOptionalVariables()
|
inline |
If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional. This allows to propagate them as if they were present in some situation.
optional bool use_optional_variables = 108 [default = true];
- Returns
- This builder for chaining.
Definition at line 18510 of file SatParameters.java.
◆ clearUseOverloadCheckerInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy. This additional level supplements the default level of reasoning as well as timetable edge finding. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];
- Returns
- This builder for chaining.
Definition at line 15251 of file SatParameters.java.
◆ clearUsePbResolution()
|
inline |
Whether to use pseudo-Boolean resolution to analyze a conflict. Note that this option only make sense if your problem is modelized using pseudo-Boolean constraints. If you only have clauses, this shouldn't change anything (except slow the solver down).
optional bool use_pb_resolution = 43 [default = false];
- Returns
- This builder for chaining.
Definition at line 13453 of file SatParameters.java.
◆ clearUsePhaseSaving()
|
inline |
If this is true, then the polarity of a variable will be the last value it was assigned to, or its default polarity if it was never assigned since the call to ResetDecisionHeuristic(). This is called 'literal phase saving'. For details see 'A Lightweight Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and A.Darwiche, In 10th International Conference on Theory and Applications of Satisfiability Testing, 2007.
optional bool use_phase_saving = 44 [default = true];
- Returns
- This builder for chaining.
Definition at line 10741 of file SatParameters.java.
◆ clearUsePrecedencesInDisjunctiveConstraint()
|
inline |
When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further. For instance if task A and B are both before C and task A and B are in disjunction, then we can deduce that task C must start after duration(A) + duration(B) instead of simply max(duration(A), duration(B)), provided that the start time for all task was currently zero. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];
- Returns
- This builder for chaining.
Definition at line 15176 of file SatParameters.java.
◆ clearUseRelaxationLns()
|
inline |
Turns on a lns worker which solves relaxed version of the original problem by removing constraints from the problem in order to get better bounds.
optional bool use_relaxation_lns = 150 [default = false];
- Returns
- This builder for chaining.
Definition at line 18258 of file SatParameters.java.
◆ clearUseRinsLns()
|
inline |
Turns on relaxation induced neighborhood generator.
optional bool use_rins_lns = 129 [default = true];
- Returns
- This builder for chaining.
Definition at line 18144 of file SatParameters.java.
◆ clearUseSatInprocessing()
|
inline |
optional bool use_sat_inprocessing = 163 [default = false];
- Returns
- This builder for chaining.
Definition at line 14358 of file SatParameters.java.
◆ clearUseTimetableEdgeFindingInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with timetable edge finding, i.e., an additional level of reasoning based on the conjunction of energy and mandatory parts. This additional level supplements the default level of reasoning as well as overload_checker. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];
- Returns
- This builder for chaining.
Definition at line 15326 of file SatParameters.java.
◆ clearVariableActivityDecay()
|
inline |
Each time a conflict is found, the activities of some variables are increased by one. Then, the activity of all variables are multiplied by variable_activity_decay. To implement this efficiently, the activity of all the variables is not decayed at each conflict. Instead, the activity increment is multiplied by 1 / decay. When an activity reach max_variable_activity_value, all the activity are multiplied by 1 / max_variable_activity_value.
optional double variable_activity_decay = 15 [default = 0.8];
- Returns
- This builder for chaining.
Definition at line 11799 of file SatParameters.java.
◆ clone()
|
inline |
Definition at line 10074 of file SatParameters.java.
◆ getAbsoluteGapLimit()
|
inline |
Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit. The exact definition is:
- Absolute: abs(O - B)
- Relative: abs(O - B) / max(1, abs(O)). Important: The relative gap depends on the objective offset! If you artificially shift the objective, you will get widely different value of the relative gap. Note that if the gap is reached, the search status will be OPTIMAL. But one can check the best objective bound to see the actual gap.
optional double absolute_gap_limit = 159 [default = 0];
- Returns
- The absoluteGapLimit.
Implements SatParametersOrBuilder.
Definition at line 13110 of file SatParameters.java.
◆ getAddCgCuts()
|
inline |
Whether we generate and add Chvatal-Gomory cuts to the LP at root node. Note that for now, this is not heavily tunned.
optional bool add_cg_cuts = 117 [default = true];
- Returns
- The addCgCuts.
Implements SatParametersOrBuilder.
Definition at line 15755 of file SatParameters.java.
◆ getAddKnapsackCuts()
|
inline |
Whether we generate knapsack cuts. Note that in our setting where all variables are integer and bounded on both side, such a cut could be applied to any constraint.
optional bool add_knapsack_cuts = 111 [default = false];
- Returns
- The addKnapsackCuts.
Implements SatParametersOrBuilder.
Definition at line 15694 of file SatParameters.java.
◆ getAddLinMaxCuts()
|
inline |
For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)
optional bool add_lin_max_cuts = 152 [default = true];
- Returns
- The addLinMaxCuts.
Implements SatParametersOrBuilder.
Definition at line 15938 of file SatParameters.java.
◆ getAddLpConstraintsLazily()
|
inline |
If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch. A constraint that is only added like this is known as a "lazy" constraint in the literature, except that we currently consider all constraints as lazy here.
optional bool add_lp_constraints_lazily = 112 [default = true];
- Returns
- The addLpConstraintsLazily.
Implements SatParametersOrBuilder.
Definition at line 16082 of file SatParameters.java.
◆ getAddMirCuts()
|
inline |
Whether we generate MIR cuts at root node. Note that for now, this is not heavily tunned.
optional bool add_mir_cuts = 120 [default = true];
- Returns
- The addMirCuts.
Implements SatParametersOrBuilder.
Definition at line 15814 of file SatParameters.java.
◆ getAlsoBumpVariablesInConflictReasons()
|
inline |
When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped. This is addition to the variables in the conflict, and the one that were used during conflict resolution.
optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];
- Returns
- The alsoBumpVariablesInConflictReasons.
Implements SatParametersOrBuilder.
Definition at line 11048 of file SatParameters.java.
◆ getAutoDetectGreaterThanAtLeastOneOf()
|
inline |
If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present. This is usually useful to have but can be slow on model with a lot of precedence.
optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];
- Returns
- The autoDetectGreaterThanAtLeastOneOf.
Implements SatParametersOrBuilder.
Definition at line 17499 of file SatParameters.java.
◆ getBinaryMinimizationAlgorithm()
|
inline |
optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];
- Returns
- The binaryMinimizationAlgorithm.
Implements SatParametersOrBuilder.
Definition at line 11143 of file SatParameters.java.
◆ getBinarySearchNumConflicts()
|
inline |
If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict. This can quickly reduce the objective domain on some problems.
optional int32 binary_search_num_conflicts = 99 [default = -1];
- Returns
- The binarySearchNumConflicts.
Implements SatParametersOrBuilder.
Definition at line 17152 of file SatParameters.java.
◆ getBlockingRestartMultiplier()
|
inline |
optional double blocking_restart_multiplier = 66 [default = 1.4];
- Returns
- The blockingRestartMultiplier.
Implements SatParametersOrBuilder.
Definition at line 12659 of file SatParameters.java.
◆ getBlockingRestartWindowSize()
|
inline |
optional int32 blocking_restart_window_size = 65 [default = 5000];
- Returns
- The blockingRestartWindowSize.
Implements SatParametersOrBuilder.
Definition at line 12620 of file SatParameters.java.
◆ getBooleanEncodingLevel()
|
inline |
A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.
optional int32 boolean_encoding_level = 107 [default = 1];
- Returns
- The booleanEncodingLevel.
Implements SatParametersOrBuilder.
Definition at line 15507 of file SatParameters.java.
◆ getCatchSigintSignal()
|
inline |
Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve. If set, catching the SIGINT signal will terminate the search gracefully, as if a time limit was reached.
optional bool catch_sigint_signal = 135 [default = true];
- Returns
- The catchSigintSignal.
Implements SatParametersOrBuilder.
Definition at line 18736 of file SatParameters.java.
◆ getClauseActivityDecay()
|
inline |
Clause activity parameters (same effect as the one on the variables).
optional double clause_activity_decay = 17 [default = 0.999];
- Returns
- The clauseActivityDecay.
Implements SatParametersOrBuilder.
Definition at line 12012 of file SatParameters.java.
◆ getClauseCleanupLbdBound()
|
inline |
All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.
optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
- Returns
- The clauseCleanupLbdBound.
Implements SatParametersOrBuilder.
Definition at line 11421 of file SatParameters.java.
◆ getClauseCleanupOrdering()
|
inline |
optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];
- Returns
- The clauseCleanupOrdering.
Implements SatParametersOrBuilder.
Definition at line 11469 of file SatParameters.java.
◆ getClauseCleanupPeriod()
|
inline |
Trigger a cleanup when this number of "deletable" clauses is learned.
optional int32 clause_cleanup_period = 11 [default = 10000];
- Returns
- The clauseCleanupPeriod.
Implements SatParametersOrBuilder.
Definition at line 11262 of file SatParameters.java.
◆ getClauseCleanupProtection()
|
inline |
optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];
- Returns
- The clauseCleanupProtection.
Implements SatParametersOrBuilder.
Definition at line 11367 of file SatParameters.java.
◆ getClauseCleanupTarget()
|
inline |
During a cleanup, we will always keep that number of "deletable" clauses. Note that this doesn't include the "protected" clauses.
optional int32 clause_cleanup_target = 13 [default = 10000];
- Returns
- The clauseCleanupTarget.
Implements SatParametersOrBuilder.
Definition at line 11319 of file SatParameters.java.
◆ getCountAssumptionLevelsInLbd()
|
inline |
Whether or not the assumption levels are taken into account during the LBD computation. According to the reference below, not counting them improves the solver in some situation. Note that this only impact solves under assumptions. Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction" Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes in Computer Science Volume 7962, 2013, pp 309-317.
optional bool count_assumption_levels_in_lbd = 49 [default = true];
- Returns
- The countAssumptionLevelsInLbd.
Implements SatParametersOrBuilder.
Definition at line 13563 of file SatParameters.java.
◆ getCoverOptimization()
|
inline |
If true, when the max-sat algo find a core, we compute the minimal number of literals in the core that needs to be true to have a feasible solution.
optional bool cover_optimization = 89 [default = true];
- Returns
- The coverOptimization.
Implements SatParametersOrBuilder.
Definition at line 14920 of file SatParameters.java.
◆ getCpModelMaxNumPresolveOperations()
|
inline |
If positive, try to stop just after that many presolve rules have been applied. This is mainly useful for debugging presolve.
optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];
- Returns
- The cpModelMaxNumPresolveOperations.
Implements SatParametersOrBuilder.
Definition at line 14181 of file SatParameters.java.
◆ getCpModelPostsolveWithFullSolver()
|
inline |
Advanced usage. We have two different postsolve code. The default one should be better and it allows for a more powerful presolve, but some rarely used features like not fully assigning all variables require the other one.
optional bool cp_model_postsolve_with_full_solver = 162 [default = false];
- Returns
- The cpModelPostsolveWithFullSolver.
Implements SatParametersOrBuilder.
Definition at line 14118 of file SatParameters.java.
◆ getCpModelPresolve()
|
inline |
Whether we presolve the cp_model before solving it.
optional bool cp_model_presolve = 86 [default = true];
- Returns
- The cpModelPresolve.
Implements SatParametersOrBuilder.
Definition at line 14057 of file SatParameters.java.
◆ getCpModelProbingLevel()
|
inline |
How much effort do we spend on probing. 0 disables it completely.
optional int32 cp_model_probing_level = 110 [default = 2];
- Returns
- The cpModelProbingLevel.
Implements SatParametersOrBuilder.
Definition at line 14238 of file SatParameters.java.
◆ getCpModelUseSatPresolve()
|
inline |
Whether we also use the sat presolve when cp_model_presolve is true.
optional bool cp_model_use_sat_presolve = 93 [default = true];
- Returns
- The cpModelUseSatPresolve.
Implements SatParametersOrBuilder.
Definition at line 14293 of file SatParameters.java.
◆ getCutActiveCountDecay()
|
inline |
optional double cut_active_count_decay = 156 [default = 0.8];
- Returns
- The cutActiveCountDecay.
Implements SatParametersOrBuilder.
Definition at line 16387 of file SatParameters.java.
◆ getCutCleanupTarget()
|
inline |
Target number of constraints to remove during cleanup.
optional int32 cut_cleanup_target = 157 [default = 1000];
- Returns
- The cutCleanupTarget.
Implements SatParametersOrBuilder.
Definition at line 16434 of file SatParameters.java.
◆ getCutMaxActiveCountValue()
|
inline |
These parameters are similar to sat clause management activity parameters. They are effective only if the number of generated cuts exceed the storage limit. Default values are based on a few experiments on miplib instances.
optional double cut_max_active_count_value = 155 [default = 10000000000];
- Returns
- The cutMaxActiveCountValue.
Implements SatParametersOrBuilder.
Definition at line 16336 of file SatParameters.java.
◆ getDefaultInstanceForType()
|
inline |
Definition at line 9473 of file SatParameters.java.
◆ getDefaultRestartAlgorithms()
|
inline |
optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
- Returns
- The defaultRestartAlgorithms.
Implements SatParametersOrBuilder.
Definition at line 12259 of file SatParameters.java.
◆ getDefaultRestartAlgorithmsBytes()
|
inline |
optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
- Returns
- The bytes for defaultRestartAlgorithms.
Implements SatParametersOrBuilder.
Definition at line 12278 of file SatParameters.java.
◆ getDescriptor()
|
inlinestatic |
Definition at line 9151 of file SatParameters.java.
◆ getDescriptorForType()
|
inline |
Definition at line 9468 of file SatParameters.java.
◆ getDiversifyLnsParams()
|
inline |
If true, registers more lns subsolvers with different parameters.
optional bool diversify_lns_params = 137 [default = false];
- Returns
- The diversifyLnsParams.
Implements SatParametersOrBuilder.
Definition at line 18287 of file SatParameters.java.
◆ getEnumerateAllSolutions()
|
inline |
Whether we enumerate all solutions of a problem without objective. Note that setting this to true automatically disable the presolve. This is because the presolve rules only guarantee the existence of one feasible solution to the presolved problem. TODO(user): Activate the presolve but with just the rules that do not change the set of feasible solutions.
optional bool enumerate_all_solutions = 87 [default = false];
- Returns
- The enumerateAllSolutions.
Implements SatParametersOrBuilder.
Definition at line 17298 of file SatParameters.java.
◆ getExpandAutomatonConstraints()
|
inline |
If true, the automaton constraints are expanded.
optional bool expand_automaton_constraints = 143 [default = true];
- Returns
- The expandAutomatonConstraints.
Implements SatParametersOrBuilder.
Definition at line 14446 of file SatParameters.java.
◆ getExpandElementConstraints()
|
inline |
If true, the element constraints are expanded into many linear constraints of the form (index == i) => (element[i] == target).
optional bool expand_element_constraints = 140 [default = true];
- Returns
- The expandElementConstraints.
Implements SatParametersOrBuilder.
Definition at line 14389 of file SatParameters.java.
◆ getExpandTableConstraints()
|
inline |
If true, the positive table constraints are expanded. Note that currently, negative table constraints are always expanded.
optional bool expand_table_constraints = 158 [default = true];
- Returns
- The expandTableConstraints.
Implements SatParametersOrBuilder.
Definition at line 14503 of file SatParameters.java.
◆ getExploitAllLpSolution()
|
inline |
If true and the Lp relaxation of the problem has a solution, try to exploit it. This is same as above except in this case the lp solution might not be an integer solution.
optional bool exploit_all_lp_solution = 116 [default = true];
- Returns
- The exploitAllLpSolution.
Implements SatParametersOrBuilder.
Definition at line 16721 of file SatParameters.java.
◆ getExploitBestSolution()
|
inline |
When branching on a variable, follow the last best solution value.
optional bool exploit_best_solution = 130 [default = false];
- Returns
- The exploitBestSolution.
Implements SatParametersOrBuilder.
Definition at line 16780 of file SatParameters.java.
◆ getExploitIntegerLpSolution()
|
inline |
If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it. Note that since the LP relaxation may not contain all the constraints, such a solution is not necessarily a solution of the full problem.
optional bool exploit_integer_lp_solution = 94 [default = true];
- Returns
- The exploitIntegerLpSolution.
Implements SatParametersOrBuilder.
Definition at line 16656 of file SatParameters.java.
◆ getExploitObjective()
|
inline |
When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.
optional bool exploit_objective = 131 [default = true];
- Returns
- The exploitObjective.
Implements SatParametersOrBuilder.
Definition at line 16900 of file SatParameters.java.
◆ getExploitRelaxationSolution()
|
inline |
When branching on a variable, follow the last best relaxation solution value. We use the relaxation with the tightest bound on the objective as the best relaxation solution.
optional bool exploit_relaxation_solution = 161 [default = false];
- Returns
- The exploitRelaxationSolution.
Implements SatParametersOrBuilder.
Definition at line 16839 of file SatParameters.java.
◆ getFillTightenedDomainsInResponse()
|
inline |
If true, add information about the derived variable domains to the CpSolverResponse. It is an option because it makes the response slighly bigger and there is a bit more work involved during the postsolve to construct it, but it should still have a low overhead. See the tightened_variables field in CpSolverResponse for more details.
optional bool fill_tightened_domains_in_response = 132 [default = false];
- Returns
- The fillTightenedDomainsInResponse.
Implements SatParametersOrBuilder.
Definition at line 17371 of file SatParameters.java.
◆ getFindMultipleCores()
|
inline |
Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.
optional bool find_multiple_cores = 84 [default = true];
- Returns
- The findMultipleCores.
Implements SatParametersOrBuilder.
Definition at line 14861 of file SatParameters.java.
◆ getGlucoseDecayIncrement()
|
inline |
optional double glucose_decay_increment = 23 [default = 0.01];
- Returns
- The glucoseDecayIncrement.
Implements SatParametersOrBuilder.
Definition at line 11926 of file SatParameters.java.
◆ getGlucoseDecayIncrementPeriod()
|
inline |
optional int32 glucose_decay_increment_period = 24 [default = 5000];
- Returns
- The glucoseDecayIncrementPeriod.
Implements SatParametersOrBuilder.
Definition at line 11965 of file SatParameters.java.
◆ getGlucoseMaxDecay()
|
inline |
The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95. This "hack" seems to work well and comes from: Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013 http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136
optional double glucose_max_decay = 22 [default = 0.95];
- Returns
- The glucoseMaxDecay.
Implements SatParametersOrBuilder.
Definition at line 11873 of file SatParameters.java.
◆ getHintConflictLimit()
|
inline |
When we try to follow the hint, we do a FIXED_SEARCH using the hint until this number of conflict is reached.
optional int32 hint_conflict_limit = 153 [default = 10];
- Returns
- The hintConflictLimit.
Implements SatParametersOrBuilder.
Definition at line 16593 of file SatParameters.java.
◆ getInitialPolarity()
|
inline |
optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];
- Returns
- The initialPolarity.
Implements SatParametersOrBuilder.
Definition at line 10639 of file SatParameters.java.
◆ getInitialVariablesActivity()
|
inline |
The initial value of the variables activity. A non-zero value only make sense when use_erwa_heuristic is true. Experiments with a value of 1e-2 together with the ERWA heuristic showed slighthly better result than simply using zero. The idea is that when the "learning rate" of a variable becomes lower than this value, then we prefer to branch on never explored before variables. This is not in the ERWA paper.
optional double initial_variables_activity = 76 [default = 0];
- Returns
- The initialVariablesActivity.
Implements SatParametersOrBuilder.
Definition at line 10977 of file SatParameters.java.
◆ getInstantiateAllVariables()
|
inline |
If true, the solver will add a default integer branching strategy to the already defined search strategy.
optional bool instantiate_all_variables = 106 [default = true];
- Returns
- The instantiateAllVariables.
Implements SatParametersOrBuilder.
Definition at line 17436 of file SatParameters.java.
◆ getInterleaveBatchSize()
|
inline |
optional int32 interleave_batch_size = 134 [default = 1];
- Returns
- The interleaveBatchSize.
Implements SatParametersOrBuilder.
Definition at line 17812 of file SatParameters.java.
◆ getInterleaveSearch()
|
inline |
Experimental. If this is true, then we interleave all our major search strategy and distribute the work amongst num_search_workers. The search is deterministic (independently of num_search_workers!), and we schedule and wait for interleave_batch_size task to be completed before synchronizing and scheduling the next batch of tasks.
optional bool interleave_search = 136 [default = false];
- Returns
- The interleaveSearch.
Implements SatParametersOrBuilder.
Definition at line 17757 of file SatParameters.java.
◆ getLinearizationLevel()
|
inline |
A non-negative level indicating the type of constraints we consider in the LP relaxation. At level zero, no LP relaxation is used. At level 1, only the linear constraint and full encoding are added. At level 2, we also add all the Boolean constraints.
optional int32 linearization_level = 90 [default = 1];
- Returns
- The linearizationLevel.
Implements SatParametersOrBuilder.
Definition at line 15444 of file SatParameters.java.
◆ getLnsFocusOnDecisionVariables()
|
inline |
optional bool lns_focus_on_decision_variables = 105 [default = false];
- Returns
- The lnsFocusOnDecisionVariables.
Implements SatParametersOrBuilder.
Definition at line 18071 of file SatParameters.java.
◆ getLogSearchProgress()
|
inline |
Whether the solver should log the search progress to LOG(INFO).
optional bool log_search_progress = 41 [default = false];
- Returns
- The logSearchProgress.
Implements SatParametersOrBuilder.
Definition at line 13360 of file SatParameters.java.
◆ getMaxAllDiffCutSize()
|
inline |
Cut generator for all diffs can add too many cuts for large all_diff constraints. This parameter restricts the large all_diff constraints to have a cut generator.
optional int32 max_all_diff_cut_size = 148 [default = 7];
- Returns
- The maxAllDiffCutSize.
Implements SatParametersOrBuilder.
Definition at line 15875 of file SatParameters.java.
◆ getMaxClauseActivityValue()
|
inline |
optional double max_clause_activity_value = 18 [default = 1e+20];
- Returns
- The maxClauseActivityValue.
Implements SatParametersOrBuilder.
Definition at line 12059 of file SatParameters.java.
◆ getMaxConsecutiveInactiveCount()
|
inline |
If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP. Note that it might be added again later if it become violated by the current LP solution.
optional int32 max_consecutive_inactive_count = 121 [default = 100];
- Returns
- The maxConsecutiveInactiveCount.
Implements SatParametersOrBuilder.
Definition at line 16273 of file SatParameters.java.
◆ getMaxCutRoundsAtLevelZero()
|
inline |
Max number of time we perform cut generation and resolve the LP at level 0.
optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];
- Returns
- The maxCutRoundsAtLevelZero.
Implements SatParametersOrBuilder.
Definition at line 16214 of file SatParameters.java.
◆ getMaxDeterministicTime()
|
inline |
Maximum time allowed in deterministic time to solve a problem. The deterministic time should be correlated with the real time used by the solver, the time unit being as close as possible to a second.
optional double max_deterministic_time = 67 [default = inf];
- Returns
- The maxDeterministicTime.
Implements SatParametersOrBuilder.
Definition at line 12891 of file SatParameters.java.
◆ getMaxIntegerRoundingScaling()
|
inline |
In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive). The lower this is, the lower the integer coefficients of the cut will be. Note that cut generated by lower values are not necessarily worse than cut generated by larger value. There is no strict dominance relationship. Setting this to 2 result in the "strong fractional rouding" of Letchford and Lodi.
optional int32 max_integer_rounding_scaling = 119 [default = 600];
- Returns
- The maxIntegerRoundingScaling.
Implements SatParametersOrBuilder.
Definition at line 16009 of file SatParameters.java.
◆ getMaxMemoryInMb()
|
inline |
Maximum memory allowed for the whole thread containing the solver. The solver will abort as soon as it detects that this limit is crossed. As a result, this limit is approximative, but usually the solver will not go too much over.
optional int64 max_memory_in_mb = 40 [default = 10000];
- Returns
- The maxMemoryInMb.
Implements SatParametersOrBuilder.
Definition at line 13031 of file SatParameters.java.
◆ getMaxNumberOfConflicts()
|
inline |
Maximum number of conflicts allowed to solve a problem. TODO(user,user): Maybe change the way the conflict limit is enforced? currently it is enforced on each independent internal SAT solve, rather than on the overall number of conflicts across all solves. So in the context of an optimization problem, this is not really usable directly by a client.
optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];
- Returns
- The maxNumberOfConflicts.
Implements SatParametersOrBuilder.
Definition at line 12960 of file SatParameters.java.
◆ getMaxNumCuts()
|
inline |
The limit on the number of cuts in our cut pool. When this is reached we do not generate cuts anymore. TODO(user): We should probably remove this parameters, and just always generate cuts but only keep the best n or something.
optional int32 max_num_cuts = 91 [default = 10000];
- Returns
- The maxNumCuts.
Implements SatParametersOrBuilder.
Definition at line 15570 of file SatParameters.java.
◆ getMaxPresolveIterations()
|
inline |
In case of large reduction in a presolve iteration, we perform multiple presolve iterations. This parameter controls the maximum number of such presolve iterations.
optional int32 max_presolve_iterations = 138 [default = 3];
- Returns
- The maxPresolveIterations.
Implements SatParametersOrBuilder.
Definition at line 13998 of file SatParameters.java.
◆ getMaxSatAssumptionOrder()
|
inline |
optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];
- Returns
- The maxSatAssumptionOrder.
Implements SatParametersOrBuilder.
Definition at line 14968 of file SatParameters.java.
◆ getMaxSatReverseAssumptionOrder()
|
inline |
If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.
optional bool max_sat_reverse_assumption_order = 52 [default = false];
- Returns
- The maxSatReverseAssumptionOrder.
Implements SatParametersOrBuilder.
Definition at line 15022 of file SatParameters.java.
◆ getMaxSatStratification()
|
inline |
optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];
- Returns
- The maxSatStratification.
Implements SatParametersOrBuilder.
Definition at line 15070 of file SatParameters.java.
◆ getMaxTimeInSeconds()
|
inline |
Maximum time allowed in seconds to solve a problem. The counter will starts at the beginning of the Solve() call.
optional double max_time_in_seconds = 36 [default = inf];
- Returns
- The maxTimeInSeconds.
Implements SatParametersOrBuilder.
Definition at line 12830 of file SatParameters.java.
◆ getMaxVariableActivityValue()
|
inline |
optional double max_variable_activity_value = 16 [default = 1e+100];
- Returns
- The maxVariableActivityValue.
Implements SatParametersOrBuilder.
Definition at line 11820 of file SatParameters.java.
◆ getMergeAtMostOneWorkLimit()
|
inline |
optional double merge_at_most_one_work_limit = 146 [default = 100000000];
- Returns
- The mergeAtMostOneWorkLimit.
Implements SatParametersOrBuilder.
Definition at line 14623 of file SatParameters.java.
◆ getMergeNoOverlapWorkLimit()
|
inline |
During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints. This code can be slow, so we have a limit in place on the number of explored nodes in the underlying graph. The internal limit is an int64, but we use double here to simplify manual input.
optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];
- Returns
- The mergeNoOverlapWorkLimit.
Implements SatParametersOrBuilder.
Definition at line 14568 of file SatParameters.java.
◆ getMinimizationAlgorithm()
|
inline |
optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];
- Returns
- The minimizationAlgorithm.
Implements SatParametersOrBuilder.
Definition at line 11100 of file SatParameters.java.
◆ getMinimizeCore()
|
inline |
Whether we use a simple heuristic to try to minimize an UNSAT core.
optional bool minimize_core = 50 [default = true];
- Returns
- The minimizeCore.
Implements SatParametersOrBuilder.
Definition at line 14804 of file SatParameters.java.
◆ getMinimizeReductionDuringPbResolution()
|
inline |
A different algorithm during PB resolution. It minimizes the number of calls to ReduceCoefficients() which can be time consuming. However, the search space will be different and if the coefficients are large, this may lead to integer overflows that could otherwise be prevented.
optional bool minimize_reduction_during_pb_resolution = 48 [default = false];
- Returns
- The minimizeReductionDuringPbResolution.
Implements SatParametersOrBuilder.
Definition at line 13488 of file SatParameters.java.
◆ getMinimizeWithPropagationNumDecisions()
|
inline |
optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];
- Returns
- The minimizeWithPropagationNumDecisions.
Implements SatParametersOrBuilder.
Definition at line 11702 of file SatParameters.java.
◆ getMinimizeWithPropagationRestartPeriod()
|
inline |
Parameters for an heuristic similar to the one descibed in "An effective learnt clause minimization approach for CDCL Sat Solvers", https://www.ijcai.org/proceedings/2017/0098.pdf For now, we have a somewhat simpler implementation where every x restart we spend y decisions on clause minimization. The minimization technique is the same as the one used to minimize core in max-sat. We also minimize problem clauses and not just the learned clause that we keep forever like in the paper. Changing these parameters or the kind of clause we minimize seems to have a big impact on the overall perf on our benchmarks. So this technique seems definitely useful, but it is hard to tune properly.
optional int32 minimize_with_propagation_restart_period = 96 [default = 10];
- Returns
- The minimizeWithPropagationRestartPeriod.
Implements SatParametersOrBuilder.
Definition at line 11635 of file SatParameters.java.
◆ getMinOrthogonalityForLpConstraints()
|
inline |
While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call. Orthogonality is defined as 1 - cosine(vector angle between constraints). A value of zero disable this feature.
optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];
- Returns
- The minOrthogonalityForLpConstraints.
Implements SatParametersOrBuilder.
Definition at line 16151 of file SatParameters.java.
◆ getMipCheckPrecision()
|
inline |
As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted coefficient precision during scaling. When we cannot, we will report MODEL_INVALID if the relative preicision is larger than this parameter.
optional double mip_check_precision = 128 [default = 0.0001];
- Returns
- The mipCheckPrecision.
Implements SatParametersOrBuilder.
Definition at line 19156 of file SatParameters.java.
◆ getMipMaxActivityExponent()
|
inline |
To avoid integer overflow, we always force the maximum possible constraint activity (and objective value) according to the initial variable domain to be smaller than 2 to this given power. Because of this, we cannot always reach the "mip_wanted_precision" parameter above. This can go as high as 62, but some internal algo currently abort early if they might run into integer overflow, so it is better to keep it a bit lower than this.
optional int32 mip_max_activity_exponent = 127 [default = 53];
- Returns
- The mipMaxActivityExponent.
Implements SatParametersOrBuilder.
Definition at line 19083 of file SatParameters.java.
◆ getMipMaxBound()
|
inline |
We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use. If the MIP model expect larger variable value in the solution, then the converted model will likely not be relevant.
optional double mip_max_bound = 124 [default = 10000000];
- Returns
- The mipMaxBound.
Implements SatParametersOrBuilder.
Definition at line 18862 of file SatParameters.java.
◆ getMipVarScaling()
|
inline |
All continuous variable of the problem will be multiplied by this factor. By default, we don't do any variable scaling and rely on the MIP model to specify continuous variable domain with the wanted precision.
optional double mip_var_scaling = 125 [default = 1];
- Returns
- The mipVarScaling.
Implements SatParametersOrBuilder.
Definition at line 18925 of file SatParameters.java.
◆ getMipWantedPrecision()
|
inline |
When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients. We will choose the lowest power such that we have this relative precision on each of the constraint (resp. objective) coefficient. We also use this to decide by how much we relax the constraint bounds so that we can have a feasible integer solution of constraints involving continuous variable. This is required for instance when you have an == rhs constraint as in many situation you cannot have a perfect equality with integer variables and coefficients.
optional double mip_wanted_precision = 126 [default = 1e-06];
- Returns
- The mipWantedPrecision.
Implements SatParametersOrBuilder.
Definition at line 19000 of file SatParameters.java.
◆ getNewConstraintsBatchSize()
|
inline |
Add that many lazy contraints (or cuts) at once in the LP. Note that at the beginning of the solve, we do add more than this.
optional int32 new_constraints_batch_size = 122 [default = 50];
- Returns
- The newConstraintsBatchSize.
Implements SatParametersOrBuilder.
Definition at line 16491 of file SatParameters.java.
◆ getNumConflictsBeforeStrategyChanges()
|
inline |
After each restart, if the number of conflict since the last strategy change is greater that this, then we increment a "strategy_counter" that can be use to change the search strategy used by the following restarts.
optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];
- Returns
- The numConflictsBeforeStrategyChanges.
Implements SatParametersOrBuilder.
Definition at line 12710 of file SatParameters.java.
◆ getNumSearchWorkers()
|
inline |
Specify the number of parallel workers to use during search. A number <= 1 means no parallelism. As of 2020-04-10, if you're using SAT via MPSolver (to solve integer programs) this field is overridden with a value of 8, if the field is not set *explicitly*. Thus, always set this field explicitly or via MPSolver::SetNumThreads().
optional int32 num_search_workers = 100 [default = 1];
- Returns
- The numSearchWorkers.
Implements SatParametersOrBuilder.
Definition at line 17684 of file SatParameters.java.
◆ getOnlyAddCutsAtLevelZero()
|
inline |
For the cut that can be generated at any level, this control if we only try to generate them at the root node.
optional bool only_add_cuts_at_level_zero = 92 [default = false];
- Returns
- The onlyAddCutsAtLevelZero.
Implements SatParametersOrBuilder.
Definition at line 15633 of file SatParameters.java.
◆ getOptimizeWithCore()
|
inline |
The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one. If this is true, then we use a core-based approach (like in max-SAT) when we try to increase the lower bound instead.
optional bool optimize_with_core = 83 [default = false];
- Returns
- The optimizeWithCore.
Implements SatParametersOrBuilder.
Definition at line 17085 of file SatParameters.java.
◆ getOptimizeWithMaxHs()
|
inline |
This has no effect if optimize_with_core is false. If true, use a different core-based algorithm similar to the max-HS algo for max-SAT. This is a hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT one. This is also related to the PhD work of tobyodavies@ "Automatic Logic-Based Benders Decomposition with MiniZinc" http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489
optional bool optimize_with_max_hs = 85 [default = false];
- Returns
- The optimizeWithMaxHs.
Implements SatParametersOrBuilder.
Definition at line 17223 of file SatParameters.java.
◆ getPbCleanupIncrement()
|
inline |
Same as for the clauses, but for the learned pseudo-Boolean constraints.
optional int32 pb_cleanup_increment = 46 [default = 200];
- Returns
- The pbCleanupIncrement.
Implements SatParametersOrBuilder.
Definition at line 11521 of file SatParameters.java.
◆ getPbCleanupRatio()
|
inline |
optional double pb_cleanup_ratio = 47 [default = 0.5];
- Returns
- The pbCleanupRatio.
Implements SatParametersOrBuilder.
Definition at line 11568 of file SatParameters.java.
◆ getPreferredVariableOrder()
|
inline |
optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
- Returns
- The preferredVariableOrder.
Implements SatParametersOrBuilder.
Definition at line 10596 of file SatParameters.java.
◆ getPresolveBlockedClause()
|
inline |
Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.
optional bool presolve_blocked_clause = 88 [default = true];
- Returns
- The presolveBlockedClause.
Implements SatParametersOrBuilder.
Definition at line 13815 of file SatParameters.java.
◆ getPresolveBvaThreshold()
|
inline |
Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold. The algorithm described in the paper uses 0, but quick experiments showed that 1 is a good value. It may not be worth it to add a new variable just to remove one clause.
optional int32 presolve_bva_threshold = 73 [default = 1];
- Returns
- The presolveBvaThreshold.
Implements SatParametersOrBuilder.
Definition at line 13933 of file SatParameters.java.
◆ getPresolveBveClauseWeight()
|
inline |
During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.
optional int32 presolve_bve_clause_weight = 55 [default = 3];
- Returns
- The presolveBveClauseWeight.
Implements SatParametersOrBuilder.
Definition at line 13697 of file SatParameters.java.
◆ getPresolveBveThreshold()
|
inline |
During presolve, only try to perform the bounded variable elimination (BVE) of a variable x if the number of occurrences of x times the number of occurrences of not(x) is not greater than this parameter.
optional int32 presolve_bve_threshold = 54 [default = 500];
- Returns
- The presolveBveThreshold.
Implements SatParametersOrBuilder.
Definition at line 13636 of file SatParameters.java.
◆ getPresolveProbingDeterministicTimeLimit()
|
inline |
The maximum "deterministic" time limit to spend in probing. A value of zero will disable the probing.
optional double presolve_probing_deterministic_time_limit = 57 [default = 30];
- Returns
- The presolveProbingDeterministicTimeLimit.
Implements SatParametersOrBuilder.
Definition at line 13756 of file SatParameters.java.
◆ getPresolveSubstitutionLevel()
|
inline |
How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve. This currently only concerns variable appearing only in linear constraints. For now the value 0 turns it off and any positive value performs substitution.
optional int32 presolve_substitution_level = 147 [default = 1];
- Returns
- The presolveSubstitutionLevel.
Implements SatParametersOrBuilder.
Definition at line 14676 of file SatParameters.java.
◆ getPresolveUseBva()
|
inline |
Whether or not we use Bounded Variable Addition (BVA) in the presolve.
optional bool presolve_use_bva = 72 [default = true];
- Returns
- The presolveUseBva.
Implements SatParametersOrBuilder.
Definition at line 13872 of file SatParameters.java.
◆ getProbingPeriodAtRoot()
|
inline |
If set at zero (the default), it is disabled. Otherwise the solver attempts probing at every 'probing_period' root node. Period of 1 enables probing at every root node.
optional int64 probing_period_at_root = 142 [default = 0];
- Returns
- The probingPeriodAtRoot.
Implements SatParametersOrBuilder.
Definition at line 16961 of file SatParameters.java.
◆ getPseudoCostReliabilityThreshold()
|
inline |
The solver ignores the pseudo costs of variables with number of recordings less than this threshold.
optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
- Returns
- The pseudoCostReliabilityThreshold.
Implements SatParametersOrBuilder.
Definition at line 17022 of file SatParameters.java.
◆ getRandomBranchesRatio()
|
inline |
A number between 0 and 1 that indicates the proportion of branching variables that are selected randomly instead of choosing the first variable from the given variable_ordering strategy.
optional double random_branches_ratio = 32 [default = 0];
- Returns
- The randomBranchesRatio.
Implements SatParametersOrBuilder.
Definition at line 10845 of file SatParameters.java.
◆ getRandomizeSearch()
|
inline |
Randomize fixed search.
optional bool randomize_search = 103 [default = false];
- Returns
- The randomizeSearch.
Implements SatParametersOrBuilder.
Definition at line 18342 of file SatParameters.java.
◆ getRandomPolarityRatio()
|
inline |
The proportion of polarity chosen at random. Note that this take precedence over the phase saving heuristic. This is different from initial_polarity:POLARITY_RANDOM because it will select a new random polarity each time the variable is branched upon instead of selecting one initially and then always taking this choice.
optional double random_polarity_ratio = 45 [default = 0];
- Returns
- The randomPolarityRatio.
Implements SatParametersOrBuilder.
Definition at line 10778 of file SatParameters.java.
◆ getRandomSeed()
|
inline |
At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed. If you change the random seed, the solver may make different choices during the solving process. For some problems, the running time may vary a lot depending on small change in the solving algorithm. Running the solver with different seeds enables to have more robust benchmarks when evaluating new features.
optional int32 random_seed = 31 [default = 1];
- Returns
- The randomSeed.
Implements SatParametersOrBuilder.
Definition at line 13295 of file SatParameters.java.
◆ getReduceMemoryUsageInInterleaveMode()
|
inline |
Temporary parameter until the memory usage is more optimized.
optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];
- Returns
- The reduceMemoryUsageInInterleaveMode.
Implements SatParametersOrBuilder.
Definition at line 17859 of file SatParameters.java.
◆ getRelativeGapLimit()
|
inline |
optional double relative_gap_limit = 160 [default = 0];
- Returns
- The relativeGapLimit.
Implements SatParametersOrBuilder.
Definition at line 13175 of file SatParameters.java.
◆ getRestartAlgorithms()
|
inline |
The restart strategies will change each time the strategy_counter is increased. The current strategy will simply be the one at index strategy_counter modulo the number of strategy. Note that if this list includes a NO_RESTART, nothing will change when it is reached because the strategy_counter will only increment after a restart. The idea of switching of search strategy tailored for SAT/UNSAT comes from Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/. But more generally, it seems REALLY beneficial to try different strategy.
repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;
- Parameters
-
index The index of the element to return.
- Returns
- The restartAlgorithms at the given index.
Implements SatParametersOrBuilder.
Definition at line 12145 of file SatParameters.java.
◆ getRestartAlgorithmsCount()
|
inline |
The restart strategies will change each time the strategy_counter is increased. The current strategy will simply be the one at index strategy_counter modulo the number of strategy. Note that if this list includes a NO_RESTART, nothing will change when it is reached because the strategy_counter will only increment after a restart. The idea of switching of search strategy tailored for SAT/UNSAT comes from Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/. But more generally, it seems REALLY beneficial to try different strategy.
repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;
- Returns
- The count of restartAlgorithms.
Implements SatParametersOrBuilder.
Definition at line 12126 of file SatParameters.java.
◆ getRestartAlgorithmsList()
|
inline |
The restart strategies will change each time the strategy_counter is increased. The current strategy will simply be the one at index strategy_counter modulo the number of strategy. Note that if this list includes a NO_RESTART, nothing will change when it is reached because the strategy_counter will only increment after a restart. The idea of switching of search strategy tailored for SAT/UNSAT comes from Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/. But more generally, it seems REALLY beneficial to try different strategy.
repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;
- Returns
- A list containing the restartAlgorithms.
Implements SatParametersOrBuilder.
Definition at line 12107 of file SatParameters.java.
◆ getRestartDlAverageRatio()
|
inline |
In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.
optional double restart_dl_average_ratio = 63 [default = 1];
- Returns
- The restartDlAverageRatio.
Implements SatParametersOrBuilder.
Definition at line 12469 of file SatParameters.java.
◆ getRestartLbdAverageRatio()
|
inline |
optional double restart_lbd_average_ratio = 71 [default = 1];
- Returns
- The restartLbdAverageRatio.
Implements SatParametersOrBuilder.
Definition at line 12518 of file SatParameters.java.
◆ getRestartPeriod()
|
inline |
Restart period for the FIXED_RESTART strategy. This is also the multiplier used by the LUBY_RESTART strategy.
optional int32 restart_period = 30 [default = 50];
- Returns
- The restartPeriod.
Implements SatParametersOrBuilder.
Definition at line 12355 of file SatParameters.java.
◆ getRestartRunningWindowSize()
|
inline |
Size of the window for the moving average restarts.
optional int32 restart_running_window_size = 62 [default = 50];
- Returns
- The restartRunningWindowSize.
Implements SatParametersOrBuilder.
Definition at line 12412 of file SatParameters.java.
◆ getSearchBranching()
|
inline |
optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
- Returns
- The searchBranching.
Implements SatParametersOrBuilder.
Definition at line 16539 of file SatParameters.java.
◆ getSearchRandomizationTolerance()
|
inline |
Search randomization will collect equivalent 'max valued' variables, and pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST, all unassigned variables are equivalent. If the variable strategy is CHOOSE_LOWEST_MIN, and `lm` is the current lowest min of all unassigned variables, then the set of max valued variables will be all unassigned variables where lm <= variable min <= lm + search_randomization_tolerance
optional int64 search_randomization_tolerance = 104 [default = 0];
- Returns
- The searchRandomizationTolerance.
Implements SatParametersOrBuilder.
Definition at line 18409 of file SatParameters.java.
◆ getShareLevelZeroBounds()
|
inline |
Allows sharing of the bounds of modified variables at level 0.
optional bool share_level_zero_bounds = 114 [default = true];
- Returns
- The shareLevelZeroBounds.
Implements SatParametersOrBuilder.
Definition at line 17969 of file SatParameters.java.
◆ getShareObjectiveBounds()
|
inline |
Allows objective sharing between workers.
optional bool share_objective_bounds = 113 [default = true];
- Returns
- The shareObjectiveBounds.
Implements SatParametersOrBuilder.
Definition at line 17914 of file SatParameters.java.
◆ getStopAfterFirstSolution()
|
inline |
For an optimization problem, stop the solver as soon as we have a solution.
optional bool stop_after_first_solution = 98 [default = false];
- Returns
- The stopAfterFirstSolution.
Implements SatParametersOrBuilder.
Definition at line 17560 of file SatParameters.java.
◆ getStopAfterPresolve()
|
inline |
Mainly used when improving the presolver. When true, stops the solver after the presolve is complete.
optional bool stop_after_presolve = 149 [default = false];
- Returns
- The stopAfterPresolve.
Implements SatParametersOrBuilder.
Definition at line 17617 of file SatParameters.java.
◆ getStrategyChangeIncreaseRatio()
|
inline |
The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.
optional double strategy_change_increase_ratio = 69 [default = 0];
- Returns
- The strategyChangeIncreaseRatio.
Implements SatParametersOrBuilder.
Definition at line 12771 of file SatParameters.java.
◆ getSubsumptionDuringConflictAnalysis()
|
inline |
At a really low cost, during the 1-UIP conflict computation, it is easy to detect if some of the involved reasons are subsumed by the current conflict. When this is true, such clauses are detached and later removed from the problem.
optional bool subsumption_during_conflict_analysis = 56 [default = true];
- Returns
- The subsumptionDuringConflictAnalysis.
Implements SatParametersOrBuilder.
Definition at line 11201 of file SatParameters.java.
◆ getTreatBinaryClausesSeparately()
|
inline |
If true, the binary clauses are treated separately from the others. This should be faster and uses less memory. However it changes the propagation order.
optional bool treat_binary_clauses_separately = 33 [default = true];
- Returns
- The treatBinaryClausesSeparately.
Implements SatParametersOrBuilder.
Definition at line 13226 of file SatParameters.java.
◆ getUseBlockingRestart()
|
inline |
Block a moving restart algorithm if the trail size of the current conflict is greater than the multiplier times the moving average of the trail size at the previous conflicts.
optional bool use_blocking_restart = 64 [default = false];
- Returns
- The useBlockingRestart.
Implements SatParametersOrBuilder.
Definition at line 12569 of file SatParameters.java.
◆ getUseBranchingInLp()
|
inline |
If true, the solver attemts to generate more info inside lp propagator by branching on some variables if certain criteria are met during the search tree exploration.
optional bool use_branching_in_lp = 139 [default = false];
- Returns
- The useBranchingInLp.
Implements SatParametersOrBuilder.
Definition at line 18610 of file SatParameters.java.
◆ getUseCombinedNoOverlap()
|
inline |
This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem. Like 1000 intervals, but 1M intervals in the no-overlap constraints covering them.
optional bool use_combined_no_overlap = 133 [default = false];
- Returns
- The useCombinedNoOverlap.
Implements SatParametersOrBuilder.
Definition at line 18673 of file SatParameters.java.
◆ getUseDisjunctiveConstraintInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with propagators from the disjunctive constraint to improve the inference on a set of tasks that are disjunctive at the root of the problem. This additional level supplements the default level of reasoning. Propagators of the cumulative constraint will not be used at all if all the tasks are disjunctive at root node. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];
- Returns
- The useDisjunctiveConstraintInCumulativeConstraint.
Implements SatParametersOrBuilder.
Definition at line 15369 of file SatParameters.java.
◆ getUseErwaHeuristic()
|
inline |
Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as described in "Learning Rate Based Branching Heuristic for SAT solvers", J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.
optional bool use_erwa_heuristic = 75 [default = false];
- Returns
- The useErwaHeuristic.
Implements SatParametersOrBuilder.
Definition at line 10908 of file SatParameters.java.
◆ getUseExactLpReason()
|
inline |
The solver usually exploit the LP relaxation of a model. If this option is true, then whatever is infered by the LP will be used like an heuristic to compute EXACT propagation on the IP. So with this option, there is no numerical imprecision issues.
optional bool use_exact_lp_reason = 109 [default = true];
- Returns
- The useExactLpReason.
Implements SatParametersOrBuilder.
Definition at line 18545 of file SatParameters.java.
◆ getUseFeasibilityPump()
|
inline |
Adds a feasibility pump subsolver along with lns subsolvers.
optional bool use_feasibility_pump = 164 [default = false];
- Returns
- The useFeasibilityPump.
Implements SatParametersOrBuilder.
Definition at line 18173 of file SatParameters.java.
◆ getUseImpliedBounds()
|
inline |
Stores and exploits "implied-bounds" in the solver. That is, relations of the form literal => (var >= bound). This is currently used to derive stronger cuts.
optional bool use_implied_bounds = 144 [default = true];
- Returns
- The useImpliedBounds.
Implements SatParametersOrBuilder.
Definition at line 18799 of file SatParameters.java.
◆ getUseLnsOnly()
|
inline |
LNS parameters.
optional bool use_lns_only = 101 [default = false];
- Returns
- The useLnsOnly.
Implements SatParametersOrBuilder.
Definition at line 18024 of file SatParameters.java.
◆ getUseOptimizationHints()
|
inline |
For an optimization problem, whether we follow some hints in order to find a better first solution. For a variable with hint, the solver will always try to follow the hint. It will revert to the variable_branching default otherwise.
optional bool use_optimization_hints = 35 [default = true];
- Returns
- The useOptimizationHints.
Implements SatParametersOrBuilder.
Definition at line 14743 of file SatParameters.java.
◆ getUseOptionalVariables()
|
inline |
If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional. This allows to propagate them as if they were present in some situation.
optional bool use_optional_variables = 108 [default = true];
- Returns
- The useOptionalVariables.
Implements SatParametersOrBuilder.
Definition at line 18480 of file SatParameters.java.
◆ getUseOverloadCheckerInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy. This additional level supplements the default level of reasoning as well as timetable edge finding. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];
- Returns
- The useOverloadCheckerInCumulativeConstraint.
Implements SatParametersOrBuilder.
Definition at line 15215 of file SatParameters.java.
◆ getUsePbResolution()
|
inline |
Whether to use pseudo-Boolean resolution to analyze a conflict. Note that this option only make sense if your problem is modelized using pseudo-Boolean constraints. If you only have clauses, this shouldn't change anything (except slow the solver down).
optional bool use_pb_resolution = 43 [default = false];
- Returns
- The usePbResolution.
Implements SatParametersOrBuilder.
Definition at line 13421 of file SatParameters.java.
◆ getUsePhaseSaving()
|
inline |
If this is true, then the polarity of a variable will be the last value it was assigned to, or its default polarity if it was never assigned since the call to ResetDecisionHeuristic(). This is called 'literal phase saving'. For details see 'A Lightweight Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and A.Darwiche, In 10th International Conference on Theory and Applications of Satisfiability Testing, 2007.
optional bool use_phase_saving = 44 [default = true];
- Returns
- The usePhaseSaving.
Implements SatParametersOrBuilder.
Definition at line 10703 of file SatParameters.java.
◆ getUsePrecedencesInDisjunctiveConstraint()
|
inline |
When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further. For instance if task A and B are both before C and task A and B are in disjunction, then we can deduce that task C must start after duration(A) + duration(B) instead of simply max(duration(A), duration(B)), provided that the start time for all task was currently zero. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];
- Returns
- The usePrecedencesInDisjunctiveConstraint.
Implements SatParametersOrBuilder.
Definition at line 15136 of file SatParameters.java.
◆ getUseRelaxationLns()
|
inline |
Turns on a lns worker which solves relaxed version of the original problem by removing constraints from the problem in order to get better bounds.
optional bool use_relaxation_lns = 150 [default = false];
- Returns
- The useRelaxationLns.
Implements SatParametersOrBuilder.
Definition at line 18230 of file SatParameters.java.
◆ getUseRinsLns()
|
inline |
Turns on relaxation induced neighborhood generator.
optional bool use_rins_lns = 129 [default = true];
- Returns
- The useRinsLns.
Implements SatParametersOrBuilder.
Definition at line 18118 of file SatParameters.java.
◆ getUseSatInprocessing()
|
inline |
optional bool use_sat_inprocessing = 163 [default = false];
- Returns
- The useSatInprocessing.
Implements SatParametersOrBuilder.
Definition at line 14340 of file SatParameters.java.
◆ getUseTimetableEdgeFindingInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with timetable edge finding, i.e., an additional level of reasoning based on the conjunction of energy and mandatory parts. This additional level supplements the default level of reasoning as well as overload_checker. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];
- Returns
- The useTimetableEdgeFindingInCumulativeConstraint.
Implements SatParametersOrBuilder.
Definition at line 15290 of file SatParameters.java.
◆ getVariableActivityDecay()
|
inline |
Each time a conflict is found, the activities of some variables are increased by one. Then, the activity of all variables are multiplied by variable_activity_decay. To implement this efficiently, the activity of all the variables is not decayed at each conflict. Instead, the activity increment is multiplied by 1 / decay. When an activity reach max_variable_activity_value, all the activity are multiplied by 1 / max_variable_activity_value.
optional double variable_activity_decay = 15 [default = 0.8];
- Returns
- The variableActivityDecay.
Implements SatParametersOrBuilder.
Definition at line 11761 of file SatParameters.java.
◆ hasAbsoluteGapLimit()
|
inline |
Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit. The exact definition is:
- Absolute: abs(O - B)
- Relative: abs(O - B) / max(1, abs(O)). Important: The relative gap depends on the objective offset! If you artificially shift the objective, you will get widely different value of the relative gap. Note that if the gap is reached, the search status will be OPTIMAL. But one can check the best objective bound to see the actual gap.
optional double absolute_gap_limit = 159 [default = 0];
- Returns
- Whether the absoluteGapLimit field is set.
Implements SatParametersOrBuilder.
Definition at line 13089 of file SatParameters.java.
◆ hasAddCgCuts()
|
inline |
Whether we generate and add Chvatal-Gomory cuts to the LP at root node. Note that for now, this is not heavily tunned.
optional bool add_cg_cuts = 117 [default = true];
- Returns
- Whether the addCgCuts field is set.
Implements SatParametersOrBuilder.
Definition at line 15742 of file SatParameters.java.
◆ hasAddKnapsackCuts()
|
inline |
Whether we generate knapsack cuts. Note that in our setting where all variables are integer and bounded on both side, such a cut could be applied to any constraint.
optional bool add_knapsack_cuts = 111 [default = false];
- Returns
- Whether the addKnapsackCuts field is set.
Implements SatParametersOrBuilder.
Definition at line 15680 of file SatParameters.java.
◆ hasAddLinMaxCuts()
|
inline |
For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)
optional bool add_lin_max_cuts = 152 [default = true];
- Returns
- Whether the addLinMaxCuts field is set.
Implements SatParametersOrBuilder.
Definition at line 15924 of file SatParameters.java.
◆ hasAddLpConstraintsLazily()
|
inline |
If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch. A constraint that is only added like this is known as a "lazy" constraint in the literature, except that we currently consider all constraints as lazy here.
optional bool add_lp_constraints_lazily = 112 [default = true];
- Returns
- Whether the addLpConstraintsLazily field is set.
Implements SatParametersOrBuilder.
Definition at line 16067 of file SatParameters.java.
◆ hasAddMirCuts()
|
inline |
Whether we generate MIR cuts at root node. Note that for now, this is not heavily tunned.
optional bool add_mir_cuts = 120 [default = true];
- Returns
- Whether the addMirCuts field is set.
Implements SatParametersOrBuilder.
Definition at line 15801 of file SatParameters.java.
◆ hasAlsoBumpVariablesInConflictReasons()
|
inline |
When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped. This is addition to the variables in the conflict, and the one that were used during conflict resolution.
optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];
- Returns
- Whether the alsoBumpVariablesInConflictReasons field is set.
Implements SatParametersOrBuilder.
Definition at line 11033 of file SatParameters.java.
◆ hasAutoDetectGreaterThanAtLeastOneOf()
|
inline |
If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present. This is usually useful to have but can be slow on model with a lot of precedence.
optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];
- Returns
- Whether the autoDetectGreaterThanAtLeastOneOf field is set.
Implements SatParametersOrBuilder.
Definition at line 17484 of file SatParameters.java.
◆ hasBinaryMinimizationAlgorithm()
|
inline |
optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];
- Returns
- Whether the binaryMinimizationAlgorithm field is set.
Implements SatParametersOrBuilder.
Definition at line 11135 of file SatParameters.java.
◆ hasBinarySearchNumConflicts()
|
inline |
If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict. This can quickly reduce the objective domain on some problems.
optional int32 binary_search_num_conflicts = 99 [default = -1];
- Returns
- Whether the binarySearchNumConflicts field is set.
Implements SatParametersOrBuilder.
Definition at line 17137 of file SatParameters.java.
◆ hasBlockingRestartMultiplier()
|
inline |
optional double blocking_restart_multiplier = 66 [default = 1.4];
- Returns
- Whether the blockingRestartMultiplier field is set.
Implements SatParametersOrBuilder.
Definition at line 12651 of file SatParameters.java.
◆ hasBlockingRestartWindowSize()
|
inline |
optional int32 blocking_restart_window_size = 65 [default = 5000];
- Returns
- Whether the blockingRestartWindowSize field is set.
Implements SatParametersOrBuilder.
Definition at line 12612 of file SatParameters.java.
◆ hasBooleanEncodingLevel()
|
inline |
A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.
optional int32 boolean_encoding_level = 107 [default = 1];
- Returns
- Whether the booleanEncodingLevel field is set.
Implements SatParametersOrBuilder.
Definition at line 15494 of file SatParameters.java.
◆ hasCatchSigintSignal()
|
inline |
Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve. If set, catching the SIGINT signal will terminate the search gracefully, as if a time limit was reached.
optional bool catch_sigint_signal = 135 [default = true];
- Returns
- Whether the catchSigintSignal field is set.
Implements SatParametersOrBuilder.
Definition at line 18722 of file SatParameters.java.
◆ hasClauseActivityDecay()
|
inline |
Clause activity parameters (same effect as the one on the variables).
optional double clause_activity_decay = 17 [default = 0.999];
- Returns
- Whether the clauseActivityDecay field is set.
Implements SatParametersOrBuilder.
Definition at line 12000 of file SatParameters.java.
◆ hasClauseCleanupLbdBound()
|
inline |
All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.
optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
- Returns
- Whether the clauseCleanupLbdBound field is set.
Implements SatParametersOrBuilder.
Definition at line 11408 of file SatParameters.java.
◆ hasClauseCleanupOrdering()
|
inline |
optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];
- Returns
- Whether the clauseCleanupOrdering field is set.
Implements SatParametersOrBuilder.
Definition at line 11461 of file SatParameters.java.
◆ hasClauseCleanupPeriod()
|
inline |
Trigger a cleanup when this number of "deletable" clauses is learned.
optional int32 clause_cleanup_period = 11 [default = 10000];
- Returns
- Whether the clauseCleanupPeriod field is set.
Implements SatParametersOrBuilder.
Definition at line 11250 of file SatParameters.java.
◆ hasClauseCleanupProtection()
|
inline |
optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];
- Returns
- Whether the clauseCleanupProtection field is set.
Implements SatParametersOrBuilder.
Definition at line 11359 of file SatParameters.java.
◆ hasClauseCleanupTarget()
|
inline |
During a cleanup, we will always keep that number of "deletable" clauses. Note that this doesn't include the "protected" clauses.
optional int32 clause_cleanup_target = 13 [default = 10000];
- Returns
- Whether the clauseCleanupTarget field is set.
Implements SatParametersOrBuilder.
Definition at line 11306 of file SatParameters.java.
◆ hasCountAssumptionLevelsInLbd()
|
inline |
Whether or not the assumption levels are taken into account during the LBD computation. According to the reference below, not counting them improves the solver in some situation. Note that this only impact solves under assumptions. Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction" Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes in Computer Science Volume 7962, 2013, pp 309-317.
optional bool count_assumption_levels_in_lbd = 49 [default = true];
- Returns
- Whether the countAssumptionLevelsInLbd field is set.
Implements SatParametersOrBuilder.
Definition at line 13544 of file SatParameters.java.
◆ hasCoverOptimization()
|
inline |
If true, when the max-sat algo find a core, we compute the minimal number of literals in the core that needs to be true to have a feasible solution.
optional bool cover_optimization = 89 [default = true];
- Returns
- Whether the coverOptimization field is set.
Implements SatParametersOrBuilder.
Definition at line 14907 of file SatParameters.java.
◆ hasCpModelMaxNumPresolveOperations()
|
inline |
If positive, try to stop just after that many presolve rules have been applied. This is mainly useful for debugging presolve.
optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];
- Returns
- Whether the cpModelMaxNumPresolveOperations field is set.
Implements SatParametersOrBuilder.
Definition at line 14168 of file SatParameters.java.
◆ hasCpModelPostsolveWithFullSolver()
|
inline |
Advanced usage. We have two different postsolve code. The default one should be better and it allows for a more powerful presolve, but some rarely used features like not fully assigning all variables require the other one.
optional bool cp_model_postsolve_with_full_solver = 162 [default = false];
- Returns
- Whether the cpModelPostsolveWithFullSolver field is set.
Implements SatParametersOrBuilder.
Definition at line 14103 of file SatParameters.java.
◆ hasCpModelPresolve()
|
inline |
Whether we presolve the cp_model before solving it.
optional bool cp_model_presolve = 86 [default = true];
- Returns
- Whether the cpModelPresolve field is set.
Implements SatParametersOrBuilder.
Definition at line 14045 of file SatParameters.java.
◆ hasCpModelProbingLevel()
|
inline |
How much effort do we spend on probing. 0 disables it completely.
optional int32 cp_model_probing_level = 110 [default = 2];
- Returns
- Whether the cpModelProbingLevel field is set.
Implements SatParametersOrBuilder.
Definition at line 14226 of file SatParameters.java.
◆ hasCpModelUseSatPresolve()
|
inline |
Whether we also use the sat presolve when cp_model_presolve is true.
optional bool cp_model_use_sat_presolve = 93 [default = true];
- Returns
- Whether the cpModelUseSatPresolve field is set.
Implements SatParametersOrBuilder.
Definition at line 14281 of file SatParameters.java.
◆ hasCutActiveCountDecay()
|
inline |
optional double cut_active_count_decay = 156 [default = 0.8];
- Returns
- Whether the cutActiveCountDecay field is set.
Implements SatParametersOrBuilder.
Definition at line 16379 of file SatParameters.java.
◆ hasCutCleanupTarget()
|
inline |
Target number of constraints to remove during cleanup.
optional int32 cut_cleanup_target = 157 [default = 1000];
- Returns
- Whether the cutCleanupTarget field is set.
Implements SatParametersOrBuilder.
Definition at line 16422 of file SatParameters.java.
◆ hasCutMaxActiveCountValue()
|
inline |
These parameters are similar to sat clause management activity parameters. They are effective only if the number of generated cuts exceed the storage limit. Default values are based on a few experiments on miplib instances.
optional double cut_max_active_count_value = 155 [default = 10000000000];
- Returns
- Whether the cutMaxActiveCountValue field is set.
Implements SatParametersOrBuilder.
Definition at line 16322 of file SatParameters.java.
◆ hasDefaultRestartAlgorithms()
|
inline |
optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
- Returns
- Whether the defaultRestartAlgorithms field is set.
Implements SatParametersOrBuilder.
Definition at line 12252 of file SatParameters.java.
◆ hasDiversifyLnsParams()
|
inline |
If true, registers more lns subsolvers with different parameters.
optional bool diversify_lns_params = 137 [default = false];
- Returns
- Whether the diversifyLnsParams field is set.
Implements SatParametersOrBuilder.
Definition at line 18275 of file SatParameters.java.
◆ hasEnumerateAllSolutions()
|
inline |
Whether we enumerate all solutions of a problem without objective. Note that setting this to true automatically disable the presolve. This is because the presolve rules only guarantee the existence of one feasible solution to the presolved problem. TODO(user): Activate the presolve but with just the rules that do not change the set of feasible solutions.
optional bool enumerate_all_solutions = 87 [default = false];
- Returns
- Whether the enumerateAllSolutions field is set.
Implements SatParametersOrBuilder.
Definition at line 17281 of file SatParameters.java.
◆ hasExpandAutomatonConstraints()
|
inline |
If true, the automaton constraints are expanded.
optional bool expand_automaton_constraints = 143 [default = true];
- Returns
- Whether the expandAutomatonConstraints field is set.
Implements SatParametersOrBuilder.
Definition at line 14434 of file SatParameters.java.
◆ hasExpandElementConstraints()
|
inline |
If true, the element constraints are expanded into many linear constraints of the form (index == i) => (element[i] == target).
optional bool expand_element_constraints = 140 [default = true];
- Returns
- Whether the expandElementConstraints field is set.
Implements SatParametersOrBuilder.
Definition at line 14376 of file SatParameters.java.
◆ hasExpandTableConstraints()
|
inline |
If true, the positive table constraints are expanded. Note that currently, negative table constraints are always expanded.
optional bool expand_table_constraints = 158 [default = true];
- Returns
- Whether the expandTableConstraints field is set.
Implements SatParametersOrBuilder.
Definition at line 14490 of file SatParameters.java.
◆ hasExploitAllLpSolution()
|
inline |
If true and the Lp relaxation of the problem has a solution, try to exploit it. This is same as above except in this case the lp solution might not be an integer solution.
optional bool exploit_all_lp_solution = 116 [default = true];
- Returns
- Whether the exploitAllLpSolution field is set.
Implements SatParametersOrBuilder.
Definition at line 16707 of file SatParameters.java.
◆ hasExploitBestSolution()
|
inline |
When branching on a variable, follow the last best solution value.
optional bool exploit_best_solution = 130 [default = false];
- Returns
- Whether the exploitBestSolution field is set.
Implements SatParametersOrBuilder.
Definition at line 16768 of file SatParameters.java.
◆ hasExploitIntegerLpSolution()
|
inline |
If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it. Note that since the LP relaxation may not contain all the constraints, such a solution is not necessarily a solution of the full problem.
optional bool exploit_integer_lp_solution = 94 [default = true];
- Returns
- Whether the exploitIntegerLpSolution field is set.
Implements SatParametersOrBuilder.
Definition at line 16641 of file SatParameters.java.
◆ hasExploitObjective()
|
inline |
When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.
optional bool exploit_objective = 131 [default = true];
- Returns
- Whether the exploitObjective field is set.
Implements SatParametersOrBuilder.
Definition at line 16887 of file SatParameters.java.
◆ hasExploitRelaxationSolution()
|
inline |
When branching on a variable, follow the last best relaxation solution value. We use the relaxation with the tightest bound on the objective as the best relaxation solution.
optional bool exploit_relaxation_solution = 161 [default = false];
- Returns
- Whether the exploitRelaxationSolution field is set.
Implements SatParametersOrBuilder.
Definition at line 16825 of file SatParameters.java.
◆ hasFillTightenedDomainsInResponse()
|
inline |
If true, add information about the derived variable domains to the CpSolverResponse. It is an option because it makes the response slighly bigger and there is a bit more work involved during the postsolve to construct it, but it should still have a low overhead. See the tightened_variables field in CpSolverResponse for more details.
optional bool fill_tightened_domains_in_response = 132 [default = false];
- Returns
- Whether the fillTightenedDomainsInResponse field is set.
Implements SatParametersOrBuilder.
Definition at line 17355 of file SatParameters.java.
◆ hasFindMultipleCores()
|
inline |
Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.
optional bool find_multiple_cores = 84 [default = true];
- Returns
- Whether the findMultipleCores field is set.
Implements SatParametersOrBuilder.
Definition at line 14848 of file SatParameters.java.
◆ hasGlucoseDecayIncrement()
|
inline |
optional double glucose_decay_increment = 23 [default = 0.01];
- Returns
- Whether the glucoseDecayIncrement field is set.
Implements SatParametersOrBuilder.
Definition at line 11918 of file SatParameters.java.
◆ hasGlucoseDecayIncrementPeriod()
|
inline |
optional int32 glucose_decay_increment_period = 24 [default = 5000];
- Returns
- Whether the glucoseDecayIncrementPeriod field is set.
Implements SatParametersOrBuilder.
Definition at line 11957 of file SatParameters.java.
◆ hasGlucoseMaxDecay()
|
inline |
The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95. This "hack" seems to work well and comes from: Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013 http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136
optional double glucose_max_decay = 22 [default = 0.95];
- Returns
- Whether the glucoseMaxDecay field is set.
Implements SatParametersOrBuilder.
Definition at line 11858 of file SatParameters.java.
◆ hasHintConflictLimit()
|
inline |
When we try to follow the hint, we do a FIXED_SEARCH using the hint until this number of conflict is reached.
optional int32 hint_conflict_limit = 153 [default = 10];
- Returns
- Whether the hintConflictLimit field is set.
Implements SatParametersOrBuilder.
Definition at line 16580 of file SatParameters.java.
◆ hasInitialPolarity()
|
inline |
optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];
- Returns
- Whether the initialPolarity field is set.
Implements SatParametersOrBuilder.
Definition at line 10631 of file SatParameters.java.
◆ hasInitialVariablesActivity()
|
inline |
The initial value of the variables activity. A non-zero value only make sense when use_erwa_heuristic is true. Experiments with a value of 1e-2 together with the ERWA heuristic showed slighthly better result than simply using zero. The idea is that when the "learning rate" of a variable becomes lower than this value, then we prefer to branch on never explored before variables. This is not in the ERWA paper.
optional double initial_variables_activity = 76 [default = 0];
- Returns
- Whether the initialVariablesActivity field is set.
Implements SatParametersOrBuilder.
Definition at line 10960 of file SatParameters.java.
◆ hasInstantiateAllVariables()
|
inline |
If true, the solver will add a default integer branching strategy to the already defined search strategy.
optional bool instantiate_all_variables = 106 [default = true];
- Returns
- Whether the instantiateAllVariables field is set.
Implements SatParametersOrBuilder.
Definition at line 17423 of file SatParameters.java.
◆ hasInterleaveBatchSize()
|
inline |
optional int32 interleave_batch_size = 134 [default = 1];
- Returns
- Whether the interleaveBatchSize field is set.
Implements SatParametersOrBuilder.
Definition at line 17804 of file SatParameters.java.
◆ hasInterleaveSearch()
|
inline |
Experimental. If this is true, then we interleave all our major search strategy and distribute the work amongst num_search_workers. The search is deterministic (independently of num_search_workers!), and we schedule and wait for interleave_batch_size task to be completed before synchronizing and scheduling the next batch of tasks.
optional bool interleave_search = 136 [default = false];
- Returns
- Whether the interleaveSearch field is set.
Implements SatParametersOrBuilder.
Definition at line 17741 of file SatParameters.java.
◆ hasLinearizationLevel()
|
inline |
A non-negative level indicating the type of constraints we consider in the LP relaxation. At level zero, no LP relaxation is used. At level 1, only the linear constraint and full encoding are added. At level 2, we also add all the Boolean constraints.
optional int32 linearization_level = 90 [default = 1];
- Returns
- Whether the linearizationLevel field is set.
Implements SatParametersOrBuilder.
Definition at line 15429 of file SatParameters.java.
◆ hasLnsFocusOnDecisionVariables()
|
inline |
optional bool lns_focus_on_decision_variables = 105 [default = false];
- Returns
- Whether the lnsFocusOnDecisionVariables field is set.
Implements SatParametersOrBuilder.
Definition at line 18063 of file SatParameters.java.
◆ hasLogSearchProgress()
|
inline |
Whether the solver should log the search progress to LOG(INFO).
optional bool log_search_progress = 41 [default = false];
- Returns
- Whether the logSearchProgress field is set.
Implements SatParametersOrBuilder.
Definition at line 13348 of file SatParameters.java.
◆ hasMaxAllDiffCutSize()
|
inline |
Cut generator for all diffs can add too many cuts for large all_diff constraints. This parameter restricts the large all_diff constraints to have a cut generator.
optional int32 max_all_diff_cut_size = 148 [default = 7];
- Returns
- Whether the maxAllDiffCutSize field is set.
Implements SatParametersOrBuilder.
Definition at line 15861 of file SatParameters.java.
◆ hasMaxClauseActivityValue()
|
inline |
optional double max_clause_activity_value = 18 [default = 1e+20];
- Returns
- Whether the maxClauseActivityValue field is set.
Implements SatParametersOrBuilder.
Definition at line 12051 of file SatParameters.java.
◆ hasMaxConsecutiveInactiveCount()
|
inline |
If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP. Note that it might be added again later if it become violated by the current LP solution.
optional int32 max_consecutive_inactive_count = 121 [default = 100];
- Returns
- Whether the maxConsecutiveInactiveCount field is set.
Implements SatParametersOrBuilder.
Definition at line 16259 of file SatParameters.java.
◆ hasMaxCutRoundsAtLevelZero()
|
inline |
Max number of time we perform cut generation and resolve the LP at level 0.
optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];
- Returns
- Whether the maxCutRoundsAtLevelZero field is set.
Implements SatParametersOrBuilder.
Definition at line 16202 of file SatParameters.java.
◆ hasMaxDeterministicTime()
|
inline |
Maximum time allowed in deterministic time to solve a problem. The deterministic time should be correlated with the real time used by the solver, the time unit being as close as possible to a second.
optional double max_deterministic_time = 67 [default = inf];
- Returns
- Whether the maxDeterministicTime field is set.
Implements SatParametersOrBuilder.
Definition at line 12877 of file SatParameters.java.
◆ hasMaxIntegerRoundingScaling()
|
inline |
In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive). The lower this is, the lower the integer coefficients of the cut will be. Note that cut generated by lower values are not necessarily worse than cut generated by larger value. There is no strict dominance relationship. Setting this to 2 result in the "strong fractional rouding" of Letchford and Lodi.
optional int32 max_integer_rounding_scaling = 119 [default = 600];
- Returns
- Whether the maxIntegerRoundingScaling field is set.
Implements SatParametersOrBuilder.
Definition at line 15991 of file SatParameters.java.
◆ hasMaxMemoryInMb()
|
inline |
Maximum memory allowed for the whole thread containing the solver. The solver will abort as soon as it detects that this limit is crossed. As a result, this limit is approximative, but usually the solver will not go too much over.
optional int64 max_memory_in_mb = 40 [default = 10000];
- Returns
- Whether the maxMemoryInMb field is set.
Implements SatParametersOrBuilder.
Definition at line 13016 of file SatParameters.java.
◆ hasMaxNumberOfConflicts()
|
inline |
Maximum number of conflicts allowed to solve a problem. TODO(user,user): Maybe change the way the conflict limit is enforced? currently it is enforced on each independent internal SAT solve, rather than on the overall number of conflicts across all solves. So in the context of an optimization problem, this is not really usable directly by a client.
optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];
- Returns
- Whether the maxNumberOfConflicts field is set.
Implements SatParametersOrBuilder.
Definition at line 12943 of file SatParameters.java.
◆ hasMaxNumCuts()
|
inline |
The limit on the number of cuts in our cut pool. When this is reached we do not generate cuts anymore. TODO(user): We should probably remove this parameters, and just always generate cuts but only keep the best n or something.
optional int32 max_num_cuts = 91 [default = 10000];
- Returns
- Whether the maxNumCuts field is set.
Implements SatParametersOrBuilder.
Definition at line 15555 of file SatParameters.java.
◆ hasMaxPresolveIterations()
|
inline |
In case of large reduction in a presolve iteration, we perform multiple presolve iterations. This parameter controls the maximum number of such presolve iterations.
optional int32 max_presolve_iterations = 138 [default = 3];
- Returns
- Whether the maxPresolveIterations field is set.
Implements SatParametersOrBuilder.
Definition at line 13984 of file SatParameters.java.
◆ hasMaxSatAssumptionOrder()
|
inline |
optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];
- Returns
- Whether the maxSatAssumptionOrder field is set.
Implements SatParametersOrBuilder.
Definition at line 14960 of file SatParameters.java.
◆ hasMaxSatReverseAssumptionOrder()
|
inline |
If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.
optional bool max_sat_reverse_assumption_order = 52 [default = false];
- Returns
- Whether the maxSatReverseAssumptionOrder field is set.
Implements SatParametersOrBuilder.
Definition at line 15009 of file SatParameters.java.
◆ hasMaxSatStratification()
|
inline |
optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];
- Returns
- Whether the maxSatStratification field is set.
Implements SatParametersOrBuilder.
Definition at line 15062 of file SatParameters.java.
◆ hasMaxTimeInSeconds()
|
inline |
Maximum time allowed in seconds to solve a problem. The counter will starts at the beginning of the Solve() call.
optional double max_time_in_seconds = 36 [default = inf];
- Returns
- Whether the maxTimeInSeconds field is set.
Implements SatParametersOrBuilder.
Definition at line 12817 of file SatParameters.java.
◆ hasMaxVariableActivityValue()
|
inline |
optional double max_variable_activity_value = 16 [default = 1e+100];
- Returns
- Whether the maxVariableActivityValue field is set.
Implements SatParametersOrBuilder.
Definition at line 11812 of file SatParameters.java.
◆ hasMergeAtMostOneWorkLimit()
|
inline |
optional double merge_at_most_one_work_limit = 146 [default = 100000000];
- Returns
- Whether the mergeAtMostOneWorkLimit field is set.
Implements SatParametersOrBuilder.
Definition at line 14615 of file SatParameters.java.
◆ hasMergeNoOverlapWorkLimit()
|
inline |
During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints. This code can be slow, so we have a limit in place on the number of explored nodes in the underlying graph. The internal limit is an int64, but we use double here to simplify manual input.
optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];
- Returns
- Whether the mergeNoOverlapWorkLimit field is set.
Implements SatParametersOrBuilder.
Definition at line 14552 of file SatParameters.java.
◆ hasMinimizationAlgorithm()
|
inline |
optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];
- Returns
- Whether the minimizationAlgorithm field is set.
Implements SatParametersOrBuilder.
Definition at line 11092 of file SatParameters.java.
◆ hasMinimizeCore()
|
inline |
Whether we use a simple heuristic to try to minimize an UNSAT core.
optional bool minimize_core = 50 [default = true];
- Returns
- Whether the minimizeCore field is set.
Implements SatParametersOrBuilder.
Definition at line 14792 of file SatParameters.java.
◆ hasMinimizeReductionDuringPbResolution()
|
inline |
A different algorithm during PB resolution. It minimizes the number of calls to ReduceCoefficients() which can be time consuming. However, the search space will be different and if the coefficients are large, this may lead to integer overflows that could otherwise be prevented.
optional bool minimize_reduction_during_pb_resolution = 48 [default = false];
- Returns
- Whether the minimizeReductionDuringPbResolution field is set.
Implements SatParametersOrBuilder.
Definition at line 13473 of file SatParameters.java.
◆ hasMinimizeWithPropagationNumDecisions()
|
inline |
optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];
- Returns
- Whether the minimizeWithPropagationNumDecisions field is set.
Implements SatParametersOrBuilder.
Definition at line 11694 of file SatParameters.java.
◆ hasMinimizeWithPropagationRestartPeriod()
|
inline |
Parameters for an heuristic similar to the one descibed in "An effective learnt clause minimization approach for CDCL Sat Solvers", https://www.ijcai.org/proceedings/2017/0098.pdf For now, we have a somewhat simpler implementation where every x restart we spend y decisions on clause minimization. The minimization technique is the same as the one used to minimize core in max-sat. We also minimize problem clauses and not just the learned clause that we keep forever like in the paper. Changing these parameters or the kind of clause we minimize seems to have a big impact on the overall perf on our benchmarks. So this technique seems definitely useful, but it is hard to tune properly.
optional int32 minimize_with_propagation_restart_period = 96 [default = 10];
- Returns
- Whether the minimizeWithPropagationRestartPeriod field is set.
Implements SatParametersOrBuilder.
Definition at line 11613 of file SatParameters.java.
◆ hasMinOrthogonalityForLpConstraints()
|
inline |
While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call. Orthogonality is defined as 1 - cosine(vector angle between constraints). A value of zero disable this feature.
optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];
- Returns
- Whether the minOrthogonalityForLpConstraints field is set.
Implements SatParametersOrBuilder.
Definition at line 16135 of file SatParameters.java.
◆ hasMipCheckPrecision()
|
inline |
As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted coefficient precision during scaling. When we cannot, we will report MODEL_INVALID if the relative preicision is larger than this parameter.
optional double mip_check_precision = 128 [default = 0.0001];
- Returns
- Whether the mipCheckPrecision field is set.
Implements SatParametersOrBuilder.
Definition at line 19141 of file SatParameters.java.
◆ hasMipMaxActivityExponent()
|
inline |
To avoid integer overflow, we always force the maximum possible constraint activity (and objective value) according to the initial variable domain to be smaller than 2 to this given power. Because of this, we cannot always reach the "mip_wanted_precision" parameter above. This can go as high as 62, but some internal algo currently abort early if they might run into integer overflow, so it is better to keep it a bit lower than this.
optional int32 mip_max_activity_exponent = 127 [default = 53];
- Returns
- Whether the mipMaxActivityExponent field is set.
Implements SatParametersOrBuilder.
Definition at line 19065 of file SatParameters.java.
◆ hasMipMaxBound()
|
inline |
We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use. If the MIP model expect larger variable value in the solution, then the converted model will likely not be relevant.
optional double mip_max_bound = 124 [default = 10000000];
- Returns
- Whether the mipMaxBound field is set.
Implements SatParametersOrBuilder.
Definition at line 18848 of file SatParameters.java.
◆ hasMipVarScaling()
|
inline |
All continuous variable of the problem will be multiplied by this factor. By default, we don't do any variable scaling and rely on the MIP model to specify continuous variable domain with the wanted precision.
optional double mip_var_scaling = 125 [default = 1];
- Returns
- Whether the mipVarScaling field is set.
Implements SatParametersOrBuilder.
Definition at line 18911 of file SatParameters.java.
◆ hasMipWantedPrecision()
|
inline |
When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients. We will choose the lowest power such that we have this relative precision on each of the constraint (resp. objective) coefficient. We also use this to decide by how much we relax the constraint bounds so that we can have a feasible integer solution of constraints involving continuous variable. This is required for instance when you have an == rhs constraint as in many situation you cannot have a perfect equality with integer variables and coefficients.
optional double mip_wanted_precision = 126 [default = 1e-06];
- Returns
- Whether the mipWantedPrecision field is set.
Implements SatParametersOrBuilder.
Definition at line 18980 of file SatParameters.java.
◆ hasNewConstraintsBatchSize()
|
inline |
Add that many lazy contraints (or cuts) at once in the LP. Note that at the beginning of the solve, we do add more than this.
optional int32 new_constraints_batch_size = 122 [default = 50];
- Returns
- Whether the newConstraintsBatchSize field is set.
Implements SatParametersOrBuilder.
Definition at line 16478 of file SatParameters.java.
◆ hasNumConflictsBeforeStrategyChanges()
|
inline |
After each restart, if the number of conflict since the last strategy change is greater that this, then we increment a "strategy_counter" that can be use to change the search strategy used by the following restarts.
optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];
- Returns
- Whether the numConflictsBeforeStrategyChanges field is set.
Implements SatParametersOrBuilder.
Definition at line 12696 of file SatParameters.java.
◆ hasNumSearchWorkers()
|
inline |
Specify the number of parallel workers to use during search. A number <= 1 means no parallelism. As of 2020-04-10, if you're using SAT via MPSolver (to solve integer programs) this field is overridden with a value of 8, if the field is not set *explicitly*. Thus, always set this field explicitly or via MPSolver::SetNumThreads().
optional int32 num_search_workers = 100 [default = 1];
- Returns
- Whether the numSearchWorkers field is set.
Implements SatParametersOrBuilder.
Definition at line 17667 of file SatParameters.java.
◆ hasOnlyAddCutsAtLevelZero()
|
inline |
For the cut that can be generated at any level, this control if we only try to generate them at the root node.
optional bool only_add_cuts_at_level_zero = 92 [default = false];
- Returns
- Whether the onlyAddCutsAtLevelZero field is set.
Implements SatParametersOrBuilder.
Definition at line 15620 of file SatParameters.java.
◆ hasOptimizeWithCore()
|
inline |
The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one. If this is true, then we use a core-based approach (like in max-SAT) when we try to increase the lower bound instead.
optional bool optimize_with_core = 83 [default = false];
- Returns
- Whether the optimizeWithCore field is set.
Implements SatParametersOrBuilder.
Definition at line 17070 of file SatParameters.java.
◆ hasOptimizeWithMaxHs()
|
inline |
This has no effect if optimize_with_core is false. If true, use a different core-based algorithm similar to the max-HS algo for max-SAT. This is a hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT one. This is also related to the PhD work of tobyodavies@ "Automatic Logic-Based Benders Decomposition with MiniZinc" http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489
optional bool optimize_with_max_hs = 85 [default = false];
- Returns
- Whether the optimizeWithMaxHs field is set.
Implements SatParametersOrBuilder.
Definition at line 17206 of file SatParameters.java.
◆ hasPbCleanupIncrement()
|
inline |
Same as for the clauses, but for the learned pseudo-Boolean constraints.
optional int32 pb_cleanup_increment = 46 [default = 200];
- Returns
- Whether the pbCleanupIncrement field is set.
Implements SatParametersOrBuilder.
Definition at line 11509 of file SatParameters.java.
◆ hasPbCleanupRatio()
|
inline |
optional double pb_cleanup_ratio = 47 [default = 0.5];
- Returns
- Whether the pbCleanupRatio field is set.
Implements SatParametersOrBuilder.
Definition at line 11560 of file SatParameters.java.
◆ hasPreferredVariableOrder()
|
inline |
optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
- Returns
- Whether the preferredVariableOrder field is set.
Implements SatParametersOrBuilder.
Definition at line 10588 of file SatParameters.java.
◆ hasPresolveBlockedClause()
|
inline |
Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.
optional bool presolve_blocked_clause = 88 [default = true];
- Returns
- Whether the presolveBlockedClause field is set.
Implements SatParametersOrBuilder.
Definition at line 13802 of file SatParameters.java.
◆ hasPresolveBvaThreshold()
|
inline |
Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold. The algorithm described in the paper uses 0, but quick experiments showed that 1 is a good value. It may not be worth it to add a new variable just to remove one clause.
optional int32 presolve_bva_threshold = 73 [default = 1];
- Returns
- Whether the presolveBvaThreshold field is set.
Implements SatParametersOrBuilder.
Definition at line 13918 of file SatParameters.java.
◆ hasPresolveBveClauseWeight()
|
inline |
During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.
optional int32 presolve_bve_clause_weight = 55 [default = 3];
- Returns
- Whether the presolveBveClauseWeight field is set.
Implements SatParametersOrBuilder.
Definition at line 13684 of file SatParameters.java.
◆ hasPresolveBveThreshold()
|
inline |
During presolve, only try to perform the bounded variable elimination (BVE) of a variable x if the number of occurrences of x times the number of occurrences of not(x) is not greater than this parameter.
optional int32 presolve_bve_threshold = 54 [default = 500];
- Returns
- Whether the presolveBveThreshold field is set.
Implements SatParametersOrBuilder.
Definition at line 13622 of file SatParameters.java.
◆ hasPresolveProbingDeterministicTimeLimit()
|
inline |
The maximum "deterministic" time limit to spend in probing. A value of zero will disable the probing.
optional double presolve_probing_deterministic_time_limit = 57 [default = 30];
- Returns
- Whether the presolveProbingDeterministicTimeLimit field is set.
Implements SatParametersOrBuilder.
Definition at line 13743 of file SatParameters.java.
◆ hasPresolveSubstitutionLevel()
|
inline |
How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve. This currently only concerns variable appearing only in linear constraints. For now the value 0 turns it off and any positive value performs substitution.
optional int32 presolve_substitution_level = 147 [default = 1];
- Returns
- Whether the presolveSubstitutionLevel field is set.
Implements SatParametersOrBuilder.
Definition at line 14661 of file SatParameters.java.
◆ hasPresolveUseBva()
|
inline |
Whether or not we use Bounded Variable Addition (BVA) in the presolve.
optional bool presolve_use_bva = 72 [default = true];
- Returns
- Whether the presolveUseBva field is set.
Implements SatParametersOrBuilder.
Definition at line 13860 of file SatParameters.java.
◆ hasProbingPeriodAtRoot()
|
inline |
If set at zero (the default), it is disabled. Otherwise the solver attempts probing at every 'probing_period' root node. Period of 1 enables probing at every root node.
optional int64 probing_period_at_root = 142 [default = 0];
- Returns
- Whether the probingPeriodAtRoot field is set.
Implements SatParametersOrBuilder.
Definition at line 16947 of file SatParameters.java.
◆ hasPseudoCostReliabilityThreshold()
|
inline |
The solver ignores the pseudo costs of variables with number of recordings less than this threshold.
optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
- Returns
- Whether the pseudoCostReliabilityThreshold field is set.
Implements SatParametersOrBuilder.
Definition at line 17009 of file SatParameters.java.
◆ hasRandomBranchesRatio()
|
inline |
A number between 0 and 1 that indicates the proportion of branching variables that are selected randomly instead of choosing the first variable from the given variable_ordering strategy.
optional double random_branches_ratio = 32 [default = 0];
- Returns
- Whether the randomBranchesRatio field is set.
Implements SatParametersOrBuilder.
Definition at line 10831 of file SatParameters.java.
◆ hasRandomizeSearch()
|
inline |
Randomize fixed search.
optional bool randomize_search = 103 [default = false];
- Returns
- Whether the randomizeSearch field is set.
Implements SatParametersOrBuilder.
Definition at line 18330 of file SatParameters.java.
◆ hasRandomPolarityRatio()
|
inline |
The proportion of polarity chosen at random. Note that this take precedence over the phase saving heuristic. This is different from initial_polarity:POLARITY_RANDOM because it will select a new random polarity each time the variable is branched upon instead of selecting one initially and then always taking this choice.
optional double random_polarity_ratio = 45 [default = 0];
- Returns
- Whether the randomPolarityRatio field is set.
Implements SatParametersOrBuilder.
Definition at line 10762 of file SatParameters.java.
◆ hasRandomSeed()
|
inline |
At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed. If you change the random seed, the solver may make different choices during the solving process. For some problems, the running time may vary a lot depending on small change in the solving algorithm. Running the solver with different seeds enables to have more robust benchmarks when evaluating new features.
optional int32 random_seed = 31 [default = 1];
- Returns
- Whether the randomSeed field is set.
Implements SatParametersOrBuilder.
Definition at line 13278 of file SatParameters.java.
◆ hasReduceMemoryUsageInInterleaveMode()
|
inline |
Temporary parameter until the memory usage is more optimized.
optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];
- Returns
- Whether the reduceMemoryUsageInInterleaveMode field is set.
Implements SatParametersOrBuilder.
Definition at line 17847 of file SatParameters.java.
◆ hasRelativeGapLimit()
|
inline |
optional double relative_gap_limit = 160 [default = 0];
- Returns
- Whether the relativeGapLimit field is set.
Implements SatParametersOrBuilder.
Definition at line 13167 of file SatParameters.java.
◆ hasRestartDlAverageRatio()
|
inline |
In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.
optional double restart_dl_average_ratio = 63 [default = 1];
- Returns
- Whether the restartDlAverageRatio field is set.
Implements SatParametersOrBuilder.
Definition at line 12456 of file SatParameters.java.
◆ hasRestartLbdAverageRatio()
|
inline |
optional double restart_lbd_average_ratio = 71 [default = 1];
- Returns
- Whether the restartLbdAverageRatio field is set.
Implements SatParametersOrBuilder.
Definition at line 12510 of file SatParameters.java.
◆ hasRestartPeriod()
|
inline |
Restart period for the FIXED_RESTART strategy. This is also the multiplier used by the LUBY_RESTART strategy.
optional int32 restart_period = 30 [default = 50];
- Returns
- Whether the restartPeriod field is set.
Implements SatParametersOrBuilder.
Definition at line 12342 of file SatParameters.java.
◆ hasRestartRunningWindowSize()
|
inline |
Size of the window for the moving average restarts.
optional int32 restart_running_window_size = 62 [default = 50];
- Returns
- Whether the restartRunningWindowSize field is set.
Implements SatParametersOrBuilder.
Definition at line 12400 of file SatParameters.java.
◆ hasSearchBranching()
|
inline |
optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
- Returns
- Whether the searchBranching field is set.
Implements SatParametersOrBuilder.
Definition at line 16531 of file SatParameters.java.
◆ hasSearchRandomizationTolerance()
|
inline |
Search randomization will collect equivalent 'max valued' variables, and pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST, all unassigned variables are equivalent. If the variable strategy is CHOOSE_LOWEST_MIN, and `lm` is the current lowest min of all unassigned variables, then the set of max valued variables will be all unassigned variables where lm <= variable min <= lm + search_randomization_tolerance
optional int64 search_randomization_tolerance = 104 [default = 0];
- Returns
- Whether the searchRandomizationTolerance field is set.
Implements SatParametersOrBuilder.
Definition at line 18391 of file SatParameters.java.
◆ hasShareLevelZeroBounds()
|
inline |
Allows sharing of the bounds of modified variables at level 0.
optional bool share_level_zero_bounds = 114 [default = true];
- Returns
- Whether the shareLevelZeroBounds field is set.
Implements SatParametersOrBuilder.
Definition at line 17957 of file SatParameters.java.
◆ hasShareObjectiveBounds()
|
inline |
Allows objective sharing between workers.
optional bool share_objective_bounds = 113 [default = true];
- Returns
- Whether the shareObjectiveBounds field is set.
Implements SatParametersOrBuilder.
Definition at line 17902 of file SatParameters.java.
◆ hasStopAfterFirstSolution()
|
inline |
For an optimization problem, stop the solver as soon as we have a solution.
optional bool stop_after_first_solution = 98 [default = false];
- Returns
- Whether the stopAfterFirstSolution field is set.
Implements SatParametersOrBuilder.
Definition at line 17548 of file SatParameters.java.
◆ hasStopAfterPresolve()
|
inline |
Mainly used when improving the presolver. When true, stops the solver after the presolve is complete.
optional bool stop_after_presolve = 149 [default = false];
- Returns
- Whether the stopAfterPresolve field is set.
Implements SatParametersOrBuilder.
Definition at line 17604 of file SatParameters.java.
◆ hasStrategyChangeIncreaseRatio()
|
inline |
The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.
optional double strategy_change_increase_ratio = 69 [default = 0];
- Returns
- Whether the strategyChangeIncreaseRatio field is set.
Implements SatParametersOrBuilder.
Definition at line 12758 of file SatParameters.java.
◆ hasSubsumptionDuringConflictAnalysis()
|
inline |
At a really low cost, during the 1-UIP conflict computation, it is easy to detect if some of the involved reasons are subsumed by the current conflict. When this is true, such clauses are detached and later removed from the problem.
optional bool subsumption_during_conflict_analysis = 56 [default = true];
- Returns
- Whether the subsumptionDuringConflictAnalysis field is set.
Implements SatParametersOrBuilder.
Definition at line 11186 of file SatParameters.java.
◆ hasTreatBinaryClausesSeparately()
|
inline |
If true, the binary clauses are treated separately from the others. This should be faster and uses less memory. However it changes the propagation order.
optional bool treat_binary_clauses_separately = 33 [default = true];
- Returns
- Whether the treatBinaryClausesSeparately field is set.
Implements SatParametersOrBuilder.
Definition at line 13212 of file SatParameters.java.
◆ hasUseBlockingRestart()
|
inline |
Block a moving restart algorithm if the trail size of the current conflict is greater than the multiplier times the moving average of the trail size at the previous conflicts.
optional bool use_blocking_restart = 64 [default = false];
- Returns
- Whether the useBlockingRestart field is set.
Implements SatParametersOrBuilder.
Definition at line 12555 of file SatParameters.java.
◆ hasUseBranchingInLp()
|
inline |
If true, the solver attemts to generate more info inside lp propagator by branching on some variables if certain criteria are met during the search tree exploration.
optional bool use_branching_in_lp = 139 [default = false];
- Returns
- Whether the useBranchingInLp field is set.
Implements SatParametersOrBuilder.
Definition at line 18596 of file SatParameters.java.
◆ hasUseCombinedNoOverlap()
|
inline |
This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem. Like 1000 intervals, but 1M intervals in the no-overlap constraints covering them.
optional bool use_combined_no_overlap = 133 [default = false];
- Returns
- Whether the useCombinedNoOverlap field is set.
Implements SatParametersOrBuilder.
Definition at line 18659 of file SatParameters.java.
◆ hasUseDisjunctiveConstraintInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with propagators from the disjunctive constraint to improve the inference on a set of tasks that are disjunctive at the root of the problem. This additional level supplements the default level of reasoning. Propagators of the cumulative constraint will not be used at all if all the tasks are disjunctive at root node. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];
- Returns
- Whether the useDisjunctiveConstraintInCumulativeConstraint field is set.
Implements SatParametersOrBuilder.
Definition at line 15350 of file SatParameters.java.
◆ hasUseErwaHeuristic()
|
inline |
Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as described in "Learning Rate Based Branching Heuristic for SAT solvers", J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.
optional bool use_erwa_heuristic = 75 [default = false];
- Returns
- Whether the useErwaHeuristic field is set.
Implements SatParametersOrBuilder.
Definition at line 10894 of file SatParameters.java.
◆ hasUseExactLpReason()
|
inline |
The solver usually exploit the LP relaxation of a model. If this option is true, then whatever is infered by the LP will be used like an heuristic to compute EXACT propagation on the IP. So with this option, there is no numerical imprecision issues.
optional bool use_exact_lp_reason = 109 [default = true];
- Returns
- Whether the useExactLpReason field is set.
Implements SatParametersOrBuilder.
Definition at line 18530 of file SatParameters.java.
◆ hasUseFeasibilityPump()
|
inline |
Adds a feasibility pump subsolver along with lns subsolvers.
optional bool use_feasibility_pump = 164 [default = false];
- Returns
- Whether the useFeasibilityPump field is set.
Implements SatParametersOrBuilder.
Definition at line 18161 of file SatParameters.java.
◆ hasUseImpliedBounds()
|
inline |
Stores and exploits "implied-bounds" in the solver. That is, relations of the form literal => (var >= bound). This is currently used to derive stronger cuts.
optional bool use_implied_bounds = 144 [default = true];
- Returns
- Whether the useImpliedBounds field is set.
Implements SatParametersOrBuilder.
Definition at line 18785 of file SatParameters.java.
◆ hasUseLnsOnly()
|
inline |
LNS parameters.
optional bool use_lns_only = 101 [default = false];
- Returns
- Whether the useLnsOnly field is set.
Implements SatParametersOrBuilder.
Definition at line 18012 of file SatParameters.java.
◆ hasUseOptimizationHints()
|
inline |
For an optimization problem, whether we follow some hints in order to find a better first solution. For a variable with hint, the solver will always try to follow the hint. It will revert to the variable_branching default otherwise.
optional bool use_optimization_hints = 35 [default = true];
- Returns
- Whether the useOptimizationHints field is set.
Implements SatParametersOrBuilder.
Definition at line 14728 of file SatParameters.java.
◆ hasUseOptionalVariables()
|
inline |
If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional. This allows to propagate them as if they were present in some situation.
optional bool use_optional_variables = 108 [default = true];
- Returns
- Whether the useOptionalVariables field is set.
Implements SatParametersOrBuilder.
Definition at line 18466 of file SatParameters.java.
◆ hasUseOverloadCheckerInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy. This additional level supplements the default level of reasoning as well as timetable edge finding. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];
- Returns
- Whether the useOverloadCheckerInCumulativeConstraint field is set.
Implements SatParametersOrBuilder.
Definition at line 15198 of file SatParameters.java.
◆ hasUsePbResolution()
|
inline |
Whether to use pseudo-Boolean resolution to analyze a conflict. Note that this option only make sense if your problem is modelized using pseudo-Boolean constraints. If you only have clauses, this shouldn't change anything (except slow the solver down).
optional bool use_pb_resolution = 43 [default = false];
- Returns
- Whether the usePbResolution field is set.
Implements SatParametersOrBuilder.
Definition at line 13406 of file SatParameters.java.
◆ hasUsePhaseSaving()
|
inline |
If this is true, then the polarity of a variable will be the last value it was assigned to, or its default polarity if it was never assigned since the call to ResetDecisionHeuristic(). This is called 'literal phase saving'. For details see 'A Lightweight Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and A.Darwiche, In 10th International Conference on Theory and Applications of Satisfiability Testing, 2007.
optional bool use_phase_saving = 44 [default = true];
- Returns
- Whether the usePhaseSaving field is set.
Implements SatParametersOrBuilder.
Definition at line 10685 of file SatParameters.java.
◆ hasUsePrecedencesInDisjunctiveConstraint()
|
inline |
When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further. For instance if task A and B are both before C and task A and B are in disjunction, then we can deduce that task C must start after duration(A) + duration(B) instead of simply max(duration(A), duration(B)), provided that the start time for all task was currently zero. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];
- Returns
- Whether the usePrecedencesInDisjunctiveConstraint field is set.
Implements SatParametersOrBuilder.
Definition at line 15117 of file SatParameters.java.
◆ hasUseRelaxationLns()
|
inline |
Turns on a lns worker which solves relaxed version of the original problem by removing constraints from the problem in order to get better bounds.
optional bool use_relaxation_lns = 150 [default = false];
- Returns
- Whether the useRelaxationLns field is set.
Implements SatParametersOrBuilder.
Definition at line 18217 of file SatParameters.java.
◆ hasUseRinsLns()
|
inline |
Turns on relaxation induced neighborhood generator.
optional bool use_rins_lns = 129 [default = true];
- Returns
- Whether the useRinsLns field is set.
Implements SatParametersOrBuilder.
Definition at line 18106 of file SatParameters.java.
◆ hasUseSatInprocessing()
|
inline |
optional bool use_sat_inprocessing = 163 [default = false];
- Returns
- Whether the useSatInprocessing field is set.
Implements SatParametersOrBuilder.
Definition at line 14332 of file SatParameters.java.
◆ hasUseTimetableEdgeFindingInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with timetable edge finding, i.e., an additional level of reasoning based on the conjunction of energy and mandatory parts. This additional level supplements the default level of reasoning as well as overload_checker. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];
- Returns
- Whether the useTimetableEdgeFindingInCumulativeConstraint field is set.
Implements SatParametersOrBuilder.
Definition at line 15273 of file SatParameters.java.
◆ hasVariableActivityDecay()
|
inline |
Each time a conflict is found, the activities of some variables are increased by one. Then, the activity of all variables are multiplied by variable_activity_decay. To implement this efficiently, the activity of all the variables is not decayed at each conflict. Instead, the activity increment is multiplied by 1 / decay. When an activity reach max_variable_activity_value, all the activity are multiplied by 1 / max_variable_activity_value.
optional double variable_activity_decay = 15 [default = 0.8];
- Returns
- Whether the variableActivityDecay field is set.
Implements SatParametersOrBuilder.
Definition at line 11743 of file SatParameters.java.
◆ internalGetFieldAccessorTable()
|
inlineprotected |
Definition at line 9157 of file SatParameters.java.
◆ isInitialized()
|
inline |
Definition at line 10555 of file SatParameters.java.
◆ mergeFrom() [1/3]
|
inline |
Definition at line 10115 of file SatParameters.java.
◆ mergeFrom() [2/3]
|
inline |
Definition at line 10560 of file SatParameters.java.
◆ mergeFrom() [3/3]
|
inline |
Definition at line 10106 of file SatParameters.java.
◆ mergeUnknownFields()
|
inline |
Definition at line 19201 of file SatParameters.java.
◆ setAbsoluteGapLimit()
|
inline |
Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit. The exact definition is:
- Absolute: abs(O - B)
- Relative: abs(O - B) / max(1, abs(O)). Important: The relative gap depends on the objective offset! If you artificially shift the objective, you will get widely different value of the relative gap. Note that if the gap is reached, the search status will be OPTIMAL. But one can check the best objective bound to see the actual gap.
optional double absolute_gap_limit = 159 [default = 0];
- Parameters
-
value The absoluteGapLimit to set.
- Returns
- This builder for chaining.
Definition at line 13131 of file SatParameters.java.
◆ setAddCgCuts()
|
inline |
Whether we generate and add Chvatal-Gomory cuts to the LP at root node. Note that for now, this is not heavily tunned.
optional bool add_cg_cuts = 117 [default = true];
- Parameters
-
value The addCgCuts to set.
- Returns
- This builder for chaining.
Definition at line 15768 of file SatParameters.java.
◆ setAddKnapsackCuts()
|
inline |
Whether we generate knapsack cuts. Note that in our setting where all variables are integer and bounded on both side, such a cut could be applied to any constraint.
optional bool add_knapsack_cuts = 111 [default = false];
- Parameters
-
value The addKnapsackCuts to set.
- Returns
- This builder for chaining.
Definition at line 15708 of file SatParameters.java.
◆ setAddLinMaxCuts()
|
inline |
For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)
optional bool add_lin_max_cuts = 152 [default = true];
- Parameters
-
value The addLinMaxCuts to set.
- Returns
- This builder for chaining.
Definition at line 15952 of file SatParameters.java.
◆ setAddLpConstraintsLazily()
|
inline |
If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch. A constraint that is only added like this is known as a "lazy" constraint in the literature, except that we currently consider all constraints as lazy here.
optional bool add_lp_constraints_lazily = 112 [default = true];
- Parameters
-
value The addLpConstraintsLazily to set.
- Returns
- This builder for chaining.
Definition at line 16097 of file SatParameters.java.
◆ setAddMirCuts()
|
inline |
Whether we generate MIR cuts at root node. Note that for now, this is not heavily tunned.
optional bool add_mir_cuts = 120 [default = true];
- Parameters
-
value The addMirCuts to set.
- Returns
- This builder for chaining.
Definition at line 15827 of file SatParameters.java.
◆ setAlsoBumpVariablesInConflictReasons()
|
inline |
When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped. This is addition to the variables in the conflict, and the one that were used during conflict resolution.
optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];
- Parameters
-
value The alsoBumpVariablesInConflictReasons to set.
- Returns
- This builder for chaining.
Definition at line 11063 of file SatParameters.java.
◆ setAutoDetectGreaterThanAtLeastOneOf()
|
inline |
If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present. This is usually useful to have but can be slow on model with a lot of precedence.
optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];
- Parameters
-
value The autoDetectGreaterThanAtLeastOneOf to set.
- Returns
- This builder for chaining.
Definition at line 17514 of file SatParameters.java.
◆ setBinaryMinimizationAlgorithm()
|
inline |
optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];
- Parameters
-
value The binaryMinimizationAlgorithm to set.
- Returns
- This builder for chaining.
Definition at line 11153 of file SatParameters.java.
◆ setBinarySearchNumConflicts()
|
inline |
If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict. This can quickly reduce the objective domain on some problems.
optional int32 binary_search_num_conflicts = 99 [default = -1];
- Parameters
-
value The binarySearchNumConflicts to set.
- Returns
- This builder for chaining.
Definition at line 17167 of file SatParameters.java.
◆ setBlockingRestartMultiplier()
|
inline |
optional double blocking_restart_multiplier = 66 [default = 1.4];
- Parameters
-
value The blockingRestartMultiplier to set.
- Returns
- This builder for chaining.
Definition at line 12667 of file SatParameters.java.
◆ setBlockingRestartWindowSize()
|
inline |
optional int32 blocking_restart_window_size = 65 [default = 5000];
- Parameters
-
value The blockingRestartWindowSize to set.
- Returns
- This builder for chaining.
Definition at line 12628 of file SatParameters.java.
◆ setBooleanEncodingLevel()
|
inline |
A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.
optional int32 boolean_encoding_level = 107 [default = 1];
- Parameters
-
value The booleanEncodingLevel to set.
- Returns
- This builder for chaining.
Definition at line 15520 of file SatParameters.java.
◆ setCatchSigintSignal()
|
inline |
Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve. If set, catching the SIGINT signal will terminate the search gracefully, as if a time limit was reached.
optional bool catch_sigint_signal = 135 [default = true];
- Parameters
-
value The catchSigintSignal to set.
- Returns
- This builder for chaining.
Definition at line 18750 of file SatParameters.java.
◆ setClauseActivityDecay()
|
inline |
Clause activity parameters (same effect as the one on the variables).
optional double clause_activity_decay = 17 [default = 0.999];
- Parameters
-
value The clauseActivityDecay to set.
- Returns
- This builder for chaining.
Definition at line 12024 of file SatParameters.java.
◆ setClauseCleanupLbdBound()
|
inline |
All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.
optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
- Parameters
-
value The clauseCleanupLbdBound to set.
- Returns
- This builder for chaining.
Definition at line 11434 of file SatParameters.java.
◆ setClauseCleanupOrdering()
|
inline |
optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];
- Parameters
-
value The clauseCleanupOrdering to set.
- Returns
- This builder for chaining.
Definition at line 11479 of file SatParameters.java.
◆ setClauseCleanupPeriod()
|
inline |
Trigger a cleanup when this number of "deletable" clauses is learned.
optional int32 clause_cleanup_period = 11 [default = 10000];
- Parameters
-
value The clauseCleanupPeriod to set.
- Returns
- This builder for chaining.
Definition at line 11274 of file SatParameters.java.
◆ setClauseCleanupProtection()
|
inline |
optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];
- Parameters
-
value The clauseCleanupProtection to set.
- Returns
- This builder for chaining.
Definition at line 11377 of file SatParameters.java.
◆ setClauseCleanupTarget()
|
inline |
During a cleanup, we will always keep that number of "deletable" clauses. Note that this doesn't include the "protected" clauses.
optional int32 clause_cleanup_target = 13 [default = 10000];
- Parameters
-
value The clauseCleanupTarget to set.
- Returns
- This builder for chaining.
Definition at line 11332 of file SatParameters.java.
◆ setCountAssumptionLevelsInLbd()
|
inline |
Whether or not the assumption levels are taken into account during the LBD computation. According to the reference below, not counting them improves the solver in some situation. Note that this only impact solves under assumptions. Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction" Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes in Computer Science Volume 7962, 2013, pp 309-317.
optional bool count_assumption_levels_in_lbd = 49 [default = true];
- Parameters
-
value The countAssumptionLevelsInLbd to set.
- Returns
- This builder for chaining.
Definition at line 13582 of file SatParameters.java.
◆ setCoverOptimization()
|
inline |
If true, when the max-sat algo find a core, we compute the minimal number of literals in the core that needs to be true to have a feasible solution.
optional bool cover_optimization = 89 [default = true];
- Parameters
-
value The coverOptimization to set.
- Returns
- This builder for chaining.
Definition at line 14933 of file SatParameters.java.
◆ setCpModelMaxNumPresolveOperations()
|
inline |
If positive, try to stop just after that many presolve rules have been applied. This is mainly useful for debugging presolve.
optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];
- Parameters
-
value The cpModelMaxNumPresolveOperations to set.
- Returns
- This builder for chaining.
Definition at line 14194 of file SatParameters.java.
◆ setCpModelPostsolveWithFullSolver()
|
inline |
Advanced usage. We have two different postsolve code. The default one should be better and it allows for a more powerful presolve, but some rarely used features like not fully assigning all variables require the other one.
optional bool cp_model_postsolve_with_full_solver = 162 [default = false];
- Parameters
-
value The cpModelPostsolveWithFullSolver to set.
- Returns
- This builder for chaining.
Definition at line 14133 of file SatParameters.java.
◆ setCpModelPresolve()
|
inline |
Whether we presolve the cp_model before solving it.
optional bool cp_model_presolve = 86 [default = true];
- Parameters
-
value The cpModelPresolve to set.
- Returns
- This builder for chaining.
Definition at line 14069 of file SatParameters.java.
◆ setCpModelProbingLevel()
|
inline |
How much effort do we spend on probing. 0 disables it completely.
optional int32 cp_model_probing_level = 110 [default = 2];
- Parameters
-
value The cpModelProbingLevel to set.
- Returns
- This builder for chaining.
Definition at line 14250 of file SatParameters.java.
◆ setCpModelUseSatPresolve()
|
inline |
Whether we also use the sat presolve when cp_model_presolve is true.
optional bool cp_model_use_sat_presolve = 93 [default = true];
- Parameters
-
value The cpModelUseSatPresolve to set.
- Returns
- This builder for chaining.
Definition at line 14305 of file SatParameters.java.
◆ setCutActiveCountDecay()
|
inline |
optional double cut_active_count_decay = 156 [default = 0.8];
- Parameters
-
value The cutActiveCountDecay to set.
- Returns
- This builder for chaining.
Definition at line 16395 of file SatParameters.java.
◆ setCutCleanupTarget()
|
inline |
Target number of constraints to remove during cleanup.
optional int32 cut_cleanup_target = 157 [default = 1000];
- Parameters
-
value The cutCleanupTarget to set.
- Returns
- This builder for chaining.
Definition at line 16446 of file SatParameters.java.
◆ setCutMaxActiveCountValue()
|
inline |
These parameters are similar to sat clause management activity parameters. They are effective only if the number of generated cuts exceed the storage limit. Default values are based on a few experiments on miplib instances.
optional double cut_max_active_count_value = 155 [default = 10000000000];
- Parameters
-
value The cutMaxActiveCountValue to set.
- Returns
- This builder for chaining.
Definition at line 16350 of file SatParameters.java.
◆ setDefaultRestartAlgorithms()
|
inline |
optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
- Parameters
-
value The defaultRestartAlgorithms to set.
- Returns
- This builder for chaining.
Definition at line 12295 of file SatParameters.java.
◆ setDefaultRestartAlgorithmsBytes()
|
inline |
optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
- Parameters
-
value The bytes for defaultRestartAlgorithms to set.
- Returns
- This builder for chaining.
Definition at line 12320 of file SatParameters.java.
◆ setDiversifyLnsParams()
|
inline |
If true, registers more lns subsolvers with different parameters.
optional bool diversify_lns_params = 137 [default = false];
- Parameters
-
value The diversifyLnsParams to set.
- Returns
- This builder for chaining.
Definition at line 18299 of file SatParameters.java.
◆ setEnumerateAllSolutions()
|
inline |
Whether we enumerate all solutions of a problem without objective. Note that setting this to true automatically disable the presolve. This is because the presolve rules only guarantee the existence of one feasible solution to the presolved problem. TODO(user): Activate the presolve but with just the rules that do not change the set of feasible solutions.
optional bool enumerate_all_solutions = 87 [default = false];
- Parameters
-
value The enumerateAllSolutions to set.
- Returns
- This builder for chaining.
Definition at line 17315 of file SatParameters.java.
◆ setExpandAutomatonConstraints()
|
inline |
If true, the automaton constraints are expanded.
optional bool expand_automaton_constraints = 143 [default = true];
- Parameters
-
value The expandAutomatonConstraints to set.
- Returns
- This builder for chaining.
Definition at line 14458 of file SatParameters.java.
◆ setExpandElementConstraints()
|
inline |
If true, the element constraints are expanded into many linear constraints of the form (index == i) => (element[i] == target).
optional bool expand_element_constraints = 140 [default = true];
- Parameters
-
value The expandElementConstraints to set.
- Returns
- This builder for chaining.
Definition at line 14402 of file SatParameters.java.
◆ setExpandTableConstraints()
|
inline |
If true, the positive table constraints are expanded. Note that currently, negative table constraints are always expanded.
optional bool expand_table_constraints = 158 [default = true];
- Parameters
-
value The expandTableConstraints to set.
- Returns
- This builder for chaining.
Definition at line 14516 of file SatParameters.java.
◆ setExploitAllLpSolution()
|
inline |
If true and the Lp relaxation of the problem has a solution, try to exploit it. This is same as above except in this case the lp solution might not be an integer solution.
optional bool exploit_all_lp_solution = 116 [default = true];
- Parameters
-
value The exploitAllLpSolution to set.
- Returns
- This builder for chaining.
Definition at line 16735 of file SatParameters.java.
◆ setExploitBestSolution()
|
inline |
When branching on a variable, follow the last best solution value.
optional bool exploit_best_solution = 130 [default = false];
- Parameters
-
value The exploitBestSolution to set.
- Returns
- This builder for chaining.
Definition at line 16792 of file SatParameters.java.
◆ setExploitIntegerLpSolution()
|
inline |
If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it. Note that since the LP relaxation may not contain all the constraints, such a solution is not necessarily a solution of the full problem.
optional bool exploit_integer_lp_solution = 94 [default = true];
- Parameters
-
value The exploitIntegerLpSolution to set.
- Returns
- This builder for chaining.
Definition at line 16671 of file SatParameters.java.
◆ setExploitObjective()
|
inline |
When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.
optional bool exploit_objective = 131 [default = true];
- Parameters
-
value The exploitObjective to set.
- Returns
- This builder for chaining.
Definition at line 16913 of file SatParameters.java.
◆ setExploitRelaxationSolution()
|
inline |
When branching on a variable, follow the last best relaxation solution value. We use the relaxation with the tightest bound on the objective as the best relaxation solution.
optional bool exploit_relaxation_solution = 161 [default = false];
- Parameters
-
value The exploitRelaxationSolution to set.
- Returns
- This builder for chaining.
Definition at line 16853 of file SatParameters.java.
◆ setField()
|
inline |
Definition at line 10078 of file SatParameters.java.
◆ setFillTightenedDomainsInResponse()
|
inline |
If true, add information about the derived variable domains to the CpSolverResponse. It is an option because it makes the response slighly bigger and there is a bit more work involved during the postsolve to construct it, but it should still have a low overhead. See the tightened_variables field in CpSolverResponse for more details.
optional bool fill_tightened_domains_in_response = 132 [default = false];
- Parameters
-
value The fillTightenedDomainsInResponse to set.
- Returns
- This builder for chaining.
Definition at line 17387 of file SatParameters.java.
◆ setFindMultipleCores()
|
inline |
Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.
optional bool find_multiple_cores = 84 [default = true];
- Parameters
-
value The findMultipleCores to set.
- Returns
- This builder for chaining.
Definition at line 14874 of file SatParameters.java.
◆ setGlucoseDecayIncrement()
|
inline |
optional double glucose_decay_increment = 23 [default = 0.01];
- Parameters
-
value The glucoseDecayIncrement to set.
- Returns
- This builder for chaining.
Definition at line 11934 of file SatParameters.java.
◆ setGlucoseDecayIncrementPeriod()
|
inline |
optional int32 glucose_decay_increment_period = 24 [default = 5000];
- Parameters
-
value The glucoseDecayIncrementPeriod to set.
- Returns
- This builder for chaining.
Definition at line 11973 of file SatParameters.java.
◆ setGlucoseMaxDecay()
|
inline |
The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95. This "hack" seems to work well and comes from: Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013 http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136
optional double glucose_max_decay = 22 [default = 0.95];
- Parameters
-
value The glucoseMaxDecay to set.
- Returns
- This builder for chaining.
Definition at line 11888 of file SatParameters.java.
◆ setHintConflictLimit()
|
inline |
When we try to follow the hint, we do a FIXED_SEARCH using the hint until this number of conflict is reached.
optional int32 hint_conflict_limit = 153 [default = 10];
- Parameters
-
value The hintConflictLimit to set.
- Returns
- This builder for chaining.
Definition at line 16606 of file SatParameters.java.
◆ setInitialPolarity()
|
inline |
optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];
- Parameters
-
value The initialPolarity to set.
- Returns
- This builder for chaining.
Definition at line 10649 of file SatParameters.java.
◆ setInitialVariablesActivity()
|
inline |
The initial value of the variables activity. A non-zero value only make sense when use_erwa_heuristic is true. Experiments with a value of 1e-2 together with the ERWA heuristic showed slighthly better result than simply using zero. The idea is that when the "learning rate" of a variable becomes lower than this value, then we prefer to branch on never explored before variables. This is not in the ERWA paper.
optional double initial_variables_activity = 76 [default = 0];
- Parameters
-
value The initialVariablesActivity to set.
- Returns
- This builder for chaining.
Definition at line 10994 of file SatParameters.java.
◆ setInstantiateAllVariables()
|
inline |
If true, the solver will add a default integer branching strategy to the already defined search strategy.
optional bool instantiate_all_variables = 106 [default = true];
- Parameters
-
value The instantiateAllVariables to set.
- Returns
- This builder for chaining.
Definition at line 17449 of file SatParameters.java.
◆ setInterleaveBatchSize()
|
inline |
optional int32 interleave_batch_size = 134 [default = 1];
- Parameters
-
value The interleaveBatchSize to set.
- Returns
- This builder for chaining.
Definition at line 17820 of file SatParameters.java.
◆ setInterleaveSearch()
|
inline |
Experimental. If this is true, then we interleave all our major search strategy and distribute the work amongst num_search_workers. The search is deterministic (independently of num_search_workers!), and we schedule and wait for interleave_batch_size task to be completed before synchronizing and scheduling the next batch of tasks.
optional bool interleave_search = 136 [default = false];
- Parameters
-
value The interleaveSearch to set.
- Returns
- This builder for chaining.
Definition at line 17773 of file SatParameters.java.
◆ setLinearizationLevel()
|
inline |
A non-negative level indicating the type of constraints we consider in the LP relaxation. At level zero, no LP relaxation is used. At level 1, only the linear constraint and full encoding are added. At level 2, we also add all the Boolean constraints.
optional int32 linearization_level = 90 [default = 1];
- Parameters
-
value The linearizationLevel to set.
- Returns
- This builder for chaining.
Definition at line 15459 of file SatParameters.java.
◆ setLnsFocusOnDecisionVariables()
|
inline |
optional bool lns_focus_on_decision_variables = 105 [default = false];
- Parameters
-
value The lnsFocusOnDecisionVariables to set.
- Returns
- This builder for chaining.
Definition at line 18079 of file SatParameters.java.
◆ setLogSearchProgress()
|
inline |
Whether the solver should log the search progress to LOG(INFO).
optional bool log_search_progress = 41 [default = false];
- Parameters
-
value The logSearchProgress to set.
- Returns
- This builder for chaining.
Definition at line 13372 of file SatParameters.java.
◆ setMaxAllDiffCutSize()
|
inline |
Cut generator for all diffs can add too many cuts for large all_diff constraints. This parameter restricts the large all_diff constraints to have a cut generator.
optional int32 max_all_diff_cut_size = 148 [default = 7];
- Parameters
-
value The maxAllDiffCutSize to set.
- Returns
- This builder for chaining.
Definition at line 15889 of file SatParameters.java.
◆ setMaxClauseActivityValue()
|
inline |
optional double max_clause_activity_value = 18 [default = 1e+20];
- Parameters
-
value The maxClauseActivityValue to set.
- Returns
- This builder for chaining.
Definition at line 12067 of file SatParameters.java.
◆ setMaxConsecutiveInactiveCount()
|
inline |
If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP. Note that it might be added again later if it become violated by the current LP solution.
optional int32 max_consecutive_inactive_count = 121 [default = 100];
- Parameters
-
value The maxConsecutiveInactiveCount to set.
- Returns
- This builder for chaining.
Definition at line 16287 of file SatParameters.java.
◆ setMaxCutRoundsAtLevelZero()
|
inline |
Max number of time we perform cut generation and resolve the LP at level 0.
optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];
- Parameters
-
value The maxCutRoundsAtLevelZero to set.
- Returns
- This builder for chaining.
Definition at line 16226 of file SatParameters.java.
◆ setMaxDeterministicTime()
|
inline |
Maximum time allowed in deterministic time to solve a problem. The deterministic time should be correlated with the real time used by the solver, the time unit being as close as possible to a second.
optional double max_deterministic_time = 67 [default = inf];
- Parameters
-
value The maxDeterministicTime to set.
- Returns
- This builder for chaining.
Definition at line 12905 of file SatParameters.java.
◆ setMaxIntegerRoundingScaling()
|
inline |
In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive). The lower this is, the lower the integer coefficients of the cut will be. Note that cut generated by lower values are not necessarily worse than cut generated by larger value. There is no strict dominance relationship. Setting this to 2 result in the "strong fractional rouding" of Letchford and Lodi.
optional int32 max_integer_rounding_scaling = 119 [default = 600];
- Parameters
-
value The maxIntegerRoundingScaling to set.
- Returns
- This builder for chaining.
Definition at line 16027 of file SatParameters.java.
◆ setMaxMemoryInMb()
|
inline |
Maximum memory allowed for the whole thread containing the solver. The solver will abort as soon as it detects that this limit is crossed. As a result, this limit is approximative, but usually the solver will not go too much over.
optional int64 max_memory_in_mb = 40 [default = 10000];
- Parameters
-
value The maxMemoryInMb to set.
- Returns
- This builder for chaining.
Definition at line 13046 of file SatParameters.java.
◆ setMaxNumberOfConflicts()
|
inline |
Maximum number of conflicts allowed to solve a problem. TODO(user,user): Maybe change the way the conflict limit is enforced? currently it is enforced on each independent internal SAT solve, rather than on the overall number of conflicts across all solves. So in the context of an optimization problem, this is not really usable directly by a client.
optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];
- Parameters
-
value The maxNumberOfConflicts to set.
- Returns
- This builder for chaining.
Definition at line 12977 of file SatParameters.java.
◆ setMaxNumCuts()
|
inline |
The limit on the number of cuts in our cut pool. When this is reached we do not generate cuts anymore. TODO(user): We should probably remove this parameters, and just always generate cuts but only keep the best n or something.
optional int32 max_num_cuts = 91 [default = 10000];
- Parameters
-
value The maxNumCuts to set.
- Returns
- This builder for chaining.
Definition at line 15585 of file SatParameters.java.
◆ setMaxPresolveIterations()
|
inline |
In case of large reduction in a presolve iteration, we perform multiple presolve iterations. This parameter controls the maximum number of such presolve iterations.
optional int32 max_presolve_iterations = 138 [default = 3];
- Parameters
-
value The maxPresolveIterations to set.
- Returns
- This builder for chaining.
Definition at line 14012 of file SatParameters.java.
◆ setMaxSatAssumptionOrder()
|
inline |
optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];
- Parameters
-
value The maxSatAssumptionOrder to set.
- Returns
- This builder for chaining.
Definition at line 14978 of file SatParameters.java.
◆ setMaxSatReverseAssumptionOrder()
|
inline |
If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.
optional bool max_sat_reverse_assumption_order = 52 [default = false];
- Parameters
-
value The maxSatReverseAssumptionOrder to set.
- Returns
- This builder for chaining.
Definition at line 15035 of file SatParameters.java.
◆ setMaxSatStratification()
|
inline |
optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];
- Parameters
-
value The maxSatStratification to set.
- Returns
- This builder for chaining.
Definition at line 15080 of file SatParameters.java.
◆ setMaxTimeInSeconds()
|
inline |
Maximum time allowed in seconds to solve a problem. The counter will starts at the beginning of the Solve() call.
optional double max_time_in_seconds = 36 [default = inf];
- Parameters
-
value The maxTimeInSeconds to set.
- Returns
- This builder for chaining.
Definition at line 12843 of file SatParameters.java.
◆ setMaxVariableActivityValue()
|
inline |
optional double max_variable_activity_value = 16 [default = 1e+100];
- Parameters
-
value The maxVariableActivityValue to set.
- Returns
- This builder for chaining.
Definition at line 11828 of file SatParameters.java.
◆ setMergeAtMostOneWorkLimit()
|
inline |
optional double merge_at_most_one_work_limit = 146 [default = 100000000];
- Parameters
-
value The mergeAtMostOneWorkLimit to set.
- Returns
- This builder for chaining.
Definition at line 14631 of file SatParameters.java.
◆ setMergeNoOverlapWorkLimit()
|
inline |
During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints. This code can be slow, so we have a limit in place on the number of explored nodes in the underlying graph. The internal limit is an int64, but we use double here to simplify manual input.
optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];
- Parameters
-
value The mergeNoOverlapWorkLimit to set.
- Returns
- This builder for chaining.
Definition at line 14584 of file SatParameters.java.
◆ setMinimizationAlgorithm()
|
inline |
optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];
- Parameters
-
value The minimizationAlgorithm to set.
- Returns
- This builder for chaining.
Definition at line 11110 of file SatParameters.java.
◆ setMinimizeCore()
|
inline |
Whether we use a simple heuristic to try to minimize an UNSAT core.
optional bool minimize_core = 50 [default = true];
- Parameters
-
value The minimizeCore to set.
- Returns
- This builder for chaining.
Definition at line 14816 of file SatParameters.java.
◆ setMinimizeReductionDuringPbResolution()
|
inline |
A different algorithm during PB resolution. It minimizes the number of calls to ReduceCoefficients() which can be time consuming. However, the search space will be different and if the coefficients are large, this may lead to integer overflows that could otherwise be prevented.
optional bool minimize_reduction_during_pb_resolution = 48 [default = false];
- Parameters
-
value The minimizeReductionDuringPbResolution to set.
- Returns
- This builder for chaining.
Definition at line 13503 of file SatParameters.java.
◆ setMinimizeWithPropagationNumDecisions()
|
inline |
optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];
- Parameters
-
value The minimizeWithPropagationNumDecisions to set.
- Returns
- This builder for chaining.
Definition at line 11710 of file SatParameters.java.
◆ setMinimizeWithPropagationRestartPeriod()
|
inline |
Parameters for an heuristic similar to the one descibed in "An effective learnt clause minimization approach for CDCL Sat Solvers", https://www.ijcai.org/proceedings/2017/0098.pdf For now, we have a somewhat simpler implementation where every x restart we spend y decisions on clause minimization. The minimization technique is the same as the one used to minimize core in max-sat. We also minimize problem clauses and not just the learned clause that we keep forever like in the paper. Changing these parameters or the kind of clause we minimize seems to have a big impact on the overall perf on our benchmarks. So this technique seems definitely useful, but it is hard to tune properly.
optional int32 minimize_with_propagation_restart_period = 96 [default = 10];
- Parameters
-
value The minimizeWithPropagationRestartPeriod to set.
- Returns
- This builder for chaining.
Definition at line 11657 of file SatParameters.java.
◆ setMinOrthogonalityForLpConstraints()
|
inline |
While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call. Orthogonality is defined as 1 - cosine(vector angle between constraints). A value of zero disable this feature.
optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];
- Parameters
-
value The minOrthogonalityForLpConstraints to set.
- Returns
- This builder for chaining.
Definition at line 16167 of file SatParameters.java.
◆ setMipCheckPrecision()
|
inline |
As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted coefficient precision during scaling. When we cannot, we will report MODEL_INVALID if the relative preicision is larger than this parameter.
optional double mip_check_precision = 128 [default = 0.0001];
- Parameters
-
value The mipCheckPrecision to set.
- Returns
- This builder for chaining.
Definition at line 19171 of file SatParameters.java.
◆ setMipMaxActivityExponent()
|
inline |
To avoid integer overflow, we always force the maximum possible constraint activity (and objective value) according to the initial variable domain to be smaller than 2 to this given power. Because of this, we cannot always reach the "mip_wanted_precision" parameter above. This can go as high as 62, but some internal algo currently abort early if they might run into integer overflow, so it is better to keep it a bit lower than this.
optional int32 mip_max_activity_exponent = 127 [default = 53];
- Parameters
-
value The mipMaxActivityExponent to set.
- Returns
- This builder for chaining.
Definition at line 19101 of file SatParameters.java.
◆ setMipMaxBound()
|
inline |
We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use. If the MIP model expect larger variable value in the solution, then the converted model will likely not be relevant.
optional double mip_max_bound = 124 [default = 10000000];
- Parameters
-
value The mipMaxBound to set.
- Returns
- This builder for chaining.
Definition at line 18876 of file SatParameters.java.
◆ setMipVarScaling()
|
inline |
All continuous variable of the problem will be multiplied by this factor. By default, we don't do any variable scaling and rely on the MIP model to specify continuous variable domain with the wanted precision.
optional double mip_var_scaling = 125 [default = 1];
- Parameters
-
value The mipVarScaling to set.
- Returns
- This builder for chaining.
Definition at line 18939 of file SatParameters.java.
◆ setMipWantedPrecision()
|
inline |
When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients. We will choose the lowest power such that we have this relative precision on each of the constraint (resp. objective) coefficient. We also use this to decide by how much we relax the constraint bounds so that we can have a feasible integer solution of constraints involving continuous variable. This is required for instance when you have an == rhs constraint as in many situation you cannot have a perfect equality with integer variables and coefficients.
optional double mip_wanted_precision = 126 [default = 1e-06];
- Parameters
-
value The mipWantedPrecision to set.
- Returns
- This builder for chaining.
Definition at line 19020 of file SatParameters.java.
◆ setNewConstraintsBatchSize()
|
inline |
Add that many lazy contraints (or cuts) at once in the LP. Note that at the beginning of the solve, we do add more than this.
optional int32 new_constraints_batch_size = 122 [default = 50];
- Parameters
-
value The newConstraintsBatchSize to set.
- Returns
- This builder for chaining.
Definition at line 16504 of file SatParameters.java.
◆ setNumConflictsBeforeStrategyChanges()
|
inline |
After each restart, if the number of conflict since the last strategy change is greater that this, then we increment a "strategy_counter" that can be use to change the search strategy used by the following restarts.
optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];
- Parameters
-
value The numConflictsBeforeStrategyChanges to set.
- Returns
- This builder for chaining.
Definition at line 12724 of file SatParameters.java.
◆ setNumSearchWorkers()
|
inline |
Specify the number of parallel workers to use during search. A number <= 1 means no parallelism. As of 2020-04-10, if you're using SAT via MPSolver (to solve integer programs) this field is overridden with a value of 8, if the field is not set *explicitly*. Thus, always set this field explicitly or via MPSolver::SetNumThreads().
optional int32 num_search_workers = 100 [default = 1];
- Parameters
-
value The numSearchWorkers to set.
- Returns
- This builder for chaining.
Definition at line 17701 of file SatParameters.java.
◆ setOnlyAddCutsAtLevelZero()
|
inline |
For the cut that can be generated at any level, this control if we only try to generate them at the root node.
optional bool only_add_cuts_at_level_zero = 92 [default = false];
- Parameters
-
value The onlyAddCutsAtLevelZero to set.
- Returns
- This builder for chaining.
Definition at line 15646 of file SatParameters.java.
◆ setOptimizeWithCore()
|
inline |
The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one. If this is true, then we use a core-based approach (like in max-SAT) when we try to increase the lower bound instead.
optional bool optimize_with_core = 83 [default = false];
- Parameters
-
value The optimizeWithCore to set.
- Returns
- This builder for chaining.
Definition at line 17100 of file SatParameters.java.
◆ setOptimizeWithMaxHs()
|
inline |
This has no effect if optimize_with_core is false. If true, use a different core-based algorithm similar to the max-HS algo for max-SAT. This is a hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT one. This is also related to the PhD work of tobyodavies@ "Automatic Logic-Based Benders Decomposition with MiniZinc" http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489
optional bool optimize_with_max_hs = 85 [default = false];
- Parameters
-
value The optimizeWithMaxHs to set.
- Returns
- This builder for chaining.
Definition at line 17240 of file SatParameters.java.
◆ setPbCleanupIncrement()
|
inline |
Same as for the clauses, but for the learned pseudo-Boolean constraints.
optional int32 pb_cleanup_increment = 46 [default = 200];
- Parameters
-
value The pbCleanupIncrement to set.
- Returns
- This builder for chaining.
Definition at line 11533 of file SatParameters.java.
◆ setPbCleanupRatio()
|
inline |
optional double pb_cleanup_ratio = 47 [default = 0.5];
- Parameters
-
value The pbCleanupRatio to set.
- Returns
- This builder for chaining.
Definition at line 11576 of file SatParameters.java.
◆ setPreferredVariableOrder()
|
inline |
optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
- Parameters
-
value The preferredVariableOrder to set.
- Returns
- This builder for chaining.
Definition at line 10606 of file SatParameters.java.
◆ setPresolveBlockedClause()
|
inline |
Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.
optional bool presolve_blocked_clause = 88 [default = true];
- Parameters
-
value The presolveBlockedClause to set.
- Returns
- This builder for chaining.
Definition at line 13828 of file SatParameters.java.
◆ setPresolveBvaThreshold()
|
inline |
Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold. The algorithm described in the paper uses 0, but quick experiments showed that 1 is a good value. It may not be worth it to add a new variable just to remove one clause.
optional int32 presolve_bva_threshold = 73 [default = 1];
- Parameters
-
value The presolveBvaThreshold to set.
- Returns
- This builder for chaining.
Definition at line 13948 of file SatParameters.java.
◆ setPresolveBveClauseWeight()
|
inline |
During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.
optional int32 presolve_bve_clause_weight = 55 [default = 3];
- Parameters
-
value The presolveBveClauseWeight to set.
- Returns
- This builder for chaining.
Definition at line 13710 of file SatParameters.java.
◆ setPresolveBveThreshold()
|
inline |
During presolve, only try to perform the bounded variable elimination (BVE) of a variable x if the number of occurrences of x times the number of occurrences of not(x) is not greater than this parameter.
optional int32 presolve_bve_threshold = 54 [default = 500];
- Parameters
-
value The presolveBveThreshold to set.
- Returns
- This builder for chaining.
Definition at line 13650 of file SatParameters.java.
◆ setPresolveProbingDeterministicTimeLimit()
|
inline |
The maximum "deterministic" time limit to spend in probing. A value of zero will disable the probing.
optional double presolve_probing_deterministic_time_limit = 57 [default = 30];
- Parameters
-
value The presolveProbingDeterministicTimeLimit to set.
- Returns
- This builder for chaining.
Definition at line 13769 of file SatParameters.java.
◆ setPresolveSubstitutionLevel()
|
inline |
How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve. This currently only concerns variable appearing only in linear constraints. For now the value 0 turns it off and any positive value performs substitution.
optional int32 presolve_substitution_level = 147 [default = 1];
- Parameters
-
value The presolveSubstitutionLevel to set.
- Returns
- This builder for chaining.
Definition at line 14691 of file SatParameters.java.
◆ setPresolveUseBva()
|
inline |
Whether or not we use Bounded Variable Addition (BVA) in the presolve.
optional bool presolve_use_bva = 72 [default = true];
- Parameters
-
value The presolveUseBva to set.
- Returns
- This builder for chaining.
Definition at line 13884 of file SatParameters.java.
◆ setProbingPeriodAtRoot()
|
inline |
If set at zero (the default), it is disabled. Otherwise the solver attempts probing at every 'probing_period' root node. Period of 1 enables probing at every root node.
optional int64 probing_period_at_root = 142 [default = 0];
- Parameters
-
value The probingPeriodAtRoot to set.
- Returns
- This builder for chaining.
Definition at line 16975 of file SatParameters.java.
◆ setPseudoCostReliabilityThreshold()
|
inline |
The solver ignores the pseudo costs of variables with number of recordings less than this threshold.
optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
- Parameters
-
value The pseudoCostReliabilityThreshold to set.
- Returns
- This builder for chaining.
Definition at line 17035 of file SatParameters.java.
◆ setRandomBranchesRatio()
|
inline |
A number between 0 and 1 that indicates the proportion of branching variables that are selected randomly instead of choosing the first variable from the given variable_ordering strategy.
optional double random_branches_ratio = 32 [default = 0];
- Parameters
-
value The randomBranchesRatio to set.
- Returns
- This builder for chaining.
Definition at line 10859 of file SatParameters.java.
◆ setRandomizeSearch()
|
inline |
Randomize fixed search.
optional bool randomize_search = 103 [default = false];
- Parameters
-
value The randomizeSearch to set.
- Returns
- This builder for chaining.
Definition at line 18354 of file SatParameters.java.
◆ setRandomPolarityRatio()
|
inline |
The proportion of polarity chosen at random. Note that this take precedence over the phase saving heuristic. This is different from initial_polarity:POLARITY_RANDOM because it will select a new random polarity each time the variable is branched upon instead of selecting one initially and then always taking this choice.
optional double random_polarity_ratio = 45 [default = 0];
- Parameters
-
value The randomPolarityRatio to set.
- Returns
- This builder for chaining.
Definition at line 10794 of file SatParameters.java.
◆ setRandomSeed()
|
inline |
At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed. If you change the random seed, the solver may make different choices during the solving process. For some problems, the running time may vary a lot depending on small change in the solving algorithm. Running the solver with different seeds enables to have more robust benchmarks when evaluating new features.
optional int32 random_seed = 31 [default = 1];
- Parameters
-
value The randomSeed to set.
- Returns
- This builder for chaining.
Definition at line 13312 of file SatParameters.java.
◆ setReduceMemoryUsageInInterleaveMode()
|
inline |
Temporary parameter until the memory usage is more optimized.
optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];
- Parameters
-
value The reduceMemoryUsageInInterleaveMode to set.
- Returns
- This builder for chaining.
Definition at line 17871 of file SatParameters.java.
◆ setRelativeGapLimit()
|
inline |
optional double relative_gap_limit = 160 [default = 0];
- Parameters
-
value The relativeGapLimit to set.
- Returns
- This builder for chaining.
Definition at line 13183 of file SatParameters.java.
◆ setRepeatedField()
|
inline |
Definition at line 10094 of file SatParameters.java.
◆ setRestartAlgorithms()
|
inline |
The restart strategies will change each time the strategy_counter is increased. The current strategy will simply be the one at index strategy_counter modulo the number of strategy. Note that if this list includes a NO_RESTART, nothing will change when it is reached because the strategy_counter will only increment after a restart. The idea of switching of search strategy tailored for SAT/UNSAT comes from Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/. But more generally, it seems REALLY beneficial to try different strategy.
repeated .operations_research.sat.SatParameters.RestartAlgorithm restart_algorithms = 61;
- Parameters
-
index The index to set the value at. value The restartAlgorithms to set.
- Returns
- This builder for chaining.
Definition at line 12165 of file SatParameters.java.
◆ setRestartDlAverageRatio()
|
inline |
In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.
optional double restart_dl_average_ratio = 63 [default = 1];
- Parameters
-
value The restartDlAverageRatio to set.
- Returns
- This builder for chaining.
Definition at line 12482 of file SatParameters.java.
◆ setRestartLbdAverageRatio()
|
inline |
optional double restart_lbd_average_ratio = 71 [default = 1];
- Parameters
-
value The restartLbdAverageRatio to set.
- Returns
- This builder for chaining.
Definition at line 12526 of file SatParameters.java.
◆ setRestartPeriod()
|
inline |
Restart period for the FIXED_RESTART strategy. This is also the multiplier used by the LUBY_RESTART strategy.
optional int32 restart_period = 30 [default = 50];
- Parameters
-
value The restartPeriod to set.
- Returns
- This builder for chaining.
Definition at line 12368 of file SatParameters.java.
◆ setRestartRunningWindowSize()
|
inline |
Size of the window for the moving average restarts.
optional int32 restart_running_window_size = 62 [default = 50];
- Parameters
-
value The restartRunningWindowSize to set.
- Returns
- This builder for chaining.
Definition at line 12424 of file SatParameters.java.
◆ setSearchBranching()
|
inline |
optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
- Parameters
-
value The searchBranching to set.
- Returns
- This builder for chaining.
Definition at line 16549 of file SatParameters.java.
◆ setSearchRandomizationTolerance()
|
inline |
Search randomization will collect equivalent 'max valued' variables, and pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST, all unassigned variables are equivalent. If the variable strategy is CHOOSE_LOWEST_MIN, and `lm` is the current lowest min of all unassigned variables, then the set of max valued variables will be all unassigned variables where lm <= variable min <= lm + search_randomization_tolerance
optional int64 search_randomization_tolerance = 104 [default = 0];
- Parameters
-
value The searchRandomizationTolerance to set.
- Returns
- This builder for chaining.
Definition at line 18427 of file SatParameters.java.
◆ setShareLevelZeroBounds()
|
inline |
Allows sharing of the bounds of modified variables at level 0.
optional bool share_level_zero_bounds = 114 [default = true];
- Parameters
-
value The shareLevelZeroBounds to set.
- Returns
- This builder for chaining.
Definition at line 17981 of file SatParameters.java.
◆ setShareObjectiveBounds()
|
inline |
Allows objective sharing between workers.
optional bool share_objective_bounds = 113 [default = true];
- Parameters
-
value The shareObjectiveBounds to set.
- Returns
- This builder for chaining.
Definition at line 17926 of file SatParameters.java.
◆ setStopAfterFirstSolution()
|
inline |
For an optimization problem, stop the solver as soon as we have a solution.
optional bool stop_after_first_solution = 98 [default = false];
- Parameters
-
value The stopAfterFirstSolution to set.
- Returns
- This builder for chaining.
Definition at line 17572 of file SatParameters.java.
◆ setStopAfterPresolve()
|
inline |
Mainly used when improving the presolver. When true, stops the solver after the presolve is complete.
optional bool stop_after_presolve = 149 [default = false];
- Parameters
-
value The stopAfterPresolve to set.
- Returns
- This builder for chaining.
Definition at line 17630 of file SatParameters.java.
◆ setStrategyChangeIncreaseRatio()
|
inline |
The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.
optional double strategy_change_increase_ratio = 69 [default = 0];
- Parameters
-
value The strategyChangeIncreaseRatio to set.
- Returns
- This builder for chaining.
Definition at line 12784 of file SatParameters.java.
◆ setSubsumptionDuringConflictAnalysis()
|
inline |
At a really low cost, during the 1-UIP conflict computation, it is easy to detect if some of the involved reasons are subsumed by the current conflict. When this is true, such clauses are detached and later removed from the problem.
optional bool subsumption_during_conflict_analysis = 56 [default = true];
- Parameters
-
value The subsumptionDuringConflictAnalysis to set.
- Returns
- This builder for chaining.
Definition at line 11216 of file SatParameters.java.
◆ setTreatBinaryClausesSeparately()
|
inline |
If true, the binary clauses are treated separately from the others. This should be faster and uses less memory. However it changes the propagation order.
optional bool treat_binary_clauses_separately = 33 [default = true];
- Parameters
-
value The treatBinaryClausesSeparately to set.
- Returns
- This builder for chaining.
Definition at line 13240 of file SatParameters.java.
◆ setUnknownFields()
|
inline |
Definition at line 19195 of file SatParameters.java.
◆ setUseBlockingRestart()
|
inline |
Block a moving restart algorithm if the trail size of the current conflict is greater than the multiplier times the moving average of the trail size at the previous conflicts.
optional bool use_blocking_restart = 64 [default = false];
- Parameters
-
value The useBlockingRestart to set.
- Returns
- This builder for chaining.
Definition at line 12583 of file SatParameters.java.
◆ setUseBranchingInLp()
|
inline |
If true, the solver attemts to generate more info inside lp propagator by branching on some variables if certain criteria are met during the search tree exploration.
optional bool use_branching_in_lp = 139 [default = false];
- Parameters
-
value The useBranchingInLp to set.
- Returns
- This builder for chaining.
Definition at line 18624 of file SatParameters.java.
◆ setUseCombinedNoOverlap()
|
inline |
This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem. Like 1000 intervals, but 1M intervals in the no-overlap constraints covering them.
optional bool use_combined_no_overlap = 133 [default = false];
- Parameters
-
value The useCombinedNoOverlap to set.
- Returns
- This builder for chaining.
Definition at line 18687 of file SatParameters.java.
◆ setUseDisjunctiveConstraintInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with propagators from the disjunctive constraint to improve the inference on a set of tasks that are disjunctive at the root of the problem. This additional level supplements the default level of reasoning. Propagators of the cumulative constraint will not be used at all if all the tasks are disjunctive at root node. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];
- Parameters
-
value The useDisjunctiveConstraintInCumulativeConstraint to set.
- Returns
- This builder for chaining.
Definition at line 15388 of file SatParameters.java.
◆ setUseErwaHeuristic()
|
inline |
Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as described in "Learning Rate Based Branching Heuristic for SAT solvers", J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.
optional bool use_erwa_heuristic = 75 [default = false];
- Parameters
-
value The useErwaHeuristic to set.
- Returns
- This builder for chaining.
Definition at line 10922 of file SatParameters.java.
◆ setUseExactLpReason()
|
inline |
The solver usually exploit the LP relaxation of a model. If this option is true, then whatever is infered by the LP will be used like an heuristic to compute EXACT propagation on the IP. So with this option, there is no numerical imprecision issues.
optional bool use_exact_lp_reason = 109 [default = true];
- Parameters
-
value The useExactLpReason to set.
- Returns
- This builder for chaining.
Definition at line 18560 of file SatParameters.java.
◆ setUseFeasibilityPump()
|
inline |
Adds a feasibility pump subsolver along with lns subsolvers.
optional bool use_feasibility_pump = 164 [default = false];
- Parameters
-
value The useFeasibilityPump to set.
- Returns
- This builder for chaining.
Definition at line 18185 of file SatParameters.java.
◆ setUseImpliedBounds()
|
inline |
Stores and exploits "implied-bounds" in the solver. That is, relations of the form literal => (var >= bound). This is currently used to derive stronger cuts.
optional bool use_implied_bounds = 144 [default = true];
- Parameters
-
value The useImpliedBounds to set.
- Returns
- This builder for chaining.
Definition at line 18813 of file SatParameters.java.
◆ setUseLnsOnly()
|
inline |
LNS parameters.
optional bool use_lns_only = 101 [default = false];
- Parameters
-
value The useLnsOnly to set.
- Returns
- This builder for chaining.
Definition at line 18036 of file SatParameters.java.
◆ setUseOptimizationHints()
|
inline |
For an optimization problem, whether we follow some hints in order to find a better first solution. For a variable with hint, the solver will always try to follow the hint. It will revert to the variable_branching default otherwise.
optional bool use_optimization_hints = 35 [default = true];
- Parameters
-
value The useOptimizationHints to set.
- Returns
- This builder for chaining.
Definition at line 14758 of file SatParameters.java.
◆ setUseOptionalVariables()
|
inline |
If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional. This allows to propagate them as if they were present in some situation.
optional bool use_optional_variables = 108 [default = true];
- Parameters
-
value The useOptionalVariables to set.
- Returns
- This builder for chaining.
Definition at line 18494 of file SatParameters.java.
◆ setUseOverloadCheckerInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy. This additional level supplements the default level of reasoning as well as timetable edge finding. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];
- Parameters
-
value The useOverloadCheckerInCumulativeConstraint to set.
- Returns
- This builder for chaining.
Definition at line 15232 of file SatParameters.java.
◆ setUsePbResolution()
|
inline |
Whether to use pseudo-Boolean resolution to analyze a conflict. Note that this option only make sense if your problem is modelized using pseudo-Boolean constraints. If you only have clauses, this shouldn't change anything (except slow the solver down).
optional bool use_pb_resolution = 43 [default = false];
- Parameters
-
value The usePbResolution to set.
- Returns
- This builder for chaining.
Definition at line 13436 of file SatParameters.java.
◆ setUsePhaseSaving()
|
inline |
If this is true, then the polarity of a variable will be the last value it was assigned to, or its default polarity if it was never assigned since the call to ResetDecisionHeuristic(). This is called 'literal phase saving'. For details see 'A Lightweight Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and A.Darwiche, In 10th International Conference on Theory and Applications of Satisfiability Testing, 2007.
optional bool use_phase_saving = 44 [default = true];
- Parameters
-
value The usePhaseSaving to set.
- Returns
- This builder for chaining.
Definition at line 10721 of file SatParameters.java.
◆ setUsePrecedencesInDisjunctiveConstraint()
|
inline |
When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further. For instance if task A and B are both before C and task A and B are in disjunction, then we can deduce that task C must start after duration(A) + duration(B) instead of simply max(duration(A), duration(B)), provided that the start time for all task was currently zero. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];
- Parameters
-
value The usePrecedencesInDisjunctiveConstraint to set.
- Returns
- This builder for chaining.
Definition at line 15155 of file SatParameters.java.
◆ setUseRelaxationLns()
|
inline |
Turns on a lns worker which solves relaxed version of the original problem by removing constraints from the problem in order to get better bounds.
optional bool use_relaxation_lns = 150 [default = false];
- Parameters
-
value The useRelaxationLns to set.
- Returns
- This builder for chaining.
Definition at line 18243 of file SatParameters.java.
◆ setUseRinsLns()
|
inline |
Turns on relaxation induced neighborhood generator.
optional bool use_rins_lns = 129 [default = true];
- Parameters
-
value The useRinsLns to set.
- Returns
- This builder for chaining.
Definition at line 18130 of file SatParameters.java.
◆ setUseSatInprocessing()
|
inline |
optional bool use_sat_inprocessing = 163 [default = false];
- Parameters
-
value The useSatInprocessing to set.
- Returns
- This builder for chaining.
Definition at line 14348 of file SatParameters.java.
◆ setUseTimetableEdgeFindingInCumulativeConstraint()
|
inline |
When this is true, the cumulative constraint is reinforced with timetable edge finding, i.e., an additional level of reasoning based on the conjunction of energy and mandatory parts. This additional level supplements the default level of reasoning as well as overload_checker. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.
optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];
- Parameters
-
value The useTimetableEdgeFindingInCumulativeConstraint to set.
- Returns
- This builder for chaining.
Definition at line 15307 of file SatParameters.java.
◆ setVariableActivityDecay()
|
inline |
Each time a conflict is found, the activities of some variables are increased by one. Then, the activity of all variables are multiplied by variable_activity_decay. To implement this efficiently, the activity of all the variables is not decayed at each conflict. Instead, the activity increment is multiplied by 1 / decay. When an activity reach max_variable_activity_value, all the activity are multiplied by 1 / max_variable_activity_value.
optional double variable_activity_decay = 15 [default = 0.8];
- Parameters
-
value The variableActivityDecay to set.
- Returns
- This builder for chaining.
Definition at line 11779 of file SatParameters.java.
The documentation for this class was generated from the following file: