Google OR-Tools v9.9
a fast and portable software suite for combinatorial optimization
|
Container for nested types declared in the SatParameters message type. More...
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... | |
Container for nested types declared in the SatParameters message type.
Definition at line 13669 of file SatParameters.pb.cs.
Whether to expoit the binary clause to minimize learned clauses further.
Enumerator | |
---|---|
NoBinaryMinimization | |
BinaryMinimizationFirst | |
BinaryMinimizationFirstWithTransitiveReduction | |
BinaryMinimizationWithReachability | |
ExperimentalBinaryMinimization |
Definition at line 13711 of file SatParameters.pb.cs.
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 13743 of file SatParameters.pb.cs.
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 13724 of file SatParameters.pb.cs.
Do we try to minimize conflicts (greedily) when creating them.
Enumerator | |
---|---|
None | |
Simple | |
Recursive | |
Experimental |
Definition at line 13701 of file SatParameters.pb.cs.
Rounding method to use for feasibility pump.
Definition at line 13903 of file SatParameters.pb.cs.
In what order do we add the assumptions in a core-based max-sat algorithm.
Enumerator | |
---|---|
DefaultAssumptionOrder | |
OrderAssumptionByDepth | |
OrderAssumptionByWeight |
Definition at line 13786 of file SatParameters.pb.cs.
What stratification algorithm we use in the presence of weight.
Definition at line 13795 of file SatParameters.pb.cs.
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 13692 of file SatParameters.pb.cs.
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
Definition at line 13763 of file SatParameters.pb.cs.
The search branching will be used to decide how to branch on unfixed nodes.
Definition at line 13817 of file SatParameters.pb.cs.
Definition at line 13871 of file SatParameters.pb.cs.
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 13674 of file SatParameters.pb.cs.