ToySolver.SAT

A CDCL SAT solver.

It follows the design of MiniSat and SAT4J.

See also:

• http://hackage.haskell.org/package/funsat
• http://hackage.haskell.org/package/incremental-sat-solver

The Solver type

data Solver

Solver instance

newSolver :: IO Solver

Create a new Solver instance.

newSolverWithConfig :: Config -> IO Solver

Create a new Solver instance with a given configulation.

Basic data structures

type Var = Int

Variable is represented as positive integers (DIMACS format).

type Lit = Int

Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).

literal

Arguments

:: Var

variable

-> Bool

polarity

-> Lit

Construct a literal from a variable and its polarity. True (resp False) means positive (resp. negative) literal.

litNot :: Lit -> Lit

Negation of the Lit.

litVar :: Lit -> Var

Underlying variable of the Lit

litPolarity :: Lit -> Bool

Polarity of the Lit. True means positive literal and False means negative literal.

evalLit :: IModel m => m -> Lit -> Bool

Problem specification

newVar :: Solver -> IO Var

Add a new variable

newVars :: Solver -> Int -> IO [Var]

Add variables. newVars solver n = replicateM n (newVar solver)

newVars_ :: Solver -> Int -> IO ()

Add variables. newVars_ solver n = newVars solver n >> return ()

resizeVarCapacity :: Solver -> Int -> IO ()

Pre-allocate internal buffer for n variables.

Clauses

addClause :: Solver -> Clause -> IO ()

Add a clause to the solver.

type Clause = [Lit]

Disjunction of Lit.

evalClause :: IModel m => m -> Clause -> Bool

Cardinality constraints

addAtLeast

Arguments

:: Solver

The Solver argument.

-> [Lit]

set of literals {l1,l2,..} (duplicated elements are ignored)

-> Int

n.

-> IO ()

Add a cardinality constraints atleast({l1,l2,..},n).

addAtMost

Arguments

:: Solver

The Solver argument

-> [Lit]

set of literals {l1,l2,..} (duplicated elements are ignored)

-> Int

n

-> IO ()

Add a cardinality constraints atmost({l1,l2,..},n).

addExactly

Arguments

:: Solver

The Solver argument

-> [Lit]

set of literals {l1,l2,..} (duplicated elements are ignored)

-> Int

n

-> IO ()

Add a cardinality constraints exactly({l1,l2,..},n).

type AtLeast = ([Lit], Int)

type Exactly = ([Lit], Int)

evalAtLeast :: IModel m => m -> AtLeast -> Bool

evalExactly :: IModel m => m -> Exactly -> Bool

(Linear) pseudo-boolean constraints

addPBAtLeast

Arguments

:: Solver

The Solver argument.

-> PBLinSum

list of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO ()

Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≥ n.

addPBAtMost

Arguments

:: Solver

The Solver argument.

-> PBLinSum

list of [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO ()

Add a pseudo boolean constraints c1*l1 + c2*l2 + … ≤ n.

addPBExactly

Arguments

:: Solver

The Solver argument.

-> PBLinSum

list of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO ()

Add a pseudo boolean constraints c1*l1 + c2*l2 + … = n.

addPBAtLeastSoft

Arguments

:: Solver

The Solver argument.

-> Lit

Selector literal sel

-> PBLinSum

list of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO ()

Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … ≥ n.

addPBAtMostSoft

Arguments

:: Solver

The Solver argument.

-> Lit

Selector literal sel

-> PBLinSum

list of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO ()

Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … ≤ n.

addPBExactlySoft

Arguments

:: Solver

The Solver argument.

-> Lit

Selector literal sel

-> PBLinSum

list of terms [(c1,l1),(c2,l2),…]

-> Integer

n

-> IO ()

Add a soft pseudo boolean constraints sel ⇒ c1*l1 + c2*l2 + … = n.

type PBLinTerm = (Integer, Lit)

type PBLinSum = [PBLinTerm]

type PBLinAtLeast = (PBLinSum, Integer)

type PBLinExactly = (PBLinSum, Integer)

evalPBLinSum :: IModel m => m -> PBLinSum -> Integer

evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool

evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool

XOR clauses

addXORClause

Arguments

:: Solver

The Solver argument.

-> [Lit]

literals [l1, l2, …, ln]

-> Bool

rhs

-> IO ()

Add a parity constraint l1 ⊕ l2 ⊕ … ⊕ ln = rhs

addXORClauseSoft

Arguments

:: Solver

The Solver argument.

-> Lit

Selector literal sel

-> [Lit]

literals [l1, l2, …, ln]

-> Bool

rhs

-> IO ()

Add a soft parity constraint sel ⇒ l1 ⊕ l2 ⊕ … ⊕ ln = rhs

type XORClause = ([Lit], Bool)

XOR clause

'([l1,l2..ln], b)' means l1 ⊕ l2 ⊕ ⋯ ⊕ ln = b.

Note that:

• True can be represented as ([], False)
• False can be represented as ([], True)

evalXORClause :: IModel m => m -> XORClause -> Bool

Thery

setTheory :: Solver -> TheorySolver -> IO ()

Solving

solve :: Solver -> IO Bool

Solve constraints. Returns True if the problem is SATISFIABLE. Returns False if the problem is UNSATISFIABLE.

solveWith

Arguments

:: Solver

-> [Lit]

Assumptions

-> IO Bool

Solve constraints under assuptions. Returns True if the problem is SATISFIABLE. Returns False if the problem is UNSATISFIABLE.

data BudgetExceeded

Constructors

BudgetExceeded

Instances

Show BudgetExceeded

Methods

showsPrec :: Int -> BudgetExceeded -> ShowS

show :: BudgetExceeded -> String

showList :: [BudgetExceeded] -> ShowS

Exception BudgetExceeded

Methods

toException :: BudgetExceeded -> SomeException

fromException :: SomeException -> Maybe BudgetExceeded

displayException :: BudgetExceeded -> String

Extract results

class IModel a where

Minimal complete definition

evalVar

Methods

evalVar :: a -> Var -> Bool

Instances

IModel (Var -> Bool)

Methods

evalVar :: (Var -> Bool) -> Var -> Bool

IModel (UArray Var Bool)

Methods

evalVar :: UArray Var Bool -> Var -> Bool

IModel (Array Var Bool)

Methods

evalVar :: Array Var Bool -> Var -> Bool

type Model = UArray Var Bool

A model is represented as a mapping from variables to its values.

getModel :: Solver -> IO Model

After solve returns True, it returns an satisfying assignment.

getFailedAssumptions :: Solver -> IO [Lit]

After solveWith returns False, it returns a set of assumptions that leads to contradiction. In particular, if it returns an empty set, the problem is unsatisiable without any assumptions.

getAssumptionsImplications :: Solver -> IO [Lit]

EXPERIMENTAL API: After solveWith returns True or failed with BudgetExceeded exception, it returns a set of literals that are implied by assumptions.

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)

• 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

getConfig :: Solver -> IO Config

setConfig :: Solver -> Config -> IO ()

modifyConfig :: Solver -> (Config -> Config) -> IO ()

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

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

setVarPolarity :: Solver -> Var -> Bool -> IO ()

The default polarity of a variable.

setLogger :: Solver -> (String -> IO ()) -> IO ()

set callback function for receiving messages.

setRandomGen :: Solver -> GenIO -> IO ()

Set random generator used by the random variable selection

getRandomGen :: Solver -> IO GenIO

Get random generator used by the random variable selection

setConfBudget :: Solver -> Maybe Int -> IO ()

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

Deprecated

setRestartStrategy :: Solver -> RestartStrategy -> IO ()

Deprecated: Use setConfig

setRestartFirst :: Solver -> Int -> IO ()

Deprecated: Use setConfig

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

defaultRestartFirst :: Int

Deprecated: Use configRestartFirst def

default value for RestartFirst.

setRestartInc :: Solver -> Double -> IO ()

Deprecated: Use setConfig

The factor with which the restart limit is multiplied in each restart. (default 1.5)

This must be >1.

defaultRestartInc :: Double

Deprecated: Use configRestartInc def

default value for RestartInc.

setLearntSizeFirst :: Solver -> Int -> IO ()

Deprecated: Use setConfig

The initial limit for learnt clauses.

Negative value means computing default value from problem instance.

defaultLearntSizeFirst :: Int

Deprecated: Use learntSizeFirst def

default value for LearntSizeFirst.

setLearntSizeInc :: Solver -> Double -> IO ()

Deprecated: Use setConfig

The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)

This must be >1.

defaultLearntSizeInc :: Double

Deprecated: Use learntSizeInc def

default value for LearntSizeInc.

setCCMin :: Solver -> Int -> IO ()

Deprecated: Use setConfig

Controls conflict clause minimization (0=none, 1=basic, 2=deep)

defaultCCMin :: Int

Deprecated: Use ccMin def

default value for CCMin.

setLearningStrategy :: Solver -> LearningStrategy -> IO ()

Deprecated: Use setConfig

setEnablePhaseSaving :: Solver -> Bool -> IO ()

Deprecated: Use setConfig

getEnablePhaseSaving :: Solver -> IO Bool

Deprecated: Use getConfig

defaultEnablePhaseSaving :: Bool

Deprecated: Use configEnablePhaseSaving def

setEnableForwardSubsumptionRemoval :: Solver -> Bool -> IO ()

Deprecated: Use setConfig

getEnableForwardSubsumptionRemoval :: Solver -> IO Bool

Deprecated: Use getConfig

defaultEnableForwardSubsumptionRemoval :: Bool

Deprecated: Use configEnableForwardSubsumptionRemoval def

setEnableBackwardSubsumptionRemoval :: Solver -> Bool -> IO ()

Deprecated: Use setConfig

getEnableBackwardSubsumptionRemoval :: Solver -> IO Bool

Deprecated: Use getConfig

defaultEnableBackwardSubsumptionRemoval :: Bool

Deprecated: Use configEnableBackwardSubsumptionRemoval def

setCheckModel :: Solver -> Bool -> IO ()

Deprecated: Use setConfig

setRandomFreq :: Solver -> Double -> IO ()

Deprecated: Use setConfig

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

defaultRandomFreq :: Double

Deprecated: Use configRandomFreq def

setPBHandlerType :: Solver -> PBHandlerType -> IO ()

Deprecated: Use setConfig

setPBSplitClausePart :: Solver -> Bool -> IO ()

Deprecated: Use setConfig

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.

getPBSplitClausePart :: Solver -> IO Bool

See documentation of setPBSplitClausePart.

defaultPBSplitClausePart :: Bool

Deprecated: Use configEnablePBSplitClausePart def

See documentation of setPBSplitClausePart.

Read state

getNVars :: Solver -> IO Int

number of variables of the problem.

getNConstraints :: Solver -> IO Int

number of constraints.

getNLearntConstraints :: Solver -> IO Int

number of learnt constrints.

getVarFixed :: Solver -> Var -> IO LBool

getLitFixed :: Solver -> Var -> IO LBool

getFixedLiterals :: Solver -> IO [Lit]

it returns a set of literals that are fixed without any assumptions.

Read state (deprecated)

nVars :: Solver -> IO Int

Deprecated: Use getNVars instead

number of variables of the problem.

nAssigns :: Solver -> IO Int

Deprecated: nAssigns is deprecated

number of assigned variables.

nConstraints :: Solver -> IO Int

Deprecated: Use getNConstraints instead

number of constraints.

nLearnt :: Solver -> IO Int

Deprecated: Use getNLearntConstraints instead

number of learnt constrints.

Internal API

varBumpActivity :: Solver -> Var -> IO ()

varDecayActivity :: Solver -> IO ()