All Superinterfaces:: com.google.protobuf.MessageLiteOrBuilder, com.google.protobuf.MessageOrBuilder

All Known Implementing Classes:: SatParameters, SatParameters.Builder

public interface SatParametersOrBuilder
extends com.google.protobuf.MessageOrBuilder

Method Summary

Modifier and Type	Method	Description
`double`	`getAbsoluteGapLimit()`	Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit.
`boolean`	`getAddCgCuts()`	Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
`boolean`	`getAddCliqueCuts()`	Whether we generate clique cuts from the binary implication graph.
`boolean`	`getAddKnapsackCuts()`	Whether we generate knapsack cuts.
`boolean`	`getAddLinMaxCuts()`	For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et.
`boolean`	`getAddLpConstraintsLazily()`	If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch.
`boolean`	`getAddMirCuts()`	Whether we generate MIR cuts at root node.
`boolean`	`getAddZeroHalfCuts()`	Whether we generate Zero-Half cuts at root node.
`boolean`	`getAlsoBumpVariablesInConflictReasons()`	When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped.
`boolean`	`getAutoDetectGreaterThanAtLeastOneOf()`	If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present.
`SatParameters.BinaryMinizationAlgorithm`	`getBinaryMinimizationAlgorithm()`	`optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];`
`int`	`getBinarySearchNumConflicts()`	If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict.
`double`	`getBlockingRestartMultiplier()`	`optional double blocking_restart_multiplier = 66 [default = 1.4];`
`int`	`getBlockingRestartWindowSize()`	`optional int32 blocking_restart_window_size = 65 [default = 5000];`
`int`	`getBooleanEncodingLevel()`	A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.
`boolean`	`getCatchSigintSignal()`	Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve.
`double`	`getClauseActivityDecay()`	Clause activity parameters (same effect as the one on the variables).
`int`	`getClauseCleanupLbdBound()`	All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.
`SatParameters.ClauseOrdering`	`getClauseCleanupOrdering()`	`optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];`
`int`	`getClauseCleanupPeriod()`	Trigger a cleanup when this number of "deletable" clauses is learned.
`SatParameters.ClauseProtection`	`getClauseCleanupProtection()`	`optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];`
`int`	`getClauseCleanupTarget()`	During a cleanup, we will always keep that number of "deletable" clauses.
`boolean`	`getConvertIntervals()`	Temporary flag util the feature is more mature.
`boolean`	`getCountAssumptionLevelsInLbd()`	Whether or not the assumption levels are taken into account during the LBD computation.
`boolean`	`getCoverOptimization()`	If true, when the max-sat algo find a core, we compute the minimal number of literals in the core that needs to be true to have a feasible solution.
`int`	`getCpModelMaxNumPresolveOperations()`	If positive, try to stop just after that many presolve rules have been applied.
`boolean`	`getCpModelPostsolveWithFullSolver()`	Advanced usage.
`boolean`	`getCpModelPresolve()`	Whether we presolve the cp_model before solving it.
`int`	`getCpModelProbingLevel()`	How much effort do we spend on probing.
`boolean`	`getCpModelUseSatPresolve()`	Whether we also use the sat presolve when cp_model_presolve is true.
`double`	`getCutActiveCountDecay()`	`optional double cut_active_count_decay = 156 [default = 0.8];`
`int`	`getCutCleanupTarget()`	Target number of constraints to remove during cleanup.
`double`	`getCutMaxActiveCountValue()`	These parameters are similar to sat clause management activity parameters.
`java.lang.String`	`getDefaultRestartAlgorithms()`	`optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];`
`com.google.protobuf.ByteString`	`getDefaultRestartAlgorithmsBytes()`	`optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];`
`boolean`	`getDisableConstraintExpansion()`	If true, it disable all constraint expansion.
`boolean`	`getDiversifyLnsParams()`	If true, registers more lns subsolvers with different parameters.
`boolean`	`getEnumerateAllSolutions()`	Whether we enumerate all solutions of a problem without objective.
`boolean`	`getExpandAlldiffConstraints()`	If true, expand all_different constraints that are not permutations.
`boolean`	`getExpandAutomatonConstraints()`	If true, the automaton constraints are expanded.
`boolean`	`getExpandElementConstraints()`	If true, the element constraints are expanded into many linear constraints of the form (index == i) => (element[i] == target).
`boolean`	`getExpandReservoirConstraints()`	If true, expand the reservoir constraints by creating booleans for all possible precedences between event and encoding the constraint.
`boolean`	`getExpandTableConstraints()`	If true, the positive table constraints are expanded.
`boolean`	`getExploitAllLpSolution()`	If true and the Lp relaxation of the problem has a solution, try to exploit it.
`boolean`	`getExploitBestSolution()`	When branching on a variable, follow the last best solution value.
`boolean`	`getExploitIntegerLpSolution()`	If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it.
`boolean`	`getExploitObjective()`	When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.
`boolean`	`getExploitRelaxationSolution()`	When branching on a variable, follow the last best relaxation solution value.
`boolean`	`getFillTightenedDomainsInResponse()`	If true, add information about the derived variable domains to the CpSolverResponse.
`boolean`	`getFindMultipleCores()`	Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.
`SatParameters.FPRoundingMethod`	`getFpRounding()`	`optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];`
`double`	`getGlucoseDecayIncrement()`	`optional double glucose_decay_increment = 23 [default = 0.01];`
`int`	`getGlucoseDecayIncrementPeriod()`	`optional int32 glucose_decay_increment_period = 24 [default = 5000];`
`double`	`getGlucoseMaxDecay()`	The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95.
`int`	`getHintConflictLimit()`	Conflict limit used in the phase that exploit the solution hint.
`SatParameters.Polarity`	`getInitialPolarity()`	`optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];`
`double`	`getInitialVariablesActivity()`	The initial value of the variables activity.
`boolean`	`getInstantiateAllVariables()`	If true, the solver will add a default integer branching strategy to the already defined search strategy.
`int`	`getInterleaveBatchSize()`	`optional int32 interleave_batch_size = 134 [default = 1];`
`boolean`	`getInterleaveSearch()`	Experimental.
`boolean`	`getKeepAllFeasibleSolutionsInPresolve()`	If true, we disable the presolve reductions that remove feasible solutions from the search space.
`int`	`getLinearizationLevel()`	A non-negative level indicating the type of constraints we consider in the LP relaxation.
`boolean`	`getLnsExpandIntervalsInConstraintGraph()`	`optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];`
`boolean`	`getLnsFocusOnDecisionVariables()`	`optional bool lns_focus_on_decision_variables = 105 [default = false];`
`java.lang.String`	`getLogPrefix()`	Add a prefix to all logs.
`com.google.protobuf.ByteString`	`getLogPrefixBytes()`	Add a prefix to all logs.
`boolean`	`getLogSearchProgress()`	Whether the solver should log the search progress.
`boolean`	`getLogToResponse()`	Log to response proto.
`boolean`	`getLogToStdout()`	Log to stdout.
`int`	`getMaxAllDiffCutSize()`	Cut generator for all diffs can add too many cuts for large all_diff constraints.
`double`	`getMaxClauseActivityValue()`	`optional double max_clause_activity_value = 18 [default = 1e+20];`
`int`	`getMaxConsecutiveInactiveCount()`	If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP.
`int`	`getMaxCutRoundsAtLevelZero()`	Max number of time we perform cut generation and resolve the LP at level 0.
`double`	`getMaxDeterministicTime()`	Maximum time allowed in deterministic time to solve a problem.
`int`	`getMaxIntegerRoundingScaling()`	In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive).
`long`	`getMaxMemoryInMb()`	Maximum memory allowed for the whole thread containing the solver.
`long`	`getMaxNumberOfConflicts()`	Maximum number of conflicts allowed to solve a problem.
`int`	`getMaxNumCuts()`	The limit on the number of cuts in our cut pool.
`int`	`getMaxPresolveIterations()`	In case of large reduction in a presolve iteration, we perform multiple presolve iterations.
`SatParameters.MaxSatAssumptionOrder`	`getMaxSatAssumptionOrder()`	`optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];`
`boolean`	`getMaxSatReverseAssumptionOrder()`	If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.
`SatParameters.MaxSatStratificationAlgorithm`	`getMaxSatStratification()`	`optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];`
`double`	`getMaxTimeInSeconds()`	Maximum time allowed in seconds to solve a problem.
`double`	`getMaxVariableActivityValue()`	`optional double max_variable_activity_value = 16 [default = 1e+100];`
`double`	`getMergeAtMostOneWorkLimit()`	`optional double merge_at_most_one_work_limit = 146 [default = 100000000];`
`double`	`getMergeNoOverlapWorkLimit()`	During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints.
`SatParameters.ConflictMinimizationAlgorithm`	`getMinimizationAlgorithm()`	`optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];`
`boolean`	`getMinimizeCore()`	Whether we use a simple heuristic to try to minimize an UNSAT core.
`boolean`	`getMinimizeReductionDuringPbResolution()`	A different algorithm during PB resolution.
`int`	`getMinimizeWithPropagationNumDecisions()`	`optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];`
`int`	`getMinimizeWithPropagationRestartPeriod()`	Parameters for an heuristic similar to the one descibed in "An effective learnt clause minimization approach for CDCL Sat Solvers", https://www.ijcai.org/proceedings/2017/0098.pdf For now, we have a somewhat simpler implementation where every x restart we spend y decisions on clause minimization.
`double`	`getMinOrthogonalityForLpConstraints()`	While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call.
`boolean`	`getMipAutomaticallyScaleVariables()`	If true, some continuous variable might be automatially scaled.
`double`	`getMipCheckPrecision()`	As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted precision during scaling.
`int`	`getMipMaxActivityExponent()`	To avoid integer overflow, we always force the maximum possible constraint activity (and objective value) according to the initial variable domain to be smaller than 2 to this given power.
`double`	`getMipMaxBound()`	We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use.
`double`	`getMipVarScaling()`	All continuous variable of the problem will be multiplied by this factor.
`double`	`getMipWantedPrecision()`	When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients.
`java.lang.String`	`getName()`	In some context, like in a portfolio of search, it makes sense to name a given parameters set for logging purpose.
`com.google.protobuf.ByteString`	`getNameBytes()`	In some context, like in a portfolio of search, it makes sense to name a given parameters set for logging purpose.
`int`	`getNewConstraintsBatchSize()`	Add that many lazy constraints (or cuts) at once in the LP.
`int`	`getNumConflictsBeforeStrategyChanges()`	After each restart, if the number of conflict since the last strategy change is greater that this, then we increment a "strategy_counter" that can be use to change the search strategy used by the following restarts.
`int`	`getNumSearchWorkers()`	Specify the number of parallel workers to use during search.
`boolean`	`getOnlyAddCutsAtLevelZero()`	For the cut that can be generated at any level, this control if we only try to generate them at the root node.
`boolean`	`getOptimizeWithCore()`	The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one.
`boolean`	`getOptimizeWithMaxHs()`	This has no effect if optimize_with_core is false.
`int`	`getPbCleanupIncrement()`	Same as for the clauses, but for the learned pseudo-Boolean constraints.
`double`	`getPbCleanupRatio()`	`optional double pb_cleanup_ratio = 47 [default = 0.5];`
`boolean`	`getPermutePresolveConstraintOrder()`	`optional bool permute_presolve_constraint_order = 179 [default = false];`
`boolean`	`getPermuteVariableRandomly()`	This is mainly here to test the solver variability.
`int`	`getPolarityRephaseIncrement()`	If non-zero, then we change the polarity heuristic after that many number of conflicts in an arithmetically increasing fashion.
`boolean`	`getPolishLpSolution()`	Whether we try to do a few degenerate iteration at the end of an LP solve to minimize the fractionality of the integer variable in the basis.
`SatParameters.VariableOrder`	`getPreferredVariableOrder()`	`optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];`
`boolean`	`getPresolveBlockedClause()`	Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.
`int`	`getPresolveBvaThreshold()`	Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold.
`int`	`getPresolveBveClauseWeight()`	During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.
`int`	`getPresolveBveThreshold()`	During presolve, only try to perform the bounded variable elimination (BVE) of a variable x if the number of occurrences of x times the number of occurrences of not(x) is not greater than this parameter.
`boolean`	`getPresolveExtractIntegerEnforcement()`	If true, we will extract from linear constraints, enforcement literals of the form "integer variable at bound => simplified constraint".
`double`	`getPresolveProbingDeterministicTimeLimit()`	The maximum "deterministic" time limit to spend in probing.
`int`	`getPresolveSubstitutionLevel()`	How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve.
`boolean`	`getPresolveUseBva()`	Whether or not we use Bounded Variable Addition (BVA) in the presolve.
`long`	`getProbingPeriodAtRoot()`	If set at zero (the default), it is disabled.
`long`	`getPseudoCostReliabilityThreshold()`	The solver ignores the pseudo costs of variables with number of recordings less than this threshold.
`double`	`getRandomBranchesRatio()`	A number between 0 and 1 that indicates the proportion of branching variables that are selected randomly instead of choosing the first variable from the given variable_ordering strategy.
`boolean`	`getRandomizeSearch()`	Randomize fixed search.
`double`	`getRandomPolarityRatio()`	The proportion of polarity chosen at random.
`int`	`getRandomSeed()`	At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed.
`boolean`	`getReduceMemoryUsageInInterleaveMode()`	Temporary parameter until the memory usage is more optimized.
`double`	`getRelativeGapLimit()`	`optional double relative_gap_limit = 160 [default = 0];`
`boolean`	`getRepairHint()`	If true, the solver tries to repair the solution given in the hint.
`SatParameters.RestartAlgorithm`	`getRestartAlgorithms(int index)`	The restart strategies will change each time the strategy_counter is increased.
`int`	`getRestartAlgorithmsCount()`	The restart strategies will change each time the strategy_counter is increased.
`java.util.List<SatParameters.RestartAlgorithm>`	`getRestartAlgorithmsList()`	The restart strategies will change each time the strategy_counter is increased.
`double`	`getRestartDlAverageRatio()`	In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.
`double`	`getRestartLbdAverageRatio()`	`optional double restart_lbd_average_ratio = 71 [default = 1];`
`int`	`getRestartPeriod()`	Restart period for the FIXED_RESTART strategy.
`int`	`getRestartRunningWindowSize()`	Size of the window for the moving average restarts.
`SatParameters.SearchBranching`	`getSearchBranching()`	`optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];`
`long`	`getSearchRandomizationTolerance()`	Search randomization will collect equivalent 'max valued' variables, and pick one randomly.
`boolean`	`getShareLevelZeroBounds()`	Allows sharing of the bounds of modified variables at level 0.
`boolean`	`getShareObjectiveBounds()`	Allows objective sharing between workers.
`boolean`	`getStopAfterFirstSolution()`	For an optimization problem, stop the solver as soon as we have a solution.
`boolean`	`getStopAfterPresolve()`	Mainly used when improving the presolver.
`double`	`getStrategyChangeIncreaseRatio()`	The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.
`boolean`	`getSubsumptionDuringConflictAnalysis()`	At a really low cost, during the 1-UIP conflict computation, it is easy to detect if some of the involved reasons are subsumed by the current conflict.
`int`	`getSymmetryLevel()`	Whether we try to automatically detect the symmetries in a model and exploit them.
`boolean`	`getTreatBinaryClausesSeparately()`	If true, the binary clauses are treated separately from the others.
`boolean`	`getUseAbslRandom()`	`optional bool use_absl_random = 180 [default = false];`
`boolean`	`getUseBlockingRestart()`	Block a moving restart algorithm if the trail size of the current conflict is greater than the multiplier times the moving average of the trail size at the previous conflicts.
`boolean`	`getUseBranchingInLp()`	If true, the solver attemts to generate more info inside lp propagator by branching on some variables if certain criteria are met during the search tree exploration.
`boolean`	`getUseCombinedNoOverlap()`	This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem.
`boolean`	`getUseDisjunctiveConstraintInCumulativeConstraint()`	When this is true, the cumulative constraint is reinforced with propagators from the disjunctive constraint to improve the inference on a set of tasks that are disjunctive at the root of the problem.
`boolean`	`getUseErwaHeuristic()`	Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as described in "Learning Rate Based Branching Heuristic for SAT solvers", J.H.Liang, V.
`boolean`	`getUseExactLpReason()`	The solver usually exploit the LP relaxation of a model.
`boolean`	`getUseFeasibilityPump()`	Adds a feasibility pump subsolver along with lns subsolvers.
`boolean`	`getUseImpliedBounds()`	Stores and exploits "implied-bounds" in the solver.
`boolean`	`getUseLnsOnly()`	LNS parameters.
`boolean`	`getUseOptimizationHints()`	For an optimization problem, whether we follow some hints in order to find a better first solution.
`boolean`	`getUseOptionalVariables()`	If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional.
`boolean`	`getUseOverloadCheckerInCumulativeConstraint()`	When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy.
`boolean`	`getUsePbResolution()`	Whether to use pseudo-Boolean resolution to analyze a conflict.
`boolean`	`getUsePhaseSaving()`	If this is true, then the polarity of a variable will be the last value it was assigned to, or its default polarity if it was never assigned since the call to ResetDecisionHeuristic().
`boolean`	`getUsePrecedencesInDisjunctiveConstraint()`	When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further.
`boolean`	`getUseProbingSearch()`	If true, search will continuously probe Boolean variables, and integer variable bounds.
`boolean`	`getUseRelaxationLns()`	Turns on a lns worker which solves relaxed version of the original problem by removing constraints from the problem in order to get better bounds.
`boolean`	`getUseRinsLns()`	Turns on relaxation induced neighborhood generator.
`boolean`	`getUseSatInprocessing()`	`optional bool use_sat_inprocessing = 163 [default = false];`
`boolean`	`getUseTimetableEdgeFindingInCumulativeConstraint()`	When this is true, the cumulative constraint is reinforced with timetable edge finding, i.e., an additional level of reasoning based on the conjunction of energy and mandatory parts.
`double`	`getVariableActivityDecay()`	Each time a conflict is found, the activities of some variables are increased by one.
`boolean`	`hasAbsoluteGapLimit()`	Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit.
`boolean`	`hasAddCgCuts()`	Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
`boolean`	`hasAddCliqueCuts()`	Whether we generate clique cuts from the binary implication graph.
`boolean`	`hasAddKnapsackCuts()`	Whether we generate knapsack cuts.
`boolean`	`hasAddLinMaxCuts()`	For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et.
`boolean`	`hasAddLpConstraintsLazily()`	If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch.
`boolean`	`hasAddMirCuts()`	Whether we generate MIR cuts at root node.
`boolean`	`hasAddZeroHalfCuts()`	Whether we generate Zero-Half cuts at root node.
`boolean`	`hasAlsoBumpVariablesInConflictReasons()`	When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped.
`boolean`	`hasAutoDetectGreaterThanAtLeastOneOf()`	If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present.
`boolean`	`hasBinaryMinimizationAlgorithm()`	`optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];`
`boolean`	`hasBinarySearchNumConflicts()`	If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict.
`boolean`	`hasBlockingRestartMultiplier()`	`optional double blocking_restart_multiplier = 66 [default = 1.4];`
`boolean`	`hasBlockingRestartWindowSize()`	`optional int32 blocking_restart_window_size = 65 [default = 5000];`
`boolean`	`hasBooleanEncodingLevel()`	A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.
`boolean`	`hasCatchSigintSignal()`	Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve.
`boolean`	`hasClauseActivityDecay()`	Clause activity parameters (same effect as the one on the variables).
`boolean`	`hasClauseCleanupLbdBound()`	All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept.
`boolean`	`hasClauseCleanupOrdering()`	`optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];`
`boolean`	`hasClauseCleanupPeriod()`	Trigger a cleanup when this number of "deletable" clauses is learned.
`boolean`	`hasClauseCleanupProtection()`	`optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];`
`boolean`	`hasClauseCleanupTarget()`	During a cleanup, we will always keep that number of "deletable" clauses.
`boolean`	`hasConvertIntervals()`	Temporary flag util the feature is more mature.
`boolean`	`hasCountAssumptionLevelsInLbd()`	Whether or not the assumption levels are taken into account during the LBD computation.
`boolean`	`hasCoverOptimization()`	If true, when the max-sat algo find a core, we compute the minimal number of literals in the core that needs to be true to have a feasible solution.
`boolean`	`hasCpModelMaxNumPresolveOperations()`	If positive, try to stop just after that many presolve rules have been applied.
`boolean`	`hasCpModelPostsolveWithFullSolver()`	Advanced usage.
`boolean`	`hasCpModelPresolve()`	Whether we presolve the cp_model before solving it.
`boolean`	`hasCpModelProbingLevel()`	How much effort do we spend on probing.
`boolean`	`hasCpModelUseSatPresolve()`	Whether we also use the sat presolve when cp_model_presolve is true.
`boolean`	`hasCutActiveCountDecay()`	`optional double cut_active_count_decay = 156 [default = 0.8];`
`boolean`	`hasCutCleanupTarget()`	Target number of constraints to remove during cleanup.
`boolean`	`hasCutMaxActiveCountValue()`	These parameters are similar to sat clause management activity parameters.
`boolean`	`hasDefaultRestartAlgorithms()`	`optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];`
`boolean`	`hasDisableConstraintExpansion()`	If true, it disable all constraint expansion.
`boolean`	`hasDiversifyLnsParams()`	If true, registers more lns subsolvers with different parameters.
`boolean`	`hasEnumerateAllSolutions()`	Whether we enumerate all solutions of a problem without objective.
`boolean`	`hasExpandAlldiffConstraints()`	If true, expand all_different constraints that are not permutations.
`boolean`	`hasExpandAutomatonConstraints()`	If true, the automaton constraints are expanded.
`boolean`	`hasExpandElementConstraints()`	If true, the element constraints are expanded into many linear constraints of the form (index == i) => (element[i] == target).
`boolean`	`hasExpandReservoirConstraints()`	If true, expand the reservoir constraints by creating booleans for all possible precedences between event and encoding the constraint.
`boolean`	`hasExpandTableConstraints()`	If true, the positive table constraints are expanded.
`boolean`	`hasExploitAllLpSolution()`	If true and the Lp relaxation of the problem has a solution, try to exploit it.
`boolean`	`hasExploitBestSolution()`	When branching on a variable, follow the last best solution value.
`boolean`	`hasExploitIntegerLpSolution()`	If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it.
`boolean`	`hasExploitObjective()`	When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.
`boolean`	`hasExploitRelaxationSolution()`	When branching on a variable, follow the last best relaxation solution value.
`boolean`	`hasFillTightenedDomainsInResponse()`	If true, add information about the derived variable domains to the CpSolverResponse.
`boolean`	`hasFindMultipleCores()`	Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.
`boolean`	`hasFpRounding()`	`optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];`
`boolean`	`hasGlucoseDecayIncrement()`	`optional double glucose_decay_increment = 23 [default = 0.01];`
`boolean`	`hasGlucoseDecayIncrementPeriod()`	`optional int32 glucose_decay_increment_period = 24 [default = 5000];`
`boolean`	`hasGlucoseMaxDecay()`	The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95.
`boolean`	`hasHintConflictLimit()`	Conflict limit used in the phase that exploit the solution hint.
`boolean`	`hasInitialPolarity()`	`optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];`
`boolean`	`hasInitialVariablesActivity()`	The initial value of the variables activity.
`boolean`	`hasInstantiateAllVariables()`	If true, the solver will add a default integer branching strategy to the already defined search strategy.
`boolean`	`hasInterleaveBatchSize()`	`optional int32 interleave_batch_size = 134 [default = 1];`
`boolean`	`hasInterleaveSearch()`	Experimental.
`boolean`	`hasKeepAllFeasibleSolutionsInPresolve()`	If true, we disable the presolve reductions that remove feasible solutions from the search space.
`boolean`	`hasLinearizationLevel()`	A non-negative level indicating the type of constraints we consider in the LP relaxation.
`boolean`	`hasLnsExpandIntervalsInConstraintGraph()`	`optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];`
`boolean`	`hasLnsFocusOnDecisionVariables()`	`optional bool lns_focus_on_decision_variables = 105 [default = false];`
`boolean`	`hasLogPrefix()`	Add a prefix to all logs.
`boolean`	`hasLogSearchProgress()`	Whether the solver should log the search progress.
`boolean`	`hasLogToResponse()`	Log to response proto.
`boolean`	`hasLogToStdout()`	Log to stdout.
`boolean`	`hasMaxAllDiffCutSize()`	Cut generator for all diffs can add too many cuts for large all_diff constraints.
`boolean`	`hasMaxClauseActivityValue()`	`optional double max_clause_activity_value = 18 [default = 1e+20];`
`boolean`	`hasMaxConsecutiveInactiveCount()`	If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP.
`boolean`	`hasMaxCutRoundsAtLevelZero()`	Max number of time we perform cut generation and resolve the LP at level 0.
`boolean`	`hasMaxDeterministicTime()`	Maximum time allowed in deterministic time to solve a problem.
`boolean`	`hasMaxIntegerRoundingScaling()`	In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive).
`boolean`	`hasMaxMemoryInMb()`	Maximum memory allowed for the whole thread containing the solver.
`boolean`	`hasMaxNumberOfConflicts()`	Maximum number of conflicts allowed to solve a problem.
`boolean`	`hasMaxNumCuts()`	The limit on the number of cuts in our cut pool.
`boolean`	`hasMaxPresolveIterations()`	In case of large reduction in a presolve iteration, we perform multiple presolve iterations.
`boolean`	`hasMaxSatAssumptionOrder()`	`optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];`
`boolean`	`hasMaxSatReverseAssumptionOrder()`	If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.
`boolean`	`hasMaxSatStratification()`	`optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];`
`boolean`	`hasMaxTimeInSeconds()`	Maximum time allowed in seconds to solve a problem.
`boolean`	`hasMaxVariableActivityValue()`	`optional double max_variable_activity_value = 16 [default = 1e+100];`
`boolean`	`hasMergeAtMostOneWorkLimit()`	`optional double merge_at_most_one_work_limit = 146 [default = 100000000];`
`boolean`	`hasMergeNoOverlapWorkLimit()`	During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints.
`boolean`	`hasMinimizationAlgorithm()`	`optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];`
`boolean`	`hasMinimizeCore()`	Whether we use a simple heuristic to try to minimize an UNSAT core.
`boolean`	`hasMinimizeReductionDuringPbResolution()`	A different algorithm during PB resolution.
`boolean`	`hasMinimizeWithPropagationNumDecisions()`	`optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];`
`boolean`	`hasMinimizeWithPropagationRestartPeriod()`	Parameters for an heuristic similar to the one descibed in "An effective learnt clause minimization approach for CDCL Sat Solvers", https://www.ijcai.org/proceedings/2017/0098.pdf For now, we have a somewhat simpler implementation where every x restart we spend y decisions on clause minimization.
`boolean`	`hasMinOrthogonalityForLpConstraints()`	While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call.
`boolean`	`hasMipAutomaticallyScaleVariables()`	If true, some continuous variable might be automatially scaled.
`boolean`	`hasMipCheckPrecision()`	As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted precision during scaling.
`boolean`	`hasMipMaxActivityExponent()`	To avoid integer overflow, we always force the maximum possible constraint activity (and objective value) according to the initial variable domain to be smaller than 2 to this given power.
`boolean`	`hasMipMaxBound()`	We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use.
`boolean`	`hasMipVarScaling()`	All continuous variable of the problem will be multiplied by this factor.
`boolean`	`hasMipWantedPrecision()`	When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients.
`boolean`	`hasName()`	In some context, like in a portfolio of search, it makes sense to name a given parameters set for logging purpose.
`boolean`	`hasNewConstraintsBatchSize()`	Add that many lazy constraints (or cuts) at once in the LP.
`boolean`	`hasNumConflictsBeforeStrategyChanges()`	After each restart, if the number of conflict since the last strategy change is greater that this, then we increment a "strategy_counter" that can be use to change the search strategy used by the following restarts.
`boolean`	`hasNumSearchWorkers()`	Specify the number of parallel workers to use during search.
`boolean`	`hasOnlyAddCutsAtLevelZero()`	For the cut that can be generated at any level, this control if we only try to generate them at the root node.
`boolean`	`hasOptimizeWithCore()`	The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one.
`boolean`	`hasOptimizeWithMaxHs()`	This has no effect if optimize_with_core is false.
`boolean`	`hasPbCleanupIncrement()`	Same as for the clauses, but for the learned pseudo-Boolean constraints.
`boolean`	`hasPbCleanupRatio()`	`optional double pb_cleanup_ratio = 47 [default = 0.5];`
`boolean`	`hasPermutePresolveConstraintOrder()`	`optional bool permute_presolve_constraint_order = 179 [default = false];`
`boolean`	`hasPermuteVariableRandomly()`	This is mainly here to test the solver variability.
`boolean`	`hasPolarityRephaseIncrement()`	If non-zero, then we change the polarity heuristic after that many number of conflicts in an arithmetically increasing fashion.
`boolean`	`hasPolishLpSolution()`	Whether we try to do a few degenerate iteration at the end of an LP solve to minimize the fractionality of the integer variable in the basis.
`boolean`	`hasPreferredVariableOrder()`	`optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];`
`boolean`	`hasPresolveBlockedClause()`	Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.
`boolean`	`hasPresolveBvaThreshold()`	Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold.
`boolean`	`hasPresolveBveClauseWeight()`	During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.
`boolean`	`hasPresolveBveThreshold()`	During presolve, only try to perform the bounded variable elimination (BVE) of a variable x if the number of occurrences of x times the number of occurrences of not(x) is not greater than this parameter.
`boolean`	`hasPresolveExtractIntegerEnforcement()`	If true, we will extract from linear constraints, enforcement literals of the form "integer variable at bound => simplified constraint".
`boolean`	`hasPresolveProbingDeterministicTimeLimit()`	The maximum "deterministic" time limit to spend in probing.
`boolean`	`hasPresolveSubstitutionLevel()`	How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve.
`boolean`	`hasPresolveUseBva()`	Whether or not we use Bounded Variable Addition (BVA) in the presolve.
`boolean`	`hasProbingPeriodAtRoot()`	If set at zero (the default), it is disabled.
`boolean`	`hasPseudoCostReliabilityThreshold()`	The solver ignores the pseudo costs of variables with number of recordings less than this threshold.
`boolean`	`hasRandomBranchesRatio()`	A number between 0 and 1 that indicates the proportion of branching variables that are selected randomly instead of choosing the first variable from the given variable_ordering strategy.
`boolean`	`hasRandomizeSearch()`	Randomize fixed search.
`boolean`	`hasRandomPolarityRatio()`	The proportion of polarity chosen at random.
`boolean`	`hasRandomSeed()`	At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed.
`boolean`	`hasReduceMemoryUsageInInterleaveMode()`	Temporary parameter until the memory usage is more optimized.
`boolean`	`hasRelativeGapLimit()`	`optional double relative_gap_limit = 160 [default = 0];`
`boolean`	`hasRepairHint()`	If true, the solver tries to repair the solution given in the hint.
`boolean`	`hasRestartDlAverageRatio()`	In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.
`boolean`	`hasRestartLbdAverageRatio()`	`optional double restart_lbd_average_ratio = 71 [default = 1];`
`boolean`	`hasRestartPeriod()`	Restart period for the FIXED_RESTART strategy.
`boolean`	`hasRestartRunningWindowSize()`	Size of the window for the moving average restarts.
`boolean`	`hasSearchBranching()`	`optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];`
`boolean`	`hasSearchRandomizationTolerance()`	Search randomization will collect equivalent 'max valued' variables, and pick one randomly.
`boolean`	`hasShareLevelZeroBounds()`	Allows sharing of the bounds of modified variables at level 0.
`boolean`	`hasShareObjectiveBounds()`	Allows objective sharing between workers.
`boolean`	`hasStopAfterFirstSolution()`	For an optimization problem, stop the solver as soon as we have a solution.
`boolean`	`hasStopAfterPresolve()`	Mainly used when improving the presolver.
`boolean`	`hasStrategyChangeIncreaseRatio()`	The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.
`boolean`	`hasSubsumptionDuringConflictAnalysis()`	At a really low cost, during the 1-UIP conflict computation, it is easy to detect if some of the involved reasons are subsumed by the current conflict.
`boolean`	`hasSymmetryLevel()`	Whether we try to automatically detect the symmetries in a model and exploit them.
`boolean`	`hasTreatBinaryClausesSeparately()`	If true, the binary clauses are treated separately from the others.
`boolean`	`hasUseAbslRandom()`	`optional bool use_absl_random = 180 [default = false];`
`boolean`	`hasUseBlockingRestart()`	Block a moving restart algorithm if the trail size of the current conflict is greater than the multiplier times the moving average of the trail size at the previous conflicts.
`boolean`	`hasUseBranchingInLp()`	If true, the solver attemts to generate more info inside lp propagator by branching on some variables if certain criteria are met during the search tree exploration.
`boolean`	`hasUseCombinedNoOverlap()`	This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem.
`boolean`	`hasUseDisjunctiveConstraintInCumulativeConstraint()`	When this is true, the cumulative constraint is reinforced with propagators from the disjunctive constraint to improve the inference on a set of tasks that are disjunctive at the root of the problem.
`boolean`	`hasUseErwaHeuristic()`	Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as described in "Learning Rate Based Branching Heuristic for SAT solvers", J.H.Liang, V.
`boolean`	`hasUseExactLpReason()`	The solver usually exploit the LP relaxation of a model.
`boolean`	`hasUseFeasibilityPump()`	Adds a feasibility pump subsolver along with lns subsolvers.
`boolean`	`hasUseImpliedBounds()`	Stores and exploits "implied-bounds" in the solver.
`boolean`	`hasUseLnsOnly()`	LNS parameters.
`boolean`	`hasUseOptimizationHints()`	For an optimization problem, whether we follow some hints in order to find a better first solution.
`boolean`	`hasUseOptionalVariables()`	If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional.
`boolean`	`hasUseOverloadCheckerInCumulativeConstraint()`	When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy.
`boolean`	`hasUsePbResolution()`	Whether to use pseudo-Boolean resolution to analyze a conflict.
`boolean`	`hasUsePhaseSaving()`	If this is true, then the polarity of a variable will be the last value it was assigned to, or its default polarity if it was never assigned since the call to ResetDecisionHeuristic().
`boolean`	`hasUsePrecedencesInDisjunctiveConstraint()`	When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further.
`boolean`	`hasUseProbingSearch()`	If true, search will continuously probe Boolean variables, and integer variable bounds.
`boolean`	`hasUseRelaxationLns()`	Turns on a lns worker which solves relaxed version of the original problem by removing constraints from the problem in order to get better bounds.
`boolean`	`hasUseRinsLns()`	Turns on relaxation induced neighborhood generator.
`boolean`	`hasUseSatInprocessing()`	`optional bool use_sat_inprocessing = 163 [default = false];`
`boolean`	`hasUseTimetableEdgeFindingInCumulativeConstraint()`	When this is true, the cumulative constraint is reinforced with timetable edge finding, i.e., an additional level of reasoning based on the conjunction of energy and mandatory parts.
`boolean`	`hasVariableActivityDecay()`	Each time a conflict is found, the activities of some variables are increased by one.

Methods inherited from interface com.google.protobuf.MessageLiteOrBuilder

isInitialized

Methods inherited from interface com.google.protobuf.MessageOrBuilder

findInitializationErrors, getAllFields, getDefaultInstanceForType, getDescriptorForType, getField, getInitializationErrorString, getOneofFieldDescriptor, getRepeatedField, getRepeatedFieldCount, getUnknownFields, hasField, hasOneof

Method Details

hasName

boolean hasName()

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

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

Returns:: Whether the name field is set.

getName

java.lang.String getName()

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

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

Returns:: The name.

getNameBytes

com.google.protobuf.ByteString getNameBytes()
```
 In some context, like in a portfolio of search, it makes sense to name a
 given parameters set for logging purpose.
 
```
optional string name = 171 [default = ""];
Returns:

The bytes for name.
hasPreferredVariableOrder

boolean hasPreferredVariableOrder()

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

Returns:

Whether the preferredVariableOrder field is set.
getPreferredVariableOrder

SatParameters.VariableOrder getPreferredVariableOrder()

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

Returns:

The preferredVariableOrder.
hasInitialPolarity

boolean hasInitialPolarity()

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

Returns:

Whether the initialPolarity field is set.
getInitialPolarity

SatParameters.Polarity getInitialPolarity()

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

Returns:

The initialPolarity.

hasUsePhaseSaving

boolean hasUsePhaseSaving()

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

optional bool use_phase_saving = 44 [default = true];

Returns:: Whether the usePhaseSaving field is set.

getUsePhaseSaving

boolean getUsePhaseSaving()

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

optional bool use_phase_saving = 44 [default = true];

Returns:: The usePhaseSaving.

hasPolarityRephaseIncrement

boolean hasPolarityRephaseIncrement()

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

optional int32 polarity_rephase_increment = 168 [default = 1000];

Returns:: Whether the polarityRephaseIncrement field is set.

getPolarityRephaseIncrement

int getPolarityRephaseIncrement()

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

optional int32 polarity_rephase_increment = 168 [default = 1000];

Returns:: The polarityRephaseIncrement.

hasRandomPolarityRatio

boolean hasRandomPolarityRatio()

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

optional double random_polarity_ratio = 45 [default = 0];

Returns:: Whether the randomPolarityRatio field is set.

getRandomPolarityRatio

double getRandomPolarityRatio()

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

optional double random_polarity_ratio = 45 [default = 0];

Returns:: The randomPolarityRatio.

hasRandomBranchesRatio

boolean hasRandomBranchesRatio()

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

optional double random_branches_ratio = 32 [default = 0];

Returns:: Whether the randomBranchesRatio field is set.

getRandomBranchesRatio

double getRandomBranchesRatio()

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

optional double random_branches_ratio = 32 [default = 0];

Returns:: The randomBranchesRatio.

hasUseErwaHeuristic

boolean hasUseErwaHeuristic()

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

optional bool use_erwa_heuristic = 75 [default = false];

Returns:: Whether the useErwaHeuristic field is set.

getUseErwaHeuristic

boolean getUseErwaHeuristic()

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

optional bool use_erwa_heuristic = 75 [default = false];

Returns:: The useErwaHeuristic.

hasInitialVariablesActivity

boolean hasInitialVariablesActivity()

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

optional double initial_variables_activity = 76 [default = 0];

Returns:: Whether the initialVariablesActivity field is set.

getInitialVariablesActivity

double getInitialVariablesActivity()

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

optional double initial_variables_activity = 76 [default = 0];

Returns:: The initialVariablesActivity.

hasAlsoBumpVariablesInConflictReasons

boolean hasAlsoBumpVariablesInConflictReasons()

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

optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];

Returns:: Whether the alsoBumpVariablesInConflictReasons field is set.

getAlsoBumpVariablesInConflictReasons

boolean getAlsoBumpVariablesInConflictReasons()

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

optional bool also_bump_variables_in_conflict_reasons = 77 [default = false];

Returns:: The alsoBumpVariablesInConflictReasons.

hasMinimizationAlgorithm

boolean hasMinimizationAlgorithm()

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

Returns:

Whether the minimizationAlgorithm field is set.
getMinimizationAlgorithm

SatParameters.ConflictMinimizationAlgorithm getMinimizationAlgorithm()

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

Returns:

The minimizationAlgorithm.
hasBinaryMinimizationAlgorithm

boolean hasBinaryMinimizationAlgorithm()

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

Returns:

Whether the binaryMinimizationAlgorithm field is set.
getBinaryMinimizationAlgorithm

SatParameters.BinaryMinizationAlgorithm getBinaryMinimizationAlgorithm()

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

Returns:

The binaryMinimizationAlgorithm.

hasSubsumptionDuringConflictAnalysis

boolean hasSubsumptionDuringConflictAnalysis()

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

optional bool subsumption_during_conflict_analysis = 56 [default = true];

Returns:: Whether the subsumptionDuringConflictAnalysis field is set.

getSubsumptionDuringConflictAnalysis

boolean getSubsumptionDuringConflictAnalysis()

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

optional bool subsumption_during_conflict_analysis = 56 [default = true];

Returns:: The subsumptionDuringConflictAnalysis.

hasClauseCleanupPeriod

boolean hasClauseCleanupPeriod()
```
 Trigger a cleanup when this number of "deletable" clauses is learned.
 
```
optional int32 clause_cleanup_period = 11 [default = 10000];
Returns:

Whether the clauseCleanupPeriod field is set.
getClauseCleanupPeriod

int getClauseCleanupPeriod()
```
 Trigger a cleanup when this number of "deletable" clauses is learned.
 
```
optional int32 clause_cleanup_period = 11 [default = 10000];
Returns:

The clauseCleanupPeriod.
hasClauseCleanupTarget

boolean hasClauseCleanupTarget()
```
 During a cleanup, we will always keep that number of "deletable" clauses.
 Note that this doesn't include the "protected" clauses.
 
```
optional int32 clause_cleanup_target = 13 [default = 10000];
Returns:

Whether the clauseCleanupTarget field is set.
getClauseCleanupTarget

int getClauseCleanupTarget()
```
 During a cleanup, we will always keep that number of "deletable" clauses.
 Note that this doesn't include the "protected" clauses.
 
```
optional int32 clause_cleanup_target = 13 [default = 10000];
Returns:

The clauseCleanupTarget.
hasClauseCleanupProtection

boolean hasClauseCleanupProtection()

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

Returns:

Whether the clauseCleanupProtection field is set.
getClauseCleanupProtection

SatParameters.ClauseProtection getClauseCleanupProtection()

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

Returns:

The clauseCleanupProtection.
hasClauseCleanupLbdBound

boolean hasClauseCleanupLbdBound()
```
 All the clauses with a LBD (literal blocks distance) lower or equal to this
 parameters will always be kept.
 
```
optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
Returns:

Whether the clauseCleanupLbdBound field is set.
getClauseCleanupLbdBound

int getClauseCleanupLbdBound()
```
 All the clauses with a LBD (literal blocks distance) lower or equal to this
 parameters will always be kept.
 
```
optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
Returns:

The clauseCleanupLbdBound.
hasClauseCleanupOrdering

boolean hasClauseCleanupOrdering()

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

Returns:

Whether the clauseCleanupOrdering field is set.
getClauseCleanupOrdering

SatParameters.ClauseOrdering getClauseCleanupOrdering()

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

Returns:

The clauseCleanupOrdering.
hasPbCleanupIncrement

boolean hasPbCleanupIncrement()
```
 Same as for the clauses, but for the learned pseudo-Boolean constraints.
 
```
optional int32 pb_cleanup_increment = 46 [default = 200];
Returns:

Whether the pbCleanupIncrement field is set.
getPbCleanupIncrement

int getPbCleanupIncrement()
```
 Same as for the clauses, but for the learned pseudo-Boolean constraints.
 
```
optional int32 pb_cleanup_increment = 46 [default = 200];
Returns:

The pbCleanupIncrement.
hasPbCleanupRatio

boolean hasPbCleanupRatio()

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns:

Whether the pbCleanupRatio field is set.
getPbCleanupRatio

double getPbCleanupRatio()

optional double pb_cleanup_ratio = 47 [default = 0.5];

Returns:

The pbCleanupRatio.

hasMinimizeWithPropagationRestartPeriod

boolean hasMinimizeWithPropagationRestartPeriod()

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

optional int32 minimize_with_propagation_restart_period = 96 [default = 10];

Returns:: Whether the minimizeWithPropagationRestartPeriod field is set.

getMinimizeWithPropagationRestartPeriod

int getMinimizeWithPropagationRestartPeriod()

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

optional int32 minimize_with_propagation_restart_period = 96 [default = 10];

Returns:: The minimizeWithPropagationRestartPeriod.

hasMinimizeWithPropagationNumDecisions

boolean hasMinimizeWithPropagationNumDecisions()

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns:

Whether the minimizeWithPropagationNumDecisions field is set.
getMinimizeWithPropagationNumDecisions

int getMinimizeWithPropagationNumDecisions()

optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];

Returns:

The minimizeWithPropagationNumDecisions.

hasVariableActivityDecay

boolean hasVariableActivityDecay()

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

optional double variable_activity_decay = 15 [default = 0.8];

Returns:: Whether the variableActivityDecay field is set.

getVariableActivityDecay

double getVariableActivityDecay()

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

optional double variable_activity_decay = 15 [default = 0.8];

Returns:: The variableActivityDecay.

hasMaxVariableActivityValue

boolean hasMaxVariableActivityValue()

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

Returns:

Whether the maxVariableActivityValue field is set.
getMaxVariableActivityValue

double getMaxVariableActivityValue()

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

Returns:

The maxVariableActivityValue.

hasGlucoseMaxDecay

boolean hasGlucoseMaxDecay()

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

optional double glucose_max_decay = 22 [default = 0.95];

Returns:: Whether the glucoseMaxDecay field is set.

getGlucoseMaxDecay

double getGlucoseMaxDecay()

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

optional double glucose_max_decay = 22 [default = 0.95];

Returns:: The glucoseMaxDecay.

hasGlucoseDecayIncrement

boolean hasGlucoseDecayIncrement()

optional double glucose_decay_increment = 23 [default = 0.01];

Returns:

Whether the glucoseDecayIncrement field is set.
getGlucoseDecayIncrement

double getGlucoseDecayIncrement()

optional double glucose_decay_increment = 23 [default = 0.01];

Returns:

The glucoseDecayIncrement.
hasGlucoseDecayIncrementPeriod

boolean hasGlucoseDecayIncrementPeriod()

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns:

Whether the glucoseDecayIncrementPeriod field is set.
getGlucoseDecayIncrementPeriod

int getGlucoseDecayIncrementPeriod()

optional int32 glucose_decay_increment_period = 24 [default = 5000];

Returns:

The glucoseDecayIncrementPeriod.
hasClauseActivityDecay

boolean hasClauseActivityDecay()
```
 Clause activity parameters (same effect as the one on the variables).
 
```
optional double clause_activity_decay = 17 [default = 0.999];
Returns:

Whether the clauseActivityDecay field is set.
getClauseActivityDecay

double getClauseActivityDecay()
```
 Clause activity parameters (same effect as the one on the variables).
 
```
optional double clause_activity_decay = 17 [default = 0.999];
Returns:

The clauseActivityDecay.
hasMaxClauseActivityValue

boolean hasMaxClauseActivityValue()

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

Returns:

Whether the maxClauseActivityValue field is set.
getMaxClauseActivityValue

double getMaxClauseActivityValue()

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

Returns:

The maxClauseActivityValue.

getRestartAlgorithmsList

java.util.List<SatParameters.RestartAlgorithm> getRestartAlgorithmsList()

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

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

Returns:: A list containing the restartAlgorithms.

getRestartAlgorithmsCount

int getRestartAlgorithmsCount()

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

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

Returns:: The count of restartAlgorithms.

getRestartAlgorithms

SatParameters.RestartAlgorithm getRestartAlgorithms(int index)

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

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

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

hasDefaultRestartAlgorithms

boolean hasDefaultRestartAlgorithms()

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

Returns:

Whether the defaultRestartAlgorithms field is set.
getDefaultRestartAlgorithms

java.lang.String getDefaultRestartAlgorithms()

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

Returns:

The defaultRestartAlgorithms.
getDefaultRestartAlgorithmsBytes

com.google.protobuf.ByteString getDefaultRestartAlgorithmsBytes()

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

Returns:

The bytes for defaultRestartAlgorithms.
hasRestartPeriod

boolean hasRestartPeriod()
```
 Restart period for the FIXED_RESTART strategy. This is also the multiplier
 used by the LUBY_RESTART strategy.
 
```
optional int32 restart_period = 30 [default = 50];
Returns:

Whether the restartPeriod field is set.

getRestartPeriod

int getRestartPeriod()

 Restart period for the FIXED_RESTART strategy. This is also the multiplier
 used by the LUBY_RESTART strategy.

optional int32 restart_period = 30 [default = 50];

Returns:: The restartPeriod.

hasRestartRunningWindowSize

boolean hasRestartRunningWindowSize()
```
 Size of the window for the moving average restarts.
 
```
optional int32 restart_running_window_size = 62 [default = 50];
Returns:

Whether the restartRunningWindowSize field is set.
getRestartRunningWindowSize

int getRestartRunningWindowSize()
```
 Size of the window for the moving average restarts.
 
```
optional int32 restart_running_window_size = 62 [default = 50];
Returns:

The restartRunningWindowSize.
hasRestartDlAverageRatio

boolean hasRestartDlAverageRatio()
```
 In the moving average restart algorithms, a restart is triggered if the
 window average times this ratio is greater that the global average.
 
```
optional double restart_dl_average_ratio = 63 [default = 1];
Returns:

Whether the restartDlAverageRatio field is set.
getRestartDlAverageRatio

double getRestartDlAverageRatio()
```
 In the moving average restart algorithms, a restart is triggered if the
 window average times this ratio is greater that the global average.
 
```
optional double restart_dl_average_ratio = 63 [default = 1];
Returns:

The restartDlAverageRatio.
hasRestartLbdAverageRatio

boolean hasRestartLbdAverageRatio()

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns:

Whether the restartLbdAverageRatio field is set.
getRestartLbdAverageRatio

double getRestartLbdAverageRatio()

optional double restart_lbd_average_ratio = 71 [default = 1];

Returns:

The restartLbdAverageRatio.

hasUseBlockingRestart

boolean hasUseBlockingRestart()

 Block a moving restart algorithm if the trail size of the current conflict
 is greater than the multiplier times the moving average of the trail size
 at the previous conflicts.

optional bool use_blocking_restart = 64 [default = false];

Returns:: Whether the useBlockingRestart field is set.

getUseBlockingRestart

boolean getUseBlockingRestart()

 Block a moving restart algorithm if the trail size of the current conflict
 is greater than the multiplier times the moving average of the trail size
 at the previous conflicts.

optional bool use_blocking_restart = 64 [default = false];

Returns:: The useBlockingRestart.

hasBlockingRestartWindowSize

boolean hasBlockingRestartWindowSize()

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns:

Whether the blockingRestartWindowSize field is set.
getBlockingRestartWindowSize

int getBlockingRestartWindowSize()

optional int32 blocking_restart_window_size = 65 [default = 5000];

Returns:

The blockingRestartWindowSize.
hasBlockingRestartMultiplier

boolean hasBlockingRestartMultiplier()

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns:

Whether the blockingRestartMultiplier field is set.
getBlockingRestartMultiplier

double getBlockingRestartMultiplier()

optional double blocking_restart_multiplier = 66 [default = 1.4];

Returns:

The blockingRestartMultiplier.

hasNumConflictsBeforeStrategyChanges

boolean hasNumConflictsBeforeStrategyChanges()

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

optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];

Returns:: Whether the numConflictsBeforeStrategyChanges field is set.

getNumConflictsBeforeStrategyChanges

int getNumConflictsBeforeStrategyChanges()

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

optional int32 num_conflicts_before_strategy_changes = 68 [default = 0];

Returns:: The numConflictsBeforeStrategyChanges.

hasStrategyChangeIncreaseRatio

boolean hasStrategyChangeIncreaseRatio()
```
 The parameter num_conflicts_before_strategy_changes is increased by that
 much after each strategy change.
 
```
optional double strategy_change_increase_ratio = 69 [default = 0];
Returns:

Whether the strategyChangeIncreaseRatio field is set.
getStrategyChangeIncreaseRatio

double getStrategyChangeIncreaseRatio()
```
 The parameter num_conflicts_before_strategy_changes is increased by that
 much after each strategy change.
 
```
optional double strategy_change_increase_ratio = 69 [default = 0];
Returns:

The strategyChangeIncreaseRatio.
hasMaxTimeInSeconds

boolean hasMaxTimeInSeconds()
```
 Maximum time allowed in seconds to solve a problem.
 The counter will starts at the beginning of the Solve() call.
 
```
optional double max_time_in_seconds = 36 [default = inf];
Returns:

Whether the maxTimeInSeconds field is set.
getMaxTimeInSeconds

double getMaxTimeInSeconds()
```
 Maximum time allowed in seconds to solve a problem.
 The counter will starts at the beginning of the Solve() call.
 
```
optional double max_time_in_seconds = 36 [default = inf];
Returns:

The maxTimeInSeconds.

hasMaxDeterministicTime

boolean hasMaxDeterministicTime()

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

optional double max_deterministic_time = 67 [default = inf];

Returns:: Whether the maxDeterministicTime field is set.

getMaxDeterministicTime

double getMaxDeterministicTime()

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

optional double max_deterministic_time = 67 [default = inf];

Returns:: The maxDeterministicTime.

hasMaxNumberOfConflicts

boolean hasMaxNumberOfConflicts()

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

optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];

Returns:: Whether the maxNumberOfConflicts field is set.

getMaxNumberOfConflicts

long getMaxNumberOfConflicts()

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

optional int64 max_number_of_conflicts = 37 [default = 9223372036854775807];

Returns:: The maxNumberOfConflicts.

hasMaxMemoryInMb

boolean hasMaxMemoryInMb()

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

optional int64 max_memory_in_mb = 40 [default = 10000];

Returns:: Whether the maxMemoryInMb field is set.

getMaxMemoryInMb

long getMaxMemoryInMb()

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

optional int64 max_memory_in_mb = 40 [default = 10000];

Returns:: The maxMemoryInMb.

hasAbsoluteGapLimit

boolean hasAbsoluteGapLimit()

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

optional double absolute_gap_limit = 159 [default = 0];

Returns:: Whether the absoluteGapLimit field is set.

getAbsoluteGapLimit

double getAbsoluteGapLimit()

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

optional double absolute_gap_limit = 159 [default = 0];

Returns:: The absoluteGapLimit.

hasRelativeGapLimit

boolean hasRelativeGapLimit()

optional double relative_gap_limit = 160 [default = 0];

Returns:

Whether the relativeGapLimit field is set.
getRelativeGapLimit

double getRelativeGapLimit()

optional double relative_gap_limit = 160 [default = 0];

Returns:

The relativeGapLimit.
hasTreatBinaryClausesSeparately

boolean hasTreatBinaryClausesSeparately()
```
 If true, the binary clauses are treated separately from the others. This
 should be faster and uses less memory. However it changes the propagation
 order.
 
```
optional bool treat_binary_clauses_separately = 33 [default = true];
Returns:

Whether the treatBinaryClausesSeparately field is set.
getTreatBinaryClausesSeparately

boolean getTreatBinaryClausesSeparately()
```
 If true, the binary clauses are treated separately from the others. This
 should be faster and uses less memory. However it changes the propagation
 order.
 
```
optional bool treat_binary_clauses_separately = 33 [default = true];
Returns:

The treatBinaryClausesSeparately.

hasRandomSeed

boolean hasRandomSeed()

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

optional int32 random_seed = 31 [default = 1];

Returns:: Whether the randomSeed field is set.

getRandomSeed

int getRandomSeed()

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

optional int32 random_seed = 31 [default = 1];

Returns:: The randomSeed.

hasPermuteVariableRandomly

boolean hasPermuteVariableRandomly()

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

optional bool permute_variable_randomly = 178 [default = false];

Returns:: Whether the permuteVariableRandomly field is set.

getPermuteVariableRandomly

boolean getPermuteVariableRandomly()

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

optional bool permute_variable_randomly = 178 [default = false];

Returns:: The permuteVariableRandomly.

hasPermutePresolveConstraintOrder

boolean hasPermutePresolveConstraintOrder()

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns:

Whether the permutePresolveConstraintOrder field is set.
getPermutePresolveConstraintOrder

boolean getPermutePresolveConstraintOrder()

optional bool permute_presolve_constraint_order = 179 [default = false];

Returns:

The permutePresolveConstraintOrder.
hasUseAbslRandom

boolean hasUseAbslRandom()

optional bool use_absl_random = 180 [default = false];

Returns:

Whether the useAbslRandom field is set.
getUseAbslRandom

boolean getUseAbslRandom()

optional bool use_absl_random = 180 [default = false];

Returns:

The useAbslRandom.
hasLogSearchProgress

boolean hasLogSearchProgress()
```
 Whether the solver should log the search progress. By default, it logs to
 LOG(INFO). This can be overwritten by the log_destination parameter.
 
```
optional bool log_search_progress = 41 [default = false];
Returns:

Whether the logSearchProgress field is set.

getLogSearchProgress

boolean getLogSearchProgress()

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

optional bool log_search_progress = 41 [default = false];

Returns:: The logSearchProgress.

hasLogPrefix

boolean hasLogPrefix()
```
 Add a prefix to all logs.
 
```
optional string log_prefix = 185 [default = ""];
Returns:

Whether the logPrefix field is set.
getLogPrefix

java.lang.String getLogPrefix()
```
 Add a prefix to all logs.
 
```
optional string log_prefix = 185 [default = ""];
Returns:

The logPrefix.
getLogPrefixBytes

com.google.protobuf.ByteString getLogPrefixBytes()
```
 Add a prefix to all logs.
 
```
optional string log_prefix = 185 [default = ""];
Returns:

The bytes for logPrefix.
hasLogToStdout

boolean hasLogToStdout()
```
 Log to stdout.
 
```
optional bool log_to_stdout = 186 [default = true];
Returns:

Whether the logToStdout field is set.
getLogToStdout

boolean getLogToStdout()
```
 Log to stdout.
 
```
optional bool log_to_stdout = 186 [default = true];
Returns:

The logToStdout.
hasLogToResponse

boolean hasLogToResponse()
```
 Log to response proto.
 
```
optional bool log_to_response = 187 [default = false];
Returns:

Whether the logToResponse field is set.
getLogToResponse

boolean getLogToResponse()
```
 Log to response proto.
 
```
optional bool log_to_response = 187 [default = false];
Returns:

The logToResponse.

hasUsePbResolution

boolean hasUsePbResolution()

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

optional bool use_pb_resolution = 43 [default = false];

Returns:: Whether the usePbResolution field is set.

getUsePbResolution

boolean getUsePbResolution()

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

optional bool use_pb_resolution = 43 [default = false];

Returns:: The usePbResolution.

hasMinimizeReductionDuringPbResolution

boolean hasMinimizeReductionDuringPbResolution()

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

optional bool minimize_reduction_during_pb_resolution = 48 [default = false];

Returns:: Whether the minimizeReductionDuringPbResolution field is set.

getMinimizeReductionDuringPbResolution

boolean getMinimizeReductionDuringPbResolution()

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

optional bool minimize_reduction_during_pb_resolution = 48 [default = false];

Returns:: The minimizeReductionDuringPbResolution.

hasCountAssumptionLevelsInLbd

boolean hasCountAssumptionLevelsInLbd()

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

optional bool count_assumption_levels_in_lbd = 49 [default = true];

Returns:: Whether the countAssumptionLevelsInLbd field is set.

getCountAssumptionLevelsInLbd

boolean getCountAssumptionLevelsInLbd()

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

optional bool count_assumption_levels_in_lbd = 49 [default = true];

Returns:: The countAssumptionLevelsInLbd.

hasPresolveBveThreshold

boolean hasPresolveBveThreshold()

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

optional int32 presolve_bve_threshold = 54 [default = 500];

Returns:: Whether the presolveBveThreshold field is set.

getPresolveBveThreshold

int getPresolveBveThreshold()

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

optional int32 presolve_bve_threshold = 54 [default = 500];

Returns:: The presolveBveThreshold.

hasPresolveBveClauseWeight

boolean hasPresolveBveClauseWeight()
```
 During presolve, we apply BVE only if this weight times the number of
 clauses plus the number of clause literals is not increased.
 
```
optional int32 presolve_bve_clause_weight = 55 [default = 3];
Returns:

Whether the presolveBveClauseWeight field is set.
getPresolveBveClauseWeight

int getPresolveBveClauseWeight()
```
 During presolve, we apply BVE only if this weight times the number of
 clauses plus the number of clause literals is not increased.
 
```
optional int32 presolve_bve_clause_weight = 55 [default = 3];
Returns:

The presolveBveClauseWeight.
hasPresolveProbingDeterministicTimeLimit

boolean hasPresolveProbingDeterministicTimeLimit()
```
 The maximum "deterministic" time limit to spend in probing. A value of
 zero will disable the probing.
 
```
optional double presolve_probing_deterministic_time_limit = 57 [default = 30];
Returns:

Whether the presolveProbingDeterministicTimeLimit field is set.
getPresolveProbingDeterministicTimeLimit

double getPresolveProbingDeterministicTimeLimit()
```
 The maximum "deterministic" time limit to spend in probing. A value of
 zero will disable the probing.
 
```
optional double presolve_probing_deterministic_time_limit = 57 [default = 30];
Returns:

The presolveProbingDeterministicTimeLimit.
hasPresolveBlockedClause

boolean hasPresolveBlockedClause()
```
 Whether we use an heuristic to detect some basic case of blocked clause
 in the SAT presolve.
 
```
optional bool presolve_blocked_clause = 88 [default = true];
Returns:

Whether the presolveBlockedClause field is set.
getPresolveBlockedClause

boolean getPresolveBlockedClause()
```
 Whether we use an heuristic to detect some basic case of blocked clause
 in the SAT presolve.
 
```
optional bool presolve_blocked_clause = 88 [default = true];
Returns:

The presolveBlockedClause.
hasPresolveUseBva

boolean hasPresolveUseBva()
```
 Whether or not we use Bounded Variable Addition (BVA) in the presolve.
 
```
optional bool presolve_use_bva = 72 [default = true];
Returns:

Whether the presolveUseBva field is set.
getPresolveUseBva

boolean getPresolveUseBva()
```
 Whether or not we use Bounded Variable Addition (BVA) in the presolve.
 
```
optional bool presolve_use_bva = 72 [default = true];
Returns:

The presolveUseBva.

hasPresolveBvaThreshold

boolean hasPresolveBvaThreshold()

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

optional int32 presolve_bva_threshold = 73 [default = 1];

Returns:: Whether the presolveBvaThreshold field is set.

getPresolveBvaThreshold

int getPresolveBvaThreshold()

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

optional int32 presolve_bva_threshold = 73 [default = 1];

Returns:: The presolveBvaThreshold.

hasMaxPresolveIterations

boolean hasMaxPresolveIterations()

 In case of large reduction in a presolve iteration, we perform multiple
 presolve iterations. This parameter controls the maximum number of such
 presolve iterations.

optional int32 max_presolve_iterations = 138 [default = 3];

Returns:: Whether the maxPresolveIterations field is set.

getMaxPresolveIterations

int getMaxPresolveIterations()

 In case of large reduction in a presolve iteration, we perform multiple
 presolve iterations. This parameter controls the maximum number of such
 presolve iterations.

optional int32 max_presolve_iterations = 138 [default = 3];

Returns:: The maxPresolveIterations.

hasCpModelPresolve

boolean hasCpModelPresolve()
```
 Whether we presolve the cp_model before solving it.
 
```
optional bool cp_model_presolve = 86 [default = true];
Returns:

Whether the cpModelPresolve field is set.
getCpModelPresolve

boolean getCpModelPresolve()
```
 Whether we presolve the cp_model before solving it.
 
```
optional bool cp_model_presolve = 86 [default = true];
Returns:

The cpModelPresolve.

hasCpModelPostsolveWithFullSolver

boolean hasCpModelPostsolveWithFullSolver()

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

optional bool cp_model_postsolve_with_full_solver = 162 [default = false];

Returns:: Whether the cpModelPostsolveWithFullSolver field is set.

getCpModelPostsolveWithFullSolver

boolean getCpModelPostsolveWithFullSolver()

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

optional bool cp_model_postsolve_with_full_solver = 162 [default = false];

Returns:: The cpModelPostsolveWithFullSolver.

hasCpModelMaxNumPresolveOperations

boolean hasCpModelMaxNumPresolveOperations()
```
 If positive, try to stop just after that many presolve rules have been
 applied. This is mainly useful for debugging presolve.
 
```
optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];
Returns:

Whether the cpModelMaxNumPresolveOperations field is set.
getCpModelMaxNumPresolveOperations

int getCpModelMaxNumPresolveOperations()
```
 If positive, try to stop just after that many presolve rules have been
 applied. This is mainly useful for debugging presolve.
 
```
optional int32 cp_model_max_num_presolve_operations = 151 [default = 0];
Returns:

The cpModelMaxNumPresolveOperations.
hasCpModelProbingLevel

boolean hasCpModelProbingLevel()
```
 How much effort do we spend on probing. 0 disables it completely.
 
```
optional int32 cp_model_probing_level = 110 [default = 2];
Returns:

Whether the cpModelProbingLevel field is set.
getCpModelProbingLevel

int getCpModelProbingLevel()
```
 How much effort do we spend on probing. 0 disables it completely.
 
```
optional int32 cp_model_probing_level = 110 [default = 2];
Returns:

The cpModelProbingLevel.
hasCpModelUseSatPresolve

boolean hasCpModelUseSatPresolve()
```
 Whether we also use the sat presolve when cp_model_presolve is true.
 
```
optional bool cp_model_use_sat_presolve = 93 [default = true];
Returns:

Whether the cpModelUseSatPresolve field is set.
getCpModelUseSatPresolve

boolean getCpModelUseSatPresolve()
```
 Whether we also use the sat presolve when cp_model_presolve is true.
 
```
optional bool cp_model_use_sat_presolve = 93 [default = true];
Returns:

The cpModelUseSatPresolve.
hasUseSatInprocessing

boolean hasUseSatInprocessing()

optional bool use_sat_inprocessing = 163 [default = false];

Returns:

Whether the useSatInprocessing field is set.
getUseSatInprocessing

boolean getUseSatInprocessing()

optional bool use_sat_inprocessing = 163 [default = false];

Returns:

The useSatInprocessing.
hasExpandElementConstraints

boolean hasExpandElementConstraints()
```
 If true, the element constraints are expanded into many
 linear constraints of the form (index == i) => (element[i] == target).
 
```
optional bool expand_element_constraints = 140 [default = true];
Returns:

Whether the expandElementConstraints field is set.
getExpandElementConstraints

boolean getExpandElementConstraints()
```
 If true, the element constraints are expanded into many
 linear constraints of the form (index == i) => (element[i] == target).
 
```
optional bool expand_element_constraints = 140 [default = true];
Returns:

The expandElementConstraints.
hasExpandAutomatonConstraints

boolean hasExpandAutomatonConstraints()
```
 If true, the automaton constraints are expanded.
 
```
optional bool expand_automaton_constraints = 143 [default = true];
Returns:

Whether the expandAutomatonConstraints field is set.
getExpandAutomatonConstraints

boolean getExpandAutomatonConstraints()
```
 If true, the automaton constraints are expanded.
 
```
optional bool expand_automaton_constraints = 143 [default = true];
Returns:

The expandAutomatonConstraints.
hasExpandTableConstraints

boolean hasExpandTableConstraints()
```
 If true, the positive table constraints are expanded.
 Note that currently, negative table constraints are always expanded.
 
```
optional bool expand_table_constraints = 158 [default = true];
Returns:

Whether the expandTableConstraints field is set.
getExpandTableConstraints

boolean getExpandTableConstraints()
```
 If true, the positive table constraints are expanded.
 Note that currently, negative table constraints are always expanded.
 
```
optional bool expand_table_constraints = 158 [default = true];
Returns:

The expandTableConstraints.
hasExpandAlldiffConstraints

boolean hasExpandAlldiffConstraints()
```
 If true, expand all_different constraints that are not permutations.
 Permutations (#Variables = #Values) are always expanded.
 
```
optional bool expand_alldiff_constraints = 170 [default = false];
Returns:

Whether the expandAlldiffConstraints field is set.
getExpandAlldiffConstraints

boolean getExpandAlldiffConstraints()
```
 If true, expand all_different constraints that are not permutations.
 Permutations (#Variables = #Values) are always expanded.
 
```
optional bool expand_alldiff_constraints = 170 [default = false];
Returns:

The expandAlldiffConstraints.
hasExpandReservoirConstraints

boolean hasExpandReservoirConstraints()
```
 If true, expand the reservoir constraints by creating booleans for all
 possible precedences between event and encoding the constraint.
 
```
optional bool expand_reservoir_constraints = 182 [default = true];
Returns:

Whether the expandReservoirConstraints field is set.
getExpandReservoirConstraints

boolean getExpandReservoirConstraints()
```
 If true, expand the reservoir constraints by creating booleans for all
 possible precedences between event and encoding the constraint.
 
```
optional bool expand_reservoir_constraints = 182 [default = true];
Returns:

The expandReservoirConstraints.
hasDisableConstraintExpansion

boolean hasDisableConstraintExpansion()
```
 If true, it disable all constraint expansion.
 This should only be used to test the presolve of expanded constraints.
 
```
optional bool disable_constraint_expansion = 181 [default = false];
Returns:

Whether the disableConstraintExpansion field is set.
getDisableConstraintExpansion

boolean getDisableConstraintExpansion()
```
 If true, it disable all constraint expansion.
 This should only be used to test the presolve of expanded constraints.
 
```
optional bool disable_constraint_expansion = 181 [default = false];
Returns:

The disableConstraintExpansion.

hasMergeNoOverlapWorkLimit

boolean hasMergeNoOverlapWorkLimit()

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

optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];

Returns:: Whether the mergeNoOverlapWorkLimit field is set.

getMergeNoOverlapWorkLimit

double getMergeNoOverlapWorkLimit()

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

optional double merge_no_overlap_work_limit = 145 [default = 1000000000000];

Returns:: The mergeNoOverlapWorkLimit.

hasMergeAtMostOneWorkLimit

boolean hasMergeAtMostOneWorkLimit()

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns:

Whether the mergeAtMostOneWorkLimit field is set.
getMergeAtMostOneWorkLimit

double getMergeAtMostOneWorkLimit()

optional double merge_at_most_one_work_limit = 146 [default = 100000000];

Returns:

The mergeAtMostOneWorkLimit.

hasPresolveSubstitutionLevel

boolean hasPresolveSubstitutionLevel()

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

optional int32 presolve_substitution_level = 147 [default = 1];

Returns:: Whether the presolveSubstitutionLevel field is set.

getPresolveSubstitutionLevel

int getPresolveSubstitutionLevel()

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

optional int32 presolve_substitution_level = 147 [default = 1];

Returns:: The presolveSubstitutionLevel.

hasPresolveExtractIntegerEnforcement

boolean hasPresolveExtractIntegerEnforcement()

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

optional bool presolve_extract_integer_enforcement = 174 [default = false];

Returns:: Whether the presolveExtractIntegerEnforcement field is set.

getPresolveExtractIntegerEnforcement

boolean getPresolveExtractIntegerEnforcement()

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

optional bool presolve_extract_integer_enforcement = 174 [default = false];

Returns:: The presolveExtractIntegerEnforcement.

hasUseOptimizationHints

boolean hasUseOptimizationHints()

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

optional bool use_optimization_hints = 35 [default = true];

Returns:: Whether the useOptimizationHints field is set.

getUseOptimizationHints

boolean getUseOptimizationHints()

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

optional bool use_optimization_hints = 35 [default = true];

Returns:: The useOptimizationHints.

hasMinimizeCore

boolean hasMinimizeCore()
```
 Whether we use a simple heuristic to try to minimize an UNSAT core.
 
```
optional bool minimize_core = 50 [default = true];
Returns:

Whether the minimizeCore field is set.
getMinimizeCore

boolean getMinimizeCore()
```
 Whether we use a simple heuristic to try to minimize an UNSAT core.
 
```
optional bool minimize_core = 50 [default = true];
Returns:

The minimizeCore.
hasFindMultipleCores

boolean hasFindMultipleCores()
```
 Whether we try to find more independent cores for a given set of
 assumptions in the core based max-SAT algorithms.
 
```
optional bool find_multiple_cores = 84 [default = true];
Returns:

Whether the findMultipleCores field is set.
getFindMultipleCores

boolean getFindMultipleCores()
```
 Whether we try to find more independent cores for a given set of
 assumptions in the core based max-SAT algorithms.
 
```
optional bool find_multiple_cores = 84 [default = true];
Returns:

The findMultipleCores.

hasCoverOptimization

boolean hasCoverOptimization()

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

optional bool cover_optimization = 89 [default = true];

Returns:: Whether the coverOptimization field is set.

getCoverOptimization

boolean getCoverOptimization()

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

optional bool cover_optimization = 89 [default = true];

Returns:: The coverOptimization.

hasMaxSatAssumptionOrder

boolean hasMaxSatAssumptionOrder()

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

Returns:

Whether the maxSatAssumptionOrder field is set.
getMaxSatAssumptionOrder

SatParameters.MaxSatAssumptionOrder getMaxSatAssumptionOrder()

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

Returns:

The maxSatAssumptionOrder.
hasMaxSatReverseAssumptionOrder

boolean hasMaxSatReverseAssumptionOrder()
```
 If true, adds the assumption in the reverse order of the one defined by
 max_sat_assumption_order.
 
```
optional bool max_sat_reverse_assumption_order = 52 [default = false];
Returns:

Whether the maxSatReverseAssumptionOrder field is set.
getMaxSatReverseAssumptionOrder

boolean getMaxSatReverseAssumptionOrder()
```
 If true, adds the assumption in the reverse order of the one defined by
 max_sat_assumption_order.
 
```
optional bool max_sat_reverse_assumption_order = 52 [default = false];
Returns:

The maxSatReverseAssumptionOrder.
hasMaxSatStratification

boolean hasMaxSatStratification()

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

Returns:

Whether the maxSatStratification field is set.
getMaxSatStratification

SatParameters.MaxSatStratificationAlgorithm getMaxSatStratification()

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

Returns:

The maxSatStratification.

hasUsePrecedencesInDisjunctiveConstraint

boolean hasUsePrecedencesInDisjunctiveConstraint()

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

optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];

Returns:: Whether the usePrecedencesInDisjunctiveConstraint field is set.

getUsePrecedencesInDisjunctiveConstraint

boolean getUsePrecedencesInDisjunctiveConstraint()

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

optional bool use_precedences_in_disjunctive_constraint = 74 [default = true];

Returns:: The usePrecedencesInDisjunctiveConstraint.

hasUseOverloadCheckerInCumulativeConstraint

boolean hasUseOverloadCheckerInCumulativeConstraint()

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

optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];

Returns:: Whether the useOverloadCheckerInCumulativeConstraint field is set.

getUseOverloadCheckerInCumulativeConstraint

boolean getUseOverloadCheckerInCumulativeConstraint()

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

optional bool use_overload_checker_in_cumulative_constraint = 78 [default = false];

Returns:: The useOverloadCheckerInCumulativeConstraint.

hasUseTimetableEdgeFindingInCumulativeConstraint

boolean hasUseTimetableEdgeFindingInCumulativeConstraint()

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

optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];

Returns:: Whether the useTimetableEdgeFindingInCumulativeConstraint field is set.

getUseTimetableEdgeFindingInCumulativeConstraint

boolean getUseTimetableEdgeFindingInCumulativeConstraint()

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

optional bool use_timetable_edge_finding_in_cumulative_constraint = 79 [default = false];

Returns:: The useTimetableEdgeFindingInCumulativeConstraint.

hasUseDisjunctiveConstraintInCumulativeConstraint

boolean hasUseDisjunctiveConstraintInCumulativeConstraint()

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

optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];

Returns:: Whether the useDisjunctiveConstraintInCumulativeConstraint field is set.

getUseDisjunctiveConstraintInCumulativeConstraint

boolean getUseDisjunctiveConstraintInCumulativeConstraint()

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

optional bool use_disjunctive_constraint_in_cumulative_constraint = 80 [default = true];

Returns:: The useDisjunctiveConstraintInCumulativeConstraint.

hasLinearizationLevel

boolean hasLinearizationLevel()

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

optional int32 linearization_level = 90 [default = 1];

Returns:: Whether the linearizationLevel field is set.

getLinearizationLevel

int getLinearizationLevel()

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

optional int32 linearization_level = 90 [default = 1];

Returns:: The linearizationLevel.

hasBooleanEncodingLevel

boolean hasBooleanEncodingLevel()
```
 A non-negative level indicating how much we should try to fully encode
 Integer variables as Boolean.
 
```
optional int32 boolean_encoding_level = 107 [default = 1];
Returns:

Whether the booleanEncodingLevel field is set.
getBooleanEncodingLevel

int getBooleanEncodingLevel()
```
 A non-negative level indicating how much we should try to fully encode
 Integer variables as Boolean.
 
```
optional int32 boolean_encoding_level = 107 [default = 1];
Returns:

The booleanEncodingLevel.

hasMaxNumCuts

boolean hasMaxNumCuts()

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

optional int32 max_num_cuts = 91 [default = 10000];

Returns:: Whether the maxNumCuts field is set.

getMaxNumCuts

int getMaxNumCuts()

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

optional int32 max_num_cuts = 91 [default = 10000];

Returns:: The maxNumCuts.

hasOnlyAddCutsAtLevelZero

boolean hasOnlyAddCutsAtLevelZero()
```
 For the cut that can be generated at any level, this control if we only
 try to generate them at the root node.
 
```
optional bool only_add_cuts_at_level_zero = 92 [default = false];
Returns:

Whether the onlyAddCutsAtLevelZero field is set.
getOnlyAddCutsAtLevelZero

boolean getOnlyAddCutsAtLevelZero()
```
 For the cut that can be generated at any level, this control if we only
 try to generate them at the root node.
 
```
optional bool only_add_cuts_at_level_zero = 92 [default = false];
Returns:

The onlyAddCutsAtLevelZero.

hasAddKnapsackCuts

boolean hasAddKnapsackCuts()

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

optional bool add_knapsack_cuts = 111 [default = false];

Returns:: Whether the addKnapsackCuts field is set.

getAddKnapsackCuts

boolean getAddKnapsackCuts()

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

optional bool add_knapsack_cuts = 111 [default = false];

Returns:: The addKnapsackCuts.

hasAddCgCuts

boolean hasAddCgCuts()
```
 Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
 Note that for now, this is not heavily tuned.
 
```
optional bool add_cg_cuts = 117 [default = true];
Returns:

Whether the addCgCuts field is set.

getAddCgCuts

boolean getAddCgCuts()

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

optional bool add_cg_cuts = 117 [default = true];

Returns:: The addCgCuts.

hasAddMirCuts

boolean hasAddMirCuts()
```
 Whether we generate MIR cuts at root node.
 Note that for now, this is not heavily tuned.
 
```
optional bool add_mir_cuts = 120 [default = true];
Returns:

Whether the addMirCuts field is set.
getAddMirCuts

boolean getAddMirCuts()
```
 Whether we generate MIR cuts at root node.
 Note that for now, this is not heavily tuned.
 
```
optional bool add_mir_cuts = 120 [default = true];
Returns:

The addMirCuts.
hasAddZeroHalfCuts

boolean hasAddZeroHalfCuts()
```
 Whether we generate Zero-Half cuts at root node.
 Note that for now, this is not heavily tuned.
 
```
optional bool add_zero_half_cuts = 169 [default = true];
Returns:

Whether the addZeroHalfCuts field is set.
getAddZeroHalfCuts

boolean getAddZeroHalfCuts()
```
 Whether we generate Zero-Half cuts at root node.
 Note that for now, this is not heavily tuned.
 
```
optional bool add_zero_half_cuts = 169 [default = true];
Returns:

The addZeroHalfCuts.

hasAddCliqueCuts

boolean hasAddCliqueCuts()

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

optional bool add_clique_cuts = 172 [default = true];

Returns:: Whether the addCliqueCuts field is set.

getAddCliqueCuts

boolean getAddCliqueCuts()

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

optional bool add_clique_cuts = 172 [default = true];

Returns:: The addCliqueCuts.

hasMaxAllDiffCutSize

boolean hasMaxAllDiffCutSize()

 Cut generator for all diffs can add too many cuts for large all_diff
 constraints. This parameter restricts the large all_diff constraints to
 have a cut generator.

optional int32 max_all_diff_cut_size = 148 [default = 7];

Returns:: Whether the maxAllDiffCutSize field is set.

getMaxAllDiffCutSize

int getMaxAllDiffCutSize()

 Cut generator for all diffs can add too many cuts for large all_diff
 constraints. This parameter restricts the large all_diff constraints to
 have a cut generator.

optional int32 max_all_diff_cut_size = 148 [default = 7];

Returns:: The maxAllDiffCutSize.

hasAddLinMaxCuts

boolean hasAddLinMaxCuts()

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

optional bool add_lin_max_cuts = 152 [default = true];

Returns:: Whether the addLinMaxCuts field is set.

getAddLinMaxCuts

boolean getAddLinMaxCuts()

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

optional bool add_lin_max_cuts = 152 [default = true];

Returns:: The addLinMaxCuts.

hasMaxIntegerRoundingScaling

boolean hasMaxIntegerRoundingScaling()

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

optional int32 max_integer_rounding_scaling = 119 [default = 600];

Returns:: Whether the maxIntegerRoundingScaling field is set.

getMaxIntegerRoundingScaling

int getMaxIntegerRoundingScaling()

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

optional int32 max_integer_rounding_scaling = 119 [default = 600];

Returns:: The maxIntegerRoundingScaling.

hasAddLpConstraintsLazily

boolean hasAddLpConstraintsLazily()

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

optional bool add_lp_constraints_lazily = 112 [default = true];

Returns:: Whether the addLpConstraintsLazily field is set.

getAddLpConstraintsLazily

boolean getAddLpConstraintsLazily()

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

optional bool add_lp_constraints_lazily = 112 [default = true];

Returns:: The addLpConstraintsLazily.

hasMinOrthogonalityForLpConstraints

boolean hasMinOrthogonalityForLpConstraints()

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

optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];

Returns:: Whether the minOrthogonalityForLpConstraints field is set.

getMinOrthogonalityForLpConstraints

double getMinOrthogonalityForLpConstraints()

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

optional double min_orthogonality_for_lp_constraints = 115 [default = 0.05];

Returns:: The minOrthogonalityForLpConstraints.

hasMaxCutRoundsAtLevelZero

boolean hasMaxCutRoundsAtLevelZero()
```
 Max number of time we perform cut generation and resolve the LP at level 0.
 
```
optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];
Returns:

Whether the maxCutRoundsAtLevelZero field is set.
getMaxCutRoundsAtLevelZero

int getMaxCutRoundsAtLevelZero()
```
 Max number of time we perform cut generation and resolve the LP at level 0.
 
```
optional int32 max_cut_rounds_at_level_zero = 154 [default = 1];
Returns:

The maxCutRoundsAtLevelZero.

hasMaxConsecutiveInactiveCount

boolean hasMaxConsecutiveInactiveCount()

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

optional int32 max_consecutive_inactive_count = 121 [default = 100];

Returns:: Whether the maxConsecutiveInactiveCount field is set.

getMaxConsecutiveInactiveCount

int getMaxConsecutiveInactiveCount()

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

optional int32 max_consecutive_inactive_count = 121 [default = 100];

Returns:: The maxConsecutiveInactiveCount.

hasCutMaxActiveCountValue

boolean hasCutMaxActiveCountValue()

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

optional double cut_max_active_count_value = 155 [default = 10000000000];

Returns:: Whether the cutMaxActiveCountValue field is set.

getCutMaxActiveCountValue

double getCutMaxActiveCountValue()

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

optional double cut_max_active_count_value = 155 [default = 10000000000];

Returns:: The cutMaxActiveCountValue.

hasCutActiveCountDecay

boolean hasCutActiveCountDecay()

optional double cut_active_count_decay = 156 [default = 0.8];

Returns:

Whether the cutActiveCountDecay field is set.
getCutActiveCountDecay

double getCutActiveCountDecay()

optional double cut_active_count_decay = 156 [default = 0.8];

Returns:

The cutActiveCountDecay.
hasCutCleanupTarget

boolean hasCutCleanupTarget()
```
 Target number of constraints to remove during cleanup.
 
```
optional int32 cut_cleanup_target = 157 [default = 1000];
Returns:

Whether the cutCleanupTarget field is set.
getCutCleanupTarget

int getCutCleanupTarget()
```
 Target number of constraints to remove during cleanup.
 
```
optional int32 cut_cleanup_target = 157 [default = 1000];
Returns:

The cutCleanupTarget.
hasNewConstraintsBatchSize

boolean hasNewConstraintsBatchSize()
```
 Add that many lazy constraints (or cuts) at once in the LP. Note that at
 the beginning of the solve, we do add more than this.
 
```
optional int32 new_constraints_batch_size = 122 [default = 50];
Returns:

Whether the newConstraintsBatchSize field is set.
getNewConstraintsBatchSize

int getNewConstraintsBatchSize()
```
 Add that many lazy constraints (or cuts) at once in the LP. Note that at
 the beginning of the solve, we do add more than this.
 
```
optional int32 new_constraints_batch_size = 122 [default = 50];
Returns:

The newConstraintsBatchSize.
hasSearchBranching

boolean hasSearchBranching()

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

Returns:

Whether the searchBranching field is set.
getSearchBranching

SatParameters.SearchBranching getSearchBranching()

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

Returns:

The searchBranching.
hasHintConflictLimit

boolean hasHintConflictLimit()
```
 Conflict limit used in the phase that exploit the solution hint.
 
```
optional int32 hint_conflict_limit = 153 [default = 10];
Returns:

Whether the hintConflictLimit field is set.
getHintConflictLimit

int getHintConflictLimit()
```
 Conflict limit used in the phase that exploit the solution hint.
 
```
optional int32 hint_conflict_limit = 153 [default = 10];
Returns:

The hintConflictLimit.

hasRepairHint

boolean hasRepairHint()

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

optional bool repair_hint = 167 [default = false];

Returns:: Whether the repairHint field is set.

getRepairHint

boolean getRepairHint()

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

optional bool repair_hint = 167 [default = false];

Returns:: The repairHint.

hasExploitIntegerLpSolution

boolean hasExploitIntegerLpSolution()

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

optional bool exploit_integer_lp_solution = 94 [default = true];

Returns:: Whether the exploitIntegerLpSolution field is set.

getExploitIntegerLpSolution

boolean getExploitIntegerLpSolution()

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

optional bool exploit_integer_lp_solution = 94 [default = true];

Returns:: The exploitIntegerLpSolution.

hasExploitAllLpSolution

boolean hasExploitAllLpSolution()

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

optional bool exploit_all_lp_solution = 116 [default = true];

Returns:: Whether the exploitAllLpSolution field is set.

getExploitAllLpSolution

boolean getExploitAllLpSolution()

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

optional bool exploit_all_lp_solution = 116 [default = true];

Returns:: The exploitAllLpSolution.

hasExploitBestSolution

boolean hasExploitBestSolution()
```
 When branching on a variable, follow the last best solution value.
 
```
optional bool exploit_best_solution = 130 [default = false];
Returns:

Whether the exploitBestSolution field is set.
getExploitBestSolution

boolean getExploitBestSolution()
```
 When branching on a variable, follow the last best solution value.
 
```
optional bool exploit_best_solution = 130 [default = false];
Returns:

The exploitBestSolution.
hasExploitRelaxationSolution

boolean hasExploitRelaxationSolution()
```
 When branching on a variable, follow the last best relaxation solution
 value. We use the relaxation with the tightest bound on the objective as
 the best relaxation solution.
 
```
optional bool exploit_relaxation_solution = 161 [default = false];
Returns:

Whether the exploitRelaxationSolution field is set.

getExploitRelaxationSolution

boolean getExploitRelaxationSolution()

 When branching on a variable, follow the last best relaxation solution
 value. We use the relaxation with the tightest bound on the objective as
 the best relaxation solution.

optional bool exploit_relaxation_solution = 161 [default = false];

Returns:: The exploitRelaxationSolution.

hasExploitObjective

boolean hasExploitObjective()
```
 When branching an a variable that directly affect the objective,
 branch on the value that lead to the best objective first.
 
```
optional bool exploit_objective = 131 [default = true];
Returns:

Whether the exploitObjective field is set.
getExploitObjective

boolean getExploitObjective()
```
 When branching an a variable that directly affect the objective,
 branch on the value that lead to the best objective first.
 
```
optional bool exploit_objective = 131 [default = true];
Returns:

The exploitObjective.

hasProbingPeriodAtRoot

boolean hasProbingPeriodAtRoot()

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

optional int64 probing_period_at_root = 142 [default = 0];

Returns:: Whether the probingPeriodAtRoot field is set.

getProbingPeriodAtRoot

long getProbingPeriodAtRoot()

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

optional int64 probing_period_at_root = 142 [default = 0];

Returns:: The probingPeriodAtRoot.

hasUseProbingSearch

boolean hasUseProbingSearch()
```
 If true, search will continuously probe Boolean variables, and integer
 variable bounds.
 
```
optional bool use_probing_search = 176 [default = false];
Returns:

Whether the useProbingSearch field is set.
getUseProbingSearch

boolean getUseProbingSearch()
```
 If true, search will continuously probe Boolean variables, and integer
 variable bounds.
 
```
optional bool use_probing_search = 176 [default = false];
Returns:

The useProbingSearch.
hasPseudoCostReliabilityThreshold

boolean hasPseudoCostReliabilityThreshold()
```
 The solver ignores the pseudo costs of variables with number of recordings
 less than this threshold.
 
```
optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
Returns:

Whether the pseudoCostReliabilityThreshold field is set.
getPseudoCostReliabilityThreshold

long getPseudoCostReliabilityThreshold()
```
 The solver ignores the pseudo costs of variables with number of recordings
 less than this threshold.
 
```
optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
Returns:

The pseudoCostReliabilityThreshold.

hasOptimizeWithCore

boolean hasOptimizeWithCore()

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

optional bool optimize_with_core = 83 [default = false];

Returns:: Whether the optimizeWithCore field is set.

getOptimizeWithCore

boolean getOptimizeWithCore()

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

optional bool optimize_with_core = 83 [default = false];

Returns:: The optimizeWithCore.

hasBinarySearchNumConflicts

boolean hasBinarySearchNumConflicts()

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

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

Returns:: Whether the binarySearchNumConflicts field is set.

getBinarySearchNumConflicts

int getBinarySearchNumConflicts()

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

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

Returns:: The binarySearchNumConflicts.

hasOptimizeWithMaxHs

boolean hasOptimizeWithMaxHs()

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

optional bool optimize_with_max_hs = 85 [default = false];

Returns:: Whether the optimizeWithMaxHs field is set.

getOptimizeWithMaxHs

boolean getOptimizeWithMaxHs()

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

optional bool optimize_with_max_hs = 85 [default = false];

Returns:: The optimizeWithMaxHs.

hasEnumerateAllSolutions

boolean hasEnumerateAllSolutions()

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

optional bool enumerate_all_solutions = 87 [default = false];

Returns:: Whether the enumerateAllSolutions field is set.

getEnumerateAllSolutions

boolean getEnumerateAllSolutions()

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

optional bool enumerate_all_solutions = 87 [default = false];

Returns:: The enumerateAllSolutions.

hasKeepAllFeasibleSolutionsInPresolve

boolean hasKeepAllFeasibleSolutionsInPresolve()

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

optional bool keep_all_feasible_solutions_in_presolve = 173 [default = false];

Returns:: Whether the keepAllFeasibleSolutionsInPresolve field is set.

getKeepAllFeasibleSolutionsInPresolve

boolean getKeepAllFeasibleSolutionsInPresolve()

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

optional bool keep_all_feasible_solutions_in_presolve = 173 [default = false];

Returns:: The keepAllFeasibleSolutionsInPresolve.

hasFillTightenedDomainsInResponse

boolean hasFillTightenedDomainsInResponse()

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

optional bool fill_tightened_domains_in_response = 132 [default = false];

Returns:: Whether the fillTightenedDomainsInResponse field is set.

getFillTightenedDomainsInResponse

boolean getFillTightenedDomainsInResponse()

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

optional bool fill_tightened_domains_in_response = 132 [default = false];

Returns:: The fillTightenedDomainsInResponse.

hasInstantiateAllVariables

boolean hasInstantiateAllVariables()
```
 If true, the solver will add a default integer branching strategy to the
 already defined search strategy.
 
```
optional bool instantiate_all_variables = 106 [default = true];
Returns:

Whether the instantiateAllVariables field is set.
getInstantiateAllVariables

boolean getInstantiateAllVariables()
```
 If true, the solver will add a default integer branching strategy to the
 already defined search strategy.
 
```
optional bool instantiate_all_variables = 106 [default = true];
Returns:

The instantiateAllVariables.

hasAutoDetectGreaterThanAtLeastOneOf

boolean hasAutoDetectGreaterThanAtLeastOneOf()

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

optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];

Returns:: Whether the autoDetectGreaterThanAtLeastOneOf field is set.

getAutoDetectGreaterThanAtLeastOneOf

boolean getAutoDetectGreaterThanAtLeastOneOf()

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

optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];

Returns:: The autoDetectGreaterThanAtLeastOneOf.

hasStopAfterFirstSolution

boolean hasStopAfterFirstSolution()
```
 For an optimization problem, stop the solver as soon as we have a solution.
 
```
optional bool stop_after_first_solution = 98 [default = false];
Returns:

Whether the stopAfterFirstSolution field is set.
getStopAfterFirstSolution

boolean getStopAfterFirstSolution()
```
 For an optimization problem, stop the solver as soon as we have a solution.
 
```
optional bool stop_after_first_solution = 98 [default = false];
Returns:

The stopAfterFirstSolution.
hasStopAfterPresolve

boolean hasStopAfterPresolve()
```
 Mainly used when improving the presolver. When true, stops the solver after
 the presolve is complete.
 
```
optional bool stop_after_presolve = 149 [default = false];
Returns:

Whether the stopAfterPresolve field is set.
getStopAfterPresolve

boolean getStopAfterPresolve()
```
 Mainly used when improving the presolver. When true, stops the solver after
 the presolve is complete.
 
```
optional bool stop_after_presolve = 149 [default = false];
Returns:

The stopAfterPresolve.

hasNumSearchWorkers

boolean hasNumSearchWorkers()

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

optional int32 num_search_workers = 100 [default = 1];

Returns:: Whether the numSearchWorkers field is set.

getNumSearchWorkers

int getNumSearchWorkers()

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

optional int32 num_search_workers = 100 [default = 1];

Returns:: The numSearchWorkers.

hasInterleaveSearch

boolean hasInterleaveSearch()

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

optional bool interleave_search = 136 [default = false];

Returns:: Whether the interleaveSearch field is set.

getInterleaveSearch

boolean getInterleaveSearch()

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

optional bool interleave_search = 136 [default = false];

Returns:: The interleaveSearch.

hasInterleaveBatchSize

boolean hasInterleaveBatchSize()

optional int32 interleave_batch_size = 134 [default = 1];

Returns:

Whether the interleaveBatchSize field is set.
getInterleaveBatchSize

int getInterleaveBatchSize()

optional int32 interleave_batch_size = 134 [default = 1];

Returns:

The interleaveBatchSize.
hasReduceMemoryUsageInInterleaveMode

boolean hasReduceMemoryUsageInInterleaveMode()
```
 Temporary parameter until the memory usage is more optimized.
 
```
optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];
Returns:

Whether the reduceMemoryUsageInInterleaveMode field is set.
getReduceMemoryUsageInInterleaveMode

boolean getReduceMemoryUsageInInterleaveMode()
```
 Temporary parameter until the memory usage is more optimized.
 
```
optional bool reduce_memory_usage_in_interleave_mode = 141 [default = false];
Returns:

The reduceMemoryUsageInInterleaveMode.
hasShareObjectiveBounds

boolean hasShareObjectiveBounds()
```
 Allows objective sharing between workers.
 
```
optional bool share_objective_bounds = 113 [default = true];
Returns:

Whether the shareObjectiveBounds field is set.
getShareObjectiveBounds

boolean getShareObjectiveBounds()
```
 Allows objective sharing between workers.
 
```
optional bool share_objective_bounds = 113 [default = true];
Returns:

The shareObjectiveBounds.
hasShareLevelZeroBounds

boolean hasShareLevelZeroBounds()
```
 Allows sharing of the bounds of modified variables at level 0.
 
```
optional bool share_level_zero_bounds = 114 [default = true];
Returns:

Whether the shareLevelZeroBounds field is set.
getShareLevelZeroBounds

boolean getShareLevelZeroBounds()
```
 Allows sharing of the bounds of modified variables at level 0.
 
```
optional bool share_level_zero_bounds = 114 [default = true];
Returns:

The shareLevelZeroBounds.
hasUseLnsOnly

boolean hasUseLnsOnly()
```
 LNS parameters.
 
```
optional bool use_lns_only = 101 [default = false];
Returns:

Whether the useLnsOnly field is set.
getUseLnsOnly

boolean getUseLnsOnly()
```
 LNS parameters.
 
```
optional bool use_lns_only = 101 [default = false];
Returns:

The useLnsOnly.
hasLnsFocusOnDecisionVariables

boolean hasLnsFocusOnDecisionVariables()

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns:

Whether the lnsFocusOnDecisionVariables field is set.
getLnsFocusOnDecisionVariables

boolean getLnsFocusOnDecisionVariables()

optional bool lns_focus_on_decision_variables = 105 [default = false];

Returns:

The lnsFocusOnDecisionVariables.
hasLnsExpandIntervalsInConstraintGraph

boolean hasLnsExpandIntervalsInConstraintGraph()

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns:

Whether the lnsExpandIntervalsInConstraintGraph field is set.
getLnsExpandIntervalsInConstraintGraph

boolean getLnsExpandIntervalsInConstraintGraph()

optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];

Returns:

The lnsExpandIntervalsInConstraintGraph.
hasUseRinsLns

boolean hasUseRinsLns()
```
 Turns on relaxation induced neighborhood generator.
 
```
optional bool use_rins_lns = 129 [default = true];
Returns:

Whether the useRinsLns field is set.
getUseRinsLns

boolean getUseRinsLns()
```
 Turns on relaxation induced neighborhood generator.
 
```
optional bool use_rins_lns = 129 [default = true];
Returns:

The useRinsLns.
hasUseFeasibilityPump

boolean hasUseFeasibilityPump()
```
 Adds a feasibility pump subsolver along with lns subsolvers.
 
```
optional bool use_feasibility_pump = 164 [default = true];
Returns:

Whether the useFeasibilityPump field is set.
getUseFeasibilityPump

boolean getUseFeasibilityPump()
```
 Adds a feasibility pump subsolver along with lns subsolvers.
 
```
optional bool use_feasibility_pump = 164 [default = true];
Returns:

The useFeasibilityPump.
hasFpRounding

boolean hasFpRounding()

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

Returns:

Whether the fpRounding field is set.
getFpRounding

SatParameters.FPRoundingMethod getFpRounding()

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

Returns:

The fpRounding.
hasUseRelaxationLns

boolean hasUseRelaxationLns()
```
 Turns on a lns worker which solves relaxed version of the original problem
 by removing constraints from the problem in order to get better bounds.
 
```
optional bool use_relaxation_lns = 150 [default = false];
Returns:

Whether the useRelaxationLns field is set.

getUseRelaxationLns

boolean getUseRelaxationLns()

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

optional bool use_relaxation_lns = 150 [default = false];

Returns:: The useRelaxationLns.

hasDiversifyLnsParams

boolean hasDiversifyLnsParams()
```
 If true, registers more lns subsolvers with different parameters.
 
```
optional bool diversify_lns_params = 137 [default = false];
Returns:

Whether the diversifyLnsParams field is set.
getDiversifyLnsParams

boolean getDiversifyLnsParams()
```
 If true, registers more lns subsolvers with different parameters.
 
```
optional bool diversify_lns_params = 137 [default = false];
Returns:

The diversifyLnsParams.
hasRandomizeSearch

boolean hasRandomizeSearch()
```
 Randomize fixed search.
 
```
optional bool randomize_search = 103 [default = false];
Returns:

Whether the randomizeSearch field is set.
getRandomizeSearch

boolean getRandomizeSearch()
```
 Randomize fixed search.
 
```
optional bool randomize_search = 103 [default = false];
Returns:

The randomizeSearch.

hasSearchRandomizationTolerance

boolean hasSearchRandomizationTolerance()

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

optional int64 search_randomization_tolerance = 104 [default = 0];

Returns:: Whether the searchRandomizationTolerance field is set.

getSearchRandomizationTolerance

long getSearchRandomizationTolerance()

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

optional int64 search_randomization_tolerance = 104 [default = 0];

Returns:: The searchRandomizationTolerance.

hasUseOptionalVariables

boolean hasUseOptionalVariables()

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

optional bool use_optional_variables = 108 [default = true];

Returns:: Whether the useOptionalVariables field is set.

getUseOptionalVariables

boolean getUseOptionalVariables()

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

optional bool use_optional_variables = 108 [default = true];

Returns:: The useOptionalVariables.

hasUseExactLpReason

boolean hasUseExactLpReason()

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

optional bool use_exact_lp_reason = 109 [default = true];

Returns:: Whether the useExactLpReason field is set.

getUseExactLpReason

boolean getUseExactLpReason()

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

optional bool use_exact_lp_reason = 109 [default = true];

Returns:: The useExactLpReason.

hasUseBranchingInLp

boolean hasUseBranchingInLp()

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

optional bool use_branching_in_lp = 139 [default = false];

Returns:: Whether the useBranchingInLp field is set.

getUseBranchingInLp

boolean getUseBranchingInLp()

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

optional bool use_branching_in_lp = 139 [default = false];

Returns:: The useBranchingInLp.

hasUseCombinedNoOverlap

boolean hasUseCombinedNoOverlap()

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

optional bool use_combined_no_overlap = 133 [default = false];

Returns:: Whether the useCombinedNoOverlap field is set.

getUseCombinedNoOverlap

boolean getUseCombinedNoOverlap()

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

optional bool use_combined_no_overlap = 133 [default = false];

Returns:: The useCombinedNoOverlap.

hasCatchSigintSignal

boolean hasCatchSigintSignal()

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

optional bool catch_sigint_signal = 135 [default = true];

Returns:: Whether the catchSigintSignal field is set.

getCatchSigintSignal

boolean getCatchSigintSignal()

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

optional bool catch_sigint_signal = 135 [default = true];

Returns:: The catchSigintSignal.

hasUseImpliedBounds

boolean hasUseImpliedBounds()

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

optional bool use_implied_bounds = 144 [default = true];

Returns:: Whether the useImpliedBounds field is set.

getUseImpliedBounds

boolean getUseImpliedBounds()

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

optional bool use_implied_bounds = 144 [default = true];

Returns:: The useImpliedBounds.

hasPolishLpSolution

boolean hasPolishLpSolution()

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

optional bool polish_lp_solution = 175 [default = false];

Returns:: Whether the polishLpSolution field is set.

getPolishLpSolution

boolean getPolishLpSolution()

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

optional bool polish_lp_solution = 175 [default = false];

Returns:: The polishLpSolution.

hasConvertIntervals

boolean hasConvertIntervals()

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

optional bool convert_intervals = 177 [default = false];

Returns:: Whether the convertIntervals field is set.

getConvertIntervals

boolean getConvertIntervals()

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

optional bool convert_intervals = 177 [default = false];

Returns:: The convertIntervals.

hasSymmetryLevel

boolean hasSymmetryLevel()

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

optional int32 symmetry_level = 183 [default = 2];

Returns:: Whether the symmetryLevel field is set.

getSymmetryLevel

int getSymmetryLevel()

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

optional int32 symmetry_level = 183 [default = 2];

Returns:: The symmetryLevel.

hasMipMaxBound

boolean hasMipMaxBound()

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

optional double mip_max_bound = 124 [default = 10000000];

Returns:: Whether the mipMaxBound field is set.

getMipMaxBound

double getMipMaxBound()

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

optional double mip_max_bound = 124 [default = 10000000];

Returns:: The mipMaxBound.

hasMipVarScaling

boolean hasMipVarScaling()

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

optional double mip_var_scaling = 125 [default = 1];

Returns:: Whether the mipVarScaling field is set.

getMipVarScaling

double getMipVarScaling()

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

optional double mip_var_scaling = 125 [default = 1];

Returns:: The mipVarScaling.

hasMipAutomaticallyScaleVariables

boolean hasMipAutomaticallyScaleVariables()

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

optional bool mip_automatically_scale_variables = 166 [default = true];

Returns:: Whether the mipAutomaticallyScaleVariables field is set.

getMipAutomaticallyScaleVariables

boolean getMipAutomaticallyScaleVariables()

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

optional bool mip_automatically_scale_variables = 166 [default = true];

Returns:: The mipAutomaticallyScaleVariables.

hasMipWantedPrecision

boolean hasMipWantedPrecision()

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

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

Returns:: Whether the mipWantedPrecision field is set.

getMipWantedPrecision

double getMipWantedPrecision()

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

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

Returns:: The mipWantedPrecision.

hasMipMaxActivityExponent

boolean hasMipMaxActivityExponent()

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

optional int32 mip_max_activity_exponent = 127 [default = 53];

Returns:: Whether the mipMaxActivityExponent field is set.

getMipMaxActivityExponent

int getMipMaxActivityExponent()

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

optional int32 mip_max_activity_exponent = 127 [default = 53];

Returns:: The mipMaxActivityExponent.

hasMipCheckPrecision

boolean hasMipCheckPrecision()

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

optional double mip_check_precision = 128 [default = 0.0001];

Returns:: Whether the mipCheckPrecision field is set.

getMipCheckPrecision

double getMipCheckPrecision()

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

optional double mip_check_precision = 128 [default = 0.0001];

Returns:: The mipCheckPrecision.

Interface SatParametersOrBuilder

Method Summary

Methods inherited from interface com.google.protobuf.MessageLiteOrBuilder

Methods inherited from interface com.google.protobuf.MessageOrBuilder

Method Details

hasName

getName

getNameBytes

hasPreferredVariableOrder

getPreferredVariableOrder

hasInitialPolarity

getInitialPolarity

hasUsePhaseSaving

getUsePhaseSaving

hasPolarityRephaseIncrement

getPolarityRephaseIncrement

hasRandomPolarityRatio

getRandomPolarityRatio

hasRandomBranchesRatio

getRandomBranchesRatio

hasUseErwaHeuristic

getUseErwaHeuristic

hasInitialVariablesActivity

getInitialVariablesActivity

hasAlsoBumpVariablesInConflictReasons

getAlsoBumpVariablesInConflictReasons

hasMinimizationAlgorithm

getMinimizationAlgorithm

hasBinaryMinimizationAlgorithm

getBinaryMinimizationAlgorithm

hasSubsumptionDuringConflictAnalysis

getSubsumptionDuringConflictAnalysis

hasClauseCleanupPeriod

getClauseCleanupPeriod

hasClauseCleanupTarget

getClauseCleanupTarget

hasClauseCleanupProtection

getClauseCleanupProtection

hasClauseCleanupLbdBound

getClauseCleanupLbdBound

hasClauseCleanupOrdering

getClauseCleanupOrdering

hasPbCleanupIncrement

getPbCleanupIncrement

hasPbCleanupRatio

getPbCleanupRatio

hasMinimizeWithPropagationRestartPeriod

getMinimizeWithPropagationRestartPeriod

hasMinimizeWithPropagationNumDecisions

getMinimizeWithPropagationNumDecisions

hasVariableActivityDecay

getVariableActivityDecay

hasMaxVariableActivityValue

getMaxVariableActivityValue

hasGlucoseMaxDecay

getGlucoseMaxDecay

hasGlucoseDecayIncrement

getGlucoseDecayIncrement

hasGlucoseDecayIncrementPeriod

getGlucoseDecayIncrementPeriod

hasClauseActivityDecay

getClauseActivityDecay

hasMaxClauseActivityValue

getMaxClauseActivityValue

getRestartAlgorithmsList

getRestartAlgorithmsCount

getRestartAlgorithms

hasDefaultRestartAlgorithms

getDefaultRestartAlgorithms

getDefaultRestartAlgorithmsBytes

hasRestartPeriod

getRestartPeriod

hasRestartRunningWindowSize

getRestartRunningWindowSize

hasRestartDlAverageRatio

getRestartDlAverageRatio

hasRestartLbdAverageRatio

getRestartLbdAverageRatio

hasUseBlockingRestart

getUseBlockingRestart