ToySolver.SAT.Solver.CDCL.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

Show Config

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

showsPrec :: Int -> Config -> ShowS

show :: Config -> String

showList :: [Config] -> ShowS

Default Config

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

def :: Config

Eq Config

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

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

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

Ord Config

Defined in ToySolver.SAT.Solver.CDCL.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

data RestartStrategy

Restart strategy.

The default value can be obtained by def.

Constructors

MiniSATRestarts

ArminRestarts

LubyRestarts

Instances

Bounded RestartStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

minBound :: RestartStrategy

maxBound :: RestartStrategy

Enum RestartStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

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]

Show RestartStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

showsPrec :: Int -> RestartStrategy -> ShowS

show :: RestartStrategy -> String

showList :: [RestartStrategy] -> ShowS

Default RestartStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

def :: RestartStrategy

Eq RestartStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

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

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

Ord RestartStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

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

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

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

minBound :: LearningStrategy

maxBound :: LearningStrategy

Enum LearningStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

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]

Show LearningStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

showsPrec :: Int -> LearningStrategy -> ShowS

show :: LearningStrategy -> String

showList :: [LearningStrategy] -> ShowS

Default LearningStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

def :: LearningStrategy

Eq LearningStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

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

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

Ord LearningStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

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

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

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

minBound :: BranchingStrategy

maxBound :: BranchingStrategy

Enum BranchingStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

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]

Show BranchingStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

showsPrec :: Int -> BranchingStrategy -> ShowS

show :: BranchingStrategy -> String

showList :: [BranchingStrategy] -> ShowS

Default BranchingStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

def :: BranchingStrategy

Eq BranchingStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

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

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

Ord BranchingStrategy

Defined in ToySolver.SAT.Solver.CDCL.Config

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

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

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

minBound :: PBHandlerType

maxBound :: PBHandlerType

Enum PBHandlerType

Defined in ToySolver.SAT.Solver.CDCL.Config

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]

Show PBHandlerType

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

showsPrec :: Int -> PBHandlerType -> ShowS

show :: PBHandlerType -> String

showList :: [PBHandlerType] -> ShowS

Default PBHandlerType

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

def :: PBHandlerType

Eq PBHandlerType

Defined in ToySolver.SAT.Solver.CDCL.Config

Methods

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

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

Ord PBHandlerType

Defined in ToySolver.SAT.Solver.CDCL.Config

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

showPBHandlerType :: PBHandlerType -> String

parsePBHandlerType :: String -> Maybe PBHandlerType