ToySolver.SAT.Solver.CDCL

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

AddCardinality IO Solver

Defined in ToySolver.SAT.Solver.CDCL

Methods

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

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

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

AddClause IO Solver

Defined in ToySolver.SAT.Solver.CDCL

Methods

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

AddPBLin IO Solver

Defined in ToySolver.SAT.Solver.CDCL

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

AddXORClause IO Solver

Defined in ToySolver.SAT.Solver.CDCL

Methods

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

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

NewVar IO Solver

Defined in ToySolver.SAT.Solver.CDCL

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

Methods

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

Instances

AddClause IO Solver

Defined in ToySolver.SAT.Solver.CDCL

Methods

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

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

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

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer

Methods

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

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.PB

Methods

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

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.PBNLC

Methods

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

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

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

PrimMonad m => AddClause m (CNFStore m)

Defined in ToySolver.SAT.Store.CNF

Methods

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

PrimMonad m => AddClause m (PBStore m)

Defined in ToySolver.SAT.Store.PB

Methods

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

type Clause = [Lit]

Disjunction of Lit.

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

type PackedClause = Vector PackedLit

packClause :: Clause -> PackedClause

unpackClause :: PackedClause -> Clause

Cardinality constraints

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

Minimal complete definition

addAtLeast

Methods

addAtLeast

Arguments

:: a

-> [Lit]

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

-> Int

n

-> m ()

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

addAtMost

Arguments

:: a

-> [Lit]

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

-> Int

n

-> m ()

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

addExactly

Arguments

:: a

-> [Lit]

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

-> Int

n

-> m ()

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

Instances

AddCardinality IO Solver

Defined in ToySolver.SAT.Solver.CDCL

Methods

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

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

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

PrimMonad m => AddCardinality m (Encoder m)

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

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

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

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

PrimMonad m => AddCardinality m (Encoder m)

Defined in ToySolver.SAT.Encoder.PB

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)

Defined in ToySolver.SAT.Encoder.PBNLC

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)

Defined in ToySolver.SAT.Store.PB

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

Arguments

:: a

-> PBLinSum

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

-> Integer

n

-> m ()

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

addPBAtMost

Arguments

:: a

-> PBLinSum

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

-> Integer

n

-> m ()

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

addPBExactly

Arguments

:: a

-> PBLinSum

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

-> Integer

n

-> m ()

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

addPBAtLeastSoft

Arguments

:: a

-> Lit

Selector literal sel

-> PBLinSum

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

-> Integer

n

-> m ()

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

addPBAtMostSoft

Arguments

:: a

-> Lit

Selector literal sel

-> PBLinSum

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

-> Integer

n

-> m ()

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

addPBExactlySoft

Arguments

:: a

-> Lit

Selector literal sel

-> PBLinSum

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

-> Integer

n

-> m ()

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

Instances

AddPBLin IO Solver

Defined in ToySolver.SAT.Solver.CDCL

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)

Defined in ToySolver.SAT.Encoder.PB

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)

Defined in ToySolver.SAT.Encoder.PBNLC

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)

Defined in ToySolver.SAT.Store.PB

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

Arguments

:: a

-> [Lit]

literals [l1, l2, …, ln]

-> Bool

rhs

-> m ()

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

addXORClauseSoft

Arguments

:: a

-> Lit

Selector literal sel

-> [Lit]

literals [l1, l2, …, ln]

-> Bool

rhs

-> m ()

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

Instances

AddXORClause IO Solver

Defined in ToySolver.SAT.Solver.CDCL

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

Exception BudgetExceeded

Defined in ToySolver.SAT.Solver.CDCL

Methods

toException :: BudgetExceeded -> SomeException

fromException :: SomeException -> Maybe BudgetExceeded

displayException :: BudgetExceeded -> String

Show BudgetExceeded

Defined in ToySolver.SAT.Solver.CDCL

Methods

showsPrec :: Int -> BudgetExceeded -> ShowS

show :: BudgetExceeded -> String

showList :: [BudgetExceeded] -> ShowS

cancel :: Solver -> IO ()

Cancel exectution of solve or solveWith.

This can be called from other threads.

data Canceled

Constructors

Canceled

Instances

Exception Canceled

Defined in ToySolver.SAT.Solver.CDCL

Methods

toException :: Canceled -> SomeException

fromException :: SomeException -> Maybe Canceled

displayException :: Canceled -> String

Show Canceled

Defined in ToySolver.SAT.Solver.CDCL

Methods

showsPrec :: Int -> Canceled -> ShowS

show :: Canceled -> String

showList :: [Canceled] -> ShowS

Extract results

class IModel a where

Methods

evalVar :: a -> Var -> Bool

Instances

IModel (UArray Var Bool)

Defined in ToySolver.SAT.Types

Methods

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

IModel (Array Var Bool)

Defined in ToySolver.SAT.Types

Methods

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

IModel (Var -> Bool)

Defined in ToySolver.SAT.Types

Methods

evalVar :: (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 LitSet

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 LitSet

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

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

Callbacks

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

set callback function for receiving messages.

clearLogger :: Solver -> IO ()

Clear logger function set by setLogger.

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

Set a callback function used to indicate a termination requirement to the solver.

The solver will periodically call this function and check its return value during the search. If the callback function returns True the solver terminates and throws Canceled exception.

See also clearTerminateCallback and IPASIR's ipasir_set_terminate() function.

clearTerminateCallback :: Solver -> IO ()

Clear a callback function set by setTerminateCallback

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

Set a callback function used to extract learned clauses from the solver. The solver will call this function for each learned clause.

See also clearLearnCallback and IPASIR's ipasir_set_learn() function.

clearLearnCallback :: Solver -> IO ()

Clear a callback function set by setLearnCallback

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.

Internal API

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

varDecayActivity :: Solver -> IO ()