ToySolver.SAT.Config

Solver configulation

data Config

Constructors

Config

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)

Instances

Eq Config

Methods

(==) :: Config -> Config -> Bool

(/=) :: Config -> Config -> Bool

Ord Config

Methods

compare :: Config -> Config -> Ordering

(<) :: Config -> Config -> Bool

(<=) :: Config -> Config -> Bool

(>) :: Config -> Config -> Bool

(>=) :: Config -> Config -> Bool

max :: Config -> Config -> Config

min :: Config -> Config -> Config

Show Config

Methods

showsPrec :: Int -> Config -> ShowS

show :: Config -> String

showList :: [Config] -> ShowS

Default Config

Methods

def :: Config

data RestartStrategy

Restart strategy.

The default value can be obtained by def.

Constructors

MiniSATRestarts

ArminRestarts

LubyRestarts

Instances

Bounded RestartStrategy

Methods

minBound :: RestartStrategy

maxBound :: RestartStrategy

Enum RestartStrategy

Methods

succ :: RestartStrategy -> RestartStrategy

pred :: RestartStrategy -> RestartStrategy

toEnum :: Int -> RestartStrategy

fromEnum :: RestartStrategy -> Int

enumFrom :: RestartStrategy -> [RestartStrategy]

enumFromThen :: RestartStrategy -> RestartStrategy -> [RestartStrategy]

enumFromTo :: RestartStrategy -> RestartStrategy -> [RestartStrategy]

enumFromThenTo :: RestartStrategy -> RestartStrategy -> RestartStrategy -> [RestartStrategy]

Eq RestartStrategy

Methods

(==) :: RestartStrategy -> RestartStrategy -> Bool

(/=) :: RestartStrategy -> RestartStrategy -> Bool

Ord RestartStrategy

Methods

compare :: RestartStrategy -> RestartStrategy -> Ordering

(<) :: RestartStrategy -> RestartStrategy -> Bool

(<=) :: RestartStrategy -> RestartStrategy -> Bool

(>) :: RestartStrategy -> RestartStrategy -> Bool

(>=) :: RestartStrategy -> RestartStrategy -> Bool

max :: RestartStrategy -> RestartStrategy -> RestartStrategy

min :: RestartStrategy -> RestartStrategy -> RestartStrategy

Show RestartStrategy

Methods

showsPrec :: Int -> RestartStrategy -> ShowS

show :: RestartStrategy -> String

showList :: [RestartStrategy] -> ShowS

Default RestartStrategy

Methods

def :: RestartStrategy

showRestartStrategy :: RestartStrategy -> String

parseRestartStrategy :: String -> Maybe RestartStrategy

data LearningStrategy

Learning strategy.

The default value can be obtained by def.

Constructors

LearningClause

LearningHybrid

Instances

Bounded LearningStrategy

Methods

minBound :: LearningStrategy

maxBound :: LearningStrategy

Enum LearningStrategy

Methods

succ :: LearningStrategy -> LearningStrategy

pred :: LearningStrategy -> LearningStrategy

toEnum :: Int -> LearningStrategy

fromEnum :: LearningStrategy -> Int

enumFrom :: LearningStrategy -> [LearningStrategy]

enumFromThen :: LearningStrategy -> LearningStrategy -> [LearningStrategy]

enumFromTo :: LearningStrategy -> LearningStrategy -> [LearningStrategy]

enumFromThenTo :: LearningStrategy -> LearningStrategy -> LearningStrategy -> [LearningStrategy]

Eq LearningStrategy

Methods

(==) :: LearningStrategy -> LearningStrategy -> Bool

(/=) :: LearningStrategy -> LearningStrategy -> Bool

Ord LearningStrategy

Methods

compare :: LearningStrategy -> LearningStrategy -> Ordering

(<) :: LearningStrategy -> LearningStrategy -> Bool

(<=) :: LearningStrategy -> LearningStrategy -> Bool

(>) :: LearningStrategy -> LearningStrategy -> Bool

(>=) :: LearningStrategy -> LearningStrategy -> Bool

max :: LearningStrategy -> LearningStrategy -> LearningStrategy

min :: LearningStrategy -> LearningStrategy -> LearningStrategy

Show LearningStrategy

Methods

showsPrec :: Int -> LearningStrategy -> ShowS

show :: LearningStrategy -> String

showList :: [LearningStrategy] -> ShowS

Default LearningStrategy

Methods

def :: LearningStrategy

showLearningStrategy :: LearningStrategy -> String

parseLearningStrategy :: String -> Maybe LearningStrategy

data BranchingStrategy

Branching strategy.

The default value can be obtained by def.

BranchingERWA and BranchingLRB is based on [Liang et al 2016].

• J. Liang, V. Ganesh, P. Poupart, and K. Czarnecki, "Learning rate based branching heuristic for SAT solvers," in Proceedings of Theory and Applications of Satisfiability Testing (SAT 2016), pp. 123-140. http://link.springer.com/chapter/10.1007/978-3-319-40970-2_9 https://cs.uwaterloo.ca/~ppoupart/publications/sat/learning-rate-branching-heuristic-SAT.pdf

Constructors

BranchingVSIDS

VSIDS (Variable State Independent Decaying Sum) branching heuristic

BranchingERWA

ERWA (Exponential Recency Weighted Average) branching heuristic

BranchingLRB

LRB (Learning Rate Branching) heuristic

Instances

Bounded BranchingStrategy

Methods

minBound :: BranchingStrategy

maxBound :: BranchingStrategy

Enum BranchingStrategy

Methods

succ :: BranchingStrategy -> BranchingStrategy

pred :: BranchingStrategy -> BranchingStrategy

toEnum :: Int -> BranchingStrategy

fromEnum :: BranchingStrategy -> Int

enumFrom :: BranchingStrategy -> [BranchingStrategy]

enumFromThen :: BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]

enumFromTo :: BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]

enumFromThenTo :: BranchingStrategy -> BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]

Eq BranchingStrategy

Methods

(==) :: BranchingStrategy -> BranchingStrategy -> Bool

(/=) :: BranchingStrategy -> BranchingStrategy -> Bool

Ord BranchingStrategy

Methods

compare :: BranchingStrategy -> BranchingStrategy -> Ordering

(<) :: BranchingStrategy -> BranchingStrategy -> Bool

(<=) :: BranchingStrategy -> BranchingStrategy -> Bool

(>) :: BranchingStrategy -> BranchingStrategy -> Bool

(>=) :: BranchingStrategy -> BranchingStrategy -> Bool

max :: BranchingStrategy -> BranchingStrategy -> BranchingStrategy

min :: BranchingStrategy -> BranchingStrategy -> BranchingStrategy

Show BranchingStrategy

Methods

showsPrec :: Int -> BranchingStrategy -> ShowS

show :: BranchingStrategy -> String

showList :: [BranchingStrategy] -> ShowS

Default BranchingStrategy

Methods

def :: BranchingStrategy

showBranchingStrategy :: BranchingStrategy -> String

parseBranchingStrategy :: String -> Maybe BranchingStrategy

data PBHandlerType

Pseudo boolean constraint handler implimentation.

The default value can be obtained by def.

Constructors

PBHandlerTypeCounter

PBHandlerTypePueblo

Instances

Bounded PBHandlerType

Methods

minBound :: PBHandlerType

maxBound :: PBHandlerType

Enum PBHandlerType

Methods

succ :: PBHandlerType -> PBHandlerType

pred :: PBHandlerType -> PBHandlerType

toEnum :: Int -> PBHandlerType

fromEnum :: PBHandlerType -> Int

enumFrom :: PBHandlerType -> [PBHandlerType]

enumFromThen :: PBHandlerType -> PBHandlerType -> [PBHandlerType]

enumFromTo :: PBHandlerType -> PBHandlerType -> [PBHandlerType]

enumFromThenTo :: PBHandlerType -> PBHandlerType -> PBHandlerType -> [PBHandlerType]

Eq PBHandlerType

Methods

(==) :: PBHandlerType -> PBHandlerType -> Bool

(/=) :: PBHandlerType -> PBHandlerType -> Bool

Ord PBHandlerType

Methods

compare :: PBHandlerType -> PBHandlerType -> Ordering

(<) :: PBHandlerType -> PBHandlerType -> Bool

(<=) :: PBHandlerType -> PBHandlerType -> Bool

(>) :: PBHandlerType -> PBHandlerType -> Bool

(>=) :: PBHandlerType -> PBHandlerType -> Bool

max :: PBHandlerType -> PBHandlerType -> PBHandlerType

min :: PBHandlerType -> PBHandlerType -> PBHandlerType

Show PBHandlerType

Methods

showsPrec :: Int -> PBHandlerType -> ShowS

show :: PBHandlerType -> String

showList :: [PBHandlerType] -> ShowS

Default PBHandlerType

Methods

def :: PBHandlerType

showPBHandlerType :: PBHandlerType -> String

parsePBHandlerType :: String -> Maybe PBHandlerType

Deprecated

defaultRestartFirst :: Int

Deprecated: Use configRestartFirst def

default value for RestartFirst.

defaultRestartInc :: Double

Deprecated: Use configRestartInc def

default value for RestartInc.

defaultLearntSizeFirst :: Int

Deprecated: Use learntSizeFirst def

default value for LearntSizeFirst.

defaultLearntSizeInc :: Double

Deprecated: Use learntSizeInc def

default value for LearntSizeInc.

defaultCCMin :: Int

Deprecated: Use ccMin def

default value for CCMin.

defaultEnablePhaseSaving :: Bool

Deprecated: Use configEnablePhaseSaving def

defaultEnableForwardSubsumptionRemoval :: Bool

Deprecated: Use configEnableForwardSubsumptionRemoval def

defaultEnableBackwardSubsumptionRemoval :: Bool

Deprecated: Use configEnableBackwardSubsumptionRemoval def

defaultRandomFreq :: Double

Deprecated: Use configRandomFreq def

defaultPBSplitClausePart :: Bool

Deprecated: Use configEnablePBSplitClausePart def

See documentation of setPBSplitClausePart.