Solver configulation

Fields

• configRestartStrategy :: !RestartStrategy
   
• configRestartFirst :: !Int

  The initial restart limit. (default 100) Zero and negative values are used to disable restart.

• configRestartInc :: !Double

  The factor with which the restart limit is multiplied in each restart. (default 1.5) This must be >1.

• configLearningStrategy :: !LearningStrategy
   
• configLearntSizeFirst :: !Int

  The initial limit for learnt constraints. Negative value means computing default value from problem instance.

• configLearntSizeInc :: !Double

  The limit for learnt constraints is multiplied with this factor periodically. (default 1.1) This must be >1.

• configCCMin :: !Int

  Controls conflict constraint minimization (0=none, 1=local, 2=recursive)

• configBranchingStrategy :: !BranchingStrategy
   
• configERWAStepSizeFirst :: !Double

  step-size α in ERWA and LRB branching heuristic is initialized with this value. (default 0.4)

• configERWAStepSizeDec :: !Double

  step-size α in ERWA and LRB branching heuristic is decreased by this value after each conflict. (default 0.06)

• configERWAStepSizeMin :: !Double

  step-size α in ERWA and LRB branching heuristic is decreased until it reach the value. (default 0.06)

• configEMADecay :: !Double

  inverse of the variable EMA decay factor used by LRB branching heuristic. (default 1 / 0.95)

• configEnablePhaseSaving :: !Bool
   
• configEnableForwardSubsumptionRemoval :: !Bool
   
• configEnableBackwardSubsumptionRemoval :: !Bool
   
• configRandomFreq :: !Double

  The frequency with which the decision heuristic tries to choose a random variable

• configPBHandlerType :: !PBHandlerType
   
• configEnablePBSplitClausePart :: !Bool

  Split PB-constraints into a PB part and a clause part.

  Example from minisat+ paper:

  • 4 x1 + 4 x2 + 4 x3 + 4 x4 + 2y1 + y2 + y3 ≥ 4

  would be split into

  • x1 + x2 + x3 + x4 + ¬z ≥ 1 (clause part)
  • 2 y1 + y2 + y3 + 4 z ≥ 4 (PB part)

  where z is a newly introduced variable, not present in any other constraint.

  Reference:

  • N . Eéen and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.
• configCheckModel :: !Bool
   
• configVarDecay :: !Double

  Inverse of the variable activity decay factor. (default 1 / 0.95)

• configConstrDecay :: !Double

  Inverse of the constraint activity decay factor. (1 / 0.999)