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.

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.

type Clause = [Lit]

Disjunction of Lit.

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.

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

Add a clause to the solver.

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).

addPBAtLeast

Arguments

:: Solver

The Solver argument.

-> [(Integer, Lit)]

set 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.

-> [(Integer, Lit)]

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.

-> [(Integer, Lit)]

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

indicator lit

-> [(Integer, Lit)]

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

-> Integer

n

-> IO ()

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

addPBAtMostSoft

Arguments

:: Solver

The Solver argument.

-> Lit

indicator lit

-> [(Integer, Lit)]

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

-> Integer

n

-> IO ()

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

addPBExactlySoft

Arguments

:: Solver

The Solver argument.

-> Lit

indicator lit

-> [(Integer, Lit)]

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

-> Integer

n

-> IO ()

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

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

indicator lit

-> [Lit]

literals [l1, l2, …, ln]

-> Bool

rhs

-> IO ()

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

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

Exception BudgetExceeded

Typeable * BudgetExceeded

Extract results

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.

Solver configulation

data RestartStrategy

Constructors

MiniSATRestarts

ArminRestarts

LubyRestarts

Instances

Eq RestartStrategy

Ord RestartStrategy

Show RestartStrategy

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

defaultRestartStrategy :: RestartStrategy

default value for RestartStrategy.

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

The initial restart limit. (default 100) Negative value is used to disable restart.

defaultRestartFirst :: Int

default value for RestartFirst.

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

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

defaultRestartInc :: Double

default value for RestartInc.

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

The initial limit for learnt clauses.

defaultLearntSizeFirst :: Int

default value for LearntSizeFirst.

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

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

defaultLearntSizeInc :: Double

default value for LearntSizeInc.

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

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

defaultCCMin :: Int

default value for CCMin.

data LearningStrategy

Constructors

LearningClause

LearningHybrid

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

defaultLearningStrategy :: LearningStrategy

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

getEnablePhaseSaving :: Solver -> IO Bool

defaultEnablePhaseSaving :: Bool

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

getEnableForwardSubsumptionRemoval :: Solver -> IO Bool

defaultEnableForwardSubsumptionRemoval :: Bool

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

getEnableBackwardSubsumptionRemoval :: Solver -> IO Bool

defaultEnableBackwardSubsumptionRemoval :: Bool

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

The default polarity of a variable.

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

set callback function for receiving messages.

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

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

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

defaultRandomFreq :: Double

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

Set random generator used by the random variable selection

getRandomGen :: Solver -> IO StdGen

Get random generator used by the random variable selection

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

data PBHandlerType

Constructors

PBHandlerTypeCounter

PBHandlerTypePueblo

Instances

Eq PBHandlerType

Ord PBHandlerType

Show PBHandlerType

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

defaultPBHandlerType :: PBHandlerType

Read state

nVars :: Solver -> IO Int

number of variables of the problem.

nAssigns :: Solver -> IO Int

number of assigned variables.

nConstraints :: Solver -> IO Int

number of constraints.

nLearnt :: Solver -> IO Int

number of learnt constrints.

getVarFixed :: Solver -> Var -> IO LBool

getLitFixed :: Solver -> Var -> IO LBool

Internal API

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

varDecayActivity :: Solver -> IO ()