Container for nested types declared in the SatParameters message type. More...

Detailed Description

Container for nested types declared in the SatParameters message type.

Definition at line 16131 of file SatParameters.pb.cs.

Public Types
enum	VariableOrder { InOrder = 0 , InReverseOrder = 1 , InRandomOrder = 2 }
	Variables without activity (i.e. at the beginning of the search) will be tried in this preferred order. More...
enum	Polarity { True = 0 , False = 1 , Random = 2 }
	Specifies the initial polarity (true/false) when the solver branches on a variable. This can be modified later by the user, or the phase saving heuristic. More...
enum	ConflictMinimizationAlgorithm { None = 0 , Simple = 1 , Recursive = 2 , Experimental = 3 }
	Do we try to minimize conflicts (greedily) when creating them. More...
enum	BinaryMinizationAlgorithm { NoBinaryMinimization = 0 , BinaryMinimizationFirst = 1 , BinaryMinimizationFirstWithTransitiveReduction = 4 , BinaryMinimizationWithReachability = 2 , ExperimentalBinaryMinimization = 3 }
	Whether to expoit the binary clause to minimize learned clauses further. More...
enum	ClauseProtection { ProtectionNone = 0 , ProtectionAlways = 1 , ProtectionLbd = 2 }
	Each time a clause activity is bumped, the clause has a chance to be protected during the next cleanup phase. Note that clauses used as a reason are always protected. More...
enum	ClauseOrdering { ClauseActivity = 0 , ClauseLbd = 1 }
	The clauses that will be kept during a cleanup are the ones that come first under this order. We always keep or exclude ties together. More...
enum	RestartAlgorithm { NoRestart = 0 , LubyRestart = 1 , DlMovingAverageRestart = 2 , LbdMovingAverageRestart = 3 , FixedRestart = 4 }
	Restart algorithms. More...
enum	MaxSatAssumptionOrder { DefaultAssumptionOrder = 0 , OrderAssumptionByDepth = 1 , OrderAssumptionByWeight = 2 }
	In what order do we add the assumptions in a core-based max-sat algorithm. More...
enum	MaxSatStratificationAlgorithm { StratificationNone = 0 , StratificationDescent = 1 , StratificationAscent = 2 }
	What stratification algorithm we use in the presence of weight. More...
enum	SearchBranching { AutomaticSearch = 0 , FixedSearch = 1 , PortfolioSearch = 2 , LpSearch = 3 , PseudoCostSearch = 4 , PortfolioWithQuickRestartSearch = 5 , HintSearch = 6 , PartialFixedSearch = 7 , RandomizedSearch = 8 }
	The search branching will be used to decide how to branch on unfixed nodes. More...
enum	SharedTreeSplitStrategy { SplitStrategyAuto = 0 , SplitStrategyDiscrepancy = 1 , SplitStrategyObjectiveLb = 2 , SplitStrategyBalancedTree = 3 , SplitStrategyFirstProposal = 4 }
enum	FPRoundingMethod { NearestInteger = 0 , LockBased = 1 , ActiveLockBased = 3 , PropagationAssisted = 2 }
	Rounding method to use for feasibility pump. More...

Member Enumeration Documentation

◆ BinaryMinizationAlgorithm

enum Google.OrTools.Sat.SatParameters.Types.BinaryMinizationAlgorithm

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

Enumerator
NoBinaryMinimization
BinaryMinimizationFirst
BinaryMinimizationFirstWithTransitiveReduction
BinaryMinimizationWithReachability
ExperimentalBinaryMinimization

Definition at line 16173 of file SatParameters.pb.cs.

◆ ClauseOrdering

enum Google.OrTools.Sat.SatParameters.Types.ClauseOrdering

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

Enumerator
ClauseActivity	Order clause by decreasing activity, then by increasing LBD.
ClauseLbd	Order clause by increasing LBD, then by decreasing activity.

Definition at line 16205 of file SatParameters.pb.cs.

◆ ClauseProtection

enum Google.OrTools.Sat.SatParameters.Types.ClauseProtection

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

Enumerator
ProtectionNone	No protection.
ProtectionAlways	Protect all clauses whose activity is bumped.
ProtectionLbd	Only protect clause with a better LBD.

Definition at line 16186 of file SatParameters.pb.cs.

◆ ConflictMinimizationAlgorithm

enum Google.OrTools.Sat.SatParameters.Types.ConflictMinimizationAlgorithm

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

Enumerator
None
Simple
Recursive
Experimental

Definition at line 16163 of file SatParameters.pb.cs.

◆ FPRoundingMethod

enum Google.OrTools.Sat.SatParameters.Types.FPRoundingMethod

Rounding method to use for feasibility pump.

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

Definition at line 16366 of file SatParameters.pb.cs.

◆ MaxSatAssumptionOrder

enum Google.OrTools.Sat.SatParameters.Types.MaxSatAssumptionOrder

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

Enumerator
DefaultAssumptionOrder
OrderAssumptionByDepth
OrderAssumptionByWeight

Definition at line 16248 of file SatParameters.pb.cs.

◆ MaxSatStratificationAlgorithm

enum Google.OrTools.Sat.SatParameters.Types.MaxSatStratificationAlgorithm

What stratification algorithm we use in the presence of weight.

Enumerator
StratificationNone	No stratification of the problem.
StratificationDescent	Start with literals with the highest weight, and when SAT, add the literals with the next highest weight and so on.
StratificationAscent	Start with all literals. Each time a core is found with a given minimum weight, do not consider literals with a lower weight for the next core computation. If the subproblem is SAT, do like in STRATIFICATION_DESCENT and just add the literals with the next highest weight.

Definition at line 16257 of file SatParameters.pb.cs.

◆ Polarity

enum Google.OrTools.Sat.SatParameters.Types.Polarity

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

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

Enumerator
True
False
Random

Definition at line 16154 of file SatParameters.pb.cs.

◆ RestartAlgorithm

enum Google.OrTools.Sat.SatParameters.Types.RestartAlgorithm

Restart algorithms.

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

Enumerator
NoRestart
LubyRestart	Just follow a Luby sequence times restart_period.
DlMovingAverageRestart	Moving average restart based on the decision level of conflicts.
LbdMovingAverageRestart	Moving average restart based on the LBD of conflicts.
FixedRestart	Fixed period restart every restart period.

Definition at line 16225 of file SatParameters.pb.cs.

◆ SearchBranching

enum Google.OrTools.Sat.SatParameters.Types.SearchBranching

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

Enumerator
AutomaticSearch	Try to fix all literals using the underlying SAT solver's heuristics, then generate and fix literals until integer variables are fixed. New literals on integer variables are generated using the fixed search specified by the user or our default one.
FixedSearch	If used then all decisions taken by the solver are made using a fixed order as specified in the API or in the CpModelProto search_strategy field.
PortfolioSearch	Simple portfolio search used by LNS workers.
LpSearch	If used, the solver will use heuristics from the LP relaxation. This exploit the reduced costs of the variables in the relaxation.
PseudoCostSearch	If used, the solver uses the pseudo costs for branching. Pseudo costs are computed using the historical change in objective bounds when some decision are taken. Note that this works whether we use an LP or not.
PortfolioWithQuickRestartSearch	Mainly exposed here for testing. This quickly tries a lot of randomized heuristics with a low conflict limit. It usually provides a good first solution.
HintSearch	Mainly used internally. This is like FIXED_SEARCH, except we follow the solution_hint field of the CpModelProto rather than using the information provided in the search_strategy.
PartialFixedSearch	Similar to FIXED_SEARCH, but differ in how the variable not listed into the fixed search heuristics are branched on. This will always start the search tree according to the specified fixed search strategy, but will complete it using the default automatic search.
RandomizedSearch	Randomized search. Used to increase entropy in the search.

Definition at line 16279 of file SatParameters.pb.cs.

◆ SharedTreeSplitStrategy

enum Google.OrTools.Sat.SatParameters.Types.SharedTreeSplitStrategy

Enumerator
SplitStrategyAuto	Uses the default strategy, currently equivalent to SPLIT_STRATEGY_DISCREPANCY.
SplitStrategyDiscrepancy	Only accept splits if the node to be split's depth+discrepancy is minimal for the desired number of leaves. The preferred child for discrepancy calculation is the one with the lowest objective lower bound or the original branch direction if the bounds are equal. This rule allows twice as many workers to work in the preferred subtree as non-preferred.
SplitStrategyObjectiveLb	Only split nodes with an objective lb equal to the global lb. If there is no objective, this is equivalent to SPLIT_STRATEGY_FIRST_PROPOSAL.
SplitStrategyBalancedTree	Attempt to keep the shared tree balanced.
SplitStrategyFirstProposal	Workers race to split their subtree, the winner's proposal is accepted.

Definition at line 16333 of file SatParameters.pb.cs.

◆ VariableOrder

enum Google.OrTools.Sat.SatParameters.Types.VariableOrder

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

Enumerator
InOrder	As specified by the problem.
InReverseOrder
InRandomOrder

Definition at line 16136 of file SatParameters.pb.cs.

The documentation for this class was generated from the following file:

build/dotnet/Google.OrTools/ortools/sat/SatParameters.pb.cs