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

Instances

AddXORClause IO Solver

Methods

addXORClause :: Solver -> [Lit] -> Bool -> IO ()

addXORClauseSoft :: Solver -> Lit -> [Lit] -> Bool -> IO ()

AddPBLin IO Solver

Methods

addPBAtLeast :: Solver -> PBLinSum -> Integer -> IO ()

addPBAtMost :: Solver -> PBLinSum -> Integer -> IO ()

addPBExactly :: Solver -> PBLinSum -> Integer -> IO ()

addPBAtLeastSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()

addPBAtMostSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()

addPBExactlySoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()

AddCardinality IO Solver

Methods

addAtLeast :: Solver -> [Lit] -> Int -> IO ()

addAtMost :: Solver -> [Lit] -> Int -> IO ()

addExactly :: Solver -> [Lit] -> Int -> IO ()

AddClause IO Solver

Methods

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

NewVar IO Solver

Methods

newVar :: Solver -> IO Var

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

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

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 :: NewVar m a => a -> m Var

Add a new variable

newVars :: NewVar m a => a -> Int -> m [Var]

Add variables. newVars a n = replicateM n (newVar a), but maybe faster.

newVars_ :: NewVar m a => a -> Int -> m ()

Add variables. newVars_ a n = newVars a n >> return (), but maybe faster.

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

Pre-allocate internal buffer for n variables.

Clauses

class NewVar m a => AddClause m a | a -> m where

Minimal complete definition

addClause

Methods

addClause :: a -> Clause -> m ()

Instances

AddClause IO Solver

Methods

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

Monad m => AddClause m (Encoder m)

Methods

addClause :: Encoder m -> Clause -> m ()

Monad m => AddClause m (Encoder m)

Methods

addClause :: Encoder m -> Clause -> m ()

Monad m => AddClause m (Encoder m)

Methods

addClause :: Encoder m -> Clause -> m ()

PrimMonad m => AddClause m (PBStore m)

Methods

addClause :: PBStore m -> Clause -> m ()

PrimMonad m => AddClause m (CNFStore m)

Methods

addClause :: CNFStore m -> Clause -> m ()

type Clause = [Lit]

Disjunction of Lit.

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

Cardinality constraints

class AddClause m a => AddCardinality m a | a -> m where

Minimal complete definition

addAtLeast

Methods

addAtLeast :: a -> [Lit] -> Int -> m ()

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

addAtMost :: a -> [Lit] -> Int -> m ()

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

addExactly :: a -> [Lit] -> Int -> m ()

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

Instances

AddCardinality IO Solver

Methods

addAtLeast :: Solver -> [Lit] -> Int -> IO ()

addAtMost :: Solver -> [Lit] -> Int -> IO ()

addExactly :: Solver -> [Lit] -> Int -> IO ()

PrimMonad m => AddCardinality m (Encoder m)

Methods

addAtLeast :: Encoder m -> [Lit] -> Int -> m ()

addAtMost :: Encoder m -> [Lit] -> Int -> m ()

addExactly :: Encoder m -> [Lit] -> Int -> m ()

Monad m => AddCardinality m (Encoder m)

Methods

addAtLeast :: Encoder m -> [Lit] -> Int -> m ()

addAtMost :: Encoder m -> [Lit] -> Int -> m ()

addExactly :: Encoder m -> [Lit] -> Int -> m ()

PrimMonad m => AddCardinality m (PBStore m)

Methods

addAtLeast :: PBStore m -> [Lit] -> Int -> m ()

addAtMost :: PBStore m -> [Lit] -> Int -> m ()

addExactly :: PBStore m -> [Lit] -> Int -> m ()

type AtLeast = ([Lit], Int)

type Exactly = ([Lit], Int)

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

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

(Linear) pseudo-boolean constraints

class AddCardinality m a => AddPBLin m a | a -> m where

Minimal complete definition

addPBAtLeast

Methods

addPBAtLeast :: a -> PBLinSum -> Integer -> m ()

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

addPBAtMost :: a -> PBLinSum -> Integer -> m ()

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

addPBExactly :: a -> PBLinSum -> Integer -> m ()

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

addPBAtLeastSoft :: a -> Lit -> PBLinSum -> Integer -> m ()

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

addPBAtMostSoft :: a -> Lit -> PBLinSum -> Integer -> m ()

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

addPBExactlySoft :: a -> Lit -> PBLinSum -> Integer -> m ()

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

Instances

AddPBLin IO Solver

Methods

addPBAtLeast :: Solver -> PBLinSum -> Integer -> IO ()

addPBAtMost :: Solver -> PBLinSum -> Integer -> IO ()

addPBExactly :: Solver -> PBLinSum -> Integer -> IO ()

addPBAtLeastSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()

addPBAtMostSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()

addPBExactlySoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()

PrimMonad m => AddPBLin m (Encoder m)

Methods

addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m ()

addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m ()

addPBExactly :: Encoder m -> PBLinSum -> Integer -> m ()

addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

Monad m => AddPBLin m (Encoder m)

Methods

addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m ()

addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m ()

addPBExactly :: Encoder m -> PBLinSum -> Integer -> m ()

addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

PrimMonad m => AddPBLin m (PBStore m)

Methods

addPBAtLeast :: PBStore m -> PBLinSum -> Integer -> m ()

addPBAtMost :: PBStore m -> PBLinSum -> Integer -> m ()

addPBExactly :: PBStore m -> PBLinSum -> Integer -> m ()

addPBAtLeastSoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m ()

addPBAtMostSoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m ()

addPBExactlySoft :: PBStore m -> Lit -> PBLinSum -> Integer -> m ()

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

class AddClause m a => AddXORClause m a | a -> m where

Minimal complete definition

addXORClause

Methods

addXORClause :: a -> [Lit] -> Bool -> m ()

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

addXORClauseSoft :: a -> Lit -> [Lit] -> Bool -> m ()

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

Instances

AddXORClause IO Solver

Methods

addXORClause :: Solver -> [Lit] -> Bool -> IO ()

addXORClauseSoft :: Solver -> Lit -> [Lit] -> Bool -> IO ()

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

Theory

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

cancel :: Solver -> IO ()

Cancel exectution of solve or solveWith.

This can be called from other threads.

data Canceled

Constructors

Canceled

Instances

Show Canceled

Methods

showsPrec :: Int -> Canceled -> ShowS

show :: Canceled -> String

showList :: [Canceled] -> ShowS

Exception Canceled

Methods

toException :: Canceled -> SomeException

fromException :: SomeException -> Maybe Canceled

displayException :: Canceled -> 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

module ToySolver.SAT.Config

getConfig :: Solver -> IO Config

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

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

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

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.

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.

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

Deprecated: Use setConfig

The initial limit for learnt clauses.

Negative value means computing default value from problem instance.

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.

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

Deprecated: Use setConfig

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

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

Deprecated: Use setConfig

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

Deprecated: Use setConfig

getEnablePhaseSaving :: Solver -> IO Bool

Deprecated: Use getConfig

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

Deprecated: Use setConfig

getEnableForwardSubsumptionRemoval :: Solver -> IO Bool

Deprecated: Use getConfig

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

Deprecated: Use setConfig

getEnableBackwardSubsumptionRemoval :: Solver -> IO Bool

Deprecated: Use getConfig

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

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én and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.

getPBSplitClausePart :: Solver -> IO Bool

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 -> Lit -> 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 ()