sat

package
v0.0.0-...-7c7d34b Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Apr 15, 2024 License: Apache-2.0 Imports: 5 Imported by: 0

Documentation

Index

Constants

View Source 
const (
	Default_SatParameters_Name                                           = string("")
	Default_SatParameters_PreferredVariableOrder                         = SatParameters_IN_ORDER
	Default_SatParameters_InitialPolarity                                = SatParameters_POLARITY_FALSE
	Default_SatParameters_UsePhaseSaving                                 = bool(true)
	Default_SatParameters_PolarityRephaseIncrement                       = int32(1000)
	Default_SatParameters_RandomPolarityRatio                            = float64(0)
	Default_SatParameters_RandomBranchesRatio                            = float64(0)
	Default_SatParameters_UseErwaHeuristic                               = bool(false)
	Default_SatParameters_InitialVariablesActivity                       = float64(0)
	Default_SatParameters_AlsoBumpVariablesInConflictReasons             = bool(false)
	Default_SatParameters_MinimizationAlgorithm                          = SatParameters_RECURSIVE
	Default_SatParameters_BinaryMinimizationAlgorithm                    = SatParameters_BINARY_MINIMIZATION_FIRST
	Default_SatParameters_SubsumptionDuringConflictAnalysis              = bool(true)
	Default_SatParameters_ClauseCleanupPeriod                            = int32(10000)
	Default_SatParameters_ClauseCleanupTarget                            = int32(0)
	Default_SatParameters_ClauseCleanupRatio                             = float64(0.5)
	Default_SatParameters_ClauseCleanupProtection                        = SatParameters_PROTECTION_NONE
	Default_SatParameters_ClauseCleanupLbdBound                          = int32(5)
	Default_SatParameters_ClauseCleanupOrdering                          = SatParameters_CLAUSE_ACTIVITY
	Default_SatParameters_PbCleanupIncrement                             = int32(200)
	Default_SatParameters_PbCleanupRatio                                 = float64(0.5)
	Default_SatParameters_VariableActivityDecay                          = float64(0.8)
	Default_SatParameters_MaxVariableActivityValue                       = float64(1e+100)
	Default_SatParameters_GlucoseMaxDecay                                = float64(0.95)
	Default_SatParameters_GlucoseDecayIncrement                          = float64(0.01)
	Default_SatParameters_GlucoseDecayIncrementPeriod                    = int32(5000)
	Default_SatParameters_ClauseActivityDecay                            = float64(0.999)
	Default_SatParameters_MaxClauseActivityValue                         = float64(1e+20)
	Default_SatParameters_DefaultRestartAlgorithms                       = string("LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART")
	Default_SatParameters_RestartPeriod                                  = int32(50)
	Default_SatParameters_RestartRunningWindowSize                       = int32(50)
	Default_SatParameters_RestartDlAverageRatio                          = float64(1)
	Default_SatParameters_RestartLbdAverageRatio                         = float64(1)
	Default_SatParameters_UseBlockingRestart                             = bool(false)
	Default_SatParameters_BlockingRestartWindowSize                      = int32(5000)
	Default_SatParameters_BlockingRestartMultiplier                      = float64(1.4)
	Default_SatParameters_NumConflictsBeforeStrategyChanges              = int32(0)
	Default_SatParameters_StrategyChangeIncreaseRatio                    = float64(0)
	Default_SatParameters_MaxNumberOfConflicts                           = int64(9223372036854775807)
	Default_SatParameters_MaxMemoryInMb                                  = int64(10000)
	Default_SatParameters_AbsoluteGapLimit                               = float64(0.0001)
	Default_SatParameters_RelativeGapLimit                               = float64(0)
	Default_SatParameters_RandomSeed                                     = int32(1)
	Default_SatParameters_PermuteVariableRandomly                        = bool(false)
	Default_SatParameters_PermutePresolveConstraintOrder                 = bool(false)
	Default_SatParameters_UseAbslRandom                                  = bool(false)
	Default_SatParameters_LogSearchProgress                              = bool(false)
	Default_SatParameters_LogSubsolverStatistics                         = bool(false)
	Default_SatParameters_LogPrefix                                      = string("")
	Default_SatParameters_LogToStdout                                    = bool(true)
	Default_SatParameters_LogToResponse                                  = bool(false)
	Default_SatParameters_UsePbResolution                                = bool(false)
	Default_SatParameters_MinimizeReductionDuringPbResolution            = bool(false)
	Default_SatParameters_CountAssumptionLevelsInLbd                     = bool(true)
	Default_SatParameters_PresolveBveThreshold                           = int32(500)
	Default_SatParameters_PresolveBveClauseWeight                        = int32(3)
	Default_SatParameters_ProbingDeterministicTimeLimit                  = float64(1)
	Default_SatParameters_PresolveProbingDeterministicTimeLimit          = float64(30)
	Default_SatParameters_PresolveBlockedClause                          = bool(true)
	Default_SatParameters_PresolveUseBva                                 = bool(true)
	Default_SatParameters_PresolveBvaThreshold                           = int32(1)
	Default_SatParameters_MaxPresolveIterations                          = int32(3)
	Default_SatParameters_CpModelPresolve                                = bool(true)
	Default_SatParameters_CpModelProbingLevel                            = int32(2)
	Default_SatParameters_CpModelUseSatPresolve                          = bool(true)
	Default_SatParameters_DetectTableWithCost                            = bool(false)
	Default_SatParameters_TableCompressionLevel                          = int32(2)
	Default_SatParameters_ExpandAlldiffConstraints                       = bool(false)
	Default_SatParameters_ExpandReservoirConstraints                     = bool(true)
	Default_SatParameters_DisableConstraintExpansion                     = bool(false)
	Default_SatParameters_EncodeComplexLinearConstraintWithInteger       = bool(false)
	Default_SatParameters_MergeNoOverlapWorkLimit                        = float64(1e+12)
	Default_SatParameters_MergeAtMostOneWorkLimit                        = float64(1e+08)
	Default_SatParameters_PresolveSubstitutionLevel                      = int32(1)
	Default_SatParameters_PresolveExtractIntegerEnforcement              = bool(false)
	Default_SatParameters_PresolveInclusionWorkLimit                     = int64(100000000)
	Default_SatParameters_IgnoreNames                                    = bool(true)
	Default_SatParameters_InferAllDiffs                                  = bool(true)
	Default_SatParameters_FindBigLinearOverlap                           = bool(true)
	Default_SatParameters_UseSatInprocessing                             = bool(true)
	Default_SatParameters_InprocessingDtimeRatio                         = float64(0.2)
	Default_SatParameters_InprocessingProbingDtime                       = float64(1)
	Default_SatParameters_InprocessingMinimizationDtime                  = float64(1)
	Default_SatParameters_NumWorkers                                     = int32(0)
	Default_SatParameters_NumSearchWorkers                               = int32(0)
	Default_SatParameters_MinNumLnsWorkers                               = int32(2)
	Default_SatParameters_InterleaveSearch                               = bool(false)
	Default_SatParameters_InterleaveBatchSize                            = int32(0)
	Default_SatParameters_ShareObjectiveBounds                           = bool(true)
	Default_SatParameters_ShareLevelZeroBounds                           = bool(true)
	Default_SatParameters_ShareBinaryClauses                             = bool(true)
	Default_SatParameters_DebugPostsolveWithFullSolver                   = bool(false)
	Default_SatParameters_DebugMaxNumPresolveOperations                  = int32(0)
	Default_SatParameters_DebugCrashOnBadHint                            = bool(false)
	Default_SatParameters_UseOptimizationHints                           = bool(true)
	Default_SatParameters_CoreMinimizationLevel                          = int32(2)
	Default_SatParameters_FindMultipleCores                              = bool(true)
	Default_SatParameters_CoverOptimization                              = bool(true)
	Default_SatParameters_MaxSatAssumptionOrder                          = SatParameters_DEFAULT_ASSUMPTION_ORDER
	Default_SatParameters_MaxSatReverseAssumptionOrder                   = bool(false)
	Default_SatParameters_MaxSatStratification                           = SatParameters_STRATIFICATION_DESCENT
	Default_SatParameters_PropagationLoopDetectionFactor                 = float64(10)
	Default_SatParameters_UsePrecedencesInDisjunctiveConstraint          = bool(true)
	Default_SatParameters_MaxSizeToCreatePrecedenceLiteralsInDisjunctive = int32(60)
	Default_SatParameters_UseStrongPropagationInDisjunctive              = bool(false)
	Default_SatParameters_UseDynamicPrecedenceInDisjunctive              = bool(false)
	Default_SatParameters_UseDynamicPrecedenceInCumulative               = bool(false)
	Default_SatParameters_UseOverloadCheckerInCumulative                 = bool(false)
	Default_SatParameters_UseTimetableEdgeFindingInCumulative            = bool(false)
	Default_SatParameters_MaxNumIntervalsForTimetableEdgeFinding         = int32(100)
	Default_SatParameters_UseHardPrecedencesInCumulative                 = bool(false)
	Default_SatParameters_ExploitAllPrecedences                          = bool(false)
	Default_SatParameters_UseDisjunctiveConstraintInCumulative           = bool(true)
	Default_SatParameters_UseTimetablingInNoOverlap_2D                   = bool(false)
	Default_SatParameters_UseEnergeticReasoningInNoOverlap_2D            = bool(false)
	Default_SatParameters_UseAreaEnergeticReasoningInNoOverlap_2D        = bool(false)
	Default_SatParameters_MaxPairsPairwiseReasoningInNoOverlap_2D        = int32(1250)
	Default_SatParameters_UseDualSchedulingHeuristics                    = bool(true)
	Default_SatParameters_SearchBranching                                = SatParameters_AUTOMATIC_SEARCH
	Default_SatParameters_HintConflictLimit                              = int32(10)
	Default_SatParameters_RepairHint                                     = bool(false)
	Default_SatParameters_FixVariablesToTheirHintedValue                 = bool(false)
	Default_SatParameters_UseProbingSearch                               = bool(false)
	Default_SatParameters_UseExtendedProbing                             = bool(true)
	Default_SatParameters_ProbingNumCombinationsLimit                    = int32(20000)
	Default_SatParameters_UseShavingInProbingSearch                      = bool(true)
	Default_SatParameters_ShavingSearchDeterministicTime                 = float64(0.001)
	Default_SatParameters_UseObjectiveLbSearch                           = bool(false)
	Default_SatParameters_UseObjectiveShavingSearch                      = bool(false)
	Default_SatParameters_PseudoCostReliabilityThreshold                 = int64(100)
	Default_SatParameters_OptimizeWithCore                               = bool(false)
	Default_SatParameters_OptimizeWithLbTreeSearch                       = bool(false)
	Default_SatParameters_BinarySearchNumConflicts                       = int32(-1)
	Default_SatParameters_OptimizeWithMaxHs                              = bool(false)
	Default_SatParameters_UseFeasibilityJump                             = bool(true)
	Default_SatParameters_TestFeasibilityJump                            = bool(false)
	Default_SatParameters_FeasibilityJumpDecay                           = float64(0.95)
	Default_SatParameters_FeasibilityJumpLinearizationLevel              = int32(2)
	Default_SatParameters_FeasibilityJumpRestartFactor                   = int32(1)
	Default_SatParameters_FeasibilityJumpVarRandomizationProbability     = float64(0)
	Default_SatParameters_FeasibilityJumpVarPerburbationRangeRatio       = float64(0.2)
	Default_SatParameters_FeasibilityJumpEnableRestarts                  = bool(true)
	Default_SatParameters_FeasibilityJumpMaxExpandedConstraintSize       = int32(100)
	Default_SatParameters_NumViolationLs                                 = int32(0)
	Default_SatParameters_ViolationLsPerturbationPeriod                  = int32(100)
	Default_SatParameters_ViolationLsCompoundMoveProbability             = float64(0.5)
	Default_SatParameters_SharedTreeNumWorkers                           = int32(0)
	Default_SatParameters_UseSharedTreeSearch                            = bool(false)
	Default_SatParameters_SharedTreeWorkerObjectiveSplitProbability      = float64(0.5)
	Default_SatParameters_SharedTreeMaxNodesPerWorker                    = int32(128)
	Default_SatParameters_SharedTreeSplitStrategy                        = SatParameters_SPLIT_STRATEGY_AUTO
	Default_SatParameters_EnumerateAllSolutions                          = bool(false)
	Default_SatParameters_KeepAllFeasibleSolutionsInPresolve             = bool(false)
	Default_SatParameters_FillTightenedDomainsInResponse                 = bool(false)
	Default_SatParameters_FillAdditionalSolutionsInResponse              = bool(false)
	Default_SatParameters_InstantiateAllVariables                        = bool(true)
	Default_SatParameters_AutoDetectGreaterThanAtLeastOneOf              = bool(true)
	Default_SatParameters_StopAfterFirstSolution                         = bool(false)
	Default_SatParameters_StopAfterPresolve                              = bool(false)
	Default_SatParameters_StopAfterRootPropagation                       = bool(false)
	Default_SatParameters_UseLnsOnly                                     = bool(false)
	Default_SatParameters_SolutionPoolSize                               = int32(3)
	Default_SatParameters_UseRinsLns                                     = bool(true)
	Default_SatParameters_UseFeasibilityPump                             = bool(true)
	Default_SatParameters_UseLbRelaxLns                                  = bool(false)
	Default_SatParameters_FpRounding                                     = SatParameters_PROPAGATION_ASSISTED
	Default_SatParameters_DiversifyLnsParams                             = bool(false)
	Default_SatParameters_RandomizeSearch                                = bool(false)
	Default_SatParameters_SearchRandomVariablePoolSize                   = int64(0)
	Default_SatParameters_PushAllTasksTowardStart                        = bool(false)
	Default_SatParameters_UseOptionalVariables                           = bool(false)
	Default_SatParameters_UseExactLpReason                               = bool(true)
	Default_SatParameters_UseCombinedNoOverlap                           = bool(false)
	Default_SatParameters_AtMostOneMaxExpansionSize                      = int32(3)
	Default_SatParameters_CatchSigintSignal                              = bool(true)
	Default_SatParameters_UseImpliedBounds                               = bool(true)
	Default_SatParameters_PolishLpSolution                               = bool(false)
	Default_SatParameters_LpPrimalTolerance                              = float64(1e-07)
	Default_SatParameters_LpDualTolerance                                = float64(1e-07)
	Default_SatParameters_ConvertIntervals                               = bool(true)
	Default_SatParameters_SymmetryLevel                                  = int32(2)
	Default_SatParameters_NewLinearPropagation                           = bool(false)
	Default_SatParameters_LinearSplitSize                                = int32(100)
	Default_SatParameters_LinearizationLevel                             = int32(1)
	Default_SatParameters_BooleanEncodingLevel                           = int32(1)
	Default_SatParameters_MaxDomainSizeWhenEncodingEqNeqConstraints      = int32(16)
	Default_SatParameters_MaxNumCuts                                     = int32(10000)
	Default_SatParameters_CutLevel                                       = int32(1)
	Default_SatParameters_OnlyAddCutsAtLevelZero                         = bool(false)
	Default_SatParameters_AddObjectiveCut                                = bool(false)
	Default_SatParameters_AddCgCuts                                      = bool(true)
	Default_SatParameters_AddMirCuts                                     = bool(true)
	Default_SatParameters_AddZeroHalfCuts                                = bool(true)
	Default_SatParameters_AddCliqueCuts                                  = bool(true)
	Default_SatParameters_AddRltCuts                                     = bool(true)
	Default_SatParameters_MaxAllDiffCutSize                              = int32(64)
	Default_SatParameters_AddLinMaxCuts                                  = bool(true)
	Default_SatParameters_MaxIntegerRoundingScaling                      = int32(600)
	Default_SatParameters_AddLpConstraintsLazily                         = bool(true)
	Default_SatParameters_RootLpIterations                               = int32(2000)
	Default_SatParameters_MinOrthogonalityForLpConstraints               = float64(0.05)
	Default_SatParameters_MaxCutRoundsAtLevelZero                        = int32(1)
	Default_SatParameters_MaxConsecutiveInactiveCount                    = int32(100)
	Default_SatParameters_CutMaxActiveCountValue                         = float64(1e+10)
	Default_SatParameters_CutActiveCountDecay                            = float64(0.8)
	Default_SatParameters_CutCleanupTarget                               = int32(1000)
	Default_SatParameters_NewConstraintsBatchSize                        = int32(50)
	Default_SatParameters_ExploitIntegerLpSolution                       = bool(true)
	Default_SatParameters_ExploitAllLpSolution                           = bool(true)
	Default_SatParameters_ExploitBestSolution                            = bool(false)
	Default_SatParameters_ExploitRelaxationSolution                      = bool(false)
	Default_SatParameters_ExploitObjective                               = bool(true)
	Default_SatParameters_DetectLinearizedProduct                        = bool(false)
	Default_SatParameters_MipMaxBound                                    = float64(1e+07)
	Default_SatParameters_MipVarScaling                                  = float64(1)
	Default_SatParameters_MipScaleLargeDomain                            = bool(false)
	Default_SatParameters_MipAutomaticallyScaleVariables                 = bool(true)
	Default_SatParameters_OnlySolveIp                                    = bool(false)
	Default_SatParameters_MipWantedPrecision                             = float64(1e-06)
	Default_SatParameters_MipMaxActivityExponent                         = int32(53)
	Default_SatParameters_MipCheckPrecision                              = float64(0.0001)
	Default_SatParameters_MipComputeTrueObjectiveBound                   = bool(true)
	Default_SatParameters_MipMaxValidMagnitude                           = float64(1e+20)
	Default_SatParameters_MipTreatHighMagnitudeBoundsAsInfinity          = bool(false)
	Default_SatParameters_MipDropTolerance                               = float64(1e-16)
	Default_SatParameters_MipPresolveLevel                               = int32(2)
)

Default values for SatParameters fields.

Variables

View Source 
var (
	SatParameters_VariableOrder_name = map[int32]string{
		0: "IN_ORDER",
		1: "IN_REVERSE_ORDER",
		2: "IN_RANDOM_ORDER",
	}
	SatParameters_VariableOrder_value = map[string]int32{
		"IN_ORDER":         0,
		"IN_REVERSE_ORDER": 1,
		"IN_RANDOM_ORDER":  2,
	}
)

Enum value maps for SatParameters_VariableOrder.

View Source 
var (
	SatParameters_Polarity_name = map[int32]string{
		0: "POLARITY_TRUE",
		1: "POLARITY_FALSE",
		2: "POLARITY_RANDOM",
	}
	SatParameters_Polarity_value = map[string]int32{
		"POLARITY_TRUE":   0,
		"POLARITY_FALSE":  1,
		"POLARITY_RANDOM": 2,
	}
)

Enum value maps for SatParameters_Polarity.

View Source 
var (
	SatParameters_ConflictMinimizationAlgorithm_name = map[int32]string{
		0: "NONE",
		1: "SIMPLE",
		2: "RECURSIVE",
		3: "EXPERIMENTAL",
	}
	SatParameters_ConflictMinimizationAlgorithm_value = map[string]int32{
		"NONE":         0,
		"SIMPLE":       1,
		"RECURSIVE":    2,
		"EXPERIMENTAL": 3,
	}
)

Enum value maps for SatParameters_ConflictMinimizationAlgorithm.

View Source 
var (
	SatParameters_BinaryMinizationAlgorithm_name = map[int32]string{
		0: "NO_BINARY_MINIMIZATION",
		1: "BINARY_MINIMIZATION_FIRST",
		4: "BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION",
		2: "BINARY_MINIMIZATION_WITH_REACHABILITY",
		3: "EXPERIMENTAL_BINARY_MINIMIZATION",
	}
	SatParameters_BinaryMinizationAlgorithm_value = map[string]int32{
		"NO_BINARY_MINIMIZATION":                              0,
		"BINARY_MINIMIZATION_FIRST":                           1,
		"BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION": 4,
		"BINARY_MINIMIZATION_WITH_REACHABILITY":               2,
		"EXPERIMENTAL_BINARY_MINIMIZATION":                    3,
	}
)

Enum value maps for SatParameters_BinaryMinizationAlgorithm.

View Source 
var (
	SatParameters_ClauseProtection_name = map[int32]string{
		0: "PROTECTION_NONE",
		1: "PROTECTION_ALWAYS",
		2: "PROTECTION_LBD",
	}
	SatParameters_ClauseProtection_value = map[string]int32{
		"PROTECTION_NONE":   0,
		"PROTECTION_ALWAYS": 1,
		"PROTECTION_LBD":    2,
	}
)

Enum value maps for SatParameters_ClauseProtection.

View Source 
var (
	SatParameters_ClauseOrdering_name = map[int32]string{
		0: "CLAUSE_ACTIVITY",
		1: "CLAUSE_LBD",
	}
	SatParameters_ClauseOrdering_value = map[string]int32{
		"CLAUSE_ACTIVITY": 0,
		"CLAUSE_LBD":      1,
	}
)

Enum value maps for SatParameters_ClauseOrdering.

View Source 
var (
	SatParameters_RestartAlgorithm_name = map[int32]string{
		0: "NO_RESTART",
		1: "LUBY_RESTART",
		2: "DL_MOVING_AVERAGE_RESTART",
		3: "LBD_MOVING_AVERAGE_RESTART",
		4: "FIXED_RESTART",
	}
	SatParameters_RestartAlgorithm_value = map[string]int32{
		"NO_RESTART":                 0,
		"LUBY_RESTART":               1,
		"DL_MOVING_AVERAGE_RESTART":  2,
		"LBD_MOVING_AVERAGE_RESTART": 3,
		"FIXED_RESTART":              4,
	}
)

Enum value maps for SatParameters_RestartAlgorithm.

View Source 
var (
	SatParameters_MaxSatAssumptionOrder_name = map[int32]string{
		0: "DEFAULT_ASSUMPTION_ORDER",
		1: "ORDER_ASSUMPTION_BY_DEPTH",
		2: "ORDER_ASSUMPTION_BY_WEIGHT",
	}
	SatParameters_MaxSatAssumptionOrder_value = map[string]int32{
		"DEFAULT_ASSUMPTION_ORDER":   0,
		"ORDER_ASSUMPTION_BY_DEPTH":  1,
		"ORDER_ASSUMPTION_BY_WEIGHT": 2,
	}
)

Enum value maps for SatParameters_MaxSatAssumptionOrder.

View Source 
var (
	SatParameters_MaxSatStratificationAlgorithm_name = map[int32]string{
		0: "STRATIFICATION_NONE",
		1: "STRATIFICATION_DESCENT",
		2: "STRATIFICATION_ASCENT",
	}
	SatParameters_MaxSatStratificationAlgorithm_value = map[string]int32{
		"STRATIFICATION_NONE":    0,
		"STRATIFICATION_DESCENT": 1,
		"STRATIFICATION_ASCENT":  2,
	}
)

Enum value maps for SatParameters_MaxSatStratificationAlgorithm.

View Source 
var (
	SatParameters_SearchBranching_name = map[int32]string{
		0: "AUTOMATIC_SEARCH",
		1: "FIXED_SEARCH",
		2: "PORTFOLIO_SEARCH",
		3: "LP_SEARCH",
		4: "PSEUDO_COST_SEARCH",
		5: "PORTFOLIO_WITH_QUICK_RESTART_SEARCH",
		6: "HINT_SEARCH",
		7: "PARTIAL_FIXED_SEARCH",
		8: "RANDOMIZED_SEARCH",
	}
	SatParameters_SearchBranching_value = map[string]int32{
		"AUTOMATIC_SEARCH":                    0,
		"FIXED_SEARCH":                        1,
		"PORTFOLIO_SEARCH":                    2,
		"LP_SEARCH":                           3,
		"PSEUDO_COST_SEARCH":                  4,
		"PORTFOLIO_WITH_QUICK_RESTART_SEARCH": 5,
		"HINT_SEARCH":                         6,
		"PARTIAL_FIXED_SEARCH":                7,
		"RANDOMIZED_SEARCH":                   8,
	}
)

Enum value maps for SatParameters_SearchBranching.

View Source 
var (
	SatParameters_SharedTreeSplitStrategy_name = map[int32]string{
		0: "SPLIT_STRATEGY_AUTO",
		1: "SPLIT_STRATEGY_DISCREPANCY",
		2: "SPLIT_STRATEGY_OBJECTIVE_LB",
		3: "SPLIT_STRATEGY_BALANCED_TREE",
		4: "SPLIT_STRATEGY_FIRST_PROPOSAL",
	}
	SatParameters_SharedTreeSplitStrategy_value = map[string]int32{
		"SPLIT_STRATEGY_AUTO":           0,
		"SPLIT_STRATEGY_DISCREPANCY":    1,
		"SPLIT_STRATEGY_OBJECTIVE_LB":   2,
		"SPLIT_STRATEGY_BALANCED_TREE":  3,
		"SPLIT_STRATEGY_FIRST_PROPOSAL": 4,
	}
)

Enum value maps for SatParameters_SharedTreeSplitStrategy.

View Source 
var (
	SatParameters_FPRoundingMethod_name = map[int32]string{
		0: "NEAREST_INTEGER",
		1: "LOCK_BASED",
		3: "ACTIVE_LOCK_BASED",
		2: "PROPAGATION_ASSISTED",
	}
	SatParameters_FPRoundingMethod_value = map[string]int32{
		"NEAREST_INTEGER":      0,
		"LOCK_BASED":           1,
		"ACTIVE_LOCK_BASED":    3,
		"PROPAGATION_ASSISTED": 2,
	}
)

Enum value maps for SatParameters_FPRoundingMethod.

View Source 
var (
	Default_SatParameters_MaxTimeInSeconds     = float64(math.Inf(+1))
	Default_SatParameters_MaxDeterministicTime = float64(math.Inf(+1))
)

Default values for SatParameters fields.

View Source 
var File_ortools_sat_sat_parameters_proto protoreflect.FileDescriptor

Functions

This section is empty.

Types

type SatParameters 

type SatParameters struct {

	// In some context, like in a portfolio of search, it makes sense to name a
	// given parameters set for logging purpose.
	Name                   *string                      `protobuf:"bytes,171,opt,name=name,def=" json:"name,omitempty"`
	PreferredVariableOrder *SatParameters_VariableOrder `` /* 186-byte string literal not displayed */
	InitialPolarity        *SatParameters_Polarity      `` /* 158-byte string literal not displayed */
	// If this is true, then the polarity of a variable will be the last value it
	// was assigned to, or its default polarity if it was never assigned since the
	// call to ResetDecisionHeuristic().
	//
	// Actually, we use a newer version where we follow the last value in the
	// longest non-conflicting partial assignment in the current phase.
	//
	// This is called 'literal phase saving'. For details see 'A Lightweight
	// Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and
	// A.Darwiche, In 10th International Conference on Theory and Applications of
	// Satisfiability Testing, 2007.
	UsePhaseSaving *bool `protobuf:"varint,44,opt,name=use_phase_saving,json=usePhaseSaving,def=1" json:"use_phase_saving,omitempty"`
	// If non-zero, then we change the polarity heuristic after that many number
	// of conflicts in an arithmetically increasing fashion. So x the first time,
	// 2 * x the second time, etc...
	PolarityRephaseIncrement *int32 `` /* 140-byte string literal not displayed */
	// 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.
	RandomPolarityRatio *float64 `protobuf:"fixed64,45,opt,name=random_polarity_ratio,json=randomPolarityRatio,def=0" json:"random_polarity_ratio,omitempty"`
	// 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.
	RandomBranchesRatio *float64 `protobuf:"fixed64,32,opt,name=random_branches_ratio,json=randomBranchesRatio,def=0" json:"random_branches_ratio,omitempty"`
	// 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.
	UseErwaHeuristic *bool `protobuf:"varint,75,opt,name=use_erwa_heuristic,json=useErwaHeuristic,def=0" json:"use_erwa_heuristic,omitempty"`
	// 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.
	InitialVariablesActivity *float64 `` /* 137-byte string literal not displayed */
	// 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.
	AlsoBumpVariablesInConflictReasons *bool                                        `` /* 172-byte string literal not displayed */
	MinimizationAlgorithm              *SatParameters_ConflictMinimizationAlgorithm `` /* 197-byte string literal not displayed */
	BinaryMinimizationAlgorithm        *SatParameters_BinaryMinizationAlgorithm     `` /* 214-byte string literal not displayed */
	// 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.
	SubsumptionDuringConflictAnalysis *bool `` /* 165-byte string literal not displayed */
	// Trigger a cleanup when this number of "deletable" clauses is learned.
	ClauseCleanupPeriod *int32 `protobuf:"varint,11,opt,name=clause_cleanup_period,json=clauseCleanupPeriod,def=10000" json:"clause_cleanup_period,omitempty"`
	// During a cleanup, we will always keep that number of "deletable" clauses.
	// Note that this doesn't include the "protected" clauses.
	ClauseCleanupTarget *int32 `protobuf:"varint,13,opt,name=clause_cleanup_target,json=clauseCleanupTarget,def=0" json:"clause_cleanup_target,omitempty"`
	// During a cleanup, if clause_cleanup_target is 0, we will delete the
	// clause_cleanup_ratio of "deletable" clauses instead of aiming for a fixed
	// target of clauses to keep.
	ClauseCleanupRatio      *float64                        `protobuf:"fixed64,190,opt,name=clause_cleanup_ratio,json=clauseCleanupRatio,def=0.5" json:"clause_cleanup_ratio,omitempty"`
	ClauseCleanupProtection *SatParameters_ClauseProtection `` /* 193-byte string literal not displayed */
	// All the clauses with a LBD (literal blocks distance) lower or equal to this
	// parameters will always be kept.
	ClauseCleanupLbdBound *int32                        `` /* 129-byte string literal not displayed */
	ClauseCleanupOrdering *SatParameters_ClauseOrdering `` /* 185-byte string literal not displayed */
	// Same as for the clauses, but for the learned pseudo-Boolean constraints.
	PbCleanupIncrement *int32   `protobuf:"varint,46,opt,name=pb_cleanup_increment,json=pbCleanupIncrement,def=200" json:"pb_cleanup_increment,omitempty"`
	PbCleanupRatio     *float64 `protobuf:"fixed64,47,opt,name=pb_cleanup_ratio,json=pbCleanupRatio,def=0.5" json:"pb_cleanup_ratio,omitempty"`
	// 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.
	VariableActivityDecay    *float64 `` /* 130-byte string literal not displayed */
	MaxVariableActivityValue *float64 `` /* 144-byte string literal not displayed */
	// 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
	GlucoseMaxDecay             *float64 `protobuf:"fixed64,22,opt,name=glucose_max_decay,json=glucoseMaxDecay,def=0.95" json:"glucose_max_decay,omitempty"`
	GlucoseDecayIncrement       *float64 `` /* 131-byte string literal not displayed */
	GlucoseDecayIncrementPeriod *int32   `` /* 150-byte string literal not displayed */
	// Clause activity parameters (same effect as the one on the variables).
	ClauseActivityDecay    *float64 `` /* 126-byte string literal not displayed */
	MaxClauseActivityValue *float64 `` /* 137-byte string literal not displayed */
	// 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.
	RestartAlgorithms        []SatParameters_RestartAlgorithm `` /* 167-byte string literal not displayed */
	DefaultRestartAlgorithms *string                          `` /* 199-byte string literal not displayed */
	// Restart period for the FIXED_RESTART strategy. This is also the multiplier
	// used by the LUBY_RESTART strategy.
	RestartPeriod *int32 `protobuf:"varint,30,opt,name=restart_period,json=restartPeriod,def=50" json:"restart_period,omitempty"`
	// Size of the window for the moving average restarts.
	RestartRunningWindowSize *int32 `` /* 139-byte string literal not displayed */
	// In the moving average restart algorithms, a restart is triggered if the
	// window average times this ratio is greater that the global average.
	RestartDlAverageRatio  *float64 `` /* 130-byte string literal not displayed */
	RestartLbdAverageRatio *float64 `` /* 133-byte string literal not displayed */
	// 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.
	UseBlockingRestart        *bool    `protobuf:"varint,64,opt,name=use_blocking_restart,json=useBlockingRestart,def=0" json:"use_blocking_restart,omitempty"`
	BlockingRestartWindowSize *int32   `` /* 144-byte string literal not displayed */
	BlockingRestartMultiplier *float64 `` /* 142-byte string literal not displayed */
	// 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.
	NumConflictsBeforeStrategyChanges *int32 `` /* 167-byte string literal not displayed */
	// The parameter num_conflicts_before_strategy_changes is increased by that
	// much after each strategy change.
	StrategyChangeIncreaseRatio *float64 `` /* 148-byte string literal not displayed */
	// Maximum time allowed in seconds to solve a problem.
	// The counter will starts at the beginning of the Solve() call.
	MaxTimeInSeconds *float64 `protobuf:"fixed64,36,opt,name=max_time_in_seconds,json=maxTimeInSeconds,def=inf" json:"max_time_in_seconds,omitempty"`
	// 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.
	MaxDeterministicTime *float64 `` /* 127-byte string literal not displayed */
	// Maximum number of conflicts allowed to solve a problem.
	//
	// TODO(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.
	MaxNumberOfConflicts *int64 `` // kint64max
	/* 144-byte string literal not displayed */
	// 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.
	//
	// TODO(user): This is only used by the pure SAT solver, generalize to CP-SAT.
	MaxMemoryInMb *int64 `protobuf:"varint,40,opt,name=max_memory_in_mb,json=maxMemoryInMb,def=10000" json:"max_memory_in_mb,omitempty"`
	// 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.
	//
	// If the objective is integer, then any absolute gap < 1 will lead to a true
	// optimal. If the objective is floating point, a gap of zero make little
	// sense so is is why we use a non-zero default value. At the end of the
	// search, we will display a warning if OPTIMAL is reported yet the gap is
	// greater than this absolute gap.
	AbsoluteGapLimit *float64 `protobuf:"fixed64,159,opt,name=absolute_gap_limit,json=absoluteGapLimit,def=0.0001" json:"absolute_gap_limit,omitempty"`
	RelativeGapLimit *float64 `protobuf:"fixed64,160,opt,name=relative_gap_limit,json=relativeGapLimit,def=0" json:"relative_gap_limit,omitempty"`
	// 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.
	RandomSeed *int32 `protobuf:"varint,31,opt,name=random_seed,json=randomSeed,def=1" json:"random_seed,omitempty"`
	// This is mainly here to test the solver variability. Note that in tests, if
	// not explicitly set to false, all 3 options will be set to true so that
	// clients do not rely on the solver returning a specific solution if they are
	// many equivalent optimal solutions.
	PermuteVariableRandomly        *bool `` /* 134-byte string literal not displayed */
	PermutePresolveConstraintOrder *bool `` /* 157-byte string literal not displayed */
	UseAbslRandom                  *bool `protobuf:"varint,180,opt,name=use_absl_random,json=useAbslRandom,def=0" json:"use_absl_random,omitempty"`
	// Whether the solver should log the search progress. This is the maing
	// logging parameter and if this is false, none of the logging (callbacks,
	// log_to_stdout, log_to_response, ...) will do anything.
	LogSearchProgress *bool `protobuf:"varint,41,opt,name=log_search_progress,json=logSearchProgress,def=0" json:"log_search_progress,omitempty"`
	// Whether the solver should display per sub-solver search statistics.
	// This is only useful is log_search_progress is set to true, and if the
	// number of search workers is > 1. Note that in all case we display a bit
	// of stats with one line per subsolver.
	LogSubsolverStatistics *bool `` /* 131-byte string literal not displayed */
	// Add a prefix to all logs.
	LogPrefix *string `protobuf:"bytes,185,opt,name=log_prefix,json=logPrefix,def=" json:"log_prefix,omitempty"`
	// Log to stdout.
	LogToStdout *bool `protobuf:"varint,186,opt,name=log_to_stdout,json=logToStdout,def=1" json:"log_to_stdout,omitempty"`
	// Log to response proto.
	LogToResponse *bool `protobuf:"varint,187,opt,name=log_to_response,json=logToResponse,def=0" json:"log_to_response,omitempty"`
	// 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).
	UsePbResolution *bool `protobuf:"varint,43,opt,name=use_pb_resolution,json=usePbResolution,def=0" json:"use_pb_resolution,omitempty"`
	// 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.
	MinimizeReductionDuringPbResolution *bool `` /* 173-byte string literal not displayed */
	// 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.
	CountAssumptionLevelsInLbd *bool `` /* 146-byte string literal not displayed */
	// 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.
	PresolveBveThreshold *int32 `` /* 126-byte string literal not displayed */
	// During presolve, we apply BVE only if this weight times the number of
	// clauses plus the number of clause literals is not increased.
	PresolveBveClauseWeight *int32 `` /* 135-byte string literal not displayed */
	// The maximum "deterministic" time limit to spend in probing. A value of
	// zero will disable the probing.
	//
	// TODO(user): Clean up. The first one is used in CP-SAT, the other in pure
	// SAT presolve.
	ProbingDeterministicTimeLimit         *float64 `` /* 155-byte string literal not displayed */
	PresolveProbingDeterministicTimeLimit *float64 `` /* 181-byte string literal not displayed */
	// Whether we use an heuristic to detect some basic case of blocked clause
	// in the SAT presolve.
	PresolveBlockedClause *bool `` /* 127-byte string literal not displayed */
	// Whether or not we use Bounded Variable Addition (BVA) in the presolve.
	PresolveUseBva *bool `protobuf:"varint,72,opt,name=presolve_use_bva,json=presolveUseBva,def=1" json:"presolve_use_bva,omitempty"`
	// 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.
	PresolveBvaThreshold *int32 `protobuf:"varint,73,opt,name=presolve_bva_threshold,json=presolveBvaThreshold,def=1" json:"presolve_bva_threshold,omitempty"`
	// In case of large reduction in a presolve iteration, we perform multiple
	// presolve iterations. This parameter controls the maximum number of such
	// presolve iterations.
	MaxPresolveIterations *int32 `` /* 128-byte string literal not displayed */
	// Whether we presolve the cp_model before solving it.
	CpModelPresolve *bool `protobuf:"varint,86,opt,name=cp_model_presolve,json=cpModelPresolve,def=1" json:"cp_model_presolve,omitempty"`
	// How much effort do we spend on probing. 0 disables it completely.
	CpModelProbingLevel *int32 `protobuf:"varint,110,opt,name=cp_model_probing_level,json=cpModelProbingLevel,def=2" json:"cp_model_probing_level,omitempty"`
	// Whether we also use the sat presolve when cp_model_presolve is true.
	CpModelUseSatPresolve *bool `` /* 131-byte string literal not displayed */
	// If true, we detect variable that are unique to a table constraint and only
	// there to encode a cost on each tuple. This is usually the case when a WCSP
	// (weighted constraint program) is encoded into CP-SAT format.
	//
	// This can lead to a dramatic speed-up for such problems but is still
	// experimental at this point.
	DetectTableWithCost *bool `protobuf:"varint,216,opt,name=detect_table_with_cost,json=detectTableWithCost,def=0" json:"detect_table_with_cost,omitempty"`
	// How much we try to "compress" a table constraint. Compressing more leads to
	// less Booleans and faster propagation but can reduced the quality of the lp
	// relaxation. Values goes from 0 to 3 where we always try to fully compress a
	// table. At 2, we try to automatically decide if it is worth it.
	TableCompressionLevel *int32 `` /* 128-byte string literal not displayed */
	// If true, expand all_different constraints that are not permutations.
	// Permutations (#Variables = #Values) are always expanded.
	ExpandAlldiffConstraints *bool `` /* 137-byte string literal not displayed */
	// If true, expand the reservoir constraints by creating booleans for all
	// possible precedences between event and encoding the constraint.
	ExpandReservoirConstraints *bool `` /* 143-byte string literal not displayed */
	// If true, it disable all constraint expansion.
	// This should only be used to test the presolve of expanded constraints.
	DisableConstraintExpansion *bool `` /* 143-byte string literal not displayed */
	// Linear constraint with a complex right hand side (more than a single
	// interval) need to be expanded, there is a couple of way to do that.
	EncodeComplexLinearConstraintWithInteger *bool `` /* 191-byte string literal not displayed */
	// 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.
	MergeNoOverlapWorkLimit *float64 `` /* 143-byte string literal not displayed */
	MergeAtMostOneWorkLimit *float64 `` /* 145-byte string literal not displayed */
	// 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.
	PresolveSubstitutionLevel *int32 `` /* 140-byte string literal not displayed */
	// If true, we will extract from linear constraints, enforcement literals of
	// the form "integer variable at bound => simplified constraint". This should
	// always be beneficial except that we don't always handle them as efficiently
	// as we could for now. This causes problem on manna81.mps (LP relaxation not
	// as tight it seems) and on neos-3354841-apure.mps.gz (too many literals
	// created this way).
	PresolveExtractIntegerEnforcement *bool `` /* 166-byte string literal not displayed */
	// A few presolve operations involve detecting constraints included in other
	// constraint. Since there can be a quadratic number of such pairs, and
	// processing them usually involve scanning them, the complexity of these
	// operations can be big. This enforce a local deterministic limit on the
	// number of entries scanned. Default is 1e8.
	//
	// A value of zero will disable these presolve rules completely.
	PresolveInclusionWorkLimit *int64 `` /* 153-byte string literal not displayed */
	// If true, we don't keep names in our internal copy of the user given model.
	IgnoreNames *bool `protobuf:"varint,202,opt,name=ignore_names,json=ignoreNames,def=1" json:"ignore_names,omitempty"`
	// Run a max-clique code amongst all the x != y we can find and try to infer
	// set of variables that are all different. This allows to close neos16.mps
	// for instance. Note that we only run this code if there is no all_diff
	// already in the model so that if a user want to add some all_diff, we assume
	// it is well done and do not try to add more.
	InferAllDiffs *bool `protobuf:"varint,233,opt,name=infer_all_diffs,json=inferAllDiffs,def=1" json:"infer_all_diffs,omitempty"`
	// Try to find large "rectangle" in the linear constraint matrix with
	// identical lines. If such rectangle is big enough, we can introduce a new
	// integer variable corresponding to the common expression and greatly reduce
	// the number of non-zero.
	FindBigLinearOverlap *bool `` /* 127-byte string literal not displayed */
	// Enable or disable "inprocessing" which is some SAT presolving done at
	// each restart to the root level.
	UseSatInprocessing *bool `protobuf:"varint,163,opt,name=use_sat_inprocessing,json=useSatInprocessing,def=1" json:"use_sat_inprocessing,omitempty"`
	// Proportion of deterministic time we should spend on inprocessing.
	// At each "restart", if the proportion is below this ratio, we will do some
	// inprocessing, otherwise, we skip it for this restart.
	InprocessingDtimeRatio *float64 `` /* 134-byte string literal not displayed */
	// The amount of dtime we should spend on probing for each inprocessing round.
	InprocessingProbingDtime *float64 `` /* 138-byte string literal not displayed */
	// Parameters for an heuristic similar to the one described in "An effective
	// learnt clause minimization approach for CDCL Sat Solvers",
	// https://www.ijcai.org/proceedings/2017/0098.pdf
	//
	// This is the amount of dtime we should spend on this technique during each
	// inprocessing phase.
	//
	// 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.
	InprocessingMinimizationDtime *float64 `` /* 153-byte string literal not displayed */
	// Specify the number of parallel workers (i.e. threads) to use during search.
	// This should usually be lower than your number of available cpus +
	// hyperthread in your machine.
	//
	// A value of 0 means the solver will try to use all cores on the machine.
	// A number of 1 means no parallelism.
	//
	// Note that 'num_workers' is the preferred name, but if it is set to zero,
	// we will still read the deprecated 'num_search_worker'.
	//
	// 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().
	NumWorkers       *int32 `protobuf:"varint,206,opt,name=num_workers,json=numWorkers,def=0" json:"num_workers,omitempty"`
	NumSearchWorkers *int32 `protobuf:"varint,100,opt,name=num_search_workers,json=numSearchWorkers,def=0" json:"num_search_workers,omitempty"`
	// Obsolete parameter. No-op.
	MinNumLnsWorkers *int32 `protobuf:"varint,211,opt,name=min_num_lns_workers,json=minNumLnsWorkers,def=2" json:"min_num_lns_workers,omitempty"`
	// In multi-thread, the solver can be mainly seen as a portfolio of solvers
	// with different parameters. This field indicates the names of the parameters
	// that are used in multithread.
	//
	// See cp_model_search.cc to see a list of the names and the default value (if
	// left empty) that looks like:
	// - default_lp           (linearization_level:1)
	// - fixed                (only if fixed search specified or scheduling)
	// - no_lp                (linearization_level:0)
	// - max_lp               (linearization_level:2)
	// - pseudo_costs         (only if objective, change search heuristic)
	// - reduced_costs        (only if objective, change search heuristic)
	// - quick_restart        (kind of probing)
	// - quick_restart_no_lp  (kind of probing with linearization_level:0)
	// - lb_tree_search       (to improve lower bound, MIP like tree search)
	// - probing              (continuous probing and shaving)
	//
	// Also, note that some set of parameters will be ignored if they do not make
	// sense. For instance if there is no objective, pseudo_cost or reduced_cost
	// search will be ignored. Core based search will only work if the objective
	// has many terms. If there is no fixed strategy fixed will be ignored. And so
	// on.
	//
	// The order is important, as only the first usable "num_workers -
	// min_num_lns_workers" subsolvers will be scheduled. You can see in the log
	// which one are selected for a given run. All the others will be LNS if there
	// is an objective, or randomized SAT search for pure satisfiability problems.
	Subsolvers []string `protobuf:"bytes,207,rep,name=subsolvers" json:"subsolvers,omitempty"`
	// A convenient way to add more workers types.
	// These will be added at the beginning of the list.
	ExtraSubsolvers []string `protobuf:"bytes,219,rep,name=extra_subsolvers,json=extraSubsolvers" json:"extra_subsolvers,omitempty"`
	// Rather than fully specifying subsolvers, it is often convenient to just
	// remove the ones that are not useful on a given problem.
	IgnoreSubsolvers []string `protobuf:"bytes,209,rep,name=ignore_subsolvers,json=ignoreSubsolvers" json:"ignore_subsolvers,omitempty"`
	// It is possible to specify additional subsolver configuration. These can be
	// referred by their params.name() in the fields above. Note that only the
	// specified field will "overwrite" the ones of the base parameter. If a
	// subsolver_params has the name of an existing subsolver configuration, the
	// named parameters will be merged into the subsolver configuration.
	SubsolverParams []*SatParameters `protobuf:"bytes,210,rep,name=subsolver_params,json=subsolverParams" json:"subsolver_params,omitempty"`
	// Experimental. If this is true, then we interleave all our major search
	// strategy and distribute the work amongst num_workers.
	//
	// The search is deterministic (independently of num_workers!), and we
	// schedule and wait for interleave_batch_size task to be completed before
	// synchronizing and scheduling the next batch of tasks.
	InterleaveSearch    *bool  `protobuf:"varint,136,opt,name=interleave_search,json=interleaveSearch,def=0" json:"interleave_search,omitempty"`
	InterleaveBatchSize *int32 `protobuf:"varint,134,opt,name=interleave_batch_size,json=interleaveBatchSize,def=0" json:"interleave_batch_size,omitempty"`
	// Allows objective sharing between workers.
	ShareObjectiveBounds *bool `protobuf:"varint,113,opt,name=share_objective_bounds,json=shareObjectiveBounds,def=1" json:"share_objective_bounds,omitempty"`
	// Allows sharing of the bounds of modified variables at level 0.
	ShareLevelZeroBounds *bool `` /* 127-byte string literal not displayed */
	// Allows sharing of new learned binary clause between workers.
	ShareBinaryClauses *bool `protobuf:"varint,203,opt,name=share_binary_clauses,json=shareBinaryClauses,def=1" json:"share_binary_clauses,omitempty"`
	// We have two different postsolve code. The default one should be better and
	// it allows for a more powerful presolve, but it can be useful to postsolve
	// using the full solver instead.
	DebugPostsolveWithFullSolver *bool `` /* 153-byte string literal not displayed */
	// If positive, try to stop just after that many presolve rules have been
	// applied. This is mainly useful for debugging presolve.
	DebugMaxNumPresolveOperations *int32 `` /* 156-byte string literal not displayed */
	// Crash if we do not manage to complete the hint into a full solution.
	DebugCrashOnBadHint *bool `` /* 126-byte string literal not displayed */
	// 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.
	UseOptimizationHints *bool `protobuf:"varint,35,opt,name=use_optimization_hints,json=useOptimizationHints,def=1" json:"use_optimization_hints,omitempty"`
	// If positive, we spend some effort on each core:
	//   - At level 1, we use a simple heuristic to try to minimize an UNSAT core.
	//   - At level 2, we use propagation to minimize the core but also identify
	//     literal in at most one relationship in this core.
	CoreMinimizationLevel *int32 `` /* 127-byte string literal not displayed */
	// Whether we try to find more independent cores for a given set of
	// assumptions in the core based max-SAT algorithms.
	FindMultipleCores *bool `protobuf:"varint,84,opt,name=find_multiple_cores,json=findMultipleCores,def=1" json:"find_multiple_cores,omitempty"`
	// 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.
	// This is also called core exhaustion in more recent max-SAT papers.
	CoverOptimization     *bool                                `protobuf:"varint,89,opt,name=cover_optimization,json=coverOptimization,def=1" json:"cover_optimization,omitempty"`
	MaxSatAssumptionOrder *SatParameters_MaxSatAssumptionOrder `` /* 194-byte string literal not displayed */
	// If true, adds the assumption in the reverse order of the one defined by
	// max_sat_assumption_order.
	MaxSatReverseAssumptionOrder *bool                                        `` /* 152-byte string literal not displayed */
	MaxSatStratification         *SatParameters_MaxSatStratificationAlgorithm `` /* 197-byte string literal not displayed */
	// Some search decisions might cause a really large number of propagations to
	// happen when integer variables with large domains are only reduced by 1 at
	// each step. If we propagate more than the number of variable times this
	// parameters we try to take counter-measure. Setting this to 0.0 disable this
	// feature.
	//
	// TODO(user): Setting this to something like 10 helps in most cases, but the
	// code is currently buggy and can cause the solve to enter a bad state where
	// no progress is made.
	PropagationLoopDetectionFactor *float64 `` /* 159-byte string literal not displayed */
	// 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.
	UsePrecedencesInDisjunctiveConstraint *bool `` /* 179-byte string literal not displayed */
	// Create one literal for each disjunction of two pairs of tasks. This slows
	// down the solve time, but improves the lower bound of the objective in the
	// makespan case. This will be triggered if the number of intervals is less or
	// equal than the parameter and if use_strong_propagation_in_disjunctive is
	// true.
	MaxSizeToCreatePrecedenceLiteralsInDisjunctive *int32 `` /* 214-byte string literal not displayed */
	// Enable stronger and more expensive propagation on no_overlap constraint.
	UseStrongPropagationInDisjunctive *bool `` /* 168-byte string literal not displayed */
	// Whether we try to branch on decision "interval A before interval B" rather
	// than on intervals bounds. This usually works better, but slow down a bit
	// the time to find the first solution.
	//
	// These parameters are still EXPERIMENTAL, the result should be correct, but
	// it some corner cases, they can cause some failing CHECK in the solver.
	UseDynamicPrecedenceInDisjunctive *bool `` /* 168-byte string literal not displayed */
	UseDynamicPrecedenceInCumulative  *bool `` /* 165-byte string literal not displayed */
	// 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.
	UseOverloadCheckerInCumulative *bool `` /* 158-byte string literal not displayed */
	// 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.
	UseTimetableEdgeFindingInCumulative *bool `` /* 175-byte string literal not displayed */
	// Max number of intervals for the timetable_edge_finding algorithm to
	// propagate. A value of 0 disables the constraint.
	MaxNumIntervalsForTimetableEdgeFinding *int32 `` /* 189-byte string literal not displayed */
	// If true, detect and create constraint for integer variable that are "after"
	// a set of intervals in the same cumulative constraint.
	//
	// Experimental: by default we just use "direct" precedences. If
	// exploit_all_precedences is true, we explore the full precedence graph. This
	// assumes we have a DAG otherwise it fails.
	UseHardPrecedencesInCumulative *bool `` /* 159-byte string literal not displayed */
	ExploitAllPrecedences          *bool `` /* 128-byte string literal not displayed */
	// 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.
	UseDisjunctiveConstraintInCumulative *bool `` /* 176-byte string literal not displayed */
	// When this is true, the no_overlap_2d constraint is reinforced with
	// propagators from the cumulative constraints. It consists of ignoring the
	// position of rectangles in one position and projecting the no_overlap_2d on
	// the other dimension to create a cumulative constraint. This is done on both
	// axis. This additional level supplements the default level of reasoning.
	UseTimetablingInNoOverlap_2D *bool `` /* 152-byte string literal not displayed */
	// When this is true, the no_overlap_2d constraint is reinforced with
	// energetic reasoning. This additional level supplements the default level of
	// reasoning.
	UseEnergeticReasoningInNoOverlap_2D *bool `` /* 175-byte string literal not displayed */
	// When this is true, the no_overlap_2d constraint is reinforced with
	// an energetic reasoning that uses an area-based energy. This can be combined
	// with the two other overlap heuristics above.
	UseAreaEnergeticReasoningInNoOverlap_2D *bool `` /* 189-byte string literal not displayed */
	// If the number of pairs to look is below this threshold, do an extra step of
	// propagation in the no_overlap_2d constraint by looking at all pairs of
	// intervals.
	MaxPairsPairwiseReasoningInNoOverlap_2D *int32 `` /* 192-byte string literal not displayed */
	// When set, it activates a few scheduling parameters to improve the lower
	// bound of scheduling problems. This is only effective with multiple workers
	// as it modifies the reduced_cost, lb_tree_search, and probing workers.
	UseDualSchedulingHeuristics *bool                          `` /* 148-byte string literal not displayed */
	SearchBranching             *SatParameters_SearchBranching `` /* 166-byte string literal not displayed */
	// Conflict limit used in the phase that exploit the solution hint.
	HintConflictLimit *int32 `protobuf:"varint,153,opt,name=hint_conflict_limit,json=hintConflictLimit,def=10" json:"hint_conflict_limit,omitempty"`
	// If true, the solver tries to repair the solution given in the hint. This
	// search terminates after the 'hint_conflict_limit' is reached and the solver
	// switches to regular search. If false, then  we do a FIXED_SEARCH using the
	// hint until the hint_conflict_limit is reached.
	RepairHint *bool `protobuf:"varint,167,opt,name=repair_hint,json=repairHint,def=0" json:"repair_hint,omitempty"`
	// If true, variables appearing in the solution hints will be fixed to their
	// hinted value.
	FixVariablesToTheirHintedValue *bool `` /* 161-byte string literal not displayed */
	// If true, search will continuously probe Boolean variables, and integer
	// variable bounds. This parameter is set to true in parallel on the probing
	// worker.
	UseProbingSearch *bool `protobuf:"varint,176,opt,name=use_probing_search,json=useProbingSearch,def=0" json:"use_probing_search,omitempty"`
	// Use extended probing (probe bool_or, at_most_one, exactly_one).
	UseExtendedProbing *bool `protobuf:"varint,269,opt,name=use_extended_probing,json=useExtendedProbing,def=1" json:"use_extended_probing,omitempty"`
	// How many combinations of pairs or triplets of variables we want to scan.
	ProbingNumCombinationsLimit *int32 `` /* 152-byte string literal not displayed */
	// Add a shaving phase (where the solver tries to prove that the lower or
	// upper bound of a variable are infeasible) to the probing search.
	UseShavingInProbingSearch *bool `` /* 144-byte string literal not displayed */
	// Specifies the amount of deterministic time spent of each try at shaving a
	// bound in the shaving search.
	ShavingSearchDeterministicTime *float64 `` /* 162-byte string literal not displayed */
	// If true, search will search in ascending max objective value (when
	// minimizing) starting from the lower bound of the objective.
	UseObjectiveLbSearch *bool `` /* 127-byte string literal not displayed */
	// This search differs from the previous search as it will not use assumptions
	// to bound the objective, and it will recreate a full model with the
	// hardcoded objective value.
	UseObjectiveShavingSearch *bool `` /* 142-byte string literal not displayed */
	// The solver ignores the pseudo costs of variables with number of recordings
	// less than this threshold.
	PseudoCostReliabilityThreshold *int64 `` /* 159-byte string literal not displayed */
	// 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.
	OptimizeWithCore *bool `protobuf:"varint,83,opt,name=optimize_with_core,json=optimizeWithCore,def=0" json:"optimize_with_core,omitempty"`
	// Do a more conventional tree search (by opposition to SAT based one) where
	// we keep all the explored node in a tree. This is meant to be used in a
	// portfolio and focus on improving the objective lower bound. Keeping the
	// whole tree allow us to report a better objective lower bound coming from
	// the worst open node in the tree.
	OptimizeWithLbTreeSearch *bool `` /* 141-byte string literal not displayed */
	// 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.
	BinarySearchNumConflicts *int32 `` /* 139-byte string literal not displayed */
	// 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
	OptimizeWithMaxHs *bool `protobuf:"varint,85,opt,name=optimize_with_max_hs,json=optimizeWithMaxHs,def=0" json:"optimize_with_max_hs,omitempty"`
	// Parameters for an heuristic similar to the one described in the paper:
	// "Feasibility Jump: an LP-free Lagrangian MIP heuristic", Bjørnar
	// Luteberget, Giorgio Sartor, 2023, Mathematical Programming Computation.
	UseFeasibilityJump *bool `protobuf:"varint,265,opt,name=use_feasibility_jump,json=useFeasibilityJump,def=1" json:"use_feasibility_jump,omitempty"`
	// Disable every other type of subsolver, setting this turns CP-SAT into a
	// pure local-search solver.
	TestFeasibilityJump *bool `protobuf:"varint,240,opt,name=test_feasibility_jump,json=testFeasibilityJump,def=0" json:"test_feasibility_jump,omitempty"`
	// On each restart, we randomly choose if we use decay (with this parameter)
	// or no decay.
	FeasibilityJumpDecay *float64 `` /* 129-byte string literal not displayed */
	// How much do we linearize the problem in the local search code.
	FeasibilityJumpLinearizationLevel *int32 `` /* 166-byte string literal not displayed */
	// This is a factor that directly influence the work before each restart.
	// Setting this to zero disable restart, and increasing it lead to longer
	// restarts.
	FeasibilityJumpRestartFactor *int32 `` /* 151-byte string literal not displayed */
	// Probability for a variable to have a non default value upon restarts or
	// perturbations.
	FeasibilityJumpVarRandomizationProbability *float64 `` /* 196-byte string literal not displayed */
	// Max distance between the default value and the pertubated value relative to
	// the range of the domain of the variable.
	FeasibilityJumpVarPerburbationRangeRatio *float64 `` /* 194-byte string literal not displayed */
	// When stagnating, feasibility jump will either restart from a default
	// solution (with some possible randomization), or randomly pertubate the
	// current solution. This parameter selects the first option.
	FeasibilityJumpEnableRestarts *bool `` /* 154-byte string literal not displayed */
	// Maximum size of no_overlap or no_overlap_2d constraint for a quadratic
	// expansion.
	FeasibilityJumpMaxExpandedConstraintSize *int32 `` /* 193-byte string literal not displayed */
	// This will create incomplete subsolvers (that are not LNS subsolvers)
	// that use the feasibility jump code to find improving solution, treating
	// the objective improvement as a hard constraint.
	NumViolationLs *int32 `protobuf:"varint,244,opt,name=num_violation_ls,json=numViolationLs,def=0" json:"num_violation_ls,omitempty"`
	// How long violation_ls should wait before perturbating a solution.
	ViolationLsPerturbationPeriod *int32 `` /* 156-byte string literal not displayed */
	// Probability of using compound move search each restart.
	// TODO(user): Add reference to paper when published.
	ViolationLsCompoundMoveProbability *float64 `` /* 174-byte string literal not displayed */
	// Enables experimental workstealing-like shared tree search.
	// If non-zero, start this many complete worker threads to explore a shared
	// search tree. These workers communicate objective bounds and simple decision
	// nogoods relating to the shared prefix of the tree, and will avoid exploring
	// the same subtrees as one another.
	SharedTreeNumWorkers *int32 `` /* 127-byte string literal not displayed */
	// Set on shared subtree workers. Users should not set this directly.
	UseSharedTreeSearch *bool `protobuf:"varint,236,opt,name=use_shared_tree_search,json=useSharedTreeSearch,def=0" json:"use_shared_tree_search,omitempty"`
	// After their assigned prefix, shared tree workers will branch on the
	// objective with this probability. Higher numbers cause the shared tree
	// search to focus on improving the lower bound over finding primal solutions.
	SharedTreeWorkerObjectiveSplitProbability *float64 `` /* 197-byte string literal not displayed */
	// In order to limit total shared memory and communication overhead, limit the
	// total number of nodes that may be generated in the shared tree. If the
	// shared tree runs out of unassigned leaves, workers act as portfolio
	// workers. Note: this limit includes interior nodes, not just leaves.
	SharedTreeMaxNodesPerWorker *int32                                 `` /* 154-byte string literal not displayed */
	SharedTreeSplitStrategy     *SatParameters_SharedTreeSplitStrategy `` /* 203-byte string literal not displayed */
	// Whether we enumerate all solutions of a problem without objective. Note
	// that setting this to true automatically disable some presolve reduction
	// that can remove feasible solution. That is it has the same effect as
	// setting keep_all_feasible_solutions_in_presolve.
	//
	// TODO(user): Do not do that and let the user choose what behavior is best by
	// setting keep_all_feasible_solutions_in_presolve ?
	EnumerateAllSolutions *bool `` /* 127-byte string literal not displayed */
	// If true, we disable the presolve reductions that remove feasible solutions
	// from the search space. Such solution are usually dominated by a "better"
	// solution that is kept, but depending on the situation, we might want to
	// keep all solutions.
	//
	// A trivial example is when a variable is unused. If this is true, then the
	// presolve will not fix it to an arbitrary value and it will stay in the
	// search space.
	KeepAllFeasibleSolutionsInPresolve *bool `` /* 173-byte string literal not displayed */
	// 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.
	FillTightenedDomainsInResponse *bool `` /* 159-byte string literal not displayed */
	// If true, the final response addition_solutions field will be filled with
	// all solutions from our solutions pool.
	//
	// Note that if both this field and enumerate_all_solutions is true, we will
	// copy to the pool all of the solution found. So if solution_pool_size is big
	// enough, you can get all solutions this way instead of using the solution
	// callback.
	//
	// Note that this only affect the "final" solution, not the one passed to the
	// solution callbacks.
	FillAdditionalSolutionsInResponse *bool `` /* 168-byte string literal not displayed */
	// If true, the solver will add a default integer branching strategy to the
	// already defined search strategy. If not, some variable might still not be
	// fixed at the end of the search. For now we assume these variable can just
	// be set to their lower bound.
	InstantiateAllVariables *bool `` /* 134-byte string literal not displayed */
	// 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.
	AutoDetectGreaterThanAtLeastOneOf *bool `` /* 173-byte string literal not displayed */
	// For an optimization problem, stop the solver as soon as we have a solution.
	StopAfterFirstSolution *bool `` /* 132-byte string literal not displayed */
	// Mainly used when improving the presolver. When true, stops the solver after
	// the presolve is complete (or after loading and root level propagation).
	StopAfterPresolve        *bool `protobuf:"varint,149,opt,name=stop_after_presolve,json=stopAfterPresolve,def=0" json:"stop_after_presolve,omitempty"`
	StopAfterRootPropagation *bool `` /* 139-byte string literal not displayed */
	// LNS parameters.
	UseLnsOnly *bool `protobuf:"varint,101,opt,name=use_lns_only,json=useLnsOnly,def=0" json:"use_lns_only,omitempty"`
	// Size of the top-n different solutions kept by the solver.
	// This parameter must be > 0.
	// Currently this only impact the "base" solution chosen for a LNS fragment.
	SolutionPoolSize *int32 `protobuf:"varint,193,opt,name=solution_pool_size,json=solutionPoolSize,def=3" json:"solution_pool_size,omitempty"`
	// Turns on relaxation induced neighborhood generator.
	UseRinsLns *bool `protobuf:"varint,129,opt,name=use_rins_lns,json=useRinsLns,def=1" json:"use_rins_lns,omitempty"`
	// Adds a feasibility pump subsolver along with lns subsolvers.
	UseFeasibilityPump *bool `protobuf:"varint,164,opt,name=use_feasibility_pump,json=useFeasibilityPump,def=1" json:"use_feasibility_pump,omitempty"`
	// Turns on neighborhood generator based on local branching LP. Based on Huang
	// et al., "Local Branching Relaxation Heuristics for Integer Linear
	// Programs", 2023.
	UseLbRelaxLns *bool                           `protobuf:"varint,255,opt,name=use_lb_relax_lns,json=useLbRelaxLns,def=0" json:"use_lb_relax_lns,omitempty"`
	FpRounding    *SatParameters_FPRoundingMethod `` /* 153-byte string literal not displayed */
	// If true, registers more lns subsolvers with different parameters.
	DiversifyLnsParams *bool `protobuf:"varint,137,opt,name=diversify_lns_params,json=diversifyLnsParams,def=0" json:"diversify_lns_params,omitempty"`
	// Randomize fixed search.
	RandomizeSearch *bool `protobuf:"varint,103,opt,name=randomize_search,json=randomizeSearch,def=0" json:"randomize_search,omitempty"`
	// Search randomization will collect the top
	// 'search_random_variable_pool_size' valued variables, and pick one randomly.
	// The value of the variable is specific to each strategy.
	SearchRandomVariablePoolSize *int64 `` /* 153-byte string literal not displayed */
	// Experimental code: specify if the objective pushes all tasks toward the
	// start of the schedule.
	PushAllTasksTowardStart *bool `` /* 138-byte string literal not displayed */
	// 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.
	//
	// TODO(user): This is experimental and seems to lead to wrong optimal in
	// some situation. It should however gives correct solutions. Fix.
	UseOptionalVariables *bool `protobuf:"varint,108,opt,name=use_optional_variables,json=useOptionalVariables,def=0" json:"use_optional_variables,omitempty"`
	// 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.
	UseExactLpReason *bool `protobuf:"varint,109,opt,name=use_exact_lp_reason,json=useExactLpReason,def=1" json:"use_exact_lp_reason,omitempty"`
	// 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.
	UseCombinedNoOverlap *bool `` /* 127-byte string literal not displayed */
	// All at_most_one constraints with a size <= param will be replaced by a
	// quadratic number of binary implications.
	AtMostOneMaxExpansionSize *int32 `` /* 146-byte string literal not displayed */
	// 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.
	CatchSigintSignal *bool `protobuf:"varint,135,opt,name=catch_sigint_signal,json=catchSigintSignal,def=1" json:"catch_sigint_signal,omitempty"`
	// 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.
	UseImpliedBounds *bool `protobuf:"varint,144,opt,name=use_implied_bounds,json=useImpliedBounds,def=1" json:"use_implied_bounds,omitempty"`
	// Whether we try to do a few degenerate iteration at the end of an LP solve
	// to minimize the fractionality of the integer variable in the basis. This
	// helps on some problems, but not so much on others. It also cost of bit of
	// time to do such polish step.
	PolishLpSolution *bool `protobuf:"varint,175,opt,name=polish_lp_solution,json=polishLpSolution,def=0" json:"polish_lp_solution,omitempty"`
	// The internal LP tolerances used by CP-SAT. These applies to the internal
	// and scaled problem. If the domains of your variables are large it might be
	// good to use lower tolerances. If your problem is binary with low
	// coefficients, it might be good to use higher ones to speed-up the lp
	// solves.
	LpPrimalTolerance *float64 `protobuf:"fixed64,266,opt,name=lp_primal_tolerance,json=lpPrimalTolerance,def=1e-07" json:"lp_primal_tolerance,omitempty"`
	LpDualTolerance   *float64 `protobuf:"fixed64,267,opt,name=lp_dual_tolerance,json=lpDualTolerance,def=1e-07" json:"lp_dual_tolerance,omitempty"`
	// Temporary flag util the feature is more mature. This convert intervals to
	// the newer proto format that support affine start/var/end instead of just
	// variables.
	ConvertIntervals *bool `protobuf:"varint,177,opt,name=convert_intervals,json=convertIntervals,def=1" json:"convert_intervals,omitempty"`
	// Whether we try to automatically detect the symmetries in a model and
	// exploit them. Currently, at level 1 we detect them in presolve and try
	// to fix Booleans. At level 2, we also do some form of dynamic symmetry
	// breaking during search.
	SymmetryLevel *int32 `protobuf:"varint,183,opt,name=symmetry_level,json=symmetryLevel,def=2" json:"symmetry_level,omitempty"`
	// Experimental. Use new code to propagate linear constraint.
	NewLinearPropagation *bool `protobuf:"varint,224,opt,name=new_linear_propagation,json=newLinearPropagation,def=0" json:"new_linear_propagation,omitempty"`
	// Linear constraints that are not pseudo-Boolean and that are longer than
	// this size will be split into sqrt(size) intermediate sums in order to have
	// faster propation in the CP engine.
	LinearSplitSize *int32 `protobuf:"varint,256,opt,name=linear_split_size,json=linearSplitSize,def=100" json:"linear_split_size,omitempty"`
	// 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.
	LinearizationLevel *int32 `protobuf:"varint,90,opt,name=linearization_level,json=linearizationLevel,def=1" json:"linearization_level,omitempty"`
	// A non-negative level indicating how much we should try to fully encode
	// Integer variables as Boolean.
	BooleanEncodingLevel *int32 `protobuf:"varint,107,opt,name=boolean_encoding_level,json=booleanEncodingLevel,def=1" json:"boolean_encoding_level,omitempty"`
	// When loading a*x + b*y ==/!= c when x and y are both fully encoded.
	// The solver may decide to replace the linear equation by a set of clauses.
	// This is triggered if the sizes of the domains of x and y are below the
	// threshold.
	MaxDomainSizeWhenEncodingEqNeqConstraints *int32 `` /* 199-byte string literal not displayed */
	// 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.
	MaxNumCuts *int32 `protobuf:"varint,91,opt,name=max_num_cuts,json=maxNumCuts,def=10000" json:"max_num_cuts,omitempty"`
	// Control the global cut effort. Zero will turn off all cut. For now we just
	// have one level. Note also that most cuts are only used at linearization
	// level >= 2.
	CutLevel *int32 `protobuf:"varint,196,opt,name=cut_level,json=cutLevel,def=1" json:"cut_level,omitempty"`
	// For the cut that can be generated at any level, this control if we only
	// try to generate them at the root node.
	OnlyAddCutsAtLevelZero *bool `` /* 136-byte string literal not displayed */
	// When the LP objective is fractional, do we add the cut that forces the
	// linear objective expression to be greater or equal to this fractional value
	// rounded up? We can always do that since our objective is integer, and
	// combined with MIR heuristic to reduce the coefficient of such cut, it can
	// help.
	AddObjectiveCut *bool `protobuf:"varint,197,opt,name=add_objective_cut,json=addObjectiveCut,def=0" json:"add_objective_cut,omitempty"`
	// Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
	// Note that for now, this is not heavily tuned.
	AddCgCuts *bool `protobuf:"varint,117,opt,name=add_cg_cuts,json=addCgCuts,def=1" json:"add_cg_cuts,omitempty"`
	// Whether we generate MIR cuts at root node.
	// Note that for now, this is not heavily tuned.
	AddMirCuts *bool `protobuf:"varint,120,opt,name=add_mir_cuts,json=addMirCuts,def=1" json:"add_mir_cuts,omitempty"`
	// Whether we generate Zero-Half cuts at root node.
	// Note that for now, this is not heavily tuned.
	AddZeroHalfCuts *bool `protobuf:"varint,169,opt,name=add_zero_half_cuts,json=addZeroHalfCuts,def=1" json:"add_zero_half_cuts,omitempty"`
	// Whether we generate clique cuts from the binary implication graph. Note
	// that as the search goes on, this graph will contains new binary clauses
	// learned by the SAT engine.
	AddCliqueCuts *bool `protobuf:"varint,172,opt,name=add_clique_cuts,json=addCliqueCuts,def=1" json:"add_clique_cuts,omitempty"`
	// Whether we generate RLT cuts. This is still experimental but can help on
	// binary problem with a lot of clauses of size 3.
	AddRltCuts *bool `protobuf:"varint,279,opt,name=add_rlt_cuts,json=addRltCuts,def=1" json:"add_rlt_cuts,omitempty"`
	// 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.
	MaxAllDiffCutSize *int32 `protobuf:"varint,148,opt,name=max_all_diff_cut_size,json=maxAllDiffCutSize,def=64" json:"max_all_diff_cut_size,omitempty"`
	// 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)
	AddLinMaxCuts *bool `protobuf:"varint,152,opt,name=add_lin_max_cuts,json=addLinMaxCuts,def=1" json:"add_lin_max_cuts,omitempty"`
	// 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.
	MaxIntegerRoundingScaling *int32 `` /* 144-byte string literal not displayed */
	// 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.
	AddLpConstraintsLazily *bool `` /* 133-byte string literal not displayed */
	// Even at the root node, we do not want to spend too much time on the LP if
	// it is "difficult". So we solve it in "chunks" of that many iterations. The
	// solve will be continued down in the tree or the next time we go back to the
	// root node.
	RootLpIterations *int32 `protobuf:"varint,227,opt,name=root_lp_iterations,json=rootLpIterations,def=2000" json:"root_lp_iterations,omitempty"`
	// 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.
	MinOrthogonalityForLpConstraints *float64 `` /* 169-byte string literal not displayed */
	// Max number of time we perform cut generation and resolve the LP at level 0.
	MaxCutRoundsAtLevelZero *int32 `` /* 140-byte string literal not displayed */
	// 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.
	MaxConsecutiveInactiveCount *int32 `` /* 150-byte string literal not displayed */
	// 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.
	CutMaxActiveCountValue *float64 `` /* 140-byte string literal not displayed */
	CutActiveCountDecay    *float64 `` /* 127-byte string literal not displayed */
	// Target number of constraints to remove during cleanup.
	CutCleanupTarget *int32 `protobuf:"varint,157,opt,name=cut_cleanup_target,json=cutCleanupTarget,def=1000" json:"cut_cleanup_target,omitempty"`
	// Add that many lazy constraints (or cuts) at once in the LP. Note that at
	// the beginning of the solve, we do add more than this.
	NewConstraintsBatchSize *int32 `` /* 137-byte string literal not displayed */
	// 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.
	ExploitIntegerLpSolution *bool `` /* 138-byte string literal not displayed */
	// 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.
	ExploitAllLpSolution *bool `` /* 127-byte string literal not displayed */
	// When branching on a variable, follow the last best solution value.
	ExploitBestSolution *bool `protobuf:"varint,130,opt,name=exploit_best_solution,json=exploitBestSolution,def=0" json:"exploit_best_solution,omitempty"`
	// 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.
	ExploitRelaxationSolution *bool `` /* 140-byte string literal not displayed */
	// When branching an a variable that directly affect the objective,
	// branch on the value that lead to the best objective first.
	ExploitObjective *bool `protobuf:"varint,131,opt,name=exploit_objective,json=exploitObjective,def=1" json:"exploit_objective,omitempty"`
	// Infer products of Boolean or of Boolean time IntegerVariable from the
	// linear constrainst in the problem. This can be used in some cuts, altough
	// for now we don't really exploit it.
	DetectLinearizedProduct *bool `` /* 134-byte string literal not displayed */
	// 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.
	MipMaxBound *float64 `protobuf:"fixed64,124,opt,name=mip_max_bound,json=mipMaxBound,def=1e+07" json:"mip_max_bound,omitempty"`
	// 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.
	MipVarScaling *float64 `protobuf:"fixed64,125,opt,name=mip_var_scaling,json=mipVarScaling,def=1" json:"mip_var_scaling,omitempty"`
	// If this is false, then mip_var_scaling is only applied to variables with
	// "small" domain. If it is true, we scale all floating point variable
	// independenlty of their domain.
	MipScaleLargeDomain *bool `protobuf:"varint,225,opt,name=mip_scale_large_domain,json=mipScaleLargeDomain,def=0" json:"mip_scale_large_domain,omitempty"`
	// If true, some continuous variable might be automatically scaled. For now,
	// this is only the case where we detect that a variable is actually an
	// integer multiple of a constant. For instance, variables of the form k * 0.5
	// are quite frequent, and if we detect this, we will scale such variable
	// domain by 2 to make it implied integer.
	MipAutomaticallyScaleVariables *bool `` /* 157-byte string literal not displayed */
	// If one try to solve a MIP model with CP-SAT, because we assume all variable
	// to be integer after scaling, we will not necessarily have the correct
	// optimal. Note however that all feasible solutions are valid since we will
	// just solve a more restricted version of the original problem.
	//
	// This parameters is here to prevent user to think the solution is optimal
	// when it might not be. One will need to manually set this to false to solve
	// a MIP model where the optimal might be different.
	//
	// Note that this is tested after some MIP presolve steps, so even if not
	// all original variable are integer, we might end up with a pure IP after
	// presolve and after implied integer detection.
	OnlySolveIp *bool `protobuf:"varint,222,opt,name=only_solve_ip,json=onlySolveIp,def=0" json:"only_solve_ip,omitempty"`
	// When scaling constraint with double coefficients to integer coefficients,
	// we will multiply by a power of 2 and round the coefficients. We will choose
	// the lowest power such that we have no potential overflow (see
	// mip_max_activity_exponent) and the worst case constraint activity error
	// does not exceed this threshold.
	//
	// Note that we also detect constraint with rational coefficients and scale
	// them accordingly when it seems better instead of using a power of 2.
	//
	// We also relax all constraint bounds by this absolute value. For pure
	// integer constraint, if this value if lower than one, this will not change
	// anything. However it is needed when scaling MIP problems.
	//
	// If we manage to scale a constraint correctly, the maximum error we can make
	// will be twice this value (once for the scaling error and once for the
	// relaxed bounds). If we are not able to scale that well, we will display
	// that fact but still scale as best as we can.
	MipWantedPrecision *float64 `protobuf:"fixed64,126,opt,name=mip_wanted_precision,json=mipWantedPrecision,def=1e-06" json:"mip_wanted_precision,omitempty"`
	// 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.
	MipMaxActivityExponent *int32 `` /* 134-byte string literal not displayed */
	// As explained in mip_precision and mip_max_activity_exponent, we cannot
	// always reach the wanted precision during scaling. We use this threshold to
	// enphasize in the logs when the precision seems bad.
	MipCheckPrecision *float64 `protobuf:"fixed64,128,opt,name=mip_check_precision,json=mipCheckPrecision,def=0.0001" json:"mip_check_precision,omitempty"`
	// Even if we make big error when scaling the objective, we can always derive
	// a correct lower bound on the original objective by using the exact lower
	// bound on the scaled integer version of the objective. This should be fast,
	// but if you don't care about having a precise lower bound, you can turn it
	// off.
	MipComputeTrueObjectiveBound *bool `` /* 153-byte string literal not displayed */
	// Any finite values in the input MIP must be below this threshold, otherwise
	// the model will be reported invalid. This is needed to avoid floating point
	// overflow when evaluating bounds * coeff for instance. We are a bit more
	// defensive, but in practice, users shouldn't use super large values in a
	// MIP.
	MipMaxValidMagnitude *float64 `` /* 132-byte string literal not displayed */
	// By default, any variable/constraint bound with a finite value and a
	// magnitude greater than the mip_max_valid_magnitude will result with a
	// invalid model. This flags change the behavior such that such bounds are
	// silently transformed to +∞ or -∞.
	//
	// It is recommended to keep it at false, and create valid bounds.
	MipTreatHighMagnitudeBoundsAsInfinity *bool `` /* 184-byte string literal not displayed */
	// Any value in the input mip with a magnitude lower than this will be set to
	// zero. This is to avoid some issue in LP presolving.
	MipDropTolerance *float64 `protobuf:"fixed64,232,opt,name=mip_drop_tolerance,json=mipDropTolerance,def=1e-16" json:"mip_drop_tolerance,omitempty"`
	// When solving a MIP, we do some basic floating point presolving before
	// scaling the problem to integer to be handled by CP-SAT. This control how
	// much of that presolve we do. It can help to better scale floating point
	// model, but it is not always behaving nicely.
	MipPresolveLevel *int32 `protobuf:"varint,261,opt,name=mip_presolve_level,json=mipPresolveLevel,def=2" json:"mip_presolve_level,omitempty"`
	// contains filtered or unexported fields
}

Contains the definitions for all the sat algorithm parameters and their default values.

NEXT TAG: 280

func (*SatParameters) Descriptor deprecated 

func (*SatParameters) Descriptor() ([]byte, []int)

Deprecated: Use SatParameters.ProtoReflect.Descriptor instead.

func (*SatParameters) GetAbsoluteGapLimit 

func (x *SatParameters) GetAbsoluteGapLimit() float64

func (*SatParameters) GetAddCgCuts 

func (x *SatParameters) GetAddCgCuts() bool

func (*SatParameters) GetAddCliqueCuts 

func (x *SatParameters) GetAddCliqueCuts() bool

func (*SatParameters) GetAddLinMaxCuts 

func (x *SatParameters) GetAddLinMaxCuts() bool

func (*SatParameters) GetAddLpConstraintsLazily 

func (x *SatParameters) GetAddLpConstraintsLazily() bool

func (*SatParameters) GetAddMirCuts 

func (x *SatParameters) GetAddMirCuts() bool

func (*SatParameters) GetAddObjectiveCut 

func (x *SatParameters) GetAddObjectiveCut() bool

func (*SatParameters) GetAddRltCuts 

func (x *SatParameters) GetAddRltCuts() bool

func (*SatParameters) GetAddZeroHalfCuts 

func (x *SatParameters) GetAddZeroHalfCuts() bool

func (*SatParameters) GetAlsoBumpVariablesInConflictReasons 

func (x *SatParameters) GetAlsoBumpVariablesInConflictReasons() bool

func (*SatParameters) GetAtMostOneMaxExpansionSize 

func (x *SatParameters) GetAtMostOneMaxExpansionSize() int32

func (*SatParameters) GetAutoDetectGreaterThanAtLeastOneOf 

func (x *SatParameters) GetAutoDetectGreaterThanAtLeastOneOf() bool

func (*SatParameters) GetBinaryMinimizationAlgorithm 

func (x *SatParameters) GetBinaryMinimizationAlgorithm() SatParameters_BinaryMinizationAlgorithm

func (*SatParameters) GetBinarySearchNumConflicts 

func (x *SatParameters) GetBinarySearchNumConflicts() int32

func (*SatParameters) GetBlockingRestartMultiplier 

func (x *SatParameters) GetBlockingRestartMultiplier() float64

func (*SatParameters) GetBlockingRestartWindowSize 

func (x *SatParameters) GetBlockingRestartWindowSize() int32

func (*SatParameters) GetBooleanEncodingLevel 

func (x *SatParameters) GetBooleanEncodingLevel() int32

func (*SatParameters) GetCatchSigintSignal 

func (x *SatParameters) GetCatchSigintSignal() bool

func (*SatParameters) GetClauseActivityDecay 

func (x *SatParameters) GetClauseActivityDecay() float64

func (*SatParameters) GetClauseCleanupLbdBound 

func (x *SatParameters) GetClauseCleanupLbdBound() int32

func (*SatParameters) GetClauseCleanupOrdering 

func (x *SatParameters) GetClauseCleanupOrdering() SatParameters_ClauseOrdering

func (*SatParameters) GetClauseCleanupPeriod 

func (x *SatParameters) GetClauseCleanupPeriod() int32

func (*SatParameters) GetClauseCleanupProtection 

func (x *SatParameters) GetClauseCleanupProtection() SatParameters_ClauseProtection

func (*SatParameters) GetClauseCleanupRatio 

func (x *SatParameters) GetClauseCleanupRatio() float64

func (*SatParameters) GetClauseCleanupTarget 

func (x *SatParameters) GetClauseCleanupTarget() int32

func (*SatParameters) GetConvertIntervals 

func (x *SatParameters) GetConvertIntervals() bool

func (*SatParameters) GetCoreMinimizationLevel 

func (x *SatParameters) GetCoreMinimizationLevel() int32

func (*SatParameters) GetCountAssumptionLevelsInLbd 

func (x *SatParameters) GetCountAssumptionLevelsInLbd() bool

func (*SatParameters) GetCoverOptimization 

func (x *SatParameters) GetCoverOptimization() bool

func (*SatParameters) GetCpModelPresolve 

func (x *SatParameters) GetCpModelPresolve() bool

func (*SatParameters) GetCpModelProbingLevel 

func (x *SatParameters) GetCpModelProbingLevel() int32

func (*SatParameters) GetCpModelUseSatPresolve 

func (x *SatParameters) GetCpModelUseSatPresolve() bool

func (*SatParameters) GetCutActiveCountDecay 

func (x *SatParameters) GetCutActiveCountDecay() float64

func (*SatParameters) GetCutCleanupTarget 

func (x *SatParameters) GetCutCleanupTarget() int32

func (*SatParameters) GetCutLevel 

func (x *SatParameters) GetCutLevel() int32

func (*SatParameters) GetCutMaxActiveCountValue 

func (x *SatParameters) GetCutMaxActiveCountValue() float64

func (*SatParameters) GetDebugCrashOnBadHint 

func (x *SatParameters) GetDebugCrashOnBadHint() bool

func (*SatParameters) GetDebugMaxNumPresolveOperations 

func (x *SatParameters) GetDebugMaxNumPresolveOperations() int32

func (*SatParameters) GetDebugPostsolveWithFullSolver 

func (x *SatParameters) GetDebugPostsolveWithFullSolver() bool

func (*SatParameters) GetDefaultRestartAlgorithms 

func (x *SatParameters) GetDefaultRestartAlgorithms() string

func (*SatParameters) GetDetectLinearizedProduct 

func (x *SatParameters) GetDetectLinearizedProduct() bool

func (*SatParameters) GetDetectTableWithCost 

func (x *SatParameters) GetDetectTableWithCost() bool

func (*SatParameters) GetDisableConstraintExpansion 

func (x *SatParameters) GetDisableConstraintExpansion() bool

func (*SatParameters) GetDiversifyLnsParams 

func (x *SatParameters) GetDiversifyLnsParams() bool

func (*SatParameters) GetEncodeComplexLinearConstraintWithInteger 

func (x *SatParameters) GetEncodeComplexLinearConstraintWithInteger() bool

func (*SatParameters) GetEnumerateAllSolutions 

func (x *SatParameters) GetEnumerateAllSolutions() bool

func (*SatParameters) GetExpandAlldiffConstraints 

func (x *SatParameters) GetExpandAlldiffConstraints() bool

func (*SatParameters) GetExpandReservoirConstraints 

func (x *SatParameters) GetExpandReservoirConstraints() bool

func (*SatParameters) GetExploitAllLpSolution 

func (x *SatParameters) GetExploitAllLpSolution() bool

func (*SatParameters) GetExploitAllPrecedences 

func (x *SatParameters) GetExploitAllPrecedences() bool

func (*SatParameters) GetExploitBestSolution 

func (x *SatParameters) GetExploitBestSolution() bool

func (*SatParameters) GetExploitIntegerLpSolution 

func (x *SatParameters) GetExploitIntegerLpSolution() bool

func (*SatParameters) GetExploitObjective 

func (x *SatParameters) GetExploitObjective() bool

func (*SatParameters) GetExploitRelaxationSolution 

func (x *SatParameters) GetExploitRelaxationSolution() bool

func (*SatParameters) GetExtraSubsolvers 

func (x *SatParameters) GetExtraSubsolvers() []string

func (*SatParameters) GetFeasibilityJumpDecay 

func (x *SatParameters) GetFeasibilityJumpDecay() float64

func (*SatParameters) GetFeasibilityJumpEnableRestarts 

func (x *SatParameters) GetFeasibilityJumpEnableRestarts() bool

func (*SatParameters) GetFeasibilityJumpLinearizationLevel 

func (x *SatParameters) GetFeasibilityJumpLinearizationLevel() int32

func (*SatParameters) GetFeasibilityJumpMaxExpandedConstraintSize 

func (x *SatParameters) GetFeasibilityJumpMaxExpandedConstraintSize() int32

func (*SatParameters) GetFeasibilityJumpRestartFactor 

func (x *SatParameters) GetFeasibilityJumpRestartFactor() int32

func (*SatParameters) GetFeasibilityJumpVarPerburbationRangeRatio 

func (x *SatParameters) GetFeasibilityJumpVarPerburbationRangeRatio() float64

func (*SatParameters) GetFeasibilityJumpVarRandomizationProbability 

func (x *SatParameters) GetFeasibilityJumpVarRandomizationProbability() float64

func (*SatParameters) GetFillAdditionalSolutionsInResponse 

func (x *SatParameters) GetFillAdditionalSolutionsInResponse() bool

func (*SatParameters) GetFillTightenedDomainsInResponse 

func (x *SatParameters) GetFillTightenedDomainsInResponse() bool

func (*SatParameters) GetFindBigLinearOverlap 

func (x *SatParameters) GetFindBigLinearOverlap() bool

func (*SatParameters) GetFindMultipleCores 

func (x *SatParameters) GetFindMultipleCores() bool

func (*SatParameters) GetFixVariablesToTheirHintedValue 

func (x *SatParameters) GetFixVariablesToTheirHintedValue() bool

func (*SatParameters) GetFpRounding 

func (x *SatParameters) GetFpRounding() SatParameters_FPRoundingMethod

func (*SatParameters) GetGlucoseDecayIncrement 

func (x *SatParameters) GetGlucoseDecayIncrement() float64

func (*SatParameters) GetGlucoseDecayIncrementPeriod 

func (x *SatParameters) GetGlucoseDecayIncrementPeriod() int32

func (*SatParameters) GetGlucoseMaxDecay 

func (x *SatParameters) GetGlucoseMaxDecay() float64

func (*SatParameters) GetHintConflictLimit 

func (x *SatParameters) GetHintConflictLimit() int32

func (*SatParameters) GetIgnoreNames 

func (x *SatParameters) GetIgnoreNames() bool

func (*SatParameters) GetIgnoreSubsolvers 

func (x *SatParameters) GetIgnoreSubsolvers() []string

func (*SatParameters) GetInferAllDiffs 

func (x *SatParameters) GetInferAllDiffs() bool

func (*SatParameters) GetInitialPolarity 

func (x *SatParameters) GetInitialPolarity() SatParameters_Polarity

func (*SatParameters) GetInitialVariablesActivity 

func (x *SatParameters) GetInitialVariablesActivity() float64

func (*SatParameters) GetInprocessingDtimeRatio 

func (x *SatParameters) GetInprocessingDtimeRatio() float64

func (*SatParameters) GetInprocessingMinimizationDtime 

func (x *SatParameters) GetInprocessingMinimizationDtime() float64

func (*SatParameters) GetInprocessingProbingDtime 

func (x *SatParameters) GetInprocessingProbingDtime() float64

func (*SatParameters) GetInstantiateAllVariables 

func (x *SatParameters) GetInstantiateAllVariables() bool

func (*SatParameters) GetInterleaveBatchSize 

func (x *SatParameters) GetInterleaveBatchSize() int32

func (*SatParameters) GetInterleaveSearch 

func (x *SatParameters) GetInterleaveSearch() bool

func (*SatParameters) GetKeepAllFeasibleSolutionsInPresolve 

func (x *SatParameters) GetKeepAllFeasibleSolutionsInPresolve() bool

func (*SatParameters) GetLinearSplitSize 

func (x *SatParameters) GetLinearSplitSize() int32

func (*SatParameters) GetLinearizationLevel 

func (x *SatParameters) GetLinearizationLevel() int32

func (*SatParameters) GetLogPrefix 

func (x *SatParameters) GetLogPrefix() string

func (*SatParameters) GetLogSearchProgress 

func (x *SatParameters) GetLogSearchProgress() bool

func (*SatParameters) GetLogSubsolverStatistics 

func (x *SatParameters) GetLogSubsolverStatistics() bool

func (*SatParameters) GetLogToResponse 

func (x *SatParameters) GetLogToResponse() bool

func (*SatParameters) GetLogToStdout 

func (x *SatParameters) GetLogToStdout() bool

func (*SatParameters) GetLpDualTolerance 

func (x *SatParameters) GetLpDualTolerance() float64

func (*SatParameters) GetLpPrimalTolerance 

func (x *SatParameters) GetLpPrimalTolerance() float64

func (*SatParameters) GetMaxAllDiffCutSize 

func (x *SatParameters) GetMaxAllDiffCutSize() int32

func (*SatParameters) GetMaxClauseActivityValue 

func (x *SatParameters) GetMaxClauseActivityValue() float64

func (*SatParameters) GetMaxConsecutiveInactiveCount 

func (x *SatParameters) GetMaxConsecutiveInactiveCount() int32

func (*SatParameters) GetMaxCutRoundsAtLevelZero 

func (x *SatParameters) GetMaxCutRoundsAtLevelZero() int32

func (*SatParameters) GetMaxDeterministicTime 

func (x *SatParameters) GetMaxDeterministicTime() float64

func (*SatParameters) GetMaxDomainSizeWhenEncodingEqNeqConstraints 

func (x *SatParameters) GetMaxDomainSizeWhenEncodingEqNeqConstraints() int32

func (*SatParameters) GetMaxIntegerRoundingScaling 

func (x *SatParameters) GetMaxIntegerRoundingScaling() int32

func (*SatParameters) GetMaxMemoryInMb 

func (x *SatParameters) GetMaxMemoryInMb() int64

func (*SatParameters) GetMaxNumCuts 

func (x *SatParameters) GetMaxNumCuts() int32

func (*SatParameters) GetMaxNumIntervalsForTimetableEdgeFinding 

func (x *SatParameters) GetMaxNumIntervalsForTimetableEdgeFinding() int32

func (*SatParameters) GetMaxNumberOfConflicts 

func (x *SatParameters) GetMaxNumberOfConflicts() int64

func (*SatParameters) GetMaxPairsPairwiseReasoningInNoOverlap_2D 

func (x *SatParameters) GetMaxPairsPairwiseReasoningInNoOverlap_2D() int32

func (*SatParameters) GetMaxPresolveIterations 

func (x *SatParameters) GetMaxPresolveIterations() int32

func (*SatParameters) GetMaxSatAssumptionOrder 

func (x *SatParameters) GetMaxSatAssumptionOrder() SatParameters_MaxSatAssumptionOrder

func (*SatParameters) GetMaxSatReverseAssumptionOrder 

func (x *SatParameters) GetMaxSatReverseAssumptionOrder() bool

func (*SatParameters) GetMaxSatStratification 

func (x *SatParameters) GetMaxSatStratification() SatParameters_MaxSatStratificationAlgorithm

func (*SatParameters) GetMaxSizeToCreatePrecedenceLiteralsInDisjunctive 

func (x *SatParameters) GetMaxSizeToCreatePrecedenceLiteralsInDisjunctive() int32

func (*SatParameters) GetMaxTimeInSeconds 

func (x *SatParameters) GetMaxTimeInSeconds() float64

func (*SatParameters) GetMaxVariableActivityValue 

func (x *SatParameters) GetMaxVariableActivityValue() float64

func (*SatParameters) GetMergeAtMostOneWorkLimit 

func (x *SatParameters) GetMergeAtMostOneWorkLimit() float64

func (*SatParameters) GetMergeNoOverlapWorkLimit 

func (x *SatParameters) GetMergeNoOverlapWorkLimit() float64

func (*SatParameters) GetMinNumLnsWorkers 

func (x *SatParameters) GetMinNumLnsWorkers() int32

func (*SatParameters) GetMinOrthogonalityForLpConstraints 

func (x *SatParameters) GetMinOrthogonalityForLpConstraints() float64

func (*SatParameters) GetMinimizationAlgorithm 

func (x *SatParameters) GetMinimizationAlgorithm() SatParameters_ConflictMinimizationAlgorithm

func (*SatParameters) GetMinimizeReductionDuringPbResolution 

func (x *SatParameters) GetMinimizeReductionDuringPbResolution() bool

func (*SatParameters) GetMipAutomaticallyScaleVariables 

func (x *SatParameters) GetMipAutomaticallyScaleVariables() bool

func (*SatParameters) GetMipCheckPrecision 

func (x *SatParameters) GetMipCheckPrecision() float64

func (*SatParameters) GetMipComputeTrueObjectiveBound 

func (x *SatParameters) GetMipComputeTrueObjectiveBound() bool

func (*SatParameters) GetMipDropTolerance 

func (x *SatParameters) GetMipDropTolerance() float64

func (*SatParameters) GetMipMaxActivityExponent 

func (x *SatParameters) GetMipMaxActivityExponent() int32

func (*SatParameters) GetMipMaxBound 

func (x *SatParameters) GetMipMaxBound() float64

func (*SatParameters) GetMipMaxValidMagnitude 

func (x *SatParameters) GetMipMaxValidMagnitude() float64

func (*SatParameters) GetMipPresolveLevel 

func (x *SatParameters) GetMipPresolveLevel() int32

func (*SatParameters) GetMipScaleLargeDomain 

func (x *SatParameters) GetMipScaleLargeDomain() bool

func (*SatParameters) GetMipTreatHighMagnitudeBoundsAsInfinity 

func (x *SatParameters) GetMipTreatHighMagnitudeBoundsAsInfinity() bool

func (*SatParameters) GetMipVarScaling 

func (x *SatParameters) GetMipVarScaling() float64

func (*SatParameters) GetMipWantedPrecision 

func (x *SatParameters) GetMipWantedPrecision() float64

func (*SatParameters) GetName 

func (x *SatParameters) GetName() string

func (*SatParameters) GetNewConstraintsBatchSize 

func (x *SatParameters) GetNewConstraintsBatchSize() int32

func (*SatParameters) GetNewLinearPropagation 

func (x *SatParameters) GetNewLinearPropagation() bool

func (*SatParameters) GetNumConflictsBeforeStrategyChanges 

func (x *SatParameters) GetNumConflictsBeforeStrategyChanges() int32

func (*SatParameters) GetNumSearchWorkers 

func (x *SatParameters) GetNumSearchWorkers() int32

func (*SatParameters) GetNumViolationLs 

func (x *SatParameters) GetNumViolationLs() int32

func (*SatParameters) GetNumWorkers 

func (x *SatParameters) GetNumWorkers() int32

func (*SatParameters) GetOnlyAddCutsAtLevelZero 

func (x *SatParameters) GetOnlyAddCutsAtLevelZero() bool

func (*SatParameters) GetOnlySolveIp 

func (x *SatParameters) GetOnlySolveIp() bool

func (*SatParameters) GetOptimizeWithCore 

func (x *SatParameters) GetOptimizeWithCore() bool

func (*SatParameters) GetOptimizeWithLbTreeSearch 

func (x *SatParameters) GetOptimizeWithLbTreeSearch() bool

func (*SatParameters) GetOptimizeWithMaxHs 

func (x *SatParameters) GetOptimizeWithMaxHs() bool

func (*SatParameters) GetPbCleanupIncrement 

func (x *SatParameters) GetPbCleanupIncrement() int32

func (*SatParameters) GetPbCleanupRatio 

func (x *SatParameters) GetPbCleanupRatio() float64

func (*SatParameters) GetPermutePresolveConstraintOrder 

func (x *SatParameters) GetPermutePresolveConstraintOrder() bool

func (*SatParameters) GetPermuteVariableRandomly 

func (x *SatParameters) GetPermuteVariableRandomly() bool

func (*SatParameters) GetPolarityRephaseIncrement 

func (x *SatParameters) GetPolarityRephaseIncrement() int32

func (*SatParameters) GetPolishLpSolution 

func (x *SatParameters) GetPolishLpSolution() bool

func (*SatParameters) GetPreferredVariableOrder 

func (x *SatParameters) GetPreferredVariableOrder() SatParameters_VariableOrder

func (*SatParameters) GetPresolveBlockedClause 

func (x *SatParameters) GetPresolveBlockedClause() bool

func (*SatParameters) GetPresolveBvaThreshold 

func (x *SatParameters) GetPresolveBvaThreshold() int32

func (*SatParameters) GetPresolveBveClauseWeight 

func (x *SatParameters) GetPresolveBveClauseWeight() int32

func (*SatParameters) GetPresolveBveThreshold 

func (x *SatParameters) GetPresolveBveThreshold() int32

func (*SatParameters) GetPresolveExtractIntegerEnforcement 

func (x *SatParameters) GetPresolveExtractIntegerEnforcement() bool

func (*SatParameters) GetPresolveInclusionWorkLimit 

func (x *SatParameters) GetPresolveInclusionWorkLimit() int64

func (*SatParameters) GetPresolveProbingDeterministicTimeLimit 

func (x *SatParameters) GetPresolveProbingDeterministicTimeLimit() float64

func (*SatParameters) GetPresolveSubstitutionLevel 

func (x *SatParameters) GetPresolveSubstitutionLevel() int32

func (*SatParameters) GetPresolveUseBva 

func (x *SatParameters) GetPresolveUseBva() bool

func (*SatParameters) GetProbingDeterministicTimeLimit 

func (x *SatParameters) GetProbingDeterministicTimeLimit() float64

func (*SatParameters) GetProbingNumCombinationsLimit 

func (x *SatParameters) GetProbingNumCombinationsLimit() int32

func (*SatParameters) GetPropagationLoopDetectionFactor 

func (x *SatParameters) GetPropagationLoopDetectionFactor() float64

func (*SatParameters) GetPseudoCostReliabilityThreshold 

func (x *SatParameters) GetPseudoCostReliabilityThreshold() int64

func (*SatParameters) GetPushAllTasksTowardStart 

func (x *SatParameters) GetPushAllTasksTowardStart() bool

func (*SatParameters) GetRandomBranchesRatio 

func (x *SatParameters) GetRandomBranchesRatio() float64

func (*SatParameters) GetRandomPolarityRatio 

func (x *SatParameters) GetRandomPolarityRatio() float64

func (*SatParameters) GetRandomSeed 

func (x *SatParameters) GetRandomSeed() int32

func (*SatParameters) GetRandomizeSearch 

func (x *SatParameters) GetRandomizeSearch() bool

func (*SatParameters) GetRelativeGapLimit 

func (x *SatParameters) GetRelativeGapLimit() float64

func (*SatParameters) GetRepairHint 

func (x *SatParameters) GetRepairHint() bool

func (*SatParameters) GetRestartAlgorithms 

func (x *SatParameters) GetRestartAlgorithms() []SatParameters_RestartAlgorithm

func (*SatParameters) GetRestartDlAverageRatio 

func (x *SatParameters) GetRestartDlAverageRatio() float64

func (*SatParameters) GetRestartLbdAverageRatio 

func (x *SatParameters) GetRestartLbdAverageRatio() float64

func (*SatParameters) GetRestartPeriod 

func (x *SatParameters) GetRestartPeriod() int32

func (*SatParameters) GetRestartRunningWindowSize 

func (x *SatParameters) GetRestartRunningWindowSize() int32

func (*SatParameters) GetRootLpIterations 

func (x *SatParameters) GetRootLpIterations() int32

func (*SatParameters) GetSearchBranching 

func (x *SatParameters) GetSearchBranching() SatParameters_SearchBranching

func (*SatParameters) GetSearchRandomVariablePoolSize 

func (x *SatParameters) GetSearchRandomVariablePoolSize() int64

func (*SatParameters) GetShareBinaryClauses 

func (x *SatParameters) GetShareBinaryClauses() bool

func (*SatParameters) GetShareLevelZeroBounds 

func (x *SatParameters) GetShareLevelZeroBounds() bool

func (*SatParameters) GetShareObjectiveBounds 

func (x *SatParameters) GetShareObjectiveBounds() bool

func (*SatParameters) GetSharedTreeMaxNodesPerWorker 

func (x *SatParameters) GetSharedTreeMaxNodesPerWorker() int32

func (*SatParameters) GetSharedTreeNumWorkers 

func (x *SatParameters) GetSharedTreeNumWorkers() int32

func (*SatParameters) GetSharedTreeSplitStrategy 

func (x *SatParameters) GetSharedTreeSplitStrategy() SatParameters_SharedTreeSplitStrategy

func (*SatParameters) GetSharedTreeWorkerObjectiveSplitProbability 

func (x *SatParameters) GetSharedTreeWorkerObjectiveSplitProbability() float64

func (*SatParameters) GetShavingSearchDeterministicTime 

func (x *SatParameters) GetShavingSearchDeterministicTime() float64

func (*SatParameters) GetSolutionPoolSize 

func (x *SatParameters) GetSolutionPoolSize() int32

func (*SatParameters) GetStopAfterFirstSolution 

func (x *SatParameters) GetStopAfterFirstSolution() bool

func (*SatParameters) GetStopAfterPresolve 

func (x *SatParameters) GetStopAfterPresolve() bool

func (*SatParameters) GetStopAfterRootPropagation 

func (x *SatParameters) GetStopAfterRootPropagation() bool

func (*SatParameters) GetStrategyChangeIncreaseRatio 

func (x *SatParameters) GetStrategyChangeIncreaseRatio() float64

func (*SatParameters) GetSubsolverParams 

func (x *SatParameters) GetSubsolverParams() []*SatParameters

func (*SatParameters) GetSubsolvers 

func (x *SatParameters) GetSubsolvers() []string

func (*SatParameters) GetSubsumptionDuringConflictAnalysis 

func (x *SatParameters) GetSubsumptionDuringConflictAnalysis() bool

func (*SatParameters) GetSymmetryLevel 

func (x *SatParameters) GetSymmetryLevel() int32

func (*SatParameters) GetTableCompressionLevel 

func (x *SatParameters) GetTableCompressionLevel() int32

func (*SatParameters) GetTestFeasibilityJump 

func (x *SatParameters) GetTestFeasibilityJump() bool

func (*SatParameters) GetUseAbslRandom 

func (x *SatParameters) GetUseAbslRandom() bool

func (*SatParameters) GetUseAreaEnergeticReasoningInNoOverlap_2D 

func (x *SatParameters) GetUseAreaEnergeticReasoningInNoOverlap_2D() bool

func (*SatParameters) GetUseBlockingRestart 

func (x *SatParameters) GetUseBlockingRestart() bool

func (*SatParameters) GetUseCombinedNoOverlap 

func (x *SatParameters) GetUseCombinedNoOverlap() bool

func (*SatParameters) GetUseDisjunctiveConstraintInCumulative 

func (x *SatParameters) GetUseDisjunctiveConstraintInCumulative() bool

func (*SatParameters) GetUseDualSchedulingHeuristics 

func (x *SatParameters) GetUseDualSchedulingHeuristics() bool

func (*SatParameters) GetUseDynamicPrecedenceInCumulative 

func (x *SatParameters) GetUseDynamicPrecedenceInCumulative() bool

func (*SatParameters) GetUseDynamicPrecedenceInDisjunctive 

func (x *SatParameters) GetUseDynamicPrecedenceInDisjunctive() bool

func (*SatParameters) GetUseEnergeticReasoningInNoOverlap_2D 

func (x *SatParameters) GetUseEnergeticReasoningInNoOverlap_2D() bool

func (*SatParameters) GetUseErwaHeuristic 

func (x *SatParameters) GetUseErwaHeuristic() bool

func (*SatParameters) GetUseExactLpReason 

func (x *SatParameters) GetUseExactLpReason() bool

func (*SatParameters) GetUseExtendedProbing 

func (x *SatParameters) GetUseExtendedProbing() bool

func (*SatParameters) GetUseFeasibilityJump 

func (x *SatParameters) GetUseFeasibilityJump() bool

func (*SatParameters) GetUseFeasibilityPump 

func (x *SatParameters) GetUseFeasibilityPump() bool

func (*SatParameters) GetUseHardPrecedencesInCumulative 

func (x *SatParameters) GetUseHardPrecedencesInCumulative() bool

func (*SatParameters) GetUseImpliedBounds 

func (x *SatParameters) GetUseImpliedBounds() bool

func (*SatParameters) GetUseLbRelaxLns 

func (x *SatParameters) GetUseLbRelaxLns() bool

func (*SatParameters) GetUseLnsOnly 

func (x *SatParameters) GetUseLnsOnly() bool

func (*SatParameters) GetUseObjectiveLbSearch 

func (x *SatParameters) GetUseObjectiveLbSearch() bool

func (*SatParameters) GetUseObjectiveShavingSearch 

func (x *SatParameters) GetUseObjectiveShavingSearch() bool

func (*SatParameters) GetUseOptimizationHints 

func (x *SatParameters) GetUseOptimizationHints() bool

func (*SatParameters) GetUseOptionalVariables 

func (x *SatParameters) GetUseOptionalVariables() bool

func (*SatParameters) GetUseOverloadCheckerInCumulative 

func (x *SatParameters) GetUseOverloadCheckerInCumulative() bool

func (*SatParameters) GetUsePbResolution 

func (x *SatParameters) GetUsePbResolution() bool

func (*SatParameters) GetUsePhaseSaving 

func (x *SatParameters) GetUsePhaseSaving() bool

func (*SatParameters) GetUsePrecedencesInDisjunctiveConstraint 

func (x *SatParameters) GetUsePrecedencesInDisjunctiveConstraint() bool

func (*SatParameters) GetUseProbingSearch 

func (x *SatParameters) GetUseProbingSearch() bool

func (*SatParameters) GetUseRinsLns 

func (x *SatParameters) GetUseRinsLns() bool

func (*SatParameters) GetUseSatInprocessing 

func (x *SatParameters) GetUseSatInprocessing() bool

func (*SatParameters) GetUseSharedTreeSearch 

func (x *SatParameters) GetUseSharedTreeSearch() bool

func (*SatParameters) GetUseShavingInProbingSearch 

func (x *SatParameters) GetUseShavingInProbingSearch() bool

func (*SatParameters) GetUseStrongPropagationInDisjunctive 

func (x *SatParameters) GetUseStrongPropagationInDisjunctive() bool

func (*SatParameters) GetUseTimetableEdgeFindingInCumulative 

func (x *SatParameters) GetUseTimetableEdgeFindingInCumulative() bool

func (*SatParameters) GetUseTimetablingInNoOverlap_2D 

func (x *SatParameters) GetUseTimetablingInNoOverlap_2D() bool

func (*SatParameters) GetVariableActivityDecay 

func (x *SatParameters) GetVariableActivityDecay() float64

func (*SatParameters) GetViolationLsCompoundMoveProbability 

func (x *SatParameters) GetViolationLsCompoundMoveProbability() float64

func (*SatParameters) GetViolationLsPerturbationPeriod 

func (x *SatParameters) GetViolationLsPerturbationPeriod() int32

func (*SatParameters) ProtoMessage 

func (*SatParameters) ProtoMessage()

func (*SatParameters) ProtoReflect 

func (x *SatParameters) ProtoReflect() protoreflect.Message

func (*SatParameters) Reset 

func (x *SatParameters) Reset()

func (*SatParameters) String 

func (x *SatParameters) String() string

type SatParameters_BinaryMinizationAlgorithm 

type SatParameters_BinaryMinizationAlgorithm int32

Whether to expoit the binary clause to minimize learned clauses further. 

const (
	SatParameters_NO_BINARY_MINIMIZATION                              SatParameters_BinaryMinizationAlgorithm = 0
	SatParameters_BINARY_MINIMIZATION_FIRST                           SatParameters_BinaryMinizationAlgorithm = 1
	SatParameters_BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION SatParameters_BinaryMinizationAlgorithm = 4
	SatParameters_BINARY_MINIMIZATION_WITH_REACHABILITY               SatParameters_BinaryMinizationAlgorithm = 2
	SatParameters_EXPERIMENTAL_BINARY_MINIMIZATION                    SatParameters_BinaryMinizationAlgorithm = 3
)

func (SatParameters_BinaryMinizationAlgorithm) Descriptor 

func (SatParameters_BinaryMinizationAlgorithm) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_BinaryMinizationAlgorithm) Enum 

func (x SatParameters_BinaryMinizationAlgorithm) Enum() *SatParameters_BinaryMinizationAlgorithm

func (SatParameters_BinaryMinizationAlgorithm) EnumDescriptor deprecated 

func (SatParameters_BinaryMinizationAlgorithm) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_BinaryMinizationAlgorithm.Descriptor instead.

func (SatParameters_BinaryMinizationAlgorithm) Number 

func (x SatParameters_BinaryMinizationAlgorithm) Number() protoreflect.EnumNumber

func (SatParameters_BinaryMinizationAlgorithm) String 

func (x SatParameters_BinaryMinizationAlgorithm) String() string

func (SatParameters_BinaryMinizationAlgorithm) Type 

func (SatParameters_BinaryMinizationAlgorithm) Type() protoreflect.EnumType

func (*SatParameters_BinaryMinizationAlgorithm) UnmarshalJSON deprecated 

func (x *SatParameters_BinaryMinizationAlgorithm) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_ClauseOrdering 

type SatParameters_ClauseOrdering int32

The clauses that will be kept during a cleanup are the ones that come first under this order. We always keep or exclude ties together. 

const (
	// Order clause by decreasing activity, then by increasing LBD.
	SatParameters_CLAUSE_ACTIVITY SatParameters_ClauseOrdering = 0
	// Order clause by increasing LBD, then by decreasing activity.
	SatParameters_CLAUSE_LBD SatParameters_ClauseOrdering = 1
)

func (SatParameters_ClauseOrdering) Descriptor 

func (SatParameters_ClauseOrdering) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_ClauseOrdering) Enum 

func (x SatParameters_ClauseOrdering) Enum() *SatParameters_ClauseOrdering

func (SatParameters_ClauseOrdering) EnumDescriptor deprecated 

func (SatParameters_ClauseOrdering) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_ClauseOrdering.Descriptor instead.

func (SatParameters_ClauseOrdering) Number 

func (x SatParameters_ClauseOrdering) Number() protoreflect.EnumNumber

func (SatParameters_ClauseOrdering) String 

func (x SatParameters_ClauseOrdering) String() string

func (SatParameters_ClauseOrdering) Type 

func (SatParameters_ClauseOrdering) Type() protoreflect.EnumType

func (*SatParameters_ClauseOrdering) UnmarshalJSON deprecated 

func (x *SatParameters_ClauseOrdering) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_ClauseProtection 

type SatParameters_ClauseProtection int32

Each time a clause activity is bumped, the clause has a chance to be protected during the next cleanup phase. Note that clauses used as a reason are always protected. 

const (
	SatParameters_PROTECTION_NONE   SatParameters_ClauseProtection = 0 // No protection.
	SatParameters_PROTECTION_ALWAYS SatParameters_ClauseProtection = 1 // Protect all clauses whose activity is bumped.
	SatParameters_PROTECTION_LBD    SatParameters_ClauseProtection = 2 // Only protect clause with a better LBD.
)

func (SatParameters_ClauseProtection) Descriptor 

func (SatParameters_ClauseProtection) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_ClauseProtection) Enum 

func (x SatParameters_ClauseProtection) Enum() *SatParameters_ClauseProtection

func (SatParameters_ClauseProtection) EnumDescriptor deprecated 

func (SatParameters_ClauseProtection) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_ClauseProtection.Descriptor instead.

func (SatParameters_ClauseProtection) Number 

func (x SatParameters_ClauseProtection) Number() protoreflect.EnumNumber

func (SatParameters_ClauseProtection) String 

func (x SatParameters_ClauseProtection) String() string

func (SatParameters_ClauseProtection) Type 

func (SatParameters_ClauseProtection) Type() protoreflect.EnumType

func (*SatParameters_ClauseProtection) UnmarshalJSON deprecated 

func (x *SatParameters_ClauseProtection) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_ConflictMinimizationAlgorithm 

type SatParameters_ConflictMinimizationAlgorithm int32

Do we try to minimize conflicts (greedily) when creating them. 

const (
	SatParameters_NONE         SatParameters_ConflictMinimizationAlgorithm = 0
	SatParameters_SIMPLE       SatParameters_ConflictMinimizationAlgorithm = 1
	SatParameters_RECURSIVE    SatParameters_ConflictMinimizationAlgorithm = 2
	SatParameters_EXPERIMENTAL SatParameters_ConflictMinimizationAlgorithm = 3
)

func (SatParameters_ConflictMinimizationAlgorithm) Descriptor 

func (SatParameters_ConflictMinimizationAlgorithm) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_ConflictMinimizationAlgorithm) Enum 

func (x SatParameters_ConflictMinimizationAlgorithm) Enum() *SatParameters_ConflictMinimizationAlgorithm

func (SatParameters_ConflictMinimizationAlgorithm) EnumDescriptor deprecated 

func (SatParameters_ConflictMinimizationAlgorithm) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_ConflictMinimizationAlgorithm.Descriptor instead.

func (SatParameters_ConflictMinimizationAlgorithm) Number 

func (x SatParameters_ConflictMinimizationAlgorithm) Number() protoreflect.EnumNumber

func (SatParameters_ConflictMinimizationAlgorithm) String 

func (x SatParameters_ConflictMinimizationAlgorithm) String() string

func (SatParameters_ConflictMinimizationAlgorithm) Type 

func (SatParameters_ConflictMinimizationAlgorithm) Type() protoreflect.EnumType

func (*SatParameters_ConflictMinimizationAlgorithm) UnmarshalJSON deprecated 

func (x *SatParameters_ConflictMinimizationAlgorithm) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_FPRoundingMethod 

type SatParameters_FPRoundingMethod int32

Rounding method to use for feasibility pump. 

const (
	// Rounds to the nearest integer value.
	SatParameters_NEAREST_INTEGER SatParameters_FPRoundingMethod = 0
	// Counts the number of linear constraints restricting the variable in the
	// increasing values (up locks) and decreasing values (down locks). Rounds
	// the variable in the direction of lesser locks.
	SatParameters_LOCK_BASED SatParameters_FPRoundingMethod = 1
	// Similar to lock based rounding except this only considers locks of active
	// constraints from the last lp solve.
	SatParameters_ACTIVE_LOCK_BASED SatParameters_FPRoundingMethod = 3
	// This is expensive rounding algorithm. We round variables one by one and
	// propagate the bounds in between. If none of the rounded values fall in
	// the continuous domain specified by lower and upper bound, we use the
	// current lower/upper bound (whichever one is closest) instead of rounding
	// the fractional lp solution value. If both the rounded values are in the
	// domain, we round to nearest integer.
	SatParameters_PROPAGATION_ASSISTED SatParameters_FPRoundingMethod = 2
)

func (SatParameters_FPRoundingMethod) Descriptor 

func (SatParameters_FPRoundingMethod) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_FPRoundingMethod) Enum 

func (x SatParameters_FPRoundingMethod) Enum() *SatParameters_FPRoundingMethod

func (SatParameters_FPRoundingMethod) EnumDescriptor deprecated 

func (SatParameters_FPRoundingMethod) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_FPRoundingMethod.Descriptor instead.

func (SatParameters_FPRoundingMethod) Number 

func (x SatParameters_FPRoundingMethod) Number() protoreflect.EnumNumber

func (SatParameters_FPRoundingMethod) String 

func (x SatParameters_FPRoundingMethod) String() string

func (SatParameters_FPRoundingMethod) Type 

func (SatParameters_FPRoundingMethod) Type() protoreflect.EnumType

func (*SatParameters_FPRoundingMethod) UnmarshalJSON deprecated 

func (x *SatParameters_FPRoundingMethod) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_MaxSatAssumptionOrder 

type SatParameters_MaxSatAssumptionOrder int32

In what order do we add the assumptions in a core-based max-sat algorithm 

const (
	SatParameters_DEFAULT_ASSUMPTION_ORDER   SatParameters_MaxSatAssumptionOrder = 0
	SatParameters_ORDER_ASSUMPTION_BY_DEPTH  SatParameters_MaxSatAssumptionOrder = 1
	SatParameters_ORDER_ASSUMPTION_BY_WEIGHT SatParameters_MaxSatAssumptionOrder = 2
)

func (SatParameters_MaxSatAssumptionOrder) Descriptor 

func (SatParameters_MaxSatAssumptionOrder) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_MaxSatAssumptionOrder) Enum 

func (x SatParameters_MaxSatAssumptionOrder) Enum() *SatParameters_MaxSatAssumptionOrder

func (SatParameters_MaxSatAssumptionOrder) EnumDescriptor deprecated 

func (SatParameters_MaxSatAssumptionOrder) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_MaxSatAssumptionOrder.Descriptor instead.

func (SatParameters_MaxSatAssumptionOrder) Number 

func (x SatParameters_MaxSatAssumptionOrder) Number() protoreflect.EnumNumber

func (SatParameters_MaxSatAssumptionOrder) String 

func (x SatParameters_MaxSatAssumptionOrder) String() string

func (SatParameters_MaxSatAssumptionOrder) Type 

func (SatParameters_MaxSatAssumptionOrder) Type() protoreflect.EnumType

func (*SatParameters_MaxSatAssumptionOrder) UnmarshalJSON deprecated 

func (x *SatParameters_MaxSatAssumptionOrder) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_MaxSatStratificationAlgorithm 

type SatParameters_MaxSatStratificationAlgorithm int32

What stratification algorithm we use in the presence of weight. 

const (
	// No stratification of the problem.
	SatParameters_STRATIFICATION_NONE SatParameters_MaxSatStratificationAlgorithm = 0
	// Start with literals with the highest weight, and when SAT, add the
	// literals with the next highest weight and so on.
	SatParameters_STRATIFICATION_DESCENT SatParameters_MaxSatStratificationAlgorithm = 1
	// Start with all literals. Each time a core is found with a given minimum
	// weight, do not consider literals with a lower weight for the next core
	// computation. If the subproblem is SAT, do like in STRATIFICATION_DESCENT
	// and just add the literals with the next highest weight.
	SatParameters_STRATIFICATION_ASCENT SatParameters_MaxSatStratificationAlgorithm = 2
)

func (SatParameters_MaxSatStratificationAlgorithm) Descriptor 

func (SatParameters_MaxSatStratificationAlgorithm) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_MaxSatStratificationAlgorithm) Enum 

func (x SatParameters_MaxSatStratificationAlgorithm) Enum() *SatParameters_MaxSatStratificationAlgorithm

func (SatParameters_MaxSatStratificationAlgorithm) EnumDescriptor deprecated 

func (SatParameters_MaxSatStratificationAlgorithm) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_MaxSatStratificationAlgorithm.Descriptor instead.

func (SatParameters_MaxSatStratificationAlgorithm) Number 

func (x SatParameters_MaxSatStratificationAlgorithm) Number() protoreflect.EnumNumber

func (SatParameters_MaxSatStratificationAlgorithm) String 

func (x SatParameters_MaxSatStratificationAlgorithm) String() string

func (SatParameters_MaxSatStratificationAlgorithm) Type 

func (SatParameters_MaxSatStratificationAlgorithm) Type() protoreflect.EnumType

func (*SatParameters_MaxSatStratificationAlgorithm) UnmarshalJSON deprecated 

func (x *SatParameters_MaxSatStratificationAlgorithm) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_Polarity 

type SatParameters_Polarity int32

Specifies the initial polarity (true/false) when the solver branches on a variable. This can be modified later by the user, or the phase saving heuristic.

Note(user): POLARITY_FALSE is usually a good choice because of the "natural" way to express a linear boolean problem. 

const (
	SatParameters_POLARITY_TRUE   SatParameters_Polarity = 0
	SatParameters_POLARITY_FALSE  SatParameters_Polarity = 1
	SatParameters_POLARITY_RANDOM SatParameters_Polarity = 2
)

func (SatParameters_Polarity) Descriptor 

func (SatParameters_Polarity) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_Polarity) Enum 

func (x SatParameters_Polarity) Enum() *SatParameters_Polarity

func (SatParameters_Polarity) EnumDescriptor deprecated 

func (SatParameters_Polarity) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_Polarity.Descriptor instead.

func (SatParameters_Polarity) Number 

func (x SatParameters_Polarity) Number() protoreflect.EnumNumber

func (SatParameters_Polarity) String 

func (x SatParameters_Polarity) String() string

func (SatParameters_Polarity) Type 

func (SatParameters_Polarity) Type() protoreflect.EnumType

func (*SatParameters_Polarity) UnmarshalJSON deprecated 

func (x *SatParameters_Polarity) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_RestartAlgorithm 

type SatParameters_RestartAlgorithm int32

Restart algorithms.

A reference for the more advanced ones is: Gilles Audemard, Laurent Simon, "Refining Restarts Strategies for SAT and UNSAT", Principles and Practice of Constraint Programming Lecture Notes in Computer Science 2012, pp 118-126 

const (
	SatParameters_NO_RESTART SatParameters_RestartAlgorithm = 0
	// Just follow a Luby sequence times restart_period.
	SatParameters_LUBY_RESTART SatParameters_RestartAlgorithm = 1
	// Moving average restart based on the decision level of conflicts.
	SatParameters_DL_MOVING_AVERAGE_RESTART SatParameters_RestartAlgorithm = 2
	// Moving average restart based on the LBD of conflicts.
	SatParameters_LBD_MOVING_AVERAGE_RESTART SatParameters_RestartAlgorithm = 3
	// Fixed period restart every restart period.
	SatParameters_FIXED_RESTART SatParameters_RestartAlgorithm = 4
)

func (SatParameters_RestartAlgorithm) Descriptor 

func (SatParameters_RestartAlgorithm) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_RestartAlgorithm) Enum 

func (x SatParameters_RestartAlgorithm) Enum() *SatParameters_RestartAlgorithm

func (SatParameters_RestartAlgorithm) EnumDescriptor deprecated 

func (SatParameters_RestartAlgorithm) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_RestartAlgorithm.Descriptor instead.

func (SatParameters_RestartAlgorithm) Number 

func (x SatParameters_RestartAlgorithm) Number() protoreflect.EnumNumber

func (SatParameters_RestartAlgorithm) String 

func (x SatParameters_RestartAlgorithm) String() string

func (SatParameters_RestartAlgorithm) Type 

func (SatParameters_RestartAlgorithm) Type() protoreflect.EnumType

func (*SatParameters_RestartAlgorithm) UnmarshalJSON deprecated 

func (x *SatParameters_RestartAlgorithm) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_SearchBranching 

type SatParameters_SearchBranching int32

The search branching will be used to decide how to branch on unfixed nodes. 

const (
	// Try to fix all literals using the underlying SAT solver's heuristics,
	// then generate and fix literals until integer variables are fixed. New
	// literals on integer variables are generated using the fixed search
	// specified by the user or our default one.
	SatParameters_AUTOMATIC_SEARCH SatParameters_SearchBranching = 0
	// If used then all decisions taken by the solver are made using a fixed
	// order as specified in the API or in the CpModelProto search_strategy
	// field.
	SatParameters_FIXED_SEARCH SatParameters_SearchBranching = 1
	// Simple portfolio search used by LNS workers.
	SatParameters_PORTFOLIO_SEARCH SatParameters_SearchBranching = 2
	// If used, the solver will use heuristics from the LP relaxation. This
	// exploit the reduced costs of the variables in the relaxation.
	SatParameters_LP_SEARCH SatParameters_SearchBranching = 3
	// If used, the solver uses the pseudo costs for branching. Pseudo costs
	// are computed using the historical change in objective bounds when some
	// decision are taken. Note that this works whether we use an LP or not.
	SatParameters_PSEUDO_COST_SEARCH SatParameters_SearchBranching = 4
	// Mainly exposed here for testing. This quickly tries a lot of randomized
	// heuristics with a low conflict limit. It usually provides a good first
	// solution.
	SatParameters_PORTFOLIO_WITH_QUICK_RESTART_SEARCH SatParameters_SearchBranching = 5
	// Mainly used internally. This is like FIXED_SEARCH, except we follow the
	// solution_hint field of the CpModelProto rather than using the information
	// provided in the search_strategy.
	SatParameters_HINT_SEARCH SatParameters_SearchBranching = 6
	// Similar to FIXED_SEARCH, but differ in how the variable not listed into
	// the fixed search heuristics are branched on. This will always start the
	// search tree according to the specified fixed search strategy, but will
	// complete it using the default automatic search.
	SatParameters_PARTIAL_FIXED_SEARCH SatParameters_SearchBranching = 7
	// Randomized search. Used to increase entropy in the search.
	SatParameters_RANDOMIZED_SEARCH SatParameters_SearchBranching = 8
)

func (SatParameters_SearchBranching) Descriptor 

func (SatParameters_SearchBranching) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_SearchBranching) Enum 

func (x SatParameters_SearchBranching) Enum() *SatParameters_SearchBranching

func (SatParameters_SearchBranching) EnumDescriptor deprecated 

func (SatParameters_SearchBranching) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_SearchBranching.Descriptor instead.

func (SatParameters_SearchBranching) Number 

func (x SatParameters_SearchBranching) Number() protoreflect.EnumNumber

func (SatParameters_SearchBranching) String 

func (x SatParameters_SearchBranching) String() string

func (SatParameters_SearchBranching) Type 

func (SatParameters_SearchBranching) Type() protoreflect.EnumType

func (*SatParameters_SearchBranching) UnmarshalJSON deprecated 

func (x *SatParameters_SearchBranching) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_SharedTreeSplitStrategy 

type SatParameters_SharedTreeSplitStrategy int32
const (
	// Uses the default strategy, currently equivalent to
	// SPLIT_STRATEGY_DISCREPANCY.
	SatParameters_SPLIT_STRATEGY_AUTO SatParameters_SharedTreeSplitStrategy = 0
	// Only accept splits if the node to be split's depth+discrepancy is minimal
	// for the desired number of leaves.
	// The preferred child for discrepancy calculation is the one with the
	// lowest objective lower bound or the original branch direction if the
	// bounds are equal. This rule allows twice as many workers to work in the
	// preferred subtree as non-preferred.
	SatParameters_SPLIT_STRATEGY_DISCREPANCY SatParameters_SharedTreeSplitStrategy = 1
	// Only split nodes with an objective lb equal to the global lb.
	SatParameters_SPLIT_STRATEGY_OBJECTIVE_LB SatParameters_SharedTreeSplitStrategy = 2
	// Attempt to keep the shared tree balanced.
	SatParameters_SPLIT_STRATEGY_BALANCED_TREE SatParameters_SharedTreeSplitStrategy = 3
	// Workers race to split their subtree, the winner's proposal is accepted.
	SatParameters_SPLIT_STRATEGY_FIRST_PROPOSAL SatParameters_SharedTreeSplitStrategy = 4
)

func (SatParameters_SharedTreeSplitStrategy) Descriptor 

func (SatParameters_SharedTreeSplitStrategy) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_SharedTreeSplitStrategy) Enum 

func (x SatParameters_SharedTreeSplitStrategy) Enum() *SatParameters_SharedTreeSplitStrategy

func (SatParameters_SharedTreeSplitStrategy) EnumDescriptor deprecated 

func (SatParameters_SharedTreeSplitStrategy) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_SharedTreeSplitStrategy.Descriptor instead.

func (SatParameters_SharedTreeSplitStrategy) Number 

func (x SatParameters_SharedTreeSplitStrategy) Number() protoreflect.EnumNumber

func (SatParameters_SharedTreeSplitStrategy) String 

func (x SatParameters_SharedTreeSplitStrategy) String() string

func (SatParameters_SharedTreeSplitStrategy) Type 

func (SatParameters_SharedTreeSplitStrategy) Type() protoreflect.EnumType

func (*SatParameters_SharedTreeSplitStrategy) UnmarshalJSON deprecated 

func (x *SatParameters_SharedTreeSplitStrategy) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

type SatParameters_VariableOrder 

type SatParameters_VariableOrder int32

Variables without activity (i.e. at the beginning of the search) will be tried in this preferred order. 

const (
	SatParameters_IN_ORDER         SatParameters_VariableOrder = 0 // As specified by the problem.
	SatParameters_IN_REVERSE_ORDER SatParameters_VariableOrder = 1
	SatParameters_IN_RANDOM_ORDER  SatParameters_VariableOrder = 2
)

func (SatParameters_VariableOrder) Descriptor 

func (SatParameters_VariableOrder) Descriptor() protoreflect.EnumDescriptor

func (SatParameters_VariableOrder) Enum 

func (x SatParameters_VariableOrder) Enum() *SatParameters_VariableOrder

func (SatParameters_VariableOrder) EnumDescriptor deprecated 

func (SatParameters_VariableOrder) EnumDescriptor() ([]byte, []int)

Deprecated: Use SatParameters_VariableOrder.Descriptor instead.

func (SatParameters_VariableOrder) Number 

func (x SatParameters_VariableOrder) Number() protoreflect.EnumNumber

func (SatParameters_VariableOrder) String 

func (x SatParameters_VariableOrder) String() string

func (SatParameters_VariableOrder) Type 

func (SatParameters_VariableOrder) Type() protoreflect.EnumType

func (*SatParameters_VariableOrder) UnmarshalJSON deprecated 

func (x *SatParameters_VariableOrder) UnmarshalJSON(b []byte) error

Deprecated: Do not use.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.