SatParameters.Builder |
SatParameters.Builder.addAllRestartAlgorithms(java.lang.Iterable<? extends SatParameters.RestartAlgorithm> values) |
The restart strategies will change each time the strategy_counter is
increased.
|
SatParameters.Builder |
SatParameters.Builder.addRepeatedField(com.google.protobuf.Descriptors.FieldDescriptor field,
java.lang.Object value) |
|
SatParameters.Builder |
SatParameters.Builder.addRestartAlgorithms(SatParameters.RestartAlgorithm value) |
The restart strategies will change each time the strategy_counter is
increased.
|
SatParameters.Builder |
SatParameters.Builder.clear() |
|
SatParameters.Builder |
SatParameters.Builder.clearAbsoluteGapLimit() |
Stop the search when the gap between the best feasible objective (O) and
our best objective bound (B) is smaller than a limit.
|
SatParameters.Builder |
SatParameters.Builder.clearAddCgCuts() |
Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
|
SatParameters.Builder |
SatParameters.Builder.clearAddCliqueCuts() |
Whether we generate clique cuts from the binary implication graph.
|
SatParameters.Builder |
SatParameters.Builder.clearAddKnapsackCuts() |
Whether we generate knapsack cuts.
|
SatParameters.Builder |
SatParameters.Builder.clearAddLinMaxCuts() |
For the lin max constraints, generates the cuts described in "Strong
mixed-integer programming formulations for trained neural networks" by Ross
Anderson et.
|
SatParameters.Builder |
SatParameters.Builder.clearAddLpConstraintsLazily() |
If true, we start by an empty LP, and only add constraints not satisfied
by the current LP solution batch by batch.
|
SatParameters.Builder |
SatParameters.Builder.clearAddMirCuts() |
Whether we generate MIR cuts at root node.
|
SatParameters.Builder |
SatParameters.Builder.clearAddZeroHalfCuts() |
Whether we generate Zero-Half cuts at root node.
|
SatParameters.Builder |
SatParameters.Builder.clearAlsoBumpVariablesInConflictReasons() |
When this is true, then the variables that appear in any of the reason of
the variables in a conflict have their activity bumped.
|
SatParameters.Builder |
SatParameters.Builder.clearAutoDetectGreaterThanAtLeastOneOf() |
If true, then the precedences propagator try to detect for each variable if
it has a set of "optional incoming arc" for which at least one of them is
present.
|
SatParameters.Builder |
SatParameters.Builder.clearBinaryMinimizationAlgorithm() |
optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];
|
SatParameters.Builder |
SatParameters.Builder.clearBinarySearchNumConflicts() |
If non-negative, perform a binary search on the objective variable in order
to find an [min, max] interval outside of which the solver proved unsat/sat
under this amount of conflict.
|
SatParameters.Builder |
SatParameters.Builder.clearBlockingRestartMultiplier() |
optional double blocking_restart_multiplier = 66 [default = 1.4];
|
SatParameters.Builder |
SatParameters.Builder.clearBlockingRestartWindowSize() |
optional int32 blocking_restart_window_size = 65 [default = 5000];
|
SatParameters.Builder |
SatParameters.Builder.clearBooleanEncodingLevel() |
A non-negative level indicating how much we should try to fully encode
Integer variables as Boolean.
|
SatParameters.Builder |
SatParameters.Builder.clearCatchSigintSignal() |
Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals
when calling solve.
|
SatParameters.Builder |
SatParameters.Builder.clearClauseActivityDecay() |
Clause activity parameters (same effect as the one on the variables).
|
SatParameters.Builder |
SatParameters.Builder.clearClauseCleanupLbdBound() |
All the clauses with a LBD (literal blocks distance) lower or equal to this
parameters will always be kept.
|
SatParameters.Builder |
SatParameters.Builder.clearClauseCleanupOrdering() |
optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];
|
SatParameters.Builder |
SatParameters.Builder.clearClauseCleanupPeriod() |
Trigger a cleanup when this number of "deletable" clauses is learned.
|
SatParameters.Builder |
SatParameters.Builder.clearClauseCleanupProtection() |
optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];
|
SatParameters.Builder |
SatParameters.Builder.clearClauseCleanupTarget() |
During a cleanup, we will always keep that number of "deletable" clauses.
|
SatParameters.Builder |
SatParameters.Builder.clearConvertIntervals() |
Temporary flag util the feature is more mature.
|
SatParameters.Builder |
SatParameters.Builder.clearCountAssumptionLevelsInLbd() |
Whether or not the assumption levels are taken into account during the LBD
computation.
|
SatParameters.Builder |
SatParameters.Builder.clearCoverOptimization() |
If true, when the max-sat algo find a core, we compute the minimal number
of literals in the core that needs to be true to have a feasible solution.
|
SatParameters.Builder |
SatParameters.Builder.clearCpModelMaxNumPresolveOperations() |
If positive, try to stop just after that many presolve rules have been
applied.
|
SatParameters.Builder |
SatParameters.Builder.clearCpModelPostsolveWithFullSolver() |
Advanced usage.
|
SatParameters.Builder |
SatParameters.Builder.clearCpModelPresolve() |
Whether we presolve the cp_model before solving it.
|
SatParameters.Builder |
SatParameters.Builder.clearCpModelProbingLevel() |
How much effort do we spend on probing.
|
SatParameters.Builder |
SatParameters.Builder.clearCpModelUseSatPresolve() |
Whether we also use the sat presolve when cp_model_presolve is true.
|
SatParameters.Builder |
SatParameters.Builder.clearCutActiveCountDecay() |
optional double cut_active_count_decay = 156 [default = 0.8];
|
SatParameters.Builder |
SatParameters.Builder.clearCutCleanupTarget() |
Target number of constraints to remove during cleanup.
|
SatParameters.Builder |
SatParameters.Builder.clearCutMaxActiveCountValue() |
These parameters are similar to sat clause management activity parameters.
|
SatParameters.Builder |
SatParameters.Builder.clearDefaultRestartAlgorithms() |
optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
|
SatParameters.Builder |
SatParameters.Builder.clearDisableConstraintExpansion() |
If true, it disable all constraint expansion.
|
SatParameters.Builder |
SatParameters.Builder.clearDiversifyLnsParams() |
If true, registers more lns subsolvers with different parameters.
|
SatParameters.Builder |
SatParameters.Builder.clearEnumerateAllSolutions() |
Whether we enumerate all solutions of a problem without objective.
|
SatParameters.Builder |
SatParameters.Builder.clearExpandAlldiffConstraints() |
If true, expand all_different constraints that are not permutations.
|
SatParameters.Builder |
SatParameters.Builder.clearExpandAutomatonConstraints() |
If true, the automaton constraints are expanded.
|
SatParameters.Builder |
SatParameters.Builder.clearExpandElementConstraints() |
If true, the element constraints are expanded into many
linear constraints of the form (index == i) => (element[i] == target).
|
SatParameters.Builder |
SatParameters.Builder.clearExpandReservoirConstraints() |
If true, expand the reservoir constraints by creating booleans for all
possible precedences between event and encoding the constraint.
|
SatParameters.Builder |
SatParameters.Builder.clearExpandTableConstraints() |
If true, the positive table constraints are expanded.
|
SatParameters.Builder |
SatParameters.Builder.clearExploitAllLpSolution() |
If true and the Lp relaxation of the problem has a solution, try to exploit
it.
|
SatParameters.Builder |
SatParameters.Builder.clearExploitBestSolution() |
When branching on a variable, follow the last best solution value.
|
SatParameters.Builder |
SatParameters.Builder.clearExploitIntegerLpSolution() |
If true and the Lp relaxation of the problem has an integer optimal
solution, try to exploit it.
|
SatParameters.Builder |
SatParameters.Builder.clearExploitObjective() |
When branching an a variable that directly affect the objective,
branch on the value that lead to the best objective first.
|
SatParameters.Builder |
SatParameters.Builder.clearExploitRelaxationSolution() |
When branching on a variable, follow the last best relaxation solution
value.
|
SatParameters.Builder |
SatParameters.Builder.clearField(com.google.protobuf.Descriptors.FieldDescriptor field) |
|
SatParameters.Builder |
SatParameters.Builder.clearFillTightenedDomainsInResponse() |
If true, add information about the derived variable domains to the
CpSolverResponse.
|
SatParameters.Builder |
SatParameters.Builder.clearFindMultipleCores() |
Whether we try to find more independent cores for a given set of
assumptions in the core based max-SAT algorithms.
|
SatParameters.Builder |
SatParameters.Builder.clearFpRounding() |
optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];
|
SatParameters.Builder |
SatParameters.Builder.clearGlucoseDecayIncrement() |
optional double glucose_decay_increment = 23 [default = 0.01];
|
SatParameters.Builder |
SatParameters.Builder.clearGlucoseDecayIncrementPeriod() |
optional int32 glucose_decay_increment_period = 24 [default = 5000];
|
SatParameters.Builder |
SatParameters.Builder.clearGlucoseMaxDecay() |
The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until
0.95.
|
SatParameters.Builder |
SatParameters.Builder.clearHintConflictLimit() |
Conflict limit used in the phase that exploit the solution hint.
|
SatParameters.Builder |
SatParameters.Builder.clearInitialPolarity() |
optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];
|
SatParameters.Builder |
SatParameters.Builder.clearInitialVariablesActivity() |
The initial value of the variables activity.
|
SatParameters.Builder |
SatParameters.Builder.clearInstantiateAllVariables() |
If true, the solver will add a default integer branching strategy to the
already defined search strategy.
|
SatParameters.Builder |
SatParameters.Builder.clearInterleaveBatchSize() |
optional int32 interleave_batch_size = 134 [default = 1];
|
SatParameters.Builder |
SatParameters.Builder.clearInterleaveSearch() |
Experimental.
|
SatParameters.Builder |
SatParameters.Builder.clearKeepAllFeasibleSolutionsInPresolve() |
If true, we disable the presolve reductions that remove feasible solutions
from the search space.
|
SatParameters.Builder |
SatParameters.Builder.clearLinearizationLevel() |
A non-negative level indicating the type of constraints we consider in the
LP relaxation.
|
SatParameters.Builder |
SatParameters.Builder.clearLnsExpandIntervalsInConstraintGraph() |
optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];
|
SatParameters.Builder |
SatParameters.Builder.clearLnsFocusOnDecisionVariables() |
optional bool lns_focus_on_decision_variables = 105 [default = false];
|
SatParameters.Builder |
SatParameters.Builder.clearLogPrefix() |
Add a prefix to all logs.
|
SatParameters.Builder |
SatParameters.Builder.clearLogSearchProgress() |
Whether the solver should log the search progress.
|
SatParameters.Builder |
SatParameters.Builder.clearLogToResponse() |
Log to response proto.
|
SatParameters.Builder |
SatParameters.Builder.clearLogToStdout() |
Log to stdout.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxAllDiffCutSize() |
Cut generator for all diffs can add too many cuts for large all_diff
constraints.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxClauseActivityValue() |
optional double max_clause_activity_value = 18 [default = 1e+20];
|
SatParameters.Builder |
SatParameters.Builder.clearMaxConsecutiveInactiveCount() |
If a constraint/cut in LP is not active for that many consecutive OPTIMAL
solves, remove it from the LP.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxCutRoundsAtLevelZero() |
Max number of time we perform cut generation and resolve the LP at level 0.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxDeterministicTime() |
Maximum time allowed in deterministic time to solve a problem.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxIntegerRoundingScaling() |
In the integer rounding procedure used for MIR and Gomory cut, the maximum
"scaling" we use (must be positive).
|
SatParameters.Builder |
SatParameters.Builder.clearMaxMemoryInMb() |
Maximum memory allowed for the whole thread containing the solver.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxNumberOfConflicts() |
Maximum number of conflicts allowed to solve a problem.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxNumCuts() |
The limit on the number of cuts in our cut pool.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxPresolveIterations() |
In case of large reduction in a presolve iteration, we perform multiple
presolve iterations.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxSatAssumptionOrder() |
optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];
|
SatParameters.Builder |
SatParameters.Builder.clearMaxSatReverseAssumptionOrder() |
If true, adds the assumption in the reverse order of the one defined by
max_sat_assumption_order.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxSatStratification() |
optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];
|
SatParameters.Builder |
SatParameters.Builder.clearMaxTimeInSeconds() |
Maximum time allowed in seconds to solve a problem.
|
SatParameters.Builder |
SatParameters.Builder.clearMaxVariableActivityValue() |
optional double max_variable_activity_value = 16 [default = 1e+100];
|
SatParameters.Builder |
SatParameters.Builder.clearMergeAtMostOneWorkLimit() |
optional double merge_at_most_one_work_limit = 146 [default = 100000000];
|
SatParameters.Builder |
SatParameters.Builder.clearMergeNoOverlapWorkLimit() |
During presolve, we use a maximum clique heuristic to merge together
no-overlap constraints or at most one constraints.
|
SatParameters.Builder |
SatParameters.Builder.clearMinimizationAlgorithm() |
optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];
|
SatParameters.Builder |
SatParameters.Builder.clearMinimizeCore() |
Whether we use a simple heuristic to try to minimize an UNSAT core.
|
SatParameters.Builder |
SatParameters.Builder.clearMinimizeReductionDuringPbResolution() |
A different algorithm during PB resolution.
|
SatParameters.Builder |
SatParameters.Builder.clearMinimizeWithPropagationNumDecisions() |
optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];
|
SatParameters.Builder |
SatParameters.Builder.clearMinimizeWithPropagationRestartPeriod() |
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.
|
SatParameters.Builder |
SatParameters.Builder.clearMinOrthogonalityForLpConstraints() |
While adding constraints, skip the constraints which have orthogonality
less than 'min_orthogonality_for_lp_constraints' with already added
constraints during current call.
|
SatParameters.Builder |
SatParameters.Builder.clearMipAutomaticallyScaleVariables() |
If true, some continuous variable might be automatially scaled.
|
SatParameters.Builder |
SatParameters.Builder.clearMipCheckPrecision() |
As explained in mip_precision and mip_max_activity_exponent, we cannot
always reach the wanted precision during scaling.
|
SatParameters.Builder |
SatParameters.Builder.clearMipMaxActivityExponent() |
To avoid integer overflow, we always force the maximum possible constraint
activity (and objective value) according to the initial variable domain to
be smaller than 2 to this given power.
|
SatParameters.Builder |
SatParameters.Builder.clearMipMaxBound() |
We need to bound the maximum magnitude of the variables for CP-SAT, and
that is the bound we use.
|
SatParameters.Builder |
SatParameters.Builder.clearMipVarScaling() |
All continuous variable of the problem will be multiplied by this factor.
|
SatParameters.Builder |
SatParameters.Builder.clearMipWantedPrecision() |
When scaling constraint with double coefficients to integer coefficients,
we will multiply by a power of 2 and round the coefficients.
|
SatParameters.Builder |
SatParameters.Builder.clearName() |
In some context, like in a portfolio of search, it makes sense to name a
given parameters set for logging purpose.
|
SatParameters.Builder |
SatParameters.Builder.clearNewConstraintsBatchSize() |
Add that many lazy constraints (or cuts) at once in the LP.
|
SatParameters.Builder |
SatParameters.Builder.clearNumConflictsBeforeStrategyChanges() |
After each restart, if the number of conflict since the last strategy
change is greater that this, then we increment a "strategy_counter" that
can be use to change the search strategy used by the following restarts.
|
SatParameters.Builder |
SatParameters.Builder.clearNumSearchWorkers() |
Specify the number of parallel workers to use during search.
|
SatParameters.Builder |
SatParameters.Builder.clearOneof(com.google.protobuf.Descriptors.OneofDescriptor oneof) |
|
SatParameters.Builder |
SatParameters.Builder.clearOnlyAddCutsAtLevelZero() |
For the cut that can be generated at any level, this control if we only
try to generate them at the root node.
|
SatParameters.Builder |
SatParameters.Builder.clearOptimizeWithCore() |
The default optimization method is a simple "linear scan", each time trying
to find a better solution than the previous one.
|
SatParameters.Builder |
SatParameters.Builder.clearOptimizeWithMaxHs() |
This has no effect if optimize_with_core is false.
|
SatParameters.Builder |
SatParameters.Builder.clearPbCleanupIncrement() |
Same as for the clauses, but for the learned pseudo-Boolean constraints.
|
SatParameters.Builder |
SatParameters.Builder.clearPbCleanupRatio() |
optional double pb_cleanup_ratio = 47 [default = 0.5];
|
SatParameters.Builder |
SatParameters.Builder.clearPermutePresolveConstraintOrder() |
optional bool permute_presolve_constraint_order = 179 [default = false];
|
SatParameters.Builder |
SatParameters.Builder.clearPermuteVariableRandomly() |
This is mainly here to test the solver variability.
|
SatParameters.Builder |
SatParameters.Builder.clearPolarityRephaseIncrement() |
If non-zero, then we change the polarity heuristic after that many number
of conflicts in an arithmetically increasing fashion.
|
SatParameters.Builder |
SatParameters.Builder.clearPolishLpSolution() |
Whether we try to do a few degenerate iteration at the end of an LP solve
to minimize the fractionality of the integer variable in the basis.
|
SatParameters.Builder |
SatParameters.Builder.clearPreferredVariableOrder() |
optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
|
SatParameters.Builder |
SatParameters.Builder.clearPresolveBlockedClause() |
Whether we use an heuristic to detect some basic case of blocked clause
in the SAT presolve.
|
SatParameters.Builder |
SatParameters.Builder.clearPresolveBvaThreshold() |
Apply Bounded Variable Addition (BVA) if the number of clauses is reduced
by stricly more than this threshold.
|
SatParameters.Builder |
SatParameters.Builder.clearPresolveBveClauseWeight() |
During presolve, we apply BVE only if this weight times the number of
clauses plus the number of clause literals is not increased.
|
SatParameters.Builder |
SatParameters.Builder.clearPresolveBveThreshold() |
During presolve, only try to perform the bounded variable elimination (BVE)
of a variable x if the number of occurrences of x times the number of
occurrences of not(x) is not greater than this parameter.
|
SatParameters.Builder |
SatParameters.Builder.clearPresolveExtractIntegerEnforcement() |
If true, we will extract from linear constraints, enforcement literals of
the form "integer variable at bound => simplified constraint".
|
SatParameters.Builder |
SatParameters.Builder.clearPresolveProbingDeterministicTimeLimit() |
The maximum "deterministic" time limit to spend in probing.
|
SatParameters.Builder |
SatParameters.Builder.clearPresolveSubstitutionLevel() |
How much substitution (also called free variable aggregation in MIP
litterature) should we perform at presolve.
|
SatParameters.Builder |
SatParameters.Builder.clearPresolveUseBva() |
Whether or not we use Bounded Variable Addition (BVA) in the presolve.
|
SatParameters.Builder |
SatParameters.Builder.clearProbingPeriodAtRoot() |
If set at zero (the default), it is disabled.
|
SatParameters.Builder |
SatParameters.Builder.clearPseudoCostReliabilityThreshold() |
The solver ignores the pseudo costs of variables with number of recordings
less than this threshold.
|
SatParameters.Builder |
SatParameters.Builder.clearRandomBranchesRatio() |
A number between 0 and 1 that indicates the proportion of branching
variables that are selected randomly instead of choosing the first variable
from the given variable_ordering strategy.
|
SatParameters.Builder |
SatParameters.Builder.clearRandomizeSearch() |
Randomize fixed search.
|
SatParameters.Builder |
SatParameters.Builder.clearRandomPolarityRatio() |
The proportion of polarity chosen at random.
|
SatParameters.Builder |
SatParameters.Builder.clearRandomSeed() |
At the beginning of each solve, the random number generator used in some
part of the solver is reinitialized to this seed.
|
SatParameters.Builder |
SatParameters.Builder.clearReduceMemoryUsageInInterleaveMode() |
Temporary parameter until the memory usage is more optimized.
|
SatParameters.Builder |
SatParameters.Builder.clearRelativeGapLimit() |
optional double relative_gap_limit = 160 [default = 0];
|
SatParameters.Builder |
SatParameters.Builder.clearRepairHint() |
If true, the solver tries to repair the solution given in the hint.
|
SatParameters.Builder |
SatParameters.Builder.clearRestartAlgorithms() |
The restart strategies will change each time the strategy_counter is
increased.
|
SatParameters.Builder |
SatParameters.Builder.clearRestartDlAverageRatio() |
In the moving average restart algorithms, a restart is triggered if the
window average times this ratio is greater that the global average.
|
SatParameters.Builder |
SatParameters.Builder.clearRestartLbdAverageRatio() |
optional double restart_lbd_average_ratio = 71 [default = 1];
|
SatParameters.Builder |
SatParameters.Builder.clearRestartPeriod() |
Restart period for the FIXED_RESTART strategy.
|
SatParameters.Builder |
SatParameters.Builder.clearRestartRunningWindowSize() |
Size of the window for the moving average restarts.
|
SatParameters.Builder |
SatParameters.Builder.clearSearchBranching() |
optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
|
SatParameters.Builder |
SatParameters.Builder.clearSearchRandomizationTolerance() |
Search randomization will collect equivalent 'max valued' variables, and
pick one randomly.
|
SatParameters.Builder |
SatParameters.Builder.clearShareLevelZeroBounds() |
Allows sharing of the bounds of modified variables at level 0.
|
SatParameters.Builder |
SatParameters.Builder.clearShareObjectiveBounds() |
Allows objective sharing between workers.
|
SatParameters.Builder |
SatParameters.Builder.clearStopAfterFirstSolution() |
For an optimization problem, stop the solver as soon as we have a solution.
|
SatParameters.Builder |
SatParameters.Builder.clearStopAfterPresolve() |
Mainly used when improving the presolver.
|
SatParameters.Builder |
SatParameters.Builder.clearStrategyChangeIncreaseRatio() |
The parameter num_conflicts_before_strategy_changes is increased by that
much after each strategy change.
|
SatParameters.Builder |
SatParameters.Builder.clearSubsumptionDuringConflictAnalysis() |
At a really low cost, during the 1-UIP conflict computation, it is easy to
detect if some of the involved reasons are subsumed by the current
conflict.
|
SatParameters.Builder |
SatParameters.Builder.clearSymmetryLevel() |
Whether we try to automatically detect the symmetries in a model and
exploit them.
|
SatParameters.Builder |
SatParameters.Builder.clearTreatBinaryClausesSeparately() |
If true, the binary clauses are treated separately from the others.
|
SatParameters.Builder |
SatParameters.Builder.clearUseAbslRandom() |
optional bool use_absl_random = 180 [default = false];
|
SatParameters.Builder |
SatParameters.Builder.clearUseBlockingRestart() |
Block a moving restart algorithm if the trail size of the current conflict
is greater than the multiplier times the moving average of the trail size
at the previous conflicts.
|
SatParameters.Builder |
SatParameters.Builder.clearUseBranchingInLp() |
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.
|
SatParameters.Builder |
SatParameters.Builder.clearUseCombinedNoOverlap() |
This can be beneficial if there is a lot of no-overlap constraints but a
relatively low number of different intervals in the problem.
|
SatParameters.Builder |
SatParameters.Builder.clearUseDisjunctiveConstraintInCumulativeConstraint() |
When this is true, the cumulative constraint is reinforced with propagators
from the disjunctive constraint to improve the inference on a set of tasks
that are disjunctive at the root of the problem.
|
SatParameters.Builder |
SatParameters.Builder.clearUseErwaHeuristic() |
Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as
described in "Learning Rate Based Branching Heuristic for SAT solvers",
J.H.Liang, V.
|
SatParameters.Builder |
SatParameters.Builder.clearUseExactLpReason() |
The solver usually exploit the LP relaxation of a model.
|
SatParameters.Builder |
SatParameters.Builder.clearUseFeasibilityPump() |
Adds a feasibility pump subsolver along with lns subsolvers.
|
SatParameters.Builder |
SatParameters.Builder.clearUseImpliedBounds() |
Stores and exploits "implied-bounds" in the solver.
|
SatParameters.Builder |
SatParameters.Builder.clearUseLnsOnly() |
LNS parameters.
|
SatParameters.Builder |
SatParameters.Builder.clearUseOptimizationHints() |
For an optimization problem, whether we follow some hints in order to find
a better first solution.
|
SatParameters.Builder |
SatParameters.Builder.clearUseOptionalVariables() |
If true, we automatically detect variables whose constraint are always
enforced by the same literal and we mark them as optional.
|
SatParameters.Builder |
SatParameters.Builder.clearUseOverloadCheckerInCumulativeConstraint() |
When this is true, the cumulative constraint is reinforced with overload
checking, i.e., an additional level of reasoning based on energy.
|
SatParameters.Builder |
SatParameters.Builder.clearUsePbResolution() |
Whether to use pseudo-Boolean resolution to analyze a conflict.
|
SatParameters.Builder |
SatParameters.Builder.clearUsePhaseSaving() |
If this is true, then the polarity of a variable will be the last value it
was assigned to, or its default polarity if it was never assigned since the
call to ResetDecisionHeuristic().
|
SatParameters.Builder |
SatParameters.Builder.clearUsePrecedencesInDisjunctiveConstraint() |
When this is true, then a disjunctive constraint will try to use the
precedence relations between time intervals to propagate their bounds
further.
|
SatParameters.Builder |
SatParameters.Builder.clearUseProbingSearch() |
If true, search will continuously probe Boolean variables, and integer
variable bounds.
|
SatParameters.Builder |
SatParameters.Builder.clearUseRelaxationLns() |
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.
|
SatParameters.Builder |
SatParameters.Builder.clearUseRinsLns() |
Turns on relaxation induced neighborhood generator.
|
SatParameters.Builder |
SatParameters.Builder.clearUseSatInprocessing() |
optional bool use_sat_inprocessing = 163 [default = false];
|
SatParameters.Builder |
SatParameters.Builder.clearUseTimetableEdgeFindingInCumulativeConstraint() |
When this is true, the cumulative constraint is reinforced with timetable
edge finding, i.e., an additional level of reasoning based on the
conjunction of energy and mandatory parts.
|
SatParameters.Builder |
SatParameters.Builder.clearVariableActivityDecay() |
Each time a conflict is found, the activities of some variables are
increased by one.
|
SatParameters.Builder |
SatParameters.Builder.clone() |
|
SatParameters.Builder |
CpSolver.getParameters() |
Returns the builder of the parameters of the SAT solver for modification.
|
SatParameters.Builder |
SatParameters.Builder.mergeFrom(SatParameters other) |
|
SatParameters.Builder |
SatParameters.Builder.mergeFrom(com.google.protobuf.CodedInputStream input,
com.google.protobuf.ExtensionRegistryLite extensionRegistry) |
|
SatParameters.Builder |
SatParameters.Builder.mergeFrom(com.google.protobuf.Message other) |
|
SatParameters.Builder |
SatParameters.Builder.mergeUnknownFields(com.google.protobuf.UnknownFieldSet unknownFields) |
|
static SatParameters.Builder |
SatParameters.newBuilder() |
|
static SatParameters.Builder |
SatParameters.newBuilder(SatParameters prototype) |
|
SatParameters.Builder |
SatParameters.newBuilderForType() |
|
protected SatParameters.Builder |
SatParameters.newBuilderForType(com.google.protobuf.GeneratedMessageV3.BuilderParent parent) |
|
SatParameters.Builder |
SatParameters.Builder.setAbsoluteGapLimit(double value) |
Stop the search when the gap between the best feasible objective (O) and
our best objective bound (B) is smaller than a limit.
|
SatParameters.Builder |
SatParameters.Builder.setAddCgCuts(boolean value) |
Whether we generate and add Chvatal-Gomory cuts to the LP at root node.
|
SatParameters.Builder |
SatParameters.Builder.setAddCliqueCuts(boolean value) |
Whether we generate clique cuts from the binary implication graph.
|
SatParameters.Builder |
SatParameters.Builder.setAddKnapsackCuts(boolean value) |
Whether we generate knapsack cuts.
|
SatParameters.Builder |
SatParameters.Builder.setAddLinMaxCuts(boolean value) |
For the lin max constraints, generates the cuts described in "Strong
mixed-integer programming formulations for trained neural networks" by Ross
Anderson et.
|
SatParameters.Builder |
SatParameters.Builder.setAddLpConstraintsLazily(boolean value) |
If true, we start by an empty LP, and only add constraints not satisfied
by the current LP solution batch by batch.
|
SatParameters.Builder |
SatParameters.Builder.setAddMirCuts(boolean value) |
Whether we generate MIR cuts at root node.
|
SatParameters.Builder |
SatParameters.Builder.setAddZeroHalfCuts(boolean value) |
Whether we generate Zero-Half cuts at root node.
|
SatParameters.Builder |
SatParameters.Builder.setAlsoBumpVariablesInConflictReasons(boolean value) |
When this is true, then the variables that appear in any of the reason of
the variables in a conflict have their activity bumped.
|
SatParameters.Builder |
SatParameters.Builder.setAutoDetectGreaterThanAtLeastOneOf(boolean value) |
If true, then the precedences propagator try to detect for each variable if
it has a set of "optional incoming arc" for which at least one of them is
present.
|
SatParameters.Builder |
SatParameters.Builder.setBinaryMinimizationAlgorithm(SatParameters.BinaryMinizationAlgorithm value) |
optional .operations_research.sat.SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34 [default = BINARY_MINIMIZATION_FIRST];
|
SatParameters.Builder |
SatParameters.Builder.setBinarySearchNumConflicts(int value) |
If non-negative, perform a binary search on the objective variable in order
to find an [min, max] interval outside of which the solver proved unsat/sat
under this amount of conflict.
|
SatParameters.Builder |
SatParameters.Builder.setBlockingRestartMultiplier(double value) |
optional double blocking_restart_multiplier = 66 [default = 1.4];
|
SatParameters.Builder |
SatParameters.Builder.setBlockingRestartWindowSize(int value) |
optional int32 blocking_restart_window_size = 65 [default = 5000];
|
SatParameters.Builder |
SatParameters.Builder.setBooleanEncodingLevel(int value) |
A non-negative level indicating how much we should try to fully encode
Integer variables as Boolean.
|
SatParameters.Builder |
SatParameters.Builder.setCatchSigintSignal(boolean value) |
Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals
when calling solve.
|
SatParameters.Builder |
SatParameters.Builder.setClauseActivityDecay(double value) |
Clause activity parameters (same effect as the one on the variables).
|
SatParameters.Builder |
SatParameters.Builder.setClauseCleanupLbdBound(int value) |
All the clauses with a LBD (literal blocks distance) lower or equal to this
parameters will always be kept.
|
SatParameters.Builder |
SatParameters.Builder.setClauseCleanupOrdering(SatParameters.ClauseOrdering value) |
optional .operations_research.sat.SatParameters.ClauseOrdering clause_cleanup_ordering = 60 [default = CLAUSE_ACTIVITY];
|
SatParameters.Builder |
SatParameters.Builder.setClauseCleanupPeriod(int value) |
Trigger a cleanup when this number of "deletable" clauses is learned.
|
SatParameters.Builder |
SatParameters.Builder.setClauseCleanupProtection(SatParameters.ClauseProtection value) |
optional .operations_research.sat.SatParameters.ClauseProtection clause_cleanup_protection = 58 [default = PROTECTION_NONE];
|
SatParameters.Builder |
SatParameters.Builder.setClauseCleanupTarget(int value) |
During a cleanup, we will always keep that number of "deletable" clauses.
|
SatParameters.Builder |
SatParameters.Builder.setConvertIntervals(boolean value) |
Temporary flag util the feature is more mature.
|
SatParameters.Builder |
SatParameters.Builder.setCountAssumptionLevelsInLbd(boolean value) |
Whether or not the assumption levels are taken into account during the LBD
computation.
|
SatParameters.Builder |
SatParameters.Builder.setCoverOptimization(boolean value) |
If true, when the max-sat algo find a core, we compute the minimal number
of literals in the core that needs to be true to have a feasible solution.
|
SatParameters.Builder |
SatParameters.Builder.setCpModelMaxNumPresolveOperations(int value) |
If positive, try to stop just after that many presolve rules have been
applied.
|
SatParameters.Builder |
SatParameters.Builder.setCpModelPostsolveWithFullSolver(boolean value) |
Advanced usage.
|
SatParameters.Builder |
SatParameters.Builder.setCpModelPresolve(boolean value) |
Whether we presolve the cp_model before solving it.
|
SatParameters.Builder |
SatParameters.Builder.setCpModelProbingLevel(int value) |
How much effort do we spend on probing.
|
SatParameters.Builder |
SatParameters.Builder.setCpModelUseSatPresolve(boolean value) |
Whether we also use the sat presolve when cp_model_presolve is true.
|
SatParameters.Builder |
SatParameters.Builder.setCutActiveCountDecay(double value) |
optional double cut_active_count_decay = 156 [default = 0.8];
|
SatParameters.Builder |
SatParameters.Builder.setCutCleanupTarget(int value) |
Target number of constraints to remove during cleanup.
|
SatParameters.Builder |
SatParameters.Builder.setCutMaxActiveCountValue(double value) |
These parameters are similar to sat clause management activity parameters.
|
SatParameters.Builder |
SatParameters.Builder.setDefaultRestartAlgorithms(java.lang.String value) |
optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
|
SatParameters.Builder |
SatParameters.Builder.setDefaultRestartAlgorithmsBytes(com.google.protobuf.ByteString value) |
optional string default_restart_algorithms = 70 [default = "LUBY_RESTART,LBD_MOVING_AVERAGE_RESTART,DL_MOVING_AVERAGE_RESTART"];
|
SatParameters.Builder |
SatParameters.Builder.setDisableConstraintExpansion(boolean value) |
If true, it disable all constraint expansion.
|
SatParameters.Builder |
SatParameters.Builder.setDiversifyLnsParams(boolean value) |
If true, registers more lns subsolvers with different parameters.
|
SatParameters.Builder |
SatParameters.Builder.setEnumerateAllSolutions(boolean value) |
Whether we enumerate all solutions of a problem without objective.
|
SatParameters.Builder |
SatParameters.Builder.setExpandAlldiffConstraints(boolean value) |
If true, expand all_different constraints that are not permutations.
|
SatParameters.Builder |
SatParameters.Builder.setExpandAutomatonConstraints(boolean value) |
If true, the automaton constraints are expanded.
|
SatParameters.Builder |
SatParameters.Builder.setExpandElementConstraints(boolean value) |
If true, the element constraints are expanded into many
linear constraints of the form (index == i) => (element[i] == target).
|
SatParameters.Builder |
SatParameters.Builder.setExpandReservoirConstraints(boolean value) |
If true, expand the reservoir constraints by creating booleans for all
possible precedences between event and encoding the constraint.
|
SatParameters.Builder |
SatParameters.Builder.setExpandTableConstraints(boolean value) |
If true, the positive table constraints are expanded.
|
SatParameters.Builder |
SatParameters.Builder.setExploitAllLpSolution(boolean value) |
If true and the Lp relaxation of the problem has a solution, try to exploit
it.
|
SatParameters.Builder |
SatParameters.Builder.setExploitBestSolution(boolean value) |
When branching on a variable, follow the last best solution value.
|
SatParameters.Builder |
SatParameters.Builder.setExploitIntegerLpSolution(boolean value) |
If true and the Lp relaxation of the problem has an integer optimal
solution, try to exploit it.
|
SatParameters.Builder |
SatParameters.Builder.setExploitObjective(boolean value) |
When branching an a variable that directly affect the objective,
branch on the value that lead to the best objective first.
|
SatParameters.Builder |
SatParameters.Builder.setExploitRelaxationSolution(boolean value) |
When branching on a variable, follow the last best relaxation solution
value.
|
SatParameters.Builder |
SatParameters.Builder.setField(com.google.protobuf.Descriptors.FieldDescriptor field,
java.lang.Object value) |
|
SatParameters.Builder |
SatParameters.Builder.setFillTightenedDomainsInResponse(boolean value) |
If true, add information about the derived variable domains to the
CpSolverResponse.
|
SatParameters.Builder |
SatParameters.Builder.setFindMultipleCores(boolean value) |
Whether we try to find more independent cores for a given set of
assumptions in the core based max-SAT algorithms.
|
SatParameters.Builder |
SatParameters.Builder.setFpRounding(SatParameters.FPRoundingMethod value) |
optional .operations_research.sat.SatParameters.FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];
|
SatParameters.Builder |
SatParameters.Builder.setGlucoseDecayIncrement(double value) |
optional double glucose_decay_increment = 23 [default = 0.01];
|
SatParameters.Builder |
SatParameters.Builder.setGlucoseDecayIncrementPeriod(int value) |
optional int32 glucose_decay_increment_period = 24 [default = 5000];
|
SatParameters.Builder |
SatParameters.Builder.setGlucoseMaxDecay(double value) |
The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until
0.95.
|
SatParameters.Builder |
SatParameters.Builder.setHintConflictLimit(int value) |
Conflict limit used in the phase that exploit the solution hint.
|
SatParameters.Builder |
SatParameters.Builder.setInitialPolarity(SatParameters.Polarity value) |
optional .operations_research.sat.SatParameters.Polarity initial_polarity = 2 [default = POLARITY_FALSE];
|
SatParameters.Builder |
SatParameters.Builder.setInitialVariablesActivity(double value) |
The initial value of the variables activity.
|
SatParameters.Builder |
SatParameters.Builder.setInstantiateAllVariables(boolean value) |
If true, the solver will add a default integer branching strategy to the
already defined search strategy.
|
SatParameters.Builder |
SatParameters.Builder.setInterleaveBatchSize(int value) |
optional int32 interleave_batch_size = 134 [default = 1];
|
SatParameters.Builder |
SatParameters.Builder.setInterleaveSearch(boolean value) |
Experimental.
|
SatParameters.Builder |
SatParameters.Builder.setKeepAllFeasibleSolutionsInPresolve(boolean value) |
If true, we disable the presolve reductions that remove feasible solutions
from the search space.
|
SatParameters.Builder |
SatParameters.Builder.setLinearizationLevel(int value) |
A non-negative level indicating the type of constraints we consider in the
LP relaxation.
|
SatParameters.Builder |
SatParameters.Builder.setLnsExpandIntervalsInConstraintGraph(boolean value) |
optional bool lns_expand_intervals_in_constraint_graph = 184 [default = true];
|
SatParameters.Builder |
SatParameters.Builder.setLnsFocusOnDecisionVariables(boolean value) |
optional bool lns_focus_on_decision_variables = 105 [default = false];
|
SatParameters.Builder |
SatParameters.Builder.setLogPrefix(java.lang.String value) |
Add a prefix to all logs.
|
SatParameters.Builder |
SatParameters.Builder.setLogPrefixBytes(com.google.protobuf.ByteString value) |
Add a prefix to all logs.
|
SatParameters.Builder |
SatParameters.Builder.setLogSearchProgress(boolean value) |
Whether the solver should log the search progress.
|
SatParameters.Builder |
SatParameters.Builder.setLogToResponse(boolean value) |
Log to response proto.
|
SatParameters.Builder |
SatParameters.Builder.setLogToStdout(boolean value) |
Log to stdout.
|
SatParameters.Builder |
SatParameters.Builder.setMaxAllDiffCutSize(int value) |
Cut generator for all diffs can add too many cuts for large all_diff
constraints.
|
SatParameters.Builder |
SatParameters.Builder.setMaxClauseActivityValue(double value) |
optional double max_clause_activity_value = 18 [default = 1e+20];
|
SatParameters.Builder |
SatParameters.Builder.setMaxConsecutiveInactiveCount(int value) |
If a constraint/cut in LP is not active for that many consecutive OPTIMAL
solves, remove it from the LP.
|
SatParameters.Builder |
SatParameters.Builder.setMaxCutRoundsAtLevelZero(int value) |
Max number of time we perform cut generation and resolve the LP at level 0.
|
SatParameters.Builder |
SatParameters.Builder.setMaxDeterministicTime(double value) |
Maximum time allowed in deterministic time to solve a problem.
|
SatParameters.Builder |
SatParameters.Builder.setMaxIntegerRoundingScaling(int value) |
In the integer rounding procedure used for MIR and Gomory cut, the maximum
"scaling" we use (must be positive).
|
SatParameters.Builder |
SatParameters.Builder.setMaxMemoryInMb(long value) |
Maximum memory allowed for the whole thread containing the solver.
|
SatParameters.Builder |
SatParameters.Builder.setMaxNumberOfConflicts(long value) |
Maximum number of conflicts allowed to solve a problem.
|
SatParameters.Builder |
SatParameters.Builder.setMaxNumCuts(int value) |
The limit on the number of cuts in our cut pool.
|
SatParameters.Builder |
SatParameters.Builder.setMaxPresolveIterations(int value) |
In case of large reduction in a presolve iteration, we perform multiple
presolve iterations.
|
SatParameters.Builder |
SatParameters.Builder.setMaxSatAssumptionOrder(SatParameters.MaxSatAssumptionOrder value) |
optional .operations_research.sat.SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51 [default = DEFAULT_ASSUMPTION_ORDER];
|
SatParameters.Builder |
SatParameters.Builder.setMaxSatReverseAssumptionOrder(boolean value) |
If true, adds the assumption in the reverse order of the one defined by
max_sat_assumption_order.
|
SatParameters.Builder |
SatParameters.Builder.setMaxSatStratification(SatParameters.MaxSatStratificationAlgorithm value) |
optional .operations_research.sat.SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53 [default = STRATIFICATION_DESCENT];
|
SatParameters.Builder |
SatParameters.Builder.setMaxTimeInSeconds(double value) |
Maximum time allowed in seconds to solve a problem.
|
SatParameters.Builder |
SatParameters.Builder.setMaxVariableActivityValue(double value) |
optional double max_variable_activity_value = 16 [default = 1e+100];
|
SatParameters.Builder |
SatParameters.Builder.setMergeAtMostOneWorkLimit(double value) |
optional double merge_at_most_one_work_limit = 146 [default = 100000000];
|
SatParameters.Builder |
SatParameters.Builder.setMergeNoOverlapWorkLimit(double value) |
During presolve, we use a maximum clique heuristic to merge together
no-overlap constraints or at most one constraints.
|
SatParameters.Builder |
SatParameters.Builder.setMinimizationAlgorithm(SatParameters.ConflictMinimizationAlgorithm value) |
optional .operations_research.sat.SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE];
|
SatParameters.Builder |
SatParameters.Builder.setMinimizeCore(boolean value) |
Whether we use a simple heuristic to try to minimize an UNSAT core.
|
SatParameters.Builder |
SatParameters.Builder.setMinimizeReductionDuringPbResolution(boolean value) |
A different algorithm during PB resolution.
|
SatParameters.Builder |
SatParameters.Builder.setMinimizeWithPropagationNumDecisions(int value) |
optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];
|
SatParameters.Builder |
SatParameters.Builder.setMinimizeWithPropagationRestartPeriod(int value) |
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.
|
SatParameters.Builder |
SatParameters.Builder.setMinOrthogonalityForLpConstraints(double value) |
While adding constraints, skip the constraints which have orthogonality
less than 'min_orthogonality_for_lp_constraints' with already added
constraints during current call.
|
SatParameters.Builder |
SatParameters.Builder.setMipAutomaticallyScaleVariables(boolean value) |
If true, some continuous variable might be automatially scaled.
|
SatParameters.Builder |
SatParameters.Builder.setMipCheckPrecision(double value) |
As explained in mip_precision and mip_max_activity_exponent, we cannot
always reach the wanted precision during scaling.
|
SatParameters.Builder |
SatParameters.Builder.setMipMaxActivityExponent(int value) |
To avoid integer overflow, we always force the maximum possible constraint
activity (and objective value) according to the initial variable domain to
be smaller than 2 to this given power.
|
SatParameters.Builder |
SatParameters.Builder.setMipMaxBound(double value) |
We need to bound the maximum magnitude of the variables for CP-SAT, and
that is the bound we use.
|
SatParameters.Builder |
SatParameters.Builder.setMipVarScaling(double value) |
All continuous variable of the problem will be multiplied by this factor.
|
SatParameters.Builder |
SatParameters.Builder.setMipWantedPrecision(double value) |
When scaling constraint with double coefficients to integer coefficients,
we will multiply by a power of 2 and round the coefficients.
|
SatParameters.Builder |
SatParameters.Builder.setName(java.lang.String value) |
In some context, like in a portfolio of search, it makes sense to name a
given parameters set for logging purpose.
|
SatParameters.Builder |
SatParameters.Builder.setNameBytes(com.google.protobuf.ByteString value) |
In some context, like in a portfolio of search, it makes sense to name a
given parameters set for logging purpose.
|
SatParameters.Builder |
SatParameters.Builder.setNewConstraintsBatchSize(int value) |
Add that many lazy constraints (or cuts) at once in the LP.
|
SatParameters.Builder |
SatParameters.Builder.setNumConflictsBeforeStrategyChanges(int value) |
After each restart, if the number of conflict since the last strategy
change is greater that this, then we increment a "strategy_counter" that
can be use to change the search strategy used by the following restarts.
|
SatParameters.Builder |
SatParameters.Builder.setNumSearchWorkers(int value) |
Specify the number of parallel workers to use during search.
|
SatParameters.Builder |
SatParameters.Builder.setOnlyAddCutsAtLevelZero(boolean value) |
For the cut that can be generated at any level, this control if we only
try to generate them at the root node.
|
SatParameters.Builder |
SatParameters.Builder.setOptimizeWithCore(boolean value) |
The default optimization method is a simple "linear scan", each time trying
to find a better solution than the previous one.
|
SatParameters.Builder |
SatParameters.Builder.setOptimizeWithMaxHs(boolean value) |
This has no effect if optimize_with_core is false.
|
SatParameters.Builder |
SatParameters.Builder.setPbCleanupIncrement(int value) |
Same as for the clauses, but for the learned pseudo-Boolean constraints.
|
SatParameters.Builder |
SatParameters.Builder.setPbCleanupRatio(double value) |
optional double pb_cleanup_ratio = 47 [default = 0.5];
|
SatParameters.Builder |
SatParameters.Builder.setPermutePresolveConstraintOrder(boolean value) |
optional bool permute_presolve_constraint_order = 179 [default = false];
|
SatParameters.Builder |
SatParameters.Builder.setPermuteVariableRandomly(boolean value) |
This is mainly here to test the solver variability.
|
SatParameters.Builder |
SatParameters.Builder.setPolarityRephaseIncrement(int value) |
If non-zero, then we change the polarity heuristic after that many number
of conflicts in an arithmetically increasing fashion.
|
SatParameters.Builder |
SatParameters.Builder.setPolishLpSolution(boolean value) |
Whether we try to do a few degenerate iteration at the end of an LP solve
to minimize the fractionality of the integer variable in the basis.
|
SatParameters.Builder |
SatParameters.Builder.setPreferredVariableOrder(SatParameters.VariableOrder value) |
optional .operations_research.sat.SatParameters.VariableOrder preferred_variable_order = 1 [default = IN_ORDER];
|
SatParameters.Builder |
SatParameters.Builder.setPresolveBlockedClause(boolean value) |
Whether we use an heuristic to detect some basic case of blocked clause
in the SAT presolve.
|
SatParameters.Builder |
SatParameters.Builder.setPresolveBvaThreshold(int value) |
Apply Bounded Variable Addition (BVA) if the number of clauses is reduced
by stricly more than this threshold.
|
SatParameters.Builder |
SatParameters.Builder.setPresolveBveClauseWeight(int value) |
During presolve, we apply BVE only if this weight times the number of
clauses plus the number of clause literals is not increased.
|
SatParameters.Builder |
SatParameters.Builder.setPresolveBveThreshold(int value) |
During presolve, only try to perform the bounded variable elimination (BVE)
of a variable x if the number of occurrences of x times the number of
occurrences of not(x) is not greater than this parameter.
|
SatParameters.Builder |
SatParameters.Builder.setPresolveExtractIntegerEnforcement(boolean value) |
If true, we will extract from linear constraints, enforcement literals of
the form "integer variable at bound => simplified constraint".
|
SatParameters.Builder |
SatParameters.Builder.setPresolveProbingDeterministicTimeLimit(double value) |
The maximum "deterministic" time limit to spend in probing.
|
SatParameters.Builder |
SatParameters.Builder.setPresolveSubstitutionLevel(int value) |
How much substitution (also called free variable aggregation in MIP
litterature) should we perform at presolve.
|
SatParameters.Builder |
SatParameters.Builder.setPresolveUseBva(boolean value) |
Whether or not we use Bounded Variable Addition (BVA) in the presolve.
|
SatParameters.Builder |
SatParameters.Builder.setProbingPeriodAtRoot(long value) |
If set at zero (the default), it is disabled.
|
SatParameters.Builder |
SatParameters.Builder.setPseudoCostReliabilityThreshold(long value) |
The solver ignores the pseudo costs of variables with number of recordings
less than this threshold.
|
SatParameters.Builder |
SatParameters.Builder.setRandomBranchesRatio(double value) |
A number between 0 and 1 that indicates the proportion of branching
variables that are selected randomly instead of choosing the first variable
from the given variable_ordering strategy.
|
SatParameters.Builder |
SatParameters.Builder.setRandomizeSearch(boolean value) |
Randomize fixed search.
|
SatParameters.Builder |
SatParameters.Builder.setRandomPolarityRatio(double value) |
The proportion of polarity chosen at random.
|
SatParameters.Builder |
SatParameters.Builder.setRandomSeed(int value) |
At the beginning of each solve, the random number generator used in some
part of the solver is reinitialized to this seed.
|
SatParameters.Builder |
SatParameters.Builder.setReduceMemoryUsageInInterleaveMode(boolean value) |
Temporary parameter until the memory usage is more optimized.
|
SatParameters.Builder |
SatParameters.Builder.setRelativeGapLimit(double value) |
optional double relative_gap_limit = 160 [default = 0];
|
SatParameters.Builder |
SatParameters.Builder.setRepairHint(boolean value) |
If true, the solver tries to repair the solution given in the hint.
|
SatParameters.Builder |
SatParameters.Builder.setRepeatedField(com.google.protobuf.Descriptors.FieldDescriptor field,
int index,
java.lang.Object value) |
|
SatParameters.Builder |
SatParameters.Builder.setRestartAlgorithms(int index,
SatParameters.RestartAlgorithm value) |
The restart strategies will change each time the strategy_counter is
increased.
|
SatParameters.Builder |
SatParameters.Builder.setRestartDlAverageRatio(double value) |
In the moving average restart algorithms, a restart is triggered if the
window average times this ratio is greater that the global average.
|
SatParameters.Builder |
SatParameters.Builder.setRestartLbdAverageRatio(double value) |
optional double restart_lbd_average_ratio = 71 [default = 1];
|
SatParameters.Builder |
SatParameters.Builder.setRestartPeriod(int value) |
Restart period for the FIXED_RESTART strategy.
|
SatParameters.Builder |
SatParameters.Builder.setRestartRunningWindowSize(int value) |
Size of the window for the moving average restarts.
|
SatParameters.Builder |
SatParameters.Builder.setSearchBranching(SatParameters.SearchBranching value) |
optional .operations_research.sat.SatParameters.SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
|
SatParameters.Builder |
SatParameters.Builder.setSearchRandomizationTolerance(long value) |
Search randomization will collect equivalent 'max valued' variables, and
pick one randomly.
|
SatParameters.Builder |
SatParameters.Builder.setShareLevelZeroBounds(boolean value) |
Allows sharing of the bounds of modified variables at level 0.
|
SatParameters.Builder |
SatParameters.Builder.setShareObjectiveBounds(boolean value) |
Allows objective sharing between workers.
|
SatParameters.Builder |
SatParameters.Builder.setStopAfterFirstSolution(boolean value) |
For an optimization problem, stop the solver as soon as we have a solution.
|
SatParameters.Builder |
SatParameters.Builder.setStopAfterPresolve(boolean value) |
Mainly used when improving the presolver.
|
SatParameters.Builder |
SatParameters.Builder.setStrategyChangeIncreaseRatio(double value) |
The parameter num_conflicts_before_strategy_changes is increased by that
much after each strategy change.
|
SatParameters.Builder |
SatParameters.Builder.setSubsumptionDuringConflictAnalysis(boolean value) |
At a really low cost, during the 1-UIP conflict computation, it is easy to
detect if some of the involved reasons are subsumed by the current
conflict.
|
SatParameters.Builder |
SatParameters.Builder.setSymmetryLevel(int value) |
Whether we try to automatically detect the symmetries in a model and
exploit them.
|
SatParameters.Builder |
SatParameters.Builder.setTreatBinaryClausesSeparately(boolean value) |
If true, the binary clauses are treated separately from the others.
|
SatParameters.Builder |
SatParameters.Builder.setUnknownFields(com.google.protobuf.UnknownFieldSet unknownFields) |
|
SatParameters.Builder |
SatParameters.Builder.setUseAbslRandom(boolean value) |
optional bool use_absl_random = 180 [default = false];
|
SatParameters.Builder |
SatParameters.Builder.setUseBlockingRestart(boolean value) |
Block a moving restart algorithm if the trail size of the current conflict
is greater than the multiplier times the moving average of the trail size
at the previous conflicts.
|
SatParameters.Builder |
SatParameters.Builder.setUseBranchingInLp(boolean value) |
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.
|
SatParameters.Builder |
SatParameters.Builder.setUseCombinedNoOverlap(boolean value) |
This can be beneficial if there is a lot of no-overlap constraints but a
relatively low number of different intervals in the problem.
|
SatParameters.Builder |
SatParameters.Builder.setUseDisjunctiveConstraintInCumulativeConstraint(boolean value) |
When this is true, the cumulative constraint is reinforced with propagators
from the disjunctive constraint to improve the inference on a set of tasks
that are disjunctive at the root of the problem.
|
SatParameters.Builder |
SatParameters.Builder.setUseErwaHeuristic(boolean value) |
Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as
described in "Learning Rate Based Branching Heuristic for SAT solvers",
J.H.Liang, V.
|
SatParameters.Builder |
SatParameters.Builder.setUseExactLpReason(boolean value) |
The solver usually exploit the LP relaxation of a model.
|
SatParameters.Builder |
SatParameters.Builder.setUseFeasibilityPump(boolean value) |
Adds a feasibility pump subsolver along with lns subsolvers.
|
SatParameters.Builder |
SatParameters.Builder.setUseImpliedBounds(boolean value) |
Stores and exploits "implied-bounds" in the solver.
|
SatParameters.Builder |
SatParameters.Builder.setUseLnsOnly(boolean value) |
LNS parameters.
|
SatParameters.Builder |
SatParameters.Builder.setUseOptimizationHints(boolean value) |
For an optimization problem, whether we follow some hints in order to find
a better first solution.
|
SatParameters.Builder |
SatParameters.Builder.setUseOptionalVariables(boolean value) |
If true, we automatically detect variables whose constraint are always
enforced by the same literal and we mark them as optional.
|
SatParameters.Builder |
SatParameters.Builder.setUseOverloadCheckerInCumulativeConstraint(boolean value) |
When this is true, the cumulative constraint is reinforced with overload
checking, i.e., an additional level of reasoning based on energy.
|
SatParameters.Builder |
SatParameters.Builder.setUsePbResolution(boolean value) |
Whether to use pseudo-Boolean resolution to analyze a conflict.
|
SatParameters.Builder |
SatParameters.Builder.setUsePhaseSaving(boolean value) |
If this is true, then the polarity of a variable will be the last value it
was assigned to, or its default polarity if it was never assigned since the
call to ResetDecisionHeuristic().
|
SatParameters.Builder |
SatParameters.Builder.setUsePrecedencesInDisjunctiveConstraint(boolean value) |
When this is true, then a disjunctive constraint will try to use the
precedence relations between time intervals to propagate their bounds
further.
|
SatParameters.Builder |
SatParameters.Builder.setUseProbingSearch(boolean value) |
If true, search will continuously probe Boolean variables, and integer
variable bounds.
|
SatParameters.Builder |
SatParameters.Builder.setUseRelaxationLns(boolean value) |
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.
|
SatParameters.Builder |
SatParameters.Builder.setUseRinsLns(boolean value) |
Turns on relaxation induced neighborhood generator.
|
SatParameters.Builder |
SatParameters.Builder.setUseSatInprocessing(boolean value) |
optional bool use_sat_inprocessing = 163 [default = false];
|
SatParameters.Builder |
SatParameters.Builder.setUseTimetableEdgeFindingInCumulativeConstraint(boolean value) |
When this is true, the cumulative constraint is reinforced with timetable
edge finding, i.e., an additional level of reasoning based on the
conjunction of energy and mandatory parts.
|
SatParameters.Builder |
SatParameters.Builder.setVariableActivityDecay(double value) |
Each time a conflict is found, the activities of some variables are
increased by one.
|
SatParameters.Builder |
SatParameters.toBuilder() |
|