Uses of Class
com.google.ortools.sat.SatParameters.Builder

Packages that use SatParameters.Builder

Package	Description
com.google.ortools.constraintsolver
com.google.ortools.sat
com.google.ortools.sat.v1

Uses of SatParameters.Builder in com.google.ortools.constraintsolver

Methods in com.google.ortools.constraintsolver that return SatParameters.Builder

Modifier and Type	Method and Description
SatParameters.Builder	RoutingSearchParameters.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.Builder

Modifier and Type	Method and Description
RoutingSearchParameters.Builder	RoutingSearchParameters.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

Methods in com.google.ortools.sat that return SatParameters.Builder

Modifier and Type	Method and Description
SatParameters.Builder	SatParameters.Builder.addAllExtraSubsolvers(java.lang.Iterable<java.lang.String> values) A convenient way to add more workers types.
SatParameters.Builder	SatParameters.Builder.addAllFilterSubsolvers(java.lang.Iterable<java.lang.String> values) repeated string filter_subsolvers = 293;
SatParameters.Builder	SatParameters.Builder.addAllIgnoreSubsolvers(java.lang.Iterable<java.lang.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	SatParameters.Builder.addAllRestartAlgorithms(java.lang.Iterable<? extends SatParameters.RestartAlgorithm> values) The restart strategies will change each time the strategy_counter is increased.
SatParameters.Builder	SatParameters.Builder.addAllSubsolverParams(java.lang.Iterable<? extends SatParameters> values) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.addAllSubsolvers(java.lang.Iterable<java.lang.String> values) In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.
SatParameters.Builder	SatParameters.Builder.addExtraSubsolvers(java.lang.String value) A convenient way to add more workers types.
SatParameters.Builder	SatParameters.Builder.addExtraSubsolversBytes(com.google.protobuf.ByteString value) A convenient way to add more workers types.
SatParameters.Builder	SatParameters.Builder.addFilterSubsolvers(java.lang.String value) repeated string filter_subsolvers = 293;
SatParameters.Builder	SatParameters.Builder.addFilterSubsolversBytes(com.google.protobuf.ByteString value) repeated string filter_subsolvers = 293;
SatParameters.Builder	SatParameters.Builder.addIgnoreSubsolvers(java.lang.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	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	SatParameters.Builder.addRestartAlgorithms(SatParameters.RestartAlgorithm value) The restart strategies will change each time the strategy_counter is increased.
SatParameters.Builder	SatParameters.Builder.addSubsolverParams(int index, SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.addSubsolverParams(int index, SatParameters value) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.addSubsolverParams(SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.addSubsolverParams(SatParameters value) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.addSubsolverParamsBuilder() It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.addSubsolverParamsBuilder(int index) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.addSubsolvers(java.lang.String value) In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.
SatParameters.Builder	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	SatParameters.Builder.clear()
SatParameters.Builder	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	SatParameters.Builder.clearAddCgCuts() Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
SatParameters.Builder	SatParameters.Builder.clearAddCliqueCuts() Whether we generate clique cuts from the binary implication graph.
SatParameters.Builder	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	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	SatParameters.Builder.clearAddMirCuts() Whether we generate MIR cuts at root node.
SatParameters.Builder	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	SatParameters.Builder.clearAddRltCuts() Whether we generate RLT cuts.
SatParameters.Builder	SatParameters.Builder.clearAddZeroHalfCuts() Whether we generate Zero-Half cuts at root node.
SatParameters.Builder	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	SatParameters.Builder.clearAtMostOneMaxExpansionSize() All at_most_one constraints with a size <= param will be replaced by a quadratic number of binary implications.
SatParameters.Builder	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	SatParameters.Builder.clearBinaryMinimizationAlgorithm() optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];
SatParameters.Builder	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	SatParameters.Builder.clearBlockingRestartMultiplier() optional double blocking_restart_multiplier = 66 [default = 1.4];
SatParameters.Builder	SatParameters.Builder.clearBlockingRestartWindowSize() optional int32 blocking_restart_window_size = 65 [default = 5000];
SatParameters.Builder	SatParameters.Builder.clearBooleanEncodingLevel() A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.
SatParameters.Builder	SatParameters.Builder.clearCatchSigintSignal() Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve.
SatParameters.Builder	SatParameters.Builder.clearClauseActivityDecay() Clause activity parameters (same effect as the one on the variables).
SatParameters.Builder	SatParameters.Builder.clearClauseCleanupLbdBound() All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.
SatParameters.Builder	SatParameters.Builder.clearClauseCleanupOrdering() optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];
SatParameters.Builder	SatParameters.Builder.clearClauseCleanupPeriod() Trigger a cleanup when this number of "deletable" clauses is learned.
SatParameters.Builder	SatParameters.Builder.clearClauseCleanupProtection() optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];
SatParameters.Builder	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	SatParameters.Builder.clearClauseCleanupTarget() During a cleanup, we will always keep that number of "deletable" clauses.
SatParameters.Builder	SatParameters.Builder.clearConvertIntervals() Temporary flag util the feature is more mature.
SatParameters.Builder	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 core
SatParameters.Builder	SatParameters.Builder.clearCountAssumptionLevelsInLbd() Whether or not the assumption levels are taken into account during the LBD computation.
SatParameters.Builder	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	SatParameters.Builder.clearCpModelPresolve() Whether we presolve the cp_model before solving it.
SatParameters.Builder	SatParameters.Builder.clearCpModelProbingLevel() How much effort do we spend on probing. 0 disables it completely.
SatParameters.Builder	SatParameters.Builder.clearCpModelUseSatPresolve() Whether we also use the sat presolve when cp_model_presolve is true.
SatParameters.Builder	SatParameters.Builder.clearCutActiveCountDecay() optional double cut_active_count_decay = 156 [default = 0.8];
SatParameters.Builder	SatParameters.Builder.clearCutCleanupTarget() Target number of constraints to remove during cleanup.
SatParameters.Builder	SatParameters.Builder.clearCutLevel() Control the global cut effort.
SatParameters.Builder	SatParameters.Builder.clearCutMaxActiveCountValue() These parameters are similar to sat clause management activity parameters.
SatParameters.Builder	SatParameters.Builder.clearDebugCrashIfPresolveBreaksHint() Crash if presolve breaks a feasible hint.
SatParameters.Builder	SatParameters.Builder.clearDebugCrashOnBadHint() Crash if we do not manage to complete the hint into a full solution.
SatParameters.Builder	SatParameters.Builder.clearDebugMaxNumPresolveOperations() If positive, try to stop just after that many presolve rules have been applied.
SatParameters.Builder	SatParameters.Builder.clearDebugPostsolveWithFullSolver() We have two different postsolve code.
SatParameters.Builder	SatParameters.Builder.clearDefaultRestartAlgorithms() optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
SatParameters.Builder	SatParameters.Builder.clearDetectLinearizedProduct() Infer products of Boolean or of Boolean time IntegerVariable from the linear constrainst in the problem.
SatParameters.Builder	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	SatParameters.Builder.clearDisableConstraintExpansion() If true, it disable all constraint expansion.
SatParameters.Builder	SatParameters.Builder.clearDiversifyLnsParams() If true, registers more lns subsolvers with different parameters.
SatParameters.Builder	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	SatParameters.Builder.clearEncodeCumulativeAsReservoir() Encore cumulative with fixed demands and capacity as a reservoir constraint.
SatParameters.Builder	SatParameters.Builder.clearEnumerateAllSolutions() Whether we enumerate all solutions of a problem without objective.
SatParameters.Builder	SatParameters.Builder.clearExpandAlldiffConstraints() If true, expand all_different constraints that are not permutations.
SatParameters.Builder	SatParameters.Builder.clearExpandReservoirConstraints() If true, expand the reservoir constraints by creating booleans for all possible precedences between event and encoding the constraint.
SatParameters.Builder	SatParameters.Builder.clearExpandReservoirUsingCircuit() Mainly useful for testing.
SatParameters.Builder	SatParameters.Builder.clearExploitAllLpSolution() If true and the Lp relaxation of the problem has a solution, try to exploit it.
SatParameters.Builder	SatParameters.Builder.clearExploitAllPrecedences() optional bool exploit_all_precedences = 220 [default = false];
SatParameters.Builder	SatParameters.Builder.clearExploitBestSolution() When branching on a variable, follow the last best solution value.
SatParameters.Builder	SatParameters.Builder.clearExploitIntegerLpSolution() If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it.
SatParameters.Builder	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	SatParameters.Builder.clearExploitRelaxationSolution() When branching on a variable, follow the last best relaxation solution value.
SatParameters.Builder	SatParameters.Builder.clearExtraSubsolvers() A convenient way to add more workers types.
SatParameters.Builder	SatParameters.Builder.clearFeasibilityJumpBatchDtime() How much dtime for each LS batch.
SatParameters.Builder	SatParameters.Builder.clearFeasibilityJumpDecay() On each restart, we randomly choose if we use decay (with this parameter) or no decay.
SatParameters.Builder	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	SatParameters.Builder.clearFeasibilityJumpLinearizationLevel() How much do we linearize the problem in the local search code.
SatParameters.Builder	SatParameters.Builder.clearFeasibilityJumpMaxExpandedConstraintSize() Maximum size of no_overlap or no_overlap_2d constraint for a quadratic expansion.
SatParameters.Builder	SatParameters.Builder.clearFeasibilityJumpRestartFactor() This is a factor that directly influence the work before each restart.
SatParameters.Builder	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	SatParameters.Builder.clearFeasibilityJumpVarRandomizationProbability() Probability for a variable to have a non default value upon restarts or perturbations.
SatParameters.Builder	SatParameters.Builder.clearFillAdditionalSolutionsInResponse() If true, the final response addition_solutions field will be filled with all solutions from our solutions pool.
SatParameters.Builder	SatParameters.Builder.clearFillTightenedDomainsInResponse() If true, add information about the derived variable domains to the CpSolverResponse.
SatParameters.Builder	SatParameters.Builder.clearFilterSubsolvers() repeated string filter_subsolvers = 293;
SatParameters.Builder	SatParameters.Builder.clearFindBigLinearOverlap() Try to find large "rectangle" in the linear constraint matrix with identical lines.
SatParameters.Builder	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	SatParameters.Builder.clearFixVariablesToTheirHintedValue() If true, variables appearing in the solution hints will be fixed to their hinted value.
SatParameters.Builder	SatParameters.Builder.clearFpRounding() optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];
SatParameters.Builder	SatParameters.Builder.clearGlucoseDecayIncrement() optional double glucose_decay_increment = 23 [default = 0.01];
SatParameters.Builder	SatParameters.Builder.clearGlucoseDecayIncrementPeriod() optional int32 glucose_decay_increment_period = 24 [default = 5000];
SatParameters.Builder	SatParameters.Builder.clearGlucoseMaxDecay() The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95.
SatParameters.Builder	SatParameters.Builder.clearHintConflictLimit() Conflict limit used in the phase that exploit the solution hint.
SatParameters.Builder	SatParameters.Builder.clearIgnoreNames() If true, we don't keep names in our internal copy of the user given model.
SatParameters.Builder	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	SatParameters.Builder.clearInferAllDiffs() Run a max-clique code amongst all the x !
SatParameters.Builder	SatParameters.Builder.clearInitialPolarity() optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];
SatParameters.Builder	SatParameters.Builder.clearInitialVariablesActivity() The initial value of the variables activity.
SatParameters.Builder	SatParameters.Builder.clearInprocessingDtimeRatio() Proportion of deterministic time we should spend on inprocessing.
SatParameters.Builder	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	SatParameters.Builder.clearInprocessingMinimizationUseAllOrderings() optional bool inprocessing_minimization_use_all_orderings = 298 [default = false];
SatParameters.Builder	SatParameters.Builder.clearInprocessingMinimizationUseConflictAnalysis() optional bool inprocessing_minimization_use_conflict_analysis = 297 [default = true];
SatParameters.Builder	SatParameters.Builder.clearInprocessingProbingDtime() The amount of dtime we should spend on probing for each inprocessing round.
SatParameters.Builder	SatParameters.Builder.clearInstantiateAllVariables() If true, the solver will add a default integer branching strategy to the already defined search strategy.
SatParameters.Builder	SatParameters.Builder.clearInterleaveBatchSize() optional int32 interleave_batch_size = 134 [default = 0];
SatParameters.Builder	SatParameters.Builder.clearInterleaveSearch() Experimental.
SatParameters.Builder	SatParameters.Builder.clearKeepAllFeasibleSolutionsInPresolve() If true, we disable the presolve reductions that remove feasible solutions from the search space.
SatParameters.Builder	SatParameters.Builder.clearKeepSymmetryInPresolve() Experimental.
SatParameters.Builder	SatParameters.Builder.clearLbRelaxNumWorkersThreshold() Only use lb-relax if we have at least that many workers.
SatParameters.Builder	SatParameters.Builder.clearLinearizationLevel() A non-negative level indicating the type of constraints we consider in the LP relaxation.
SatParameters.Builder	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	SatParameters.Builder.clearLnsInitialDeterministicLimit() optional double lns_initial_deterministic_limit = 308 [default = 0.1];
SatParameters.Builder	SatParameters.Builder.clearLnsInitialDifficulty() Initial parameters for neighborhood generation.
SatParameters.Builder	SatParameters.Builder.clearLogPrefix() Add a prefix to all logs.
SatParameters.Builder	SatParameters.Builder.clearLogSearchProgress() Whether the solver should log the search progress.
SatParameters.Builder	SatParameters.Builder.clearLogSubsolverStatistics() Whether the solver should display per sub-solver search statistics.
SatParameters.Builder	SatParameters.Builder.clearLogToResponse() Log to response proto.
SatParameters.Builder	SatParameters.Builder.clearLogToStdout() Log to stdout.
SatParameters.Builder	SatParameters.Builder.clearLpDualTolerance() optional double lp_dual_tolerance = 267 [default = 1e-07];
SatParameters.Builder	SatParameters.Builder.clearLpPrimalTolerance() The internal LP tolerances used by CP-SAT.
SatParameters.Builder	SatParameters.Builder.clearMaxAllDiffCutSize() Cut generator for all diffs can add too many cuts for large all_diff constraints.
SatParameters.Builder	SatParameters.Builder.clearMaxClauseActivityValue() optional double max_clause_activity_value = 18 [default = 1e+20];
SatParameters.Builder	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	SatParameters.Builder.clearMaxCutRoundsAtLevelZero() Max number of time we perform cut generation and resolve the LP at level 0.
SatParameters.Builder	SatParameters.Builder.clearMaxDeterministicTime() Maximum time allowed in deterministic time to solve a problem.
SatParameters.Builder	SatParameters.Builder.clearMaxDomainSizeWhenEncodingEqNeqConstraints() When loading a*x + b*y ==/!
SatParameters.Builder	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	SatParameters.Builder.clearMaxIntegerRoundingScaling() In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive).
SatParameters.Builder	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	SatParameters.Builder.clearMaxMemoryInMb() Maximum memory allowed for the whole thread containing the solver.
SatParameters.Builder	SatParameters.Builder.clearMaxNumberOfConflicts() Maximum number of conflicts allowed to solve a problem.
SatParameters.Builder	SatParameters.Builder.clearMaxNumCuts() The limit on the number of cuts in our cut pool.
SatParameters.Builder	SatParameters.Builder.clearMaxNumDeterministicBatches() Stops after that number of batches has been scheduled.
SatParameters.Builder	SatParameters.Builder.clearMaxNumIntervalsForTimetableEdgeFinding() Max number of intervals for the timetable_edge_finding algorithm to propagate.
SatParameters.Builder	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	SatParameters.Builder.clearMaxPresolveIterations() In case of large reduction in a presolve iteration, we perform multiple presolve iterations.
SatParameters.Builder	SatParameters.Builder.clearMaxSatAssumptionOrder() optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];
SatParameters.Builder	SatParameters.Builder.clearMaxSatReverseAssumptionOrder() If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.
SatParameters.Builder	SatParameters.Builder.clearMaxSatStratification() optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];
SatParameters.Builder	SatParameters.Builder.clearMaxSizeToCreatePrecedenceLiteralsInDisjunctive() Create one literal for each disjunction of two pairs of tasks.
SatParameters.Builder	SatParameters.Builder.clearMaxTimeInSeconds() Maximum time allowed in seconds to solve a problem.
SatParameters.Builder	SatParameters.Builder.clearMaxVariableActivityValue() optional double max_variable_activity_value = 16 [default = 1e+100];
SatParameters.Builder	SatParameters.Builder.clearMergeAtMostOneWorkLimit() optional double merge_at_most_one_work_limit = 146 [default = 100000000];
SatParameters.Builder	SatParameters.Builder.clearMergeNoOverlapWorkLimit() During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints.
SatParameters.Builder	SatParameters.Builder.clearMinimizationAlgorithm() optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];
SatParameters.Builder	SatParameters.Builder.clearMinimizeReductionDuringPbResolution() A different algorithm during PB resolution.
SatParameters.Builder	SatParameters.Builder.clearMinimizeSharedClauses() Minimize and detect subsumption of shared clauses immediately after they are imported.
SatParameters.Builder	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	SatParameters.Builder.clearMipAutomaticallyScaleVariables() If true, some continuous variable might be automatically scaled.
SatParameters.Builder	SatParameters.Builder.clearMipCheckPrecision() As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted precision during scaling.
SatParameters.Builder	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	SatParameters.Builder.clearMipDropTolerance() Any value in the input mip with a magnitude lower than this will be set to zero.
SatParameters.Builder	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	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	SatParameters.Builder.clearMipMaxValidMagnitude() Any finite values in the input MIP must be below this threshold, otherwise the model will be reported invalid.
SatParameters.Builder	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	SatParameters.Builder.clearMipScaleLargeDomain() If this is false, then mip_var_scaling is only applied to variables with "small" domain.
SatParameters.Builder	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	SatParameters.Builder.clearMipVarScaling() All continuous variable of the problem will be multiplied by this factor.
SatParameters.Builder	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	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	SatParameters.Builder.clearNewConstraintsBatchSize() Add that many lazy constraints (or cuts) at once in the LP.
SatParameters.Builder	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	SatParameters.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	SatParameters.Builder.clearNumFullSubsolvers() We distinguish subsolvers that consume a full thread, and the ones that are always interleaved.
SatParameters.Builder	SatParameters.Builder.clearNumSearchWorkers() optional int32 num_search_workers = 100 [default = 0];
SatParameters.Builder	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	SatParameters.Builder.clearNumWorkers() Specify the number of parallel workers (i.e. threads) to use during search.
SatParameters.Builder	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	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	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	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	SatParameters.Builder.clearOptimizeWithMaxHs() This has no effect if optimize_with_core is false.
SatParameters.Builder	SatParameters.Builder.clearPbCleanupIncrement() Same as for the clauses, but for the learned pseudo-Boolean constraints.
SatParameters.Builder	SatParameters.Builder.clearPbCleanupRatio() optional double pb_cleanup_ratio = 47 [default = 0.5];
SatParameters.Builder	SatParameters.Builder.clearPermutePresolveConstraintOrder() optional bool permute_presolve_constraint_order = 179 [default = false];
SatParameters.Builder	SatParameters.Builder.clearPermuteVariableRandomly() This is mainly here to test the solver variability.
SatParameters.Builder	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	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	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	SatParameters.Builder.clearPreferredVariableOrder() optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
SatParameters.Builder	SatParameters.Builder.clearPresolveBlockedClause() Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.
SatParameters.Builder	SatParameters.Builder.clearPresolveBvaThreshold() Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold.
SatParameters.Builder	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	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	SatParameters.Builder.clearPresolveExtractIntegerEnforcement() If true, we will extract from linear constraints, enforcement literals of the form "integer variable at bound => simplified constraint".
SatParameters.Builder	SatParameters.Builder.clearPresolveInclusionWorkLimit() A few presolve operations involve detecting constraints included in other constraint.
SatParameters.Builder	SatParameters.Builder.clearPresolveProbingDeterministicTimeLimit() optional double presolve_probing_deterministic_time_limit = 57 [default = 30];
SatParameters.Builder	SatParameters.Builder.clearPresolveSubstitutionLevel() How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve.
SatParameters.Builder	SatParameters.Builder.clearPresolveUseBva() Whether or not we use Bounded Variable Addition (BVA) in the presolve.
SatParameters.Builder	SatParameters.Builder.clearProbingDeterministicTimeLimit() The maximum "deterministic" time limit to spend in probing.
SatParameters.Builder	SatParameters.Builder.clearProbingNumCombinationsLimit() How many combinations of pairs or triplets of variables we want to scan.
SatParameters.Builder	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	SatParameters.Builder.clearPseudoCostReliabilityThreshold() The solver ignores the pseudo costs of variables with number of recordings less than this threshold.
SatParameters.Builder	SatParameters.Builder.clearPushAllTasksTowardStart() Experimental code: specify if the objective pushes all tasks toward the start of the schedule.
SatParameters.Builder	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	SatParameters.Builder.clearRandomizeSearch() Randomize fixed search.
SatParameters.Builder	SatParameters.Builder.clearRandomPolarityRatio() The proportion of polarity chosen at random.
SatParameters.Builder	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	SatParameters.Builder.clearRelativeGapLimit() optional double relative_gap_limit = 160 [default = 0];
SatParameters.Builder	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	SatParameters.Builder.clearRepairHint() If true, the solver tries to repair the solution given in the hint.
SatParameters.Builder	SatParameters.Builder.clearRestartAlgorithms() The restart strategies will change each time the strategy_counter is increased.
SatParameters.Builder	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	SatParameters.Builder.clearRestartLbdAverageRatio() optional double restart_lbd_average_ratio = 71 [default = 1];
SatParameters.Builder	SatParameters.Builder.clearRestartPeriod() Restart period for the FIXED_RESTART strategy.
SatParameters.Builder	SatParameters.Builder.clearRestartRunningWindowSize() Size of the window for the moving average restarts.
SatParameters.Builder	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	SatParameters.Builder.clearRoutingCutDpEffort() The amount of "effort" to spend in dynamic programming for computing routing cuts.
SatParameters.Builder	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	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	SatParameters.Builder.clearSaveLpBasisInLbTreeSearch() Experimental.
SatParameters.Builder	SatParameters.Builder.clearSearchBranching() optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
SatParameters.Builder	SatParameters.Builder.clearSearchRandomVariablePoolSize() Search randomization will collect the top 'search_random_variable_pool_size' valued variables, and pick one randomly.
SatParameters.Builder	SatParameters.Builder.clearShareBinaryClauses() Allows sharing of new learned binary clause between workers.
SatParameters.Builder	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	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	SatParameters.Builder.clearSharedTreeNumWorkers() Enables shared tree search.
SatParameters.Builder	SatParameters.Builder.clearSharedTreeOpenLeavesPerWorker() How many open leaf nodes should the shared tree maintain per worker.
SatParameters.Builder	SatParameters.Builder.clearSharedTreeSplitStrategy() optional .operations_research.sat.SatParameters.SharedTreeSplitStrategy shared_tree_split_strategy = 239 [default = SPLIT_STRATEGY_AUTO];
SatParameters.Builder	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	SatParameters.Builder.clearSharedTreeWorkerEnableTrailSharing() If true, workers share more of the information from their local trail.
SatParameters.Builder	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	SatParameters.Builder.clearShareGlueClauses() Allows sharing of short glue clauses between workers.
SatParameters.Builder	SatParameters.Builder.clearShareLevelZeroBounds() Allows sharing of the bounds of modified variables at level 0.
SatParameters.Builder	SatParameters.Builder.clearShareObjectiveBounds() Allows objective sharing between workers.
SatParameters.Builder	SatParameters.Builder.clearShavingSearchDeterministicTime() Specifies the amount of deterministic time spent of each try at shaving a bound in the shaving search.
SatParameters.Builder	SatParameters.Builder.clearShavingSearchThreshold() Specifies the threshold between two modes in the shaving procedure.
SatParameters.Builder	SatParameters.Builder.clearSolutionPoolSize() Size of the top-n different solutions kept by the solver.
SatParameters.Builder	SatParameters.Builder.clearStopAfterFirstSolution() For an optimization problem, stop the solver as soon as we have a solution.
SatParameters.Builder	SatParameters.Builder.clearStopAfterPresolve() Mainly used when improving the presolver.
SatParameters.Builder	SatParameters.Builder.clearStopAfterRootPropagation() optional bool stop_after_root_propagation = 252 [default = false];
SatParameters.Builder	SatParameters.Builder.clearStrategyChangeIncreaseRatio() The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.
SatParameters.Builder	SatParameters.Builder.clearSubsolverParams() It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.clearSubsolvers() In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.
SatParameters.Builder	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	SatParameters.Builder.clearSymmetryDetectionDeterministicTimeLimit() Deterministic time limit for symmetry detection.
SatParameters.Builder	SatParameters.Builder.clearSymmetryLevel() Whether we try to automatically detect the symmetries in a model and exploit them.
SatParameters.Builder	SatParameters.Builder.clearTableCompressionLevel() How much we try to "compress" a table constraint.
SatParameters.Builder	SatParameters.Builder.clearUseAbslRandom() optional bool use_absl_random = 180 [default = false];
SatParameters.Builder	SatParameters.Builder.clearUseAllDifferentForCircuit() Turn on extra propagation for the circuit constraint.
SatParameters.Builder	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	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	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	SatParameters.Builder.clearUseConservativeScaleOverloadChecker() Enable a heuristic to solve cumulative constraints using a modified energy constraint.
SatParameters.Builder	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	SatParameters.Builder.clearUseDualSchedulingHeuristics() When set, it activates a few scheduling parameters to improve the lower bound of scheduling problems.
SatParameters.Builder	SatParameters.Builder.clearUseDynamicPrecedenceInCumulative() optional bool use_dynamic_precedence_in_cumulative = 268 [default = false];
SatParameters.Builder	SatParameters.Builder.clearUseDynamicPrecedenceInDisjunctive() Whether we try to branch on decision "interval A before interval B" rather than on intervals bounds.
SatParameters.Builder	SatParameters.Builder.clearUseEnergeticReasoningInNoOverlap2D() When this is true, the no_overlap_2d constraint is reinforced with energetic reasoning.
SatParameters.Builder	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	SatParameters.Builder.clearUseExactLpReason() The solver usually exploit the LP relaxation of a model.
SatParameters.Builder	SatParameters.Builder.clearUseExtendedProbing() Use extended probing (probe bool_or, at_most_one, exactly_one).
SatParameters.Builder	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	SatParameters.Builder.clearUseFeasibilityPump() Adds a feasibility pump subsolver along with lns subsolvers.
SatParameters.Builder	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	SatParameters.Builder.clearUseImpliedBounds() Stores and exploits "implied-bounds" in the solver.
SatParameters.Builder	SatParameters.Builder.clearUseLbRelaxLns() Turns on neighborhood generator based on local branching LP.
SatParameters.Builder	SatParameters.Builder.clearUseLns() Testing parameters used to disable all lns workers.
SatParameters.Builder	SatParameters.Builder.clearUseLnsOnly() Experimental parameters to disable everything but lns.
SatParameters.Builder	SatParameters.Builder.clearUseLsOnly() Disable every other type of subsolver, setting this turns CP-SAT into a pure local-search solver.
SatParameters.Builder	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	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	SatParameters.Builder.clearUseOptimizationHints() For an optimization problem, whether we follow some hints in order to find a better first solution.
SatParameters.Builder	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	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	SatParameters.Builder.clearUsePbResolution() Whether to use pseudo-Boolean resolution to analyze a conflict.
SatParameters.Builder	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	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	SatParameters.Builder.clearUseProbingSearch() If true, search will continuously probe Boolean variables, and integer variable bounds.
SatParameters.Builder	SatParameters.Builder.clearUseRinsLns() Turns on relaxation induced neighborhood generator.
SatParameters.Builder	SatParameters.Builder.clearUseSatInprocessing() Enable or disable "inprocessing" which is some SAT presolving done at each restart to the root level.
SatParameters.Builder	SatParameters.Builder.clearUseSharedTreeSearch() Set on shared subtree workers.
SatParameters.Builder	SatParameters.Builder.clearUseShavingInProbingSearch() 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.
SatParameters.Builder	SatParameters.Builder.clearUseStrongPropagationInDisjunctive() Enable stronger and more expensive propagation on no_overlap constraint.
SatParameters.Builder	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	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	SatParameters.Builder.clearUseTimetablingInNoOverlap2D() When this is true, the no_overlap_2d constraint is reinforced with propagators from the cumulative constraints.
SatParameters.Builder	SatParameters.Builder.clearUseTryEdgeReasoningInNoOverlap2D() optional bool use_try_edge_reasoning_in_no_overlap_2d = 299 [default = false];
SatParameters.Builder	SatParameters.Builder.clearUseVariablesShavingSearch() This search takes all Boolean or integer variables, and maximize or minimize them in order to reduce their domain.
SatParameters.Builder	SatParameters.Builder.clearVariableActivityDecay() Each time a conflict is found, the activities of some variables are increased by one.
SatParameters.Builder	SatParameters.Builder.clearViolationLsCompoundMoveProbability() Probability of using compound move search each restart.
SatParameters.Builder	SatParameters.Builder.clearViolationLsPerturbationPeriod() How long violation_ls should wait before perturbating a solution.
SatParameters.Builder	CpSolver.getParameters() Returns the builder of the parameters of the SAT solver for modification.
SatParameters.Builder	SatParameters.Builder.getSubsolverParamsBuilder(int index) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.mergeFrom(com.google.protobuf.CodedInputStream input, com.google.protobuf.ExtensionRegistryLite extensionRegistry)
SatParameters.Builder	SatParameters.Builder.mergeFrom(com.google.protobuf.Message other)
SatParameters.Builder	SatParameters.Builder.mergeFrom(SatParameters other)
static SatParameters.Builder	SatParameters.newBuilder()
static SatParameters.Builder	SatParameters.newBuilder(SatParameters prototype)
SatParameters.Builder	SatParameters.newBuilderForType()
protected SatParameters.Builder	SatParameters.newBuilderForType(com.google.protobuf.AbstractMessage.BuilderParent parent)
SatParameters.Builder	SatParameters.Builder.removeSubsolverParams(int index) It is possible to specify additional subsolver configuration.
SatParameters.Builder	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	SatParameters.Builder.setAddCgCuts(boolean value) Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
SatParameters.Builder	SatParameters.Builder.setAddCliqueCuts(boolean value) Whether we generate clique cuts from the binary implication graph.
SatParameters.Builder	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	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	SatParameters.Builder.setAddMirCuts(boolean value) Whether we generate MIR cuts at root node.
SatParameters.Builder	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	SatParameters.Builder.setAddRltCuts(boolean value) Whether we generate RLT cuts.
SatParameters.Builder	SatParameters.Builder.setAddZeroHalfCuts(boolean value) Whether we generate Zero-Half cuts at root node.
SatParameters.Builder	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	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	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	SatParameters.Builder.setBinaryMinimizationAlgorithm(SatParameters.BinaryMinizationAlgorithm value) optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];
SatParameters.Builder	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	SatParameters.Builder.setBlockingRestartMultiplier(double value) optional double blocking_restart_multiplier = 66 [default = 1.4];
SatParameters.Builder	SatParameters.Builder.setBlockingRestartWindowSize(int value) optional int32 blocking_restart_window_size = 65 [default = 5000];
SatParameters.Builder	SatParameters.Builder.setBooleanEncodingLevel(int value) A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.
SatParameters.Builder	SatParameters.Builder.setCatchSigintSignal(boolean value) Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve.
SatParameters.Builder	SatParameters.Builder.setClauseActivityDecay(double value) Clause activity parameters (same effect as the one on the variables).
SatParameters.Builder	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	SatParameters.Builder.setClauseCleanupOrdering(SatParameters.ClauseOrdering value) optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];
SatParameters.Builder	SatParameters.Builder.setClauseCleanupPeriod(int value) Trigger a cleanup when this number of "deletable" clauses is learned.
SatParameters.Builder	SatParameters.Builder.setClauseCleanupProtection(SatParameters.ClauseProtection value) optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];
SatParameters.Builder	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	SatParameters.Builder.setClauseCleanupTarget(int value) During a cleanup, we will always keep that number of "deletable" clauses.
SatParameters.Builder	SatParameters.Builder.setConvertIntervals(boolean value) Temporary flag util the feature is more mature.
SatParameters.Builder	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 core
SatParameters.Builder	SatParameters.Builder.setCountAssumptionLevelsInLbd(boolean value) Whether or not the assumption levels are taken into account during the LBD computation.
SatParameters.Builder	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	SatParameters.Builder.setCpModelPresolve(boolean value) Whether we presolve the cp_model before solving it.
SatParameters.Builder	SatParameters.Builder.setCpModelProbingLevel(int value) How much effort do we spend on probing. 0 disables it completely.
SatParameters.Builder	SatParameters.Builder.setCpModelUseSatPresolve(boolean value) Whether we also use the sat presolve when cp_model_presolve is true.
SatParameters.Builder	SatParameters.Builder.setCutActiveCountDecay(double value) optional double cut_active_count_decay = 156 [default = 0.8];
SatParameters.Builder	SatParameters.Builder.setCutCleanupTarget(int value) Target number of constraints to remove during cleanup.
SatParameters.Builder	SatParameters.Builder.setCutLevel(int value) Control the global cut effort.
SatParameters.Builder	SatParameters.Builder.setCutMaxActiveCountValue(double value) These parameters are similar to sat clause management activity parameters.
SatParameters.Builder	SatParameters.Builder.setDebugCrashIfPresolveBreaksHint(boolean value) Crash if presolve breaks a feasible hint.
SatParameters.Builder	SatParameters.Builder.setDebugCrashOnBadHint(boolean value) Crash if we do not manage to complete the hint into a full solution.
SatParameters.Builder	SatParameters.Builder.setDebugMaxNumPresolveOperations(int value) If positive, try to stop just after that many presolve rules have been applied.
SatParameters.Builder	SatParameters.Builder.setDebugPostsolveWithFullSolver(boolean value) We have two different postsolve code.
SatParameters.Builder	SatParameters.Builder.setDefaultRestartAlgorithms(java.lang.String value) optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
SatParameters.Builder	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	SatParameters.Builder.setDetectLinearizedProduct(boolean value) Infer products of Boolean or of Boolean time IntegerVariable from the linear constrainst in the problem.
SatParameters.Builder	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	SatParameters.Builder.setDisableConstraintExpansion(boolean value) If true, it disable all constraint expansion.
SatParameters.Builder	SatParameters.Builder.setDiversifyLnsParams(boolean value) If true, registers more lns subsolvers with different parameters.
SatParameters.Builder	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	SatParameters.Builder.setEncodeCumulativeAsReservoir(boolean value) Encore cumulative with fixed demands and capacity as a reservoir constraint.
SatParameters.Builder	SatParameters.Builder.setEnumerateAllSolutions(boolean value) Whether we enumerate all solutions of a problem without objective.
SatParameters.Builder	SatParameters.Builder.setExpandAlldiffConstraints(boolean value) If true, expand all_different constraints that are not permutations.
SatParameters.Builder	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	SatParameters.Builder.setExpandReservoirUsingCircuit(boolean value) Mainly useful for testing.
SatParameters.Builder	SatParameters.Builder.setExploitAllLpSolution(boolean value) If true and the Lp relaxation of the problem has a solution, try to exploit it.
SatParameters.Builder	SatParameters.Builder.setExploitAllPrecedences(boolean value) optional bool exploit_all_precedences = 220 [default = false];
SatParameters.Builder	SatParameters.Builder.setExploitBestSolution(boolean value) When branching on a variable, follow the last best solution value.
SatParameters.Builder	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	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	SatParameters.Builder.setExploitRelaxationSolution(boolean value) When branching on a variable, follow the last best relaxation solution value.
SatParameters.Builder	SatParameters.Builder.setExtraSubsolvers(int index, java.lang.String value) A convenient way to add more workers types.
SatParameters.Builder	SatParameters.Builder.setFeasibilityJumpBatchDtime(double value) How much dtime for each LS batch.
SatParameters.Builder	SatParameters.Builder.setFeasibilityJumpDecay(double value) On each restart, we randomly choose if we use decay (with this parameter) or no decay.
SatParameters.Builder	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	SatParameters.Builder.setFeasibilityJumpLinearizationLevel(int value) How much do we linearize the problem in the local search code.
SatParameters.Builder	SatParameters.Builder.setFeasibilityJumpMaxExpandedConstraintSize(int value) Maximum size of no_overlap or no_overlap_2d constraint for a quadratic expansion.
SatParameters.Builder	SatParameters.Builder.setFeasibilityJumpRestartFactor(int value) This is a factor that directly influence the work before each restart.
SatParameters.Builder	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	SatParameters.Builder.setFeasibilityJumpVarRandomizationProbability(double value) Probability for a variable to have a non default value upon restarts or perturbations.
SatParameters.Builder	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	SatParameters.Builder.setFillTightenedDomainsInResponse(boolean value) If true, add information about the derived variable domains to the CpSolverResponse.
SatParameters.Builder	SatParameters.Builder.setFilterSubsolvers(int index, java.lang.String value) repeated string filter_subsolvers = 293;
SatParameters.Builder	SatParameters.Builder.setFindBigLinearOverlap(boolean value) Try to find large "rectangle" in the linear constraint matrix with identical lines.
SatParameters.Builder	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	SatParameters.Builder.setFixVariablesToTheirHintedValue(boolean value) If true, variables appearing in the solution hints will be fixed to their hinted value.
SatParameters.Builder	SatParameters.Builder.setFpRounding(SatParameters.FPRoundingMethod value) optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];
SatParameters.Builder	SatParameters.Builder.setGlucoseDecayIncrement(double value) optional double glucose_decay_increment = 23 [default = 0.01];
SatParameters.Builder	SatParameters.Builder.setGlucoseDecayIncrementPeriod(int value) optional int32 glucose_decay_increment_period = 24 [default = 5000];
SatParameters.Builder	SatParameters.Builder.setGlucoseMaxDecay(double value) The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95.
SatParameters.Builder	SatParameters.Builder.setHintConflictLimit(int value) Conflict limit used in the phase that exploit the solution hint.
SatParameters.Builder	SatParameters.Builder.setIgnoreNames(boolean value) If true, we don't keep names in our internal copy of the user given model.
SatParameters.Builder	SatParameters.Builder.setIgnoreSubsolvers(int index, java.lang.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	SatParameters.Builder.setInferAllDiffs(boolean value) Run a max-clique code amongst all the x !
SatParameters.Builder	SatParameters.Builder.setInitialPolarity(SatParameters.Polarity value) optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];
SatParameters.Builder	SatParameters.Builder.setInitialVariablesActivity(double value) The initial value of the variables activity.
SatParameters.Builder	SatParameters.Builder.setInprocessingDtimeRatio(double value) Proportion of deterministic time we should spend on inprocessing.
SatParameters.Builder	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	SatParameters.Builder.setInprocessingMinimizationUseAllOrderings(boolean value) optional bool inprocessing_minimization_use_all_orderings = 298 [default = false];
SatParameters.Builder	SatParameters.Builder.setInprocessingMinimizationUseConflictAnalysis(boolean value) optional bool inprocessing_minimization_use_conflict_analysis = 297 [default = true];
SatParameters.Builder	SatParameters.Builder.setInprocessingProbingDtime(double value) The amount of dtime we should spend on probing for each inprocessing round.
SatParameters.Builder	SatParameters.Builder.setInstantiateAllVariables(boolean value) If true, the solver will add a default integer branching strategy to the already defined search strategy.
SatParameters.Builder	SatParameters.Builder.setInterleaveBatchSize(int value) optional int32 interleave_batch_size = 134 [default = 0];
SatParameters.Builder	SatParameters.Builder.setInterleaveSearch(boolean value) Experimental.
SatParameters.Builder	SatParameters.Builder.setKeepAllFeasibleSolutionsInPresolve(boolean value) If true, we disable the presolve reductions that remove feasible solutions from the search space.
SatParameters.Builder	SatParameters.Builder.setKeepSymmetryInPresolve(boolean value) Experimental.
SatParameters.Builder	SatParameters.Builder.setLbRelaxNumWorkersThreshold(int value) Only use lb-relax if we have at least that many workers.
SatParameters.Builder	SatParameters.Builder.setLinearizationLevel(int value) A non-negative level indicating the type of constraints we consider in the LP relaxation.
SatParameters.Builder	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	SatParameters.Builder.setLnsInitialDeterministicLimit(double value) optional double lns_initial_deterministic_limit = 308 [default = 0.1];
SatParameters.Builder	SatParameters.Builder.setLnsInitialDifficulty(double value) Initial parameters for neighborhood generation.
SatParameters.Builder	SatParameters.Builder.setLogPrefix(java.lang.String value) Add a prefix to all logs.
SatParameters.Builder	SatParameters.Builder.setLogPrefixBytes(com.google.protobuf.ByteString value) Add a prefix to all logs.
SatParameters.Builder	SatParameters.Builder.setLogSearchProgress(boolean value) Whether the solver should log the search progress.
SatParameters.Builder	SatParameters.Builder.setLogSubsolverStatistics(boolean value) Whether the solver should display per sub-solver search statistics.
SatParameters.Builder	SatParameters.Builder.setLogToResponse(boolean value) Log to response proto.
SatParameters.Builder	SatParameters.Builder.setLogToStdout(boolean value) Log to stdout.
SatParameters.Builder	SatParameters.Builder.setLpDualTolerance(double value) optional double lp_dual_tolerance = 267 [default = 1e-07];
SatParameters.Builder	SatParameters.Builder.setLpPrimalTolerance(double value) The internal LP tolerances used by CP-SAT.
SatParameters.Builder	SatParameters.Builder.setMaxAllDiffCutSize(int value) Cut generator for all diffs can add too many cuts for large all_diff constraints.
SatParameters.Builder	SatParameters.Builder.setMaxClauseActivityValue(double value) optional double max_clause_activity_value = 18 [default = 1e+20];
SatParameters.Builder	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	SatParameters.Builder.setMaxCutRoundsAtLevelZero(int value) Max number of time we perform cut generation and resolve the LP at level 0.
SatParameters.Builder	SatParameters.Builder.setMaxDeterministicTime(double value) Maximum time allowed in deterministic time to solve a problem.
SatParameters.Builder	SatParameters.Builder.setMaxDomainSizeWhenEncodingEqNeqConstraints(int value) When loading a*x + b*y ==/!
SatParameters.Builder	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	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	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	SatParameters.Builder.setMaxMemoryInMb(long value) Maximum memory allowed for the whole thread containing the solver.
SatParameters.Builder	SatParameters.Builder.setMaxNumberOfConflicts(long value) Maximum number of conflicts allowed to solve a problem.
SatParameters.Builder	SatParameters.Builder.setMaxNumCuts(int value) The limit on the number of cuts in our cut pool.
SatParameters.Builder	SatParameters.Builder.setMaxNumDeterministicBatches(int value) Stops after that number of batches has been scheduled.
SatParameters.Builder	SatParameters.Builder.setMaxNumIntervalsForTimetableEdgeFinding(int value) Max number of intervals for the timetable_edge_finding algorithm to propagate.
SatParameters.Builder	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	SatParameters.Builder.setMaxPresolveIterations(int value) In case of large reduction in a presolve iteration, we perform multiple presolve iterations.
SatParameters.Builder	SatParameters.Builder.setMaxSatAssumptionOrder(SatParameters.MaxSatAssumptionOrder value) optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];
SatParameters.Builder	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	SatParameters.Builder.setMaxSatStratification(SatParameters.MaxSatStratificationAlgorithm value) optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];
SatParameters.Builder	SatParameters.Builder.setMaxSizeToCreatePrecedenceLiteralsInDisjunctive(int value) Create one literal for each disjunction of two pairs of tasks.
SatParameters.Builder	SatParameters.Builder.setMaxTimeInSeconds(double value) Maximum time allowed in seconds to solve a problem.
SatParameters.Builder	SatParameters.Builder.setMaxVariableActivityValue(double value) optional double max_variable_activity_value = 16 [default = 1e+100];
SatParameters.Builder	SatParameters.Builder.setMergeAtMostOneWorkLimit(double value) optional double merge_at_most_one_work_limit = 146 [default = 100000000];
SatParameters.Builder	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	SatParameters.Builder.setMinimizationAlgorithm(SatParameters.ConflictMinimizationAlgorithm value) optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];
SatParameters.Builder	SatParameters.Builder.setMinimizeReductionDuringPbResolution(boolean value) A different algorithm during PB resolution.
SatParameters.Builder	SatParameters.Builder.setMinimizeSharedClauses(boolean value) Minimize and detect subsumption of shared clauses immediately after they are imported.
SatParameters.Builder	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	SatParameters.Builder.setMipAutomaticallyScaleVariables(boolean value) If true, some continuous variable might be automatically scaled.
SatParameters.Builder	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	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	SatParameters.Builder.setMipDropTolerance(double value) Any value in the input mip with a magnitude lower than this will be set to zero.
SatParameters.Builder	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	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	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	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	SatParameters.Builder.setMipScaleLargeDomain(boolean value) If this is false, then mip_var_scaling is only applied to variables with "small" domain.
SatParameters.Builder	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	SatParameters.Builder.setMipVarScaling(double value) All continuous variable of the problem will be multiplied by this factor.
SatParameters.Builder	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.
SatParameters.Builder	SatParameters.Builder.setName(java.lang.String value) In some context, like in a portfolio of search, it makes sense to name a given parameters set for logging purpose.
SatParameters.Builder	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	SatParameters.Builder.setNewConstraintsBatchSize(int value) Add that many lazy constraints (or cuts) at once in the LP.
SatParameters.Builder	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	SatParameters.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	SatParameters.Builder.setNumFullSubsolvers(int value) We distinguish subsolvers that consume a full thread, and the ones that are always interleaved.
SatParameters.Builder	SatParameters.Builder.setNumSearchWorkers(int value) optional int32 num_search_workers = 100 [default = 0];
SatParameters.Builder	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	SatParameters.Builder.setNumWorkers(int value) Specify the number of parallel workers (i.e. threads) to use during search.
SatParameters.Builder	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	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	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	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	SatParameters.Builder.setOptimizeWithMaxHs(boolean value) This has no effect if optimize_with_core is false.
SatParameters.Builder	SatParameters.Builder.setPbCleanupIncrement(int value) Same as for the clauses, but for the learned pseudo-Boolean constraints.
SatParameters.Builder	SatParameters.Builder.setPbCleanupRatio(double value) optional double pb_cleanup_ratio = 47 [default = 0.5];
SatParameters.Builder	SatParameters.Builder.setPermutePresolveConstraintOrder(boolean value) optional bool permute_presolve_constraint_order = 179 [default = false];
SatParameters.Builder	SatParameters.Builder.setPermuteVariableRandomly(boolean value) This is mainly here to test the solver variability.
SatParameters.Builder	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	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	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	SatParameters.Builder.setPreferredVariableOrder(SatParameters.VariableOrder value) optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
SatParameters.Builder	SatParameters.Builder.setPresolveBlockedClause(boolean value) Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.
SatParameters.Builder	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	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	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	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	SatParameters.Builder.setPresolveInclusionWorkLimit(long value) A few presolve operations involve detecting constraints included in other constraint.
SatParameters.Builder	SatParameters.Builder.setPresolveProbingDeterministicTimeLimit(double value) optional double presolve_probing_deterministic_time_limit = 57 [default = 30];
SatParameters.Builder	SatParameters.Builder.setPresolveSubstitutionLevel(int value) How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve.
SatParameters.Builder	SatParameters.Builder.setPresolveUseBva(boolean value) Whether or not we use Bounded Variable Addition (BVA) in the presolve.
SatParameters.Builder	SatParameters.Builder.setProbingDeterministicTimeLimit(double value) The maximum "deterministic" time limit to spend in probing.
SatParameters.Builder	SatParameters.Builder.setProbingNumCombinationsLimit(int value) How many combinations of pairs or triplets of variables we want to scan.
SatParameters.Builder	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	SatParameters.Builder.setPseudoCostReliabilityThreshold(long value) The solver ignores the pseudo costs of variables with number of recordings less than this threshold.
SatParameters.Builder	SatParameters.Builder.setPushAllTasksTowardStart(boolean value) Experimental code: specify if the objective pushes all tasks toward the start of the schedule.
SatParameters.Builder	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	SatParameters.Builder.setRandomizeSearch(boolean value) Randomize fixed search.
SatParameters.Builder	SatParameters.Builder.setRandomPolarityRatio(double value) The proportion of polarity chosen at random.
SatParameters.Builder	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	SatParameters.Builder.setRelativeGapLimit(double value) optional double relative_gap_limit = 160 [default = 0];
SatParameters.Builder	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	SatParameters.Builder.setRepairHint(boolean value) If true, the solver tries to repair the solution given in the hint.
SatParameters.Builder	SatParameters.Builder.setRestartAlgorithms(int index, SatParameters.RestartAlgorithm value) The restart strategies will change each time the strategy_counter is increased.
SatParameters.Builder	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	SatParameters.Builder.setRestartLbdAverageRatio(double value) optional double restart_lbd_average_ratio = 71 [default = 1];
SatParameters.Builder	SatParameters.Builder.setRestartPeriod(int value) Restart period for the FIXED_RESTART strategy.
SatParameters.Builder	SatParameters.Builder.setRestartRunningWindowSize(int value) Size of the window for the moving average restarts.
SatParameters.Builder	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	SatParameters.Builder.setRoutingCutDpEffort(double value) The amount of "effort" to spend in dynamic programming for computing routing cuts.
SatParameters.Builder	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	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	SatParameters.Builder.setSaveLpBasisInLbTreeSearch(boolean value) Experimental.
SatParameters.Builder	SatParameters.Builder.setSearchBranching(SatParameters.SearchBranching value) optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
SatParameters.Builder	SatParameters.Builder.setSearchRandomVariablePoolSize(long value) Search randomization will collect the top 'search_random_variable_pool_size' valued variables, and pick one randomly.
SatParameters.Builder	SatParameters.Builder.setShareBinaryClauses(boolean value) Allows sharing of new learned binary clause between workers.
SatParameters.Builder	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	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	SatParameters.Builder.setSharedTreeNumWorkers(int value) Enables shared tree search.
SatParameters.Builder	SatParameters.Builder.setSharedTreeOpenLeavesPerWorker(double value) How many open leaf nodes should the shared tree maintain per worker.
SatParameters.Builder	SatParameters.Builder.setSharedTreeSplitStrategy(SatParameters.SharedTreeSplitStrategy value) optional .operations_research.sat.SatParameters.SharedTreeSplitStrategy shared_tree_split_strategy = 239 [default = SPLIT_STRATEGY_AUTO];
SatParameters.Builder	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	SatParameters.Builder.setSharedTreeWorkerEnableTrailSharing(boolean value) If true, workers share more of the information from their local trail.
SatParameters.Builder	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	SatParameters.Builder.setShareGlueClauses(boolean value) Allows sharing of short glue clauses between workers.
SatParameters.Builder	SatParameters.Builder.setShareLevelZeroBounds(boolean value) Allows sharing of the bounds of modified variables at level 0.
SatParameters.Builder	SatParameters.Builder.setShareObjectiveBounds(boolean value) Allows objective sharing between workers.
SatParameters.Builder	SatParameters.Builder.setShavingSearchDeterministicTime(double value) Specifies the amount of deterministic time spent of each try at shaving a bound in the shaving search.
SatParameters.Builder	SatParameters.Builder.setShavingSearchThreshold(long value) Specifies the threshold between two modes in the shaving procedure.
SatParameters.Builder	SatParameters.Builder.setSolutionPoolSize(int value) Size of the top-n different solutions kept by the solver.
SatParameters.Builder	SatParameters.Builder.setStopAfterFirstSolution(boolean value) For an optimization problem, stop the solver as soon as we have a solution.
SatParameters.Builder	SatParameters.Builder.setStopAfterPresolve(boolean value) Mainly used when improving the presolver.
SatParameters.Builder	SatParameters.Builder.setStopAfterRootPropagation(boolean value) optional bool stop_after_root_propagation = 252 [default = false];
SatParameters.Builder	SatParameters.Builder.setStrategyChangeIncreaseRatio(double value) The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.
SatParameters.Builder	SatParameters.Builder.setSubsolverParams(int index, SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.setSubsolverParams(int index, SatParameters value) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.setSubsolvers(int index, java.lang.String value) In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters.
SatParameters.Builder	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	SatParameters.Builder.setSymmetryDetectionDeterministicTimeLimit(double value) Deterministic time limit for symmetry detection.
SatParameters.Builder	SatParameters.Builder.setSymmetryLevel(int value) Whether we try to automatically detect the symmetries in a model and exploit them.
SatParameters.Builder	SatParameters.Builder.setTableCompressionLevel(int value) How much we try to "compress" a table constraint.
SatParameters.Builder	SatParameters.Builder.setUseAbslRandom(boolean value) optional bool use_absl_random = 180 [default = false];
SatParameters.Builder	SatParameters.Builder.setUseAllDifferentForCircuit(boolean value) Turn on extra propagation for the circuit constraint.
SatParameters.Builder	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	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	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	SatParameters.Builder.setUseConservativeScaleOverloadChecker(boolean value) Enable a heuristic to solve cumulative constraints using a modified energy constraint.
SatParameters.Builder	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	SatParameters.Builder.setUseDualSchedulingHeuristics(boolean value) When set, it activates a few scheduling parameters to improve the lower bound of scheduling problems.
SatParameters.Builder	SatParameters.Builder.setUseDynamicPrecedenceInCumulative(boolean value) optional bool use_dynamic_precedence_in_cumulative = 268 [default = false];
SatParameters.Builder	SatParameters.Builder.setUseDynamicPrecedenceInDisjunctive(boolean value) Whether we try to branch on decision "interval A before interval B" rather than on intervals bounds.
SatParameters.Builder	SatParameters.Builder.setUseEnergeticReasoningInNoOverlap2D(boolean value) When this is true, the no_overlap_2d constraint is reinforced with energetic reasoning.
SatParameters.Builder	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	SatParameters.Builder.setUseExactLpReason(boolean value) The solver usually exploit the LP relaxation of a model.
SatParameters.Builder	SatParameters.Builder.setUseExtendedProbing(boolean value) Use extended probing (probe bool_or, at_most_one, exactly_one).
SatParameters.Builder	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	SatParameters.Builder.setUseFeasibilityPump(boolean value) Adds a feasibility pump subsolver along with lns subsolvers.
SatParameters.Builder	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	SatParameters.Builder.setUseImpliedBounds(boolean value) Stores and exploits "implied-bounds" in the solver.
SatParameters.Builder	SatParameters.Builder.setUseLbRelaxLns(boolean value) Turns on neighborhood generator based on local branching LP.
SatParameters.Builder	SatParameters.Builder.setUseLns(boolean value) Testing parameters used to disable all lns workers.
SatParameters.Builder	SatParameters.Builder.setUseLnsOnly(boolean value) Experimental parameters to disable everything but lns.
SatParameters.Builder	SatParameters.Builder.setUseLsOnly(boolean value) Disable every other type of subsolver, setting this turns CP-SAT into a pure local-search solver.
SatParameters.Builder	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	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	SatParameters.Builder.setUseOptimizationHints(boolean value) For an optimization problem, whether we follow some hints in order to find a better first solution.
SatParameters.Builder	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	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	SatParameters.Builder.setUsePbResolution(boolean value) Whether to use pseudo-Boolean resolution to analyze a conflict.
SatParameters.Builder	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	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	SatParameters.Builder.setUseProbingSearch(boolean value) If true, search will continuously probe Boolean variables, and integer variable bounds.
SatParameters.Builder	SatParameters.Builder.setUseRinsLns(boolean value) Turns on relaxation induced neighborhood generator.
SatParameters.Builder	SatParameters.Builder.setUseSatInprocessing(boolean value) Enable or disable "inprocessing" which is some SAT presolving done at each restart to the root level.
SatParameters.Builder	SatParameters.Builder.setUseSharedTreeSearch(boolean value) Set on shared subtree workers.
SatParameters.Builder	SatParameters.Builder.setUseShavingInProbingSearch(boolean 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 search.
SatParameters.Builder	SatParameters.Builder.setUseStrongPropagationInDisjunctive(boolean value) Enable stronger and more expensive propagation on no_overlap constraint.
SatParameters.Builder	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	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	SatParameters.Builder.setUseTimetablingInNoOverlap2D(boolean value) When this is true, the no_overlap_2d constraint is reinforced with propagators from the cumulative constraints.
SatParameters.Builder	SatParameters.Builder.setUseTryEdgeReasoningInNoOverlap2D(boolean value) optional bool use_try_edge_reasoning_in_no_overlap_2d = 299 [default = false];
SatParameters.Builder	SatParameters.Builder.setUseVariablesShavingSearch(boolean value) This search takes all Boolean or integer variables, and maximize or minimize them in order to reduce their domain.
SatParameters.Builder	SatParameters.Builder.setVariableActivityDecay(double value) Each time a conflict is found, the activities of some variables are increased by one.
SatParameters.Builder	SatParameters.Builder.setViolationLsCompoundMoveProbability(double value) Probability of using compound move search each restart.
SatParameters.Builder	SatParameters.Builder.setViolationLsPerturbationPeriod(int value) How long violation_ls should wait before perturbating a solution.
SatParameters.Builder	SatParameters.toBuilder()

Methods in com.google.ortools.sat that return types with arguments of type SatParameters.Builder

Modifier and Type	Method and Description
java.util.List<SatParameters.Builder>	SatParameters.Builder.getSubsolverParamsBuilderList() It is possible to specify additional subsolver configuration.

Methods in com.google.ortools.sat with parameters of type SatParameters.Builder

Modifier and Type	Method and Description
SatParameters.Builder	SatParameters.Builder.addSubsolverParams(int index, SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.
SatParameters.Builder	SatParameters.Builder.addSubsolverParams(SatParameters.Builder builderForValue) It is possible to specify additional subsolver configuration.
SatParameters.Builder	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.Builder

Modifier and Type	Method and Description
SatParameters.Builder	CpSolverRequest.Builder.getParametersBuilder() Solver parameters.

Methods in com.google.ortools.sat.v1 with parameters of type SatParameters.Builder

Modifier and Type	Method and Description
CpSolverRequest.Builder	CpSolverRequest.Builder.setParameters(SatParameters.Builder builderForValue) Solver parameters.