Uses of Class
com.google.ortools.sat.SatParameters.Builder
Packages that use SatParameters.Builder
Package
Description
-
Uses of SatParameters.Builder in com.google.ortools.constraintsolver
Methods in com.google.ortools.constraintsolver that return SatParameters.BuilderModifier and TypeMethodDescriptionRoutingSearchParameters.Builder.getSatParametersBuilder()If use_cp_sat or use_generalized_cp_sat is true, contains the SAT algorithm parameters which will be used.Methods in com.google.ortools.constraintsolver with parameters of type SatParameters.BuilderModifier and TypeMethodDescriptionRoutingSearchParameters.Builder.setSatParameters(SatParameters.Builder builderForValue) If use_cp_sat or use_generalized_cp_sat is true, contains the SAT algorithm parameters which will be used. -
Uses of SatParameters.Builder in com.google.ortools.sat
Subclasses with type arguments of type SatParameters.Builder in com.google.ortools.satModifier and TypeClassDescriptionstatic final classContains the definitions for all the sat algorithm parameters and their default values.Methods in com.google.ortools.sat that return SatParameters.BuilderModifier and TypeMethodDescriptionSatParameters.Builder.addAllExtraSubsolvers(Iterable<String> values) A convenient way to add more workers types.SatParameters.Builder.addAllFilterSubsolvers(Iterable<String> values) repeated string filter_subsolvers = 293;SatParameters.Builder.addAllIgnoreSubsolvers(Iterable<String> values) Rather than fully specifying subsolvers, it is often convenient to just remove the ones that are not useful on a given problem or only keep specific ones for testing.SatParameters.Builder.addAllRestartAlgorithms(Iterable<? extends SatParameters.RestartAlgorithm> values) The restart strategies will change each time the strategy_counter is increased.SatParameters.Builder.addAllSubsolverParams(Iterable<? extends SatParameters> values) It is possible to specify additional subsolver configuration.SatParameters.Builder.addAllSubsolvers(Iterable<String> values) In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.SatParameters.Builder.addExtraSubsolvers(String value) A convenient way to add more workers types.SatParameters.Builder.addExtraSubsolversBytes(com.google.protobuf.ByteString value) A convenient way to add more workers types.SatParameters.Builder.addFilterSubsolvers(String value) repeated string filter_subsolvers = 293;SatParameters.Builder.addFilterSubsolversBytes(com.google.protobuf.ByteString value) repeated string filter_subsolvers = 293;SatParameters.Builder.addIgnoreSubsolvers(String value) Rather than fully specifying subsolvers, it is often convenient to just remove the ones that are not useful on a given problem or only keep specific ones for testing.SatParameters.Builder.addIgnoreSubsolversBytes(com.google.protobuf.ByteString value) Rather than fully specifying subsolvers, it is often convenient to just remove the ones that are not useful on a given problem or only keep specific ones for testing.SatParameters.Builder.addRestartAlgorithms(SatParameters.RestartAlgorithm value) The restart strategies will change each time the strategy_counter is increased.SatParameters.Builder.addSubsolverParams(int index, SatParameters value) It is possible to specify additional subsolver configuration.SatParameters.Builder.addSubsolverParams(int index, SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.SatParameters.Builder.addSubsolverParams(SatParameters value) It is possible to specify additional subsolver configuration.SatParameters.Builder.addSubsolverParams(SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.SatParameters.Builder.addSubsolverParamsBuilder()It is possible to specify additional subsolver configuration.SatParameters.Builder.addSubsolverParamsBuilder(int index) It is possible to specify additional subsolver configuration.SatParameters.Builder.addSubsolvers(String value) In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.SatParameters.Builder.addSubsolversBytes(com.google.protobuf.ByteString value) In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.SatParameters.Builder.clear()SatParameters.Builder.clearAbsoluteGapLimit()Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit.SatParameters.Builder.clearAddCgCuts()Whether we generate and add Chvatal-Gomory cuts to the LP at root node.SatParameters.Builder.clearAddCliqueCuts()Whether we generate clique cuts from the binary implication graph.SatParameters.Builder.clearAddLinMaxCuts()For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et.SatParameters.Builder.clearAddLpConstraintsLazily()If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch.SatParameters.Builder.clearAddMirCuts()Whether we generate MIR cuts at root node.SatParameters.Builder.clearAddObjectiveCut()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?SatParameters.Builder.clearAddRltCuts()Whether we generate RLT cuts.SatParameters.Builder.clearAddZeroHalfCuts()Whether we generate Zero-Half cuts at root node.SatParameters.Builder.clearAlsoBumpVariablesInConflictReasons()When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped.SatParameters.Builder.clearAtMostOneMaxExpansionSize()All at_most_one constraints with a size <= param will be replaced by a quadratic number of binary implications.SatParameters.Builder.clearAutoDetectGreaterThanAtLeastOneOf()If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present.SatParameters.Builder.clearBinaryMinimizationAlgorithm()optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];SatParameters.Builder.clearBinarySearchNumConflicts()If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict.SatParameters.Builder.clearBlockingRestartMultiplier()optional double blocking_restart_multiplier = 66 [default = 1.4];SatParameters.Builder.clearBlockingRestartWindowSize()optional int32 blocking_restart_window_size = 65 [default = 5000];SatParameters.Builder.clearBooleanEncodingLevel()A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.SatParameters.Builder.clearCatchSigintSignal()Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve.SatParameters.Builder.clearClauseActivityDecay()Clause activity parameters (same effect as the one on the variables).SatParameters.Builder.clearClauseCleanupLbdBound()All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.SatParameters.Builder.clearClauseCleanupOrdering()optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];SatParameters.Builder.clearClauseCleanupPeriod()Trigger a cleanup when this number of "deletable" clauses is learned.SatParameters.Builder.clearClauseCleanupProtection()optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];SatParameters.Builder.clearClauseCleanupRatio()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.SatParameters.Builder.clearClauseCleanupTarget()During a cleanup, we will always keep that number of "deletable" clauses.SatParameters.Builder.clearConvertIntervals()Temporary flag util the feature is more mature.SatParameters.Builder.clearCoreMinimizationLevel()If positive, we spend some effort on each core: - At level 1, we use a simple heuristic to try to minimize an UNSAT coreSatParameters.Builder.clearCountAssumptionLevelsInLbd()Whether or not the assumption levels are taken into account during the LBD computation.SatParameters.Builder.clearCoverOptimization()If true, when the max-sat algo find a core, we compute the minimal number of literals in the core that needs to be true to have a feasible solution.SatParameters.Builder.clearCpModelPresolve()Whether we presolve the cp_model before solving it.SatParameters.Builder.clearCpModelProbingLevel()How much effort do we spend on probing. 0 disables it completely.SatParameters.Builder.clearCpModelUseSatPresolve()Whether we also use the sat presolve when cp_model_presolve is true.SatParameters.Builder.clearCutActiveCountDecay()optional double cut_active_count_decay = 156 [default = 0.8];SatParameters.Builder.clearCutCleanupTarget()Target number of constraints to remove during cleanup.SatParameters.Builder.clearCutLevel()Control the global cut effort.SatParameters.Builder.clearCutMaxActiveCountValue()These parameters are similar to sat clause management activity parameters.SatParameters.Builder.clearDebugCrashIfPresolveBreaksHint()Crash if presolve breaks a feasible hint.SatParameters.Builder.clearDebugCrashOnBadHint()Crash if we do not manage to complete the hint into a full solution.SatParameters.Builder.clearDebugMaxNumPresolveOperations()If positive, try to stop just after that many presolve rules have been applied.SatParameters.Builder.clearDebugPostsolveWithFullSolver()We have two different postsolve code.SatParameters.Builder.clearDefaultRestartAlgorithms()optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];SatParameters.Builder.clearDetectLinearizedProduct()Infer products of Boolean or of Boolean time IntegerVariable from the linear constrainst in the problem.SatParameters.Builder.clearDetectTableWithCost()If true, we detect variable that are unique to a table constraint and only there to encode a cost on each tuple.SatParameters.Builder.clearDisableConstraintExpansion()If true, it disable all constraint expansion.SatParameters.Builder.clearDiversifyLnsParams()If true, registers more lns subsolvers with different parameters.SatParameters.Builder.clearEncodeComplexLinearConstraintWithInteger()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.SatParameters.Builder.clearEncodeCumulativeAsReservoir()Encore cumulative with fixed demands and capacity as a reservoir constraint.SatParameters.Builder.clearEnumerateAllSolutions()Whether we enumerate all solutions of a problem without objective.SatParameters.Builder.clearExpandAlldiffConstraints()If true, expand all_different constraints that are not permutations.SatParameters.Builder.clearExpandReservoirConstraints()If true, expand the reservoir constraints by creating booleans for all possible precedences between event and encoding the constraint.SatParameters.Builder.clearExpandReservoirUsingCircuit()Mainly useful for testing.SatParameters.Builder.clearExploitAllLpSolution()If true and the Lp relaxation of the problem has a solution, try to exploit it.SatParameters.Builder.clearExploitAllPrecedences()optional bool exploit_all_precedences = 220 [default = false];SatParameters.Builder.clearExploitBestSolution()When branching on a variable, follow the last best solution value.SatParameters.Builder.clearExploitIntegerLpSolution()If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it.SatParameters.Builder.clearExploitObjective()When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.SatParameters.Builder.clearExploitRelaxationSolution()When branching on a variable, follow the last best relaxation solution value.SatParameters.Builder.clearExtraSubsolvers()A convenient way to add more workers types.SatParameters.Builder.clearFeasibilityJumpBatchDtime()How much dtime for each LS batch.SatParameters.Builder.clearFeasibilityJumpDecay()On each restart, we randomly choose if we use decay (with this parameter) or no decay.SatParameters.Builder.clearFeasibilityJumpEnableRestarts()When stagnating, feasibility jump will either restart from a default solution (with some possible randomization), or randomly pertubate the current solution.SatParameters.Builder.clearFeasibilityJumpLinearizationLevel()How much do we linearize the problem in the local search code.SatParameters.Builder.clearFeasibilityJumpMaxExpandedConstraintSize()Maximum size of no_overlap or no_overlap_2d constraint for a quadratic expansion.SatParameters.Builder.clearFeasibilityJumpRestartFactor()This is a factor that directly influence the work before each restart.SatParameters.Builder.clearFeasibilityJumpVarPerburbationRangeRatio()Max distance between the default value and the pertubated value relative to the range of the domain of the variable.SatParameters.Builder.clearFeasibilityJumpVarRandomizationProbability()Probability for a variable to have a non default value upon restarts or perturbations.SatParameters.Builder.clearFillAdditionalSolutionsInResponse()If true, the final response addition_solutions field will be filled with all solutions from our solutions pool.SatParameters.Builder.clearFillTightenedDomainsInResponse()If true, add information about the derived variable domains to the CpSolverResponse.SatParameters.Builder.clearFilterSatPostsolveClauses()Internal parameter.SatParameters.Builder.clearFilterSubsolvers()repeated string filter_subsolvers = 293;SatParameters.Builder.clearFindBigLinearOverlap()Try to find large "rectangle" in the linear constraint matrix with identical lines.SatParameters.Builder.clearFindMultipleCores()Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.SatParameters.Builder.clearFixVariablesToTheirHintedValue()If true, variables appearing in the solution hints will be fixed to their hinted value.SatParameters.Builder.clearFpRounding()optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];SatParameters.Builder.clearGlucoseDecayIncrement()optional double glucose_decay_increment = 23 [default = 0.01];SatParameters.Builder.clearGlucoseDecayIncrementPeriod()optional int32 glucose_decay_increment_period = 24 [default = 5000];SatParameters.Builder.clearGlucoseMaxDecay()The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95.SatParameters.Builder.clearHintConflictLimit()Conflict limit used in the phase that exploit the solution hint.SatParameters.Builder.clearIgnoreNames()If true, we don't keep names in our internal copy of the user given model.SatParameters.Builder.clearIgnoreSubsolvers()Rather than fully specifying subsolvers, it is often convenient to just remove the ones that are not useful on a given problem or only keep specific ones for testing.SatParameters.Builder.clearInferAllDiffs()Run a max-clique code amongst all the x !SatParameters.Builder.clearInitialPolarity()optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];SatParameters.Builder.clearInitialVariablesActivity()The initial value of the variables activity.SatParameters.Builder.clearInprocessingDtimeRatio()Proportion of deterministic time we should spend on inprocessing.SatParameters.Builder.clearInprocessingMinimizationDtime()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.SatParameters.Builder.clearInprocessingMinimizationUseAllOrderings()optional bool inprocessing_minimization_use_all_orderings = 298 [default = false];SatParameters.Builder.clearInprocessingMinimizationUseConflictAnalysis()optional bool inprocessing_minimization_use_conflict_analysis = 297 [default = true];SatParameters.Builder.clearInprocessingProbingDtime()The amount of dtime we should spend on probing for each inprocessing round.SatParameters.Builder.clearInstantiateAllVariables()If true, the solver will add a default integer branching strategy to the already defined search strategy.SatParameters.Builder.clearInterleaveBatchSize()optional int32 interleave_batch_size = 134 [default = 0];SatParameters.Builder.clearInterleaveSearch()Experimental.SatParameters.Builder.clearKeepAllFeasibleSolutionsInPresolve()If true, we disable the presolve reductions that remove feasible solutions from the search space.SatParameters.Builder.clearKeepSymmetryInPresolve()Experimental.SatParameters.Builder.clearLbRelaxNumWorkersThreshold()Only use lb-relax if we have at least that many workers.SatParameters.Builder.clearLinearizationLevel()A non-negative level indicating the type of constraints we consider in the LP relaxation.SatParameters.Builder.clearLinearSplitSize()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.SatParameters.Builder.clearLnsInitialDeterministicLimit()optional double lns_initial_deterministic_limit = 308 [default = 0.1];SatParameters.Builder.clearLnsInitialDifficulty()Initial parameters for neighborhood generation.SatParameters.Builder.clearLogPrefix()Add a prefix to all logs.SatParameters.Builder.clearLogSearchProgress()Whether the solver should log the search progress.SatParameters.Builder.clearLogSubsolverStatistics()Whether the solver should display per sub-solver search statistics.SatParameters.Builder.clearLogToResponse()Log to response proto.SatParameters.Builder.clearLogToStdout()Log to stdout.SatParameters.Builder.clearLpDualTolerance()optional double lp_dual_tolerance = 267 [default = 1e-07];SatParameters.Builder.clearLpPrimalTolerance()The internal LP tolerances used by CP-SAT.SatParameters.Builder.clearMaxAllDiffCutSize()Cut generator for all diffs can add too many cuts for large all_diff constraints.SatParameters.Builder.clearMaxAlldiffDomainSize()Max domain size for all_different constraints to be expanded.SatParameters.Builder.clearMaxClauseActivityValue()optional double max_clause_activity_value = 18 [default = 1e+20];SatParameters.Builder.clearMaxConsecutiveInactiveCount()If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP.SatParameters.Builder.clearMaxCutRoundsAtLevelZero()Max number of time we perform cut generation and resolve the LP at level 0.SatParameters.Builder.clearMaxDeterministicTime()Maximum time allowed in deterministic time to solve a problem.SatParameters.Builder.clearMaxDomainSizeWhenEncodingEqNeqConstraints()When loading a*x + b*y ==/!SatParameters.Builder.clearMaximumRegionsToSplitInDisconnectedNoOverlap2D()Detects when the space where items of a no_overlap_2d constraint can placed is disjoint (ie., fixed boxes split the domain).SatParameters.Builder.clearMaxIntegerRoundingScaling()In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive).SatParameters.Builder.clearMaxLinMaxSizeForExpansion()If the number of expressions in the lin_max is less that the max size parameter, model expansion replaces target = max(xi) by linear constraint with the introduction of new booleans bi such that bi => target == xi.SatParameters.Builder.clearMaxMemoryInMb()Maximum memory allowed for the whole thread containing the solver.SatParameters.Builder.clearMaxNumberOfConflicts()Maximum number of conflicts allowed to solve a problem.SatParameters.Builder.clearMaxNumCuts()The limit on the number of cuts in our cut pool.SatParameters.Builder.clearMaxNumDeterministicBatches()Stops after that number of batches has been scheduled.SatParameters.Builder.clearMaxNumIntervalsForTimetableEdgeFinding()Max number of intervals for the timetable_edge_finding algorithm to propagate.SatParameters.Builder.clearMaxPairsPairwiseReasoningInNoOverlap2D()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.SatParameters.Builder.clearMaxPresolveIterations()In case of large reduction in a presolve iteration, we perform multiple presolve iterations.SatParameters.Builder.clearMaxSatAssumptionOrder()optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];SatParameters.Builder.clearMaxSatReverseAssumptionOrder()If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.SatParameters.Builder.clearMaxSatStratification()optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];SatParameters.Builder.clearMaxSizeToCreatePrecedenceLiteralsInDisjunctive()Create one literal for each disjunction of two pairs of tasks.SatParameters.Builder.clearMaxTimeInSeconds()Maximum time allowed in seconds to solve a problem.SatParameters.Builder.clearMaxVariableActivityValue()optional double max_variable_activity_value = 16 [default = 1e+100];SatParameters.Builder.clearMergeAtMostOneWorkLimit()optional double merge_at_most_one_work_limit = 146 [default = 100000000];SatParameters.Builder.clearMergeNoOverlapWorkLimit()During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints.SatParameters.Builder.clearMinimizationAlgorithm()optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];SatParameters.Builder.clearMinimizeReductionDuringPbResolution()A different algorithm during PB resolution.SatParameters.Builder.clearMinimizeSharedClauses()Minimize and detect subsumption of shared clauses immediately after they are imported.SatParameters.Builder.clearMinOrthogonalityForLpConstraints()While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call.SatParameters.Builder.clearMipAutomaticallyScaleVariables()If true, some continuous variable might be automatically scaled.SatParameters.Builder.clearMipCheckPrecision()As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted precision during scaling.SatParameters.Builder.clearMipComputeTrueObjectiveBound()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.SatParameters.Builder.clearMipDropTolerance()Any value in the input mip with a magnitude lower than this will be set to zero.SatParameters.Builder.clearMipMaxActivityExponent()To avoid integer overflow, we always force the maximum possible constraint activity (and objective value) according to the initial variable domain to be smaller than 2 to this given power.SatParameters.Builder.clearMipMaxBound()We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use.SatParameters.Builder.clearMipMaxValidMagnitude()Any finite values in the input MIP must be below this threshold, otherwise the model will be reported invalid.SatParameters.Builder.clearMipPresolveLevel()When solving a MIP, we do some basic floating point presolving before scaling the problem to integer to be handled by CP-SAT.SatParameters.Builder.clearMipScaleLargeDomain()If this is false, then mip_var_scaling is only applied to variables with "small" domain.SatParameters.Builder.clearMipTreatHighMagnitudeBoundsAsInfinity()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.SatParameters.Builder.clearMipVarScaling()All continuous variable of the problem will be multiplied by this factor.SatParameters.Builder.clearMipWantedPrecision()When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients.SatParameters.Builder.clearName()In some context, like in a portfolio of search, it makes sense to name a given parameters set for logging purpose.SatParameters.Builder.clearNewConstraintsBatchSize()Add that many lazy constraints (or cuts) at once in the LP.SatParameters.Builder.clearNewLinearPropagation()The new linear propagation code treat all constraints at once and use an adaptation of Bellman-Ford-Tarjan to propagate constraint in a smarter order and potentially detect propagation cycle earlier.SatParameters.Builder.clearNoOverlap2DBooleanRelationsLimit()If less than this number of boxes are present in a no-overlap 2d, we create 4 Booleans per pair of boxes: - Box 2 is after Box 1 on xSatParameters.Builder.clearNumConflictsBeforeStrategyChanges()After each restart, if the number of conflict since the last strategy change is greater that this, then we increment a "strategy_counter" that can be use to change the search strategy used by the following restarts.SatParameters.Builder.clearNumFullSubsolvers()We distinguish subsolvers that consume a full thread, and the ones that are always interleaved.SatParameters.Builder.clearNumSearchWorkers()optional int32 num_search_workers = 100 [default = 0];SatParameters.Builder.clearNumViolationLs()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.SatParameters.Builder.clearNumWorkers()Specify the number of parallel workers (i.e. threads) to use during search.SatParameters.Builder.clearOnlyAddCutsAtLevelZero()For the cut that can be generated at any level, this control if we only try to generate them at the root node.SatParameters.Builder.clearOnlySolveIp()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.SatParameters.Builder.clearOptimizeWithCore()The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one.SatParameters.Builder.clearOptimizeWithLbTreeSearch()Do a more conventional tree search (by opposition to SAT based one) where we keep all the explored node in a tree.SatParameters.Builder.clearOptimizeWithMaxHs()This has no effect if optimize_with_core is false.SatParameters.Builder.clearPbCleanupIncrement()Same as for the clauses, but for the learned pseudo-Boolean constraints.SatParameters.Builder.clearPbCleanupRatio()optional double pb_cleanup_ratio = 47 [default = 0.5];SatParameters.Builder.clearPermutePresolveConstraintOrder()optional bool permute_presolve_constraint_order = 179 [default = false];SatParameters.Builder.clearPermuteVariableRandomly()This is mainly here to test the solver variability.SatParameters.Builder.clearPolarityExploitLsHints()If true and we have first solution LS workers, tries in some phase to follow a LS solutions that violates has litle constraints as possible.SatParameters.Builder.clearPolarityRephaseIncrement()If non-zero, then we change the polarity heuristic after that many number of conflicts in an arithmetically increasing fashion.SatParameters.Builder.clearPolishLpSolution()Whether we try to do a few degenerate iteration at the end of an LP solve to minimize the fractionality of the integer variable in the basis.SatParameters.Builder.clearPreferredVariableOrder()optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];SatParameters.Builder.clearPresolveBlockedClause()Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.SatParameters.Builder.clearPresolveBvaThreshold()Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold.SatParameters.Builder.clearPresolveBveClauseWeight()During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.SatParameters.Builder.clearPresolveBveThreshold()During presolve, only try to perform the bounded variable elimination (BVE) of a variable x if the number of occurrences of x times the number of occurrences of not(x) is not greater than this parameter.SatParameters.Builder.clearPresolveExtractIntegerEnforcement()If true, we will extract from linear constraints, enforcement literals of the form "integer variable at bound => simplified constraint".SatParameters.Builder.clearPresolveInclusionWorkLimit()A few presolve operations involve detecting constraints included in other constraint.SatParameters.Builder.clearPresolveProbingDeterministicTimeLimit()optional double presolve_probing_deterministic_time_limit = 57 [default = 30];SatParameters.Builder.clearPresolveSubstitutionLevel()How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve.SatParameters.Builder.clearPresolveUseBva()Whether or not we use Bounded Variable Addition (BVA) in the presolve.SatParameters.Builder.clearProbingDeterministicTimeLimit()The maximum "deterministic" time limit to spend in probing.SatParameters.Builder.clearProbingNumCombinationsLimit()How many combinations of pairs or triplets of variables we want to scan.SatParameters.Builder.clearPropagationLoopDetectionFactor()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.SatParameters.Builder.clearPseudoCostReliabilityThreshold()The solver ignores the pseudo costs of variables with number of recordings less than this threshold.SatParameters.Builder.clearPushAllTasksTowardStart()Experimental code: specify if the objective pushes all tasks toward the start of the schedule.SatParameters.Builder.clearRandomBranchesRatio()A number between 0 and 1 that indicates the proportion of branching variables that are selected randomly instead of choosing the first variable from the given variable_ordering strategy.SatParameters.Builder.clearRandomizeSearch()Randomize fixed search.SatParameters.Builder.clearRandomPolarityRatio()The proportion of polarity chosen at random.SatParameters.Builder.clearRandomSeed()At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed.SatParameters.Builder.clearRelativeGapLimit()optional double relative_gap_limit = 160 [default = 0];SatParameters.Builder.clearRemoveFixedVariablesEarly()If cp_model_presolve is true and there is a large proportion of fixed variable after the first model copy, remap all the model to a dense set of variable before the full presolve even starts.SatParameters.Builder.clearRepairHint()If true, the solver tries to repair the solution given in the hint.SatParameters.Builder.clearRestartAlgorithms()The restart strategies will change each time the strategy_counter is increased.SatParameters.Builder.clearRestartDlAverageRatio()In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.SatParameters.Builder.clearRestartLbdAverageRatio()optional double restart_lbd_average_ratio = 71 [default = 1];SatParameters.Builder.clearRestartPeriod()Restart period for the FIXED_RESTART strategy.SatParameters.Builder.clearRestartRunningWindowSize()Size of the window for the moving average restarts.SatParameters.Builder.clearRootLpIterations()Even at the root node, we do not want to spend too much time on the LP if it is "difficult".SatParameters.Builder.clearRoutingCutDpEffort()The amount of "effort" to spend in dynamic programming for computing routing cuts.SatParameters.Builder.clearRoutingCutMaxInfeasiblePathLength()If the length of an infeasible path is less than this value, a cut will be added to exclude it.SatParameters.Builder.clearRoutingCutSubsetSizeForBinaryRelationBound()If the size of a subset of nodes of a RoutesConstraint is less than this value, use linear constraints of size 1 and 2 (such as capacity and time window constraints) enforced by the arc literals to compute cuts for this subset (unless the subset size is less than routing_cut_subset_size_for_tight_binary_relation_bound, in which case the corresponding algorithm is used instead).SatParameters.Builder.clearRoutingCutSubsetSizeForExactBinaryRelationBound()Similar to above, but with an even stronger algorithm in O(n!).SatParameters.Builder.clearRoutingCutSubsetSizeForShortestPathsBound()Similar to routing_cut_subset_size_for_exact_binary_relation_bound but use a bound based on shortest path distances (which respect triangular inequality).SatParameters.Builder.clearRoutingCutSubsetSizeForTightBinaryRelationBound()Similar to above, but with a different algorithm producing better cuts, at the price of a higher O(2^n) complexity, where n is the subset size.SatParameters.Builder.clearSaveLpBasisInLbTreeSearch()Experimental.SatParameters.Builder.clearSearchBranching()optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];SatParameters.Builder.clearSearchRandomVariablePoolSize()Search randomization will collect the top 'search_random_variable_pool_size' valued variables, and pick one randomly.SatParameters.Builder.clearShareBinaryClauses()Allows sharing of new learned binary clause between workers.SatParameters.Builder.clearSharedTreeBalanceTolerance()How much deeper compared to the ideal max depth of the tree is considered "balanced" enough to still accept a split.SatParameters.Builder.clearSharedTreeMaxNodesPerWorker()In order to limit total shared memory and communication overhead, limit the total number of nodes that may be generated in the shared tree.SatParameters.Builder.clearSharedTreeNumWorkers()Enables shared tree search.SatParameters.Builder.clearSharedTreeOpenLeavesPerWorker()How many open leaf nodes should the shared tree maintain per worker.SatParameters.Builder.clearSharedTreeSplitStrategy()optional .operations_research.sat.SatParameters.SharedTreeSplitStrategy shared_tree_split_strategy = 239 [default = SPLIT_STRATEGY_AUTO];SatParameters.Builder.clearSharedTreeWorkerEnablePhaseSharing()If true, shared tree workers share their target phase when returning an assigned subtree for the next worker to use.SatParameters.Builder.clearSharedTreeWorkerEnableTrailSharing()If true, workers share more of the information from their local trail.SatParameters.Builder.clearSharedTreeWorkerMinRestartsPerSubtree()Minimum restarts before a worker will replace a subtree that looks "bad" based on the average LBD of learned clauses.SatParameters.Builder.clearShareGlueClauses()Allows sharing of short glue clauses between workers.SatParameters.Builder.clearShareGlueClausesDtime()The amount of dtime between each export of shared glue clauses.SatParameters.Builder.clearShareLevelZeroBounds()Allows sharing of the bounds of modified variables at level 0.SatParameters.Builder.clearShareObjectiveBounds()Allows objective sharing between workers.SatParameters.Builder.clearShavingDeterministicTimeInProbingSearch()Add a shaving phase (where the solver tries to prove that the lower or upper bound of a variable are infeasible) to the probing searchSatParameters.Builder.clearShavingSearchDeterministicTime()Specifies the amount of deterministic time spent of each try at shaving a bound in the shaving search.SatParameters.Builder.clearShavingSearchThreshold()Specifies the threshold between two modes in the shaving procedure.SatParameters.Builder.clearSolutionPoolSize()Size of the top-n different solutions kept by the solver.SatParameters.Builder.clearStopAfterFirstSolution()For an optimization problem, stop the solver as soon as we have a solution.SatParameters.Builder.clearStopAfterPresolve()Mainly used when improving the presolver.SatParameters.Builder.clearStopAfterRootPropagation()optional bool stop_after_root_propagation = 252 [default = false];SatParameters.Builder.clearStrategyChangeIncreaseRatio()The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.SatParameters.Builder.clearSubsolverParams()It is possible to specify additional subsolver configuration.SatParameters.Builder.clearSubsolvers()In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.SatParameters.Builder.clearSubsumptionDuringConflictAnalysis()At a really low cost, during the 1-UIP conflict computation, it is easy to detect if some of the involved reasons are subsumed by the current conflict.SatParameters.Builder.clearSymmetryDetectionDeterministicTimeLimit()Deterministic time limit for symmetry detection.SatParameters.Builder.clearSymmetryLevel()Whether we try to automatically detect the symmetries in a model and exploit them.SatParameters.Builder.clearTableCompressionLevel()How much we try to "compress" a table constraint.SatParameters.Builder.clearUseAbslRandom()optional bool use_absl_random = 180 [default = false];SatParameters.Builder.clearUseAllDifferentForCircuit()Turn on extra propagation for the circuit constraint.SatParameters.Builder.clearUseAreaEnergeticReasoningInNoOverlap2D()When this is true, the no_overlap_2d constraint is reinforced with an energetic reasoning that uses an area-based energy.SatParameters.Builder.clearUseBlockingRestart()Block a moving restart algorithm if the trail size of the current conflict is greater than the multiplier times the moving average of the trail size at the previous conflicts.SatParameters.Builder.clearUseCombinedNoOverlap()This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem.SatParameters.Builder.clearUseConservativeScaleOverloadChecker()Enable a heuristic to solve cumulative constraints using a modified energy constraint.SatParameters.Builder.clearUseDisjunctiveConstraintInCumulative()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.SatParameters.Builder.clearUseDualSchedulingHeuristics()When set, it activates a few scheduling parameters to improve the lower bound of scheduling problems.SatParameters.Builder.clearUseDynamicPrecedenceInCumulative()optional bool use_dynamic_precedence_in_cumulative = 268 [default = false];SatParameters.Builder.clearUseDynamicPrecedenceInDisjunctive()Whether we try to branch on decision "interval A before interval B" rather than on intervals bounds.SatParameters.Builder.clearUseEnergeticReasoningInNoOverlap2D()When this is true, the no_overlap_2d constraint is reinforced with energetic reasoning.SatParameters.Builder.clearUseErwaHeuristic()Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as described in "Learning Rate Based Branching Heuristic for SAT solvers", J.H.Liang, V.SatParameters.Builder.clearUseExactLpReason()The solver usually exploit the LP relaxation of a model.SatParameters.Builder.clearUseExtendedProbing()Use extended probing (probe bool_or, at_most_one, exactly_one).SatParameters.Builder.clearUseFeasibilityJump()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.SatParameters.Builder.clearUseFeasibilityPump()Adds a feasibility pump subsolver along with lns subsolvers.SatParameters.Builder.clearUseHardPrecedencesInCumulative()If true, detect and create constraint for integer variable that are "after" a set of intervals in the same cumulative constraint.SatParameters.Builder.clearUseImpliedBounds()Stores and exploits "implied-bounds" in the solver.SatParameters.Builder.clearUseLbRelaxLns()Turns on neighborhood generator based on local branching LP.SatParameters.Builder.clearUseLinear3ForNoOverlap2DPrecedences()When set, this activates a propagator for the no_overlap_2d constraint that uses any eventual linear constraints of the model in the form `{start interval 1} - {end interval 2} + c*w <= ub` to detect that two intervals must overlap in one dimension for some values of `w`.SatParameters.Builder.clearUseLns()Testing parameters used to disable all lns workers.SatParameters.Builder.clearUseLnsOnly()Experimental parameters to disable everything but lns.SatParameters.Builder.clearUseLsOnly()Disable every other type of subsolver, setting this turns CP-SAT into a pure local-search solver.SatParameters.Builder.clearUseObjectiveLbSearch()If true, search will search in ascending max objective value (when minimizing) starting from the lower bound of the objective.SatParameters.Builder.clearUseObjectiveShavingSearch()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.SatParameters.Builder.clearUseOptimizationHints()For an optimization problem, whether we follow some hints in order to find a better first solution.SatParameters.Builder.clearUseOptionalVariables()If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional.SatParameters.Builder.clearUseOverloadCheckerInCumulative()When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy.SatParameters.Builder.clearUsePbResolution()Whether to use pseudo-Boolean resolution to analyze a conflict.SatParameters.Builder.clearUsePhaseSaving()If this is true, then the polarity of a variable will be the last value it was assigned to, or its default polarity if it was never assigned since the call to ResetDecisionHeuristic().SatParameters.Builder.clearUsePrecedencesInDisjunctiveConstraint()When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further.SatParameters.Builder.clearUseProbingSearch()If true, search will continuously probe Boolean variables, and integer variable bounds.SatParameters.Builder.clearUseRinsLns()Turns on relaxation induced neighborhood generator.SatParameters.Builder.clearUseSatInprocessing()Enable or disable "inprocessing" which is some SAT presolving done at each restart to the root level.SatParameters.Builder.clearUseSharedTreeSearch()Set on shared subtree workers.SatParameters.Builder.clearUseStrongPropagationInDisjunctive()Enable stronger and more expensive propagation on no_overlap constraint.SatParameters.Builder.clearUseSymmetryInLp()When we have symmetry, it is possible to "fold" all variables from the same orbit into a single variable, while having the same power of LP relaxation.SatParameters.Builder.clearUseTimetableEdgeFindingInCumulative()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.SatParameters.Builder.clearUseTimetablingInNoOverlap2D()When this is true, the no_overlap_2d constraint is reinforced with propagators from the cumulative constraints.SatParameters.Builder.clearUseTryEdgeReasoningInNoOverlap2D()optional bool use_try_edge_reasoning_in_no_overlap_2d = 299 [default = false];SatParameters.Builder.clearVariableActivityDecay()Each time a conflict is found, the activities of some variables are increased by one.SatParameters.Builder.clearVariablesShavingLevel()This search takes all Boolean or integer variables, and maximize or minimize them in order to reduce their domain. -1 is automatic, otherwise value 0 disables it, and 1, 2, or 3 changes something.SatParameters.Builder.clearViolationLsCompoundMoveProbability()Probability of using compound move search each restart.SatParameters.Builder.clearViolationLsPerturbationPeriod()How long violation_ls should wait before perturbating a solution.CpSolver.getParameters()Returns the builder of the parameters of the SAT solver for modification.SatParameters.Builder.getSubsolverParamsBuilder(int index) It is possible to specify additional subsolver configuration.SatParameters.Builder.mergeFrom(SatParameters other) SatParameters.Builder.mergeFrom(com.google.protobuf.CodedInputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry) SatParameters.Builder.mergeFrom(com.google.protobuf.Message other) static SatParameters.BuilderSatParameters.newBuilder()static SatParameters.BuilderSatParameters.newBuilder(SatParameters prototype) SatParameters.newBuilderForType()protected SatParameters.BuilderSatParameters.newBuilderForType(com.google.protobuf.AbstractMessage.BuilderParent parent) SatParameters.Builder.removeSubsolverParams(int index) It is possible to specify additional subsolver configuration.SatParameters.Builder.setAbsoluteGapLimit(double value) Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit.SatParameters.Builder.setAddCgCuts(boolean value) Whether we generate and add Chvatal-Gomory cuts to the LP at root node.SatParameters.Builder.setAddCliqueCuts(boolean value) Whether we generate clique cuts from the binary implication graph.SatParameters.Builder.setAddLinMaxCuts(boolean value) For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et.SatParameters.Builder.setAddLpConstraintsLazily(boolean value) If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch.SatParameters.Builder.setAddMirCuts(boolean value) Whether we generate MIR cuts at root node.SatParameters.Builder.setAddObjectiveCut(boolean value) 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?SatParameters.Builder.setAddRltCuts(boolean value) Whether we generate RLT cuts.SatParameters.Builder.setAddZeroHalfCuts(boolean value) Whether we generate Zero-Half cuts at root node.SatParameters.Builder.setAlsoBumpVariablesInConflictReasons(boolean value) When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped.SatParameters.Builder.setAtMostOneMaxExpansionSize(int value) All at_most_one constraints with a size <= param will be replaced by a quadratic number of binary implications.SatParameters.Builder.setAutoDetectGreaterThanAtLeastOneOf(boolean value) If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present.SatParameters.Builder.setBinaryMinimizationAlgorithm(SatParameters.BinaryMinizationAlgorithm value) optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];SatParameters.Builder.setBinarySearchNumConflicts(int value) If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict.SatParameters.Builder.setBlockingRestartMultiplier(double value) optional double blocking_restart_multiplier = 66 [default = 1.4];SatParameters.Builder.setBlockingRestartWindowSize(int value) optional int32 blocking_restart_window_size = 65 [default = 5000];SatParameters.Builder.setBooleanEncodingLevel(int value) A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.SatParameters.Builder.setCatchSigintSignal(boolean value) Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve.SatParameters.Builder.setClauseActivityDecay(double value) Clause activity parameters (same effect as the one on the variables).SatParameters.Builder.setClauseCleanupLbdBound(int value) All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.SatParameters.Builder.setClauseCleanupOrdering(SatParameters.ClauseOrdering value) optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];SatParameters.Builder.setClauseCleanupPeriod(int value) Trigger a cleanup when this number of "deletable" clauses is learned.SatParameters.Builder.setClauseCleanupProtection(SatParameters.ClauseProtection value) optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];SatParameters.Builder.setClauseCleanupRatio(double value) 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.SatParameters.Builder.setClauseCleanupTarget(int value) During a cleanup, we will always keep that number of "deletable" clauses.SatParameters.Builder.setConvertIntervals(boolean value) Temporary flag util the feature is more mature.SatParameters.Builder.setCoreMinimizationLevel(int value) If positive, we spend some effort on each core: - At level 1, we use a simple heuristic to try to minimize an UNSAT coreSatParameters.Builder.setCountAssumptionLevelsInLbd(boolean value) Whether or not the assumption levels are taken into account during the LBD computation.SatParameters.Builder.setCoverOptimization(boolean value) 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.SatParameters.Builder.setCpModelPresolve(boolean value) Whether we presolve the cp_model before solving it.SatParameters.Builder.setCpModelProbingLevel(int value) How much effort do we spend on probing. 0 disables it completely.SatParameters.Builder.setCpModelUseSatPresolve(boolean value) Whether we also use the sat presolve when cp_model_presolve is true.SatParameters.Builder.setCutActiveCountDecay(double value) optional double cut_active_count_decay = 156 [default = 0.8];SatParameters.Builder.setCutCleanupTarget(int value) Target number of constraints to remove during cleanup.SatParameters.Builder.setCutLevel(int value) Control the global cut effort.SatParameters.Builder.setCutMaxActiveCountValue(double value) These parameters are similar to sat clause management activity parameters.SatParameters.Builder.setDebugCrashIfPresolveBreaksHint(boolean value) Crash if presolve breaks a feasible hint.SatParameters.Builder.setDebugCrashOnBadHint(boolean value) Crash if we do not manage to complete the hint into a full solution.SatParameters.Builder.setDebugMaxNumPresolveOperations(int value) If positive, try to stop just after that many presolve rules have been applied.SatParameters.Builder.setDebugPostsolveWithFullSolver(boolean value) We have two different postsolve code.SatParameters.Builder.setDefaultRestartAlgorithms(String value) optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];SatParameters.Builder.setDefaultRestartAlgorithmsBytes(com.google.protobuf.ByteString value) optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];SatParameters.Builder.setDetectLinearizedProduct(boolean value) Infer products of Boolean or of Boolean time IntegerVariable from the linear constrainst in the problem.SatParameters.Builder.setDetectTableWithCost(boolean value) If true, we detect variable that are unique to a table constraint and only there to encode a cost on each tuple.SatParameters.Builder.setDisableConstraintExpansion(boolean value) If true, it disable all constraint expansion.SatParameters.Builder.setDiversifyLnsParams(boolean value) If true, registers more lns subsolvers with different parameters.SatParameters.Builder.setEncodeComplexLinearConstraintWithInteger(boolean value) 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.SatParameters.Builder.setEncodeCumulativeAsReservoir(boolean value) Encore cumulative with fixed demands and capacity as a reservoir constraint.SatParameters.Builder.setEnumerateAllSolutions(boolean value) Whether we enumerate all solutions of a problem without objective.SatParameters.Builder.setExpandAlldiffConstraints(boolean value) If true, expand all_different constraints that are not permutations.SatParameters.Builder.setExpandReservoirConstraints(boolean value) If true, expand the reservoir constraints by creating booleans for all possible precedences between event and encoding the constraint.SatParameters.Builder.setExpandReservoirUsingCircuit(boolean value) Mainly useful for testing.SatParameters.Builder.setExploitAllLpSolution(boolean value) If true and the Lp relaxation of the problem has a solution, try to exploit it.SatParameters.Builder.setExploitAllPrecedences(boolean value) optional bool exploit_all_precedences = 220 [default = false];SatParameters.Builder.setExploitBestSolution(boolean value) When branching on a variable, follow the last best solution value.SatParameters.Builder.setExploitIntegerLpSolution(boolean value) If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it.SatParameters.Builder.setExploitObjective(boolean value) When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.SatParameters.Builder.setExploitRelaxationSolution(boolean value) When branching on a variable, follow the last best relaxation solution value.SatParameters.Builder.setExtraSubsolvers(int index, String value) A convenient way to add more workers types.SatParameters.Builder.setFeasibilityJumpBatchDtime(double value) How much dtime for each LS batch.SatParameters.Builder.setFeasibilityJumpDecay(double value) On each restart, we randomly choose if we use decay (with this parameter) or no decay.SatParameters.Builder.setFeasibilityJumpEnableRestarts(boolean value) When stagnating, feasibility jump will either restart from a default solution (with some possible randomization), or randomly pertubate the current solution.SatParameters.Builder.setFeasibilityJumpLinearizationLevel(int value) How much do we linearize the problem in the local search code.SatParameters.Builder.setFeasibilityJumpMaxExpandedConstraintSize(int value) Maximum size of no_overlap or no_overlap_2d constraint for a quadratic expansion.SatParameters.Builder.setFeasibilityJumpRestartFactor(int value) This is a factor that directly influence the work before each restart.SatParameters.Builder.setFeasibilityJumpVarPerburbationRangeRatio(double value) Max distance between the default value and the pertubated value relative to the range of the domain of the variable.SatParameters.Builder.setFeasibilityJumpVarRandomizationProbability(double value) Probability for a variable to have a non default value upon restarts or perturbations.SatParameters.Builder.setFillAdditionalSolutionsInResponse(boolean value) If true, the final response addition_solutions field will be filled with all solutions from our solutions pool.SatParameters.Builder.setFillTightenedDomainsInResponse(boolean value) If true, add information about the derived variable domains to the CpSolverResponse.SatParameters.Builder.setFilterSatPostsolveClauses(boolean value) Internal parameter.SatParameters.Builder.setFilterSubsolvers(int index, String value) repeated string filter_subsolvers = 293;SatParameters.Builder.setFindBigLinearOverlap(boolean value) Try to find large "rectangle" in the linear constraint matrix with identical lines.SatParameters.Builder.setFindMultipleCores(boolean value) Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.SatParameters.Builder.setFixVariablesToTheirHintedValue(boolean value) If true, variables appearing in the solution hints will be fixed to their hinted value.SatParameters.Builder.setFpRounding(SatParameters.FPRoundingMethod value) optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];SatParameters.Builder.setGlucoseDecayIncrement(double value) optional double glucose_decay_increment = 23 [default = 0.01];SatParameters.Builder.setGlucoseDecayIncrementPeriod(int value) optional int32 glucose_decay_increment_period = 24 [default = 5000];SatParameters.Builder.setGlucoseMaxDecay(double value) The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95.SatParameters.Builder.setHintConflictLimit(int value) Conflict limit used in the phase that exploit the solution hint.SatParameters.Builder.setIgnoreNames(boolean value) If true, we don't keep names in our internal copy of the user given model.SatParameters.Builder.setIgnoreSubsolvers(int index, String value) Rather than fully specifying subsolvers, it is often convenient to just remove the ones that are not useful on a given problem or only keep specific ones for testing.SatParameters.Builder.setInferAllDiffs(boolean value) Run a max-clique code amongst all the x !SatParameters.Builder.setInitialPolarity(SatParameters.Polarity value) optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];SatParameters.Builder.setInitialVariablesActivity(double value) The initial value of the variables activity.SatParameters.Builder.setInprocessingDtimeRatio(double value) Proportion of deterministic time we should spend on inprocessing.SatParameters.Builder.setInprocessingMinimizationDtime(double value) 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.SatParameters.Builder.setInprocessingMinimizationUseAllOrderings(boolean value) optional bool inprocessing_minimization_use_all_orderings = 298 [default = false];SatParameters.Builder.setInprocessingMinimizationUseConflictAnalysis(boolean value) optional bool inprocessing_minimization_use_conflict_analysis = 297 [default = true];SatParameters.Builder.setInprocessingProbingDtime(double value) The amount of dtime we should spend on probing for each inprocessing round.SatParameters.Builder.setInstantiateAllVariables(boolean value) If true, the solver will add a default integer branching strategy to the already defined search strategy.SatParameters.Builder.setInterleaveBatchSize(int value) optional int32 interleave_batch_size = 134 [default = 0];SatParameters.Builder.setInterleaveSearch(boolean value) Experimental.SatParameters.Builder.setKeepAllFeasibleSolutionsInPresolve(boolean value) If true, we disable the presolve reductions that remove feasible solutions from the search space.SatParameters.Builder.setKeepSymmetryInPresolve(boolean value) Experimental.SatParameters.Builder.setLbRelaxNumWorkersThreshold(int value) Only use lb-relax if we have at least that many workers.SatParameters.Builder.setLinearizationLevel(int value) A non-negative level indicating the type of constraints we consider in the LP relaxation.SatParameters.Builder.setLinearSplitSize(int value) 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.SatParameters.Builder.setLnsInitialDeterministicLimit(double value) optional double lns_initial_deterministic_limit = 308 [default = 0.1];SatParameters.Builder.setLnsInitialDifficulty(double value) Initial parameters for neighborhood generation.SatParameters.Builder.setLogPrefix(String value) Add a prefix to all logs.SatParameters.Builder.setLogPrefixBytes(com.google.protobuf.ByteString value) Add a prefix to all logs.SatParameters.Builder.setLogSearchProgress(boolean value) Whether the solver should log the search progress.SatParameters.Builder.setLogSubsolverStatistics(boolean value) Whether the solver should display per sub-solver search statistics.SatParameters.Builder.setLogToResponse(boolean value) Log to response proto.SatParameters.Builder.setLogToStdout(boolean value) Log to stdout.SatParameters.Builder.setLpDualTolerance(double value) optional double lp_dual_tolerance = 267 [default = 1e-07];SatParameters.Builder.setLpPrimalTolerance(double value) The internal LP tolerances used by CP-SAT.SatParameters.Builder.setMaxAllDiffCutSize(int value) Cut generator for all diffs can add too many cuts for large all_diff constraints.SatParameters.Builder.setMaxAlldiffDomainSize(int value) Max domain size for all_different constraints to be expanded.SatParameters.Builder.setMaxClauseActivityValue(double value) optional double max_clause_activity_value = 18 [default = 1e+20];SatParameters.Builder.setMaxConsecutiveInactiveCount(int value) If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP.SatParameters.Builder.setMaxCutRoundsAtLevelZero(int value) Max number of time we perform cut generation and resolve the LP at level 0.SatParameters.Builder.setMaxDeterministicTime(double value) Maximum time allowed in deterministic time to solve a problem.SatParameters.Builder.setMaxDomainSizeWhenEncodingEqNeqConstraints(int value) When loading a*x + b*y ==/!SatParameters.Builder.setMaximumRegionsToSplitInDisconnectedNoOverlap2D(int value) Detects when the space where items of a no_overlap_2d constraint can placed is disjoint (ie., fixed boxes split the domain).SatParameters.Builder.setMaxIntegerRoundingScaling(int value) In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive).SatParameters.Builder.setMaxLinMaxSizeForExpansion(int value) If the number of expressions in the lin_max is less that the max size parameter, model expansion replaces target = max(xi) by linear constraint with the introduction of new booleans bi such that bi => target == xi.SatParameters.Builder.setMaxMemoryInMb(long value) Maximum memory allowed for the whole thread containing the solver.SatParameters.Builder.setMaxNumberOfConflicts(long value) Maximum number of conflicts allowed to solve a problem.SatParameters.Builder.setMaxNumCuts(int value) The limit on the number of cuts in our cut pool.SatParameters.Builder.setMaxNumDeterministicBatches(int value) Stops after that number of batches has been scheduled.SatParameters.Builder.setMaxNumIntervalsForTimetableEdgeFinding(int value) Max number of intervals for the timetable_edge_finding algorithm to propagate.SatParameters.Builder.setMaxPairsPairwiseReasoningInNoOverlap2D(int value) 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.SatParameters.Builder.setMaxPresolveIterations(int value) In case of large reduction in a presolve iteration, we perform multiple presolve iterations.SatParameters.Builder.setMaxSatAssumptionOrder(SatParameters.MaxSatAssumptionOrder value) optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];SatParameters.Builder.setMaxSatReverseAssumptionOrder(boolean value) If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.SatParameters.Builder.setMaxSatStratification(SatParameters.MaxSatStratificationAlgorithm value) optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];SatParameters.Builder.setMaxSizeToCreatePrecedenceLiteralsInDisjunctive(int value) Create one literal for each disjunction of two pairs of tasks.SatParameters.Builder.setMaxTimeInSeconds(double value) Maximum time allowed in seconds to solve a problem.SatParameters.Builder.setMaxVariableActivityValue(double value) optional double max_variable_activity_value = 16 [default = 1e+100];SatParameters.Builder.setMergeAtMostOneWorkLimit(double value) optional double merge_at_most_one_work_limit = 146 [default = 100000000];SatParameters.Builder.setMergeNoOverlapWorkLimit(double value) During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints.SatParameters.Builder.setMinimizationAlgorithm(SatParameters.ConflictMinimizationAlgorithm value) optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];SatParameters.Builder.setMinimizeReductionDuringPbResolution(boolean value) A different algorithm during PB resolution.SatParameters.Builder.setMinimizeSharedClauses(boolean value) Minimize and detect subsumption of shared clauses immediately after they are imported.SatParameters.Builder.setMinOrthogonalityForLpConstraints(double value) While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call.SatParameters.Builder.setMipAutomaticallyScaleVariables(boolean value) If true, some continuous variable might be automatically scaled.SatParameters.Builder.setMipCheckPrecision(double value) As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted precision during scaling.SatParameters.Builder.setMipComputeTrueObjectiveBound(boolean value) 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.SatParameters.Builder.setMipDropTolerance(double value) Any value in the input mip with a magnitude lower than this will be set to zero.SatParameters.Builder.setMipMaxActivityExponent(int value) 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.SatParameters.Builder.setMipMaxBound(double value) We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use.SatParameters.Builder.setMipMaxValidMagnitude(double value) Any finite values in the input MIP must be below this threshold, otherwise the model will be reported invalid.SatParameters.Builder.setMipPresolveLevel(int value) When solving a MIP, we do some basic floating point presolving before scaling the problem to integer to be handled by CP-SAT.SatParameters.Builder.setMipScaleLargeDomain(boolean value) If this is false, then mip_var_scaling is only applied to variables with "small" domain.SatParameters.Builder.setMipTreatHighMagnitudeBoundsAsInfinity(boolean value) 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.SatParameters.Builder.setMipVarScaling(double value) All continuous variable of the problem will be multiplied by this factor.SatParameters.Builder.setMipWantedPrecision(double value) When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients.In some context, like in a portfolio of search, it makes sense to name a given parameters set for logging purpose.SatParameters.Builder.setNameBytes(com.google.protobuf.ByteString value) In some context, like in a portfolio of search, it makes sense to name a given parameters set for logging purpose.SatParameters.Builder.setNewConstraintsBatchSize(int value) Add that many lazy constraints (or cuts) at once in the LP.SatParameters.Builder.setNewLinearPropagation(boolean value) The new linear propagation code treat all constraints at once and use an adaptation of Bellman-Ford-Tarjan to propagate constraint in a smarter order and potentially detect propagation cycle earlier.SatParameters.Builder.setNoOverlap2DBooleanRelationsLimit(int value) If less than this number of boxes are present in a no-overlap 2d, we create 4 Booleans per pair of boxes: - Box 2 is after Box 1 on xSatParameters.Builder.setNumConflictsBeforeStrategyChanges(int value) 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.SatParameters.Builder.setNumFullSubsolvers(int value) We distinguish subsolvers that consume a full thread, and the ones that are always interleaved.SatParameters.Builder.setNumSearchWorkers(int value) optional int32 num_search_workers = 100 [default = 0];SatParameters.Builder.setNumViolationLs(int value) 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.SatParameters.Builder.setNumWorkers(int value) Specify the number of parallel workers (i.e. threads) to use during search.SatParameters.Builder.setOnlyAddCutsAtLevelZero(boolean value) For the cut that can be generated at any level, this control if we only try to generate them at the root node.SatParameters.Builder.setOnlySolveIp(boolean value) 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.SatParameters.Builder.setOptimizeWithCore(boolean value) The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one.SatParameters.Builder.setOptimizeWithLbTreeSearch(boolean value) Do a more conventional tree search (by opposition to SAT based one) where we keep all the explored node in a tree.SatParameters.Builder.setOptimizeWithMaxHs(boolean value) This has no effect if optimize_with_core is false.SatParameters.Builder.setPbCleanupIncrement(int value) Same as for the clauses, but for the learned pseudo-Boolean constraints.SatParameters.Builder.setPbCleanupRatio(double value) optional double pb_cleanup_ratio = 47 [default = 0.5];SatParameters.Builder.setPermutePresolveConstraintOrder(boolean value) optional bool permute_presolve_constraint_order = 179 [default = false];SatParameters.Builder.setPermuteVariableRandomly(boolean value) This is mainly here to test the solver variability.SatParameters.Builder.setPolarityExploitLsHints(boolean value) If true and we have first solution LS workers, tries in some phase to follow a LS solutions that violates has litle constraints as possible.SatParameters.Builder.setPolarityRephaseIncrement(int value) If non-zero, then we change the polarity heuristic after that many number of conflicts in an arithmetically increasing fashion.SatParameters.Builder.setPolishLpSolution(boolean value) 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.SatParameters.Builder.setPreferredVariableOrder(SatParameters.VariableOrder value) optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];SatParameters.Builder.setPresolveBlockedClause(boolean value) Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.SatParameters.Builder.setPresolveBvaThreshold(int value) Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold.SatParameters.Builder.setPresolveBveClauseWeight(int value) During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.SatParameters.Builder.setPresolveBveThreshold(int value) 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.SatParameters.Builder.setPresolveExtractIntegerEnforcement(boolean value) If true, we will extract from linear constraints, enforcement literals of the form "integer variable at bound => simplified constraint".SatParameters.Builder.setPresolveInclusionWorkLimit(long value) A few presolve operations involve detecting constraints included in other constraint.SatParameters.Builder.setPresolveProbingDeterministicTimeLimit(double value) optional double presolve_probing_deterministic_time_limit = 57 [default = 30];SatParameters.Builder.setPresolveSubstitutionLevel(int value) How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve.SatParameters.Builder.setPresolveUseBva(boolean value) Whether or not we use Bounded Variable Addition (BVA) in the presolve.SatParameters.Builder.setProbingDeterministicTimeLimit(double value) The maximum "deterministic" time limit to spend in probing.SatParameters.Builder.setProbingNumCombinationsLimit(int value) How many combinations of pairs or triplets of variables we want to scan.SatParameters.Builder.setPropagationLoopDetectionFactor(double value) 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.SatParameters.Builder.setPseudoCostReliabilityThreshold(long value) The solver ignores the pseudo costs of variables with number of recordings less than this threshold.SatParameters.Builder.setPushAllTasksTowardStart(boolean value) Experimental code: specify if the objective pushes all tasks toward the start of the schedule.SatParameters.Builder.setRandomBranchesRatio(double value) 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.SatParameters.Builder.setRandomizeSearch(boolean value) Randomize fixed search.SatParameters.Builder.setRandomPolarityRatio(double value) The proportion of polarity chosen at random.SatParameters.Builder.setRandomSeed(int value) At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed.SatParameters.Builder.setRelativeGapLimit(double value) optional double relative_gap_limit = 160 [default = 0];SatParameters.Builder.setRemoveFixedVariablesEarly(boolean value) If cp_model_presolve is true and there is a large proportion of fixed variable after the first model copy, remap all the model to a dense set of variable before the full presolve even starts.SatParameters.Builder.setRepairHint(boolean value) If true, the solver tries to repair the solution given in the hint.SatParameters.Builder.setRestartAlgorithms(int index, SatParameters.RestartAlgorithm value) The restart strategies will change each time the strategy_counter is increased.SatParameters.Builder.setRestartDlAverageRatio(double value) In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.SatParameters.Builder.setRestartLbdAverageRatio(double value) optional double restart_lbd_average_ratio = 71 [default = 1];SatParameters.Builder.setRestartPeriod(int value) Restart period for the FIXED_RESTART strategy.SatParameters.Builder.setRestartRunningWindowSize(int value) Size of the window for the moving average restarts.SatParameters.Builder.setRootLpIterations(int value) Even at the root node, we do not want to spend too much time on the LP if it is "difficult".SatParameters.Builder.setRoutingCutDpEffort(double value) The amount of "effort" to spend in dynamic programming for computing routing cuts.SatParameters.Builder.setRoutingCutMaxInfeasiblePathLength(int value) If the length of an infeasible path is less than this value, a cut will be added to exclude it.SatParameters.Builder.setRoutingCutSubsetSizeForBinaryRelationBound(int value) If the size of a subset of nodes of a RoutesConstraint is less than this value, use linear constraints of size 1 and 2 (such as capacity and time window constraints) enforced by the arc literals to compute cuts for this subset (unless the subset size is less than routing_cut_subset_size_for_tight_binary_relation_bound, in which case the corresponding algorithm is used instead).SatParameters.Builder.setRoutingCutSubsetSizeForExactBinaryRelationBound(int value) Similar to above, but with an even stronger algorithm in O(n!).SatParameters.Builder.setRoutingCutSubsetSizeForShortestPathsBound(int value) Similar to routing_cut_subset_size_for_exact_binary_relation_bound but use a bound based on shortest path distances (which respect triangular inequality).SatParameters.Builder.setRoutingCutSubsetSizeForTightBinaryRelationBound(int value) Similar to above, but with a different algorithm producing better cuts, at the price of a higher O(2^n) complexity, where n is the subset size.SatParameters.Builder.setSaveLpBasisInLbTreeSearch(boolean value) Experimental.SatParameters.Builder.setSearchBranching(SatParameters.SearchBranching value) optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];SatParameters.Builder.setSearchRandomVariablePoolSize(long value) Search randomization will collect the top 'search_random_variable_pool_size' valued variables, and pick one randomly.SatParameters.Builder.setShareBinaryClauses(boolean value) Allows sharing of new learned binary clause between workers.SatParameters.Builder.setSharedTreeBalanceTolerance(int value) How much deeper compared to the ideal max depth of the tree is considered "balanced" enough to still accept a split.SatParameters.Builder.setSharedTreeMaxNodesPerWorker(int value) In order to limit total shared memory and communication overhead, limit the total number of nodes that may be generated in the shared tree.SatParameters.Builder.setSharedTreeNumWorkers(int value) Enables shared tree search.SatParameters.Builder.setSharedTreeOpenLeavesPerWorker(double value) How many open leaf nodes should the shared tree maintain per worker.SatParameters.Builder.setSharedTreeSplitStrategy(SatParameters.SharedTreeSplitStrategy value) optional .operations_research.sat.SatParameters.SharedTreeSplitStrategy shared_tree_split_strategy = 239 [default = SPLIT_STRATEGY_AUTO];SatParameters.Builder.setSharedTreeWorkerEnablePhaseSharing(boolean value) If true, shared tree workers share their target phase when returning an assigned subtree for the next worker to use.SatParameters.Builder.setSharedTreeWorkerEnableTrailSharing(boolean value) If true, workers share more of the information from their local trail.SatParameters.Builder.setSharedTreeWorkerMinRestartsPerSubtree(int value) Minimum restarts before a worker will replace a subtree that looks "bad" based on the average LBD of learned clauses.SatParameters.Builder.setShareGlueClauses(boolean value) Allows sharing of short glue clauses between workers.SatParameters.Builder.setShareGlueClausesDtime(double value) The amount of dtime between each export of shared glue clauses.SatParameters.Builder.setShareLevelZeroBounds(boolean value) Allows sharing of the bounds of modified variables at level 0.SatParameters.Builder.setShareObjectiveBounds(boolean value) Allows objective sharing between workers.SatParameters.Builder.setShavingDeterministicTimeInProbingSearch(double value) Add a shaving phase (where the solver tries to prove that the lower or upper bound of a variable are infeasible) to the probing searchSatParameters.Builder.setShavingSearchDeterministicTime(double value) Specifies the amount of deterministic time spent of each try at shaving a bound in the shaving search.SatParameters.Builder.setShavingSearchThreshold(long value) Specifies the threshold between two modes in the shaving procedure.SatParameters.Builder.setSolutionPoolSize(int value) Size of the top-n different solutions kept by the solver.SatParameters.Builder.setStopAfterFirstSolution(boolean value) For an optimization problem, stop the solver as soon as we have a solution.SatParameters.Builder.setStopAfterPresolve(boolean value) Mainly used when improving the presolver.SatParameters.Builder.setStopAfterRootPropagation(boolean value) optional bool stop_after_root_propagation = 252 [default = false];SatParameters.Builder.setStrategyChangeIncreaseRatio(double value) The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.SatParameters.Builder.setSubsolverParams(int index, SatParameters value) It is possible to specify additional subsolver configuration.SatParameters.Builder.setSubsolverParams(int index, SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.SatParameters.Builder.setSubsolvers(int index, String value) In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.SatParameters.Builder.setSubsumptionDuringConflictAnalysis(boolean value) 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.SatParameters.Builder.setSymmetryDetectionDeterministicTimeLimit(double value) Deterministic time limit for symmetry detection.SatParameters.Builder.setSymmetryLevel(int value) Whether we try to automatically detect the symmetries in a model and exploit them.SatParameters.Builder.setTableCompressionLevel(int value) How much we try to "compress" a table constraint.SatParameters.Builder.setUseAbslRandom(boolean value) optional bool use_absl_random = 180 [default = false];SatParameters.Builder.setUseAllDifferentForCircuit(boolean value) Turn on extra propagation for the circuit constraint.SatParameters.Builder.setUseAreaEnergeticReasoningInNoOverlap2D(boolean value) When this is true, the no_overlap_2d constraint is reinforced with an energetic reasoning that uses an area-based energy.SatParameters.Builder.setUseBlockingRestart(boolean value) 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.SatParameters.Builder.setUseCombinedNoOverlap(boolean value) This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem.SatParameters.Builder.setUseConservativeScaleOverloadChecker(boolean value) Enable a heuristic to solve cumulative constraints using a modified energy constraint.SatParameters.Builder.setUseDisjunctiveConstraintInCumulative(boolean value) 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.SatParameters.Builder.setUseDualSchedulingHeuristics(boolean value) When set, it activates a few scheduling parameters to improve the lower bound of scheduling problems.SatParameters.Builder.setUseDynamicPrecedenceInCumulative(boolean value) optional bool use_dynamic_precedence_in_cumulative = 268 [default = false];SatParameters.Builder.setUseDynamicPrecedenceInDisjunctive(boolean value) Whether we try to branch on decision "interval A before interval B" rather than on intervals bounds.SatParameters.Builder.setUseEnergeticReasoningInNoOverlap2D(boolean value) When this is true, the no_overlap_2d constraint is reinforced with energetic reasoning.SatParameters.Builder.setUseErwaHeuristic(boolean value) 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.SatParameters.Builder.setUseExactLpReason(boolean value) The solver usually exploit the LP relaxation of a model.SatParameters.Builder.setUseExtendedProbing(boolean value) Use extended probing (probe bool_or, at_most_one, exactly_one).SatParameters.Builder.setUseFeasibilityJump(boolean value) 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.SatParameters.Builder.setUseFeasibilityPump(boolean value) Adds a feasibility pump subsolver along with lns subsolvers.SatParameters.Builder.setUseHardPrecedencesInCumulative(boolean value) If true, detect and create constraint for integer variable that are "after" a set of intervals in the same cumulative constraint.SatParameters.Builder.setUseImpliedBounds(boolean value) Stores and exploits "implied-bounds" in the solver.SatParameters.Builder.setUseLbRelaxLns(boolean value) Turns on neighborhood generator based on local branching LP.SatParameters.Builder.setUseLinear3ForNoOverlap2DPrecedences(boolean value) When set, this activates a propagator for the no_overlap_2d constraint that uses any eventual linear constraints of the model in the form `{start interval 1} - {end interval 2} + c*w <= ub` to detect that two intervals must overlap in one dimension for some values of `w`.SatParameters.Builder.setUseLns(boolean value) Testing parameters used to disable all lns workers.SatParameters.Builder.setUseLnsOnly(boolean value) Experimental parameters to disable everything but lns.SatParameters.Builder.setUseLsOnly(boolean value) Disable every other type of subsolver, setting this turns CP-SAT into a pure local-search solver.SatParameters.Builder.setUseObjectiveLbSearch(boolean value) If true, search will search in ascending max objective value (when minimizing) starting from the lower bound of the objective.SatParameters.Builder.setUseObjectiveShavingSearch(boolean value) 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.SatParameters.Builder.setUseOptimizationHints(boolean value) For an optimization problem, whether we follow some hints in order to find a better first solution.SatParameters.Builder.setUseOptionalVariables(boolean value) If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional.SatParameters.Builder.setUseOverloadCheckerInCumulative(boolean value) When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy.SatParameters.Builder.setUsePbResolution(boolean value) Whether to use pseudo-Boolean resolution to analyze a conflict.SatParameters.Builder.setUsePhaseSaving(boolean value) 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().SatParameters.Builder.setUsePrecedencesInDisjunctiveConstraint(boolean value) When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further.SatParameters.Builder.setUseProbingSearch(boolean value) If true, search will continuously probe Boolean variables, and integer variable bounds.SatParameters.Builder.setUseRinsLns(boolean value) Turns on relaxation induced neighborhood generator.SatParameters.Builder.setUseSatInprocessing(boolean value) Enable or disable "inprocessing" which is some SAT presolving done at each restart to the root level.SatParameters.Builder.setUseSharedTreeSearch(boolean value) Set on shared subtree workers.SatParameters.Builder.setUseStrongPropagationInDisjunctive(boolean value) Enable stronger and more expensive propagation on no_overlap constraint.SatParameters.Builder.setUseSymmetryInLp(boolean value) When we have symmetry, it is possible to "fold" all variables from the same orbit into a single variable, while having the same power of LP relaxation.SatParameters.Builder.setUseTimetableEdgeFindingInCumulative(boolean value) 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.SatParameters.Builder.setUseTimetablingInNoOverlap2D(boolean value) When this is true, the no_overlap_2d constraint is reinforced with propagators from the cumulative constraints.SatParameters.Builder.setUseTryEdgeReasoningInNoOverlap2D(boolean value) optional bool use_try_edge_reasoning_in_no_overlap_2d = 299 [default = false];SatParameters.Builder.setVariableActivityDecay(double value) Each time a conflict is found, the activities of some variables are increased by one.SatParameters.Builder.setVariablesShavingLevel(int value) This search takes all Boolean or integer variables, and maximize or minimize them in order to reduce their domain. -1 is automatic, otherwise value 0 disables it, and 1, 2, or 3 changes something.SatParameters.Builder.setViolationLsCompoundMoveProbability(double value) Probability of using compound move search each restart.SatParameters.Builder.setViolationLsPerturbationPeriod(int value) How long violation_ls should wait before perturbating a solution.SatParameters.toBuilder()Methods in com.google.ortools.sat that return types with arguments of type SatParameters.BuilderModifier and TypeMethodDescriptionSatParameters.Builder.getSubsolverParamsBuilderList()It is possible to specify additional subsolver configuration.Methods in com.google.ortools.sat with parameters of type SatParameters.BuilderModifier and TypeMethodDescriptionSatParameters.Builder.addSubsolverParams(int index, SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.SatParameters.Builder.addSubsolverParams(SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.SatParameters.Builder.setSubsolverParams(int index, SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration. -
Uses of SatParameters.Builder in com.google.ortools.sat.v1
Methods in com.google.ortools.sat.v1 that return SatParameters.BuilderModifier and TypeMethodDescriptionCpSolverRequest.Builder.getParametersBuilder()Solver parameters.Methods in com.google.ortools.sat.v1 with parameters of type SatParameters.BuilderModifier and TypeMethodDescriptionCpSolverRequest.Builder.setParameters(SatParameters.Builder builderForValue) Solver parameters.