ToySolver.SAT.Types

Variable

type Var = Int

Variable is represented as positive integers (DIMACS format).

type VarSet = IntSet

type VarMap = IntMap

validVar :: Var -> Bool

Model

class IModel a where

Methods

evalVar :: a -> Var -> Bool

Instances

IModel (Var -> Bool)

Defined in ToySolver.SAT.Types

Methods

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

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

type Model = UArray Var Bool

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

restrictModel :: Int -> Model -> Model

Restrict model to first nv variables.

Literal

type Lit = Int

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

type LitSet = IntSet

type LitMap = IntMap

litUndef :: Lit

validLit :: Lit -> Bool

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

Clause

type Clause = [Lit]

Disjunction of Lit.

normalizeClause :: Clause -> Maybe Clause

Normalizing clause

Nothing if the clause is trivially true.

instantiateClause :: forall m. Monad m => (Lit -> m LBool) -> Clause -> m (Maybe Clause)

clauseSubsume :: Clause -> Clause -> Bool

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

clauseToPBLinAtLeast :: Clause -> PBLinAtLeast

Packed Clause

type PackedVar = PackedLit

type PackedLit = Int32

packLit :: Lit -> PackedLit

unpackLit :: PackedLit -> Lit

type PackedClause = Vector PackedLit

packClause :: Clause -> PackedClause

unpackClause :: PackedClause -> Clause

Cardinality Constraint

type AtLeast = ([Lit], Int)

type Exactly = ([Lit], Int)

normalizeAtLeast :: AtLeast -> AtLeast

instantiateAtLeast :: forall m. Monad m => (Lit -> m LBool) -> AtLeast -> m AtLeast

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

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

(Linear) Pseudo Boolean Constraint

type PBLinTerm = (Integer, Lit)

type PBLinSum = [PBLinTerm]

type PBLinAtLeast = (PBLinSum, Integer)

type PBLinExactly = (PBLinSum, Integer)

normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer)

normalizing PB term of the form c1 x1 + c2 x2 ... cn xn + c into d1 x1 + d2 x2 ... dm xm + d where d1,...,dm ≥ 1.

normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast

normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn >= b.

normalizePBLinExactly :: PBLinExactly -> PBLinExactly

normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn = b.

instantiatePBLinAtLeast :: forall m. Monad m => (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast

instantiatePBLinExactly :: Monad m => (Lit -> m LBool) -> PBLinExactly -> m PBLinExactly

cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast

cardinalityReduction :: PBLinAtLeast -> AtLeast

negatePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast

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

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

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

pbLinLowerBound :: PBLinSum -> Integer

pbLinUpperBound :: PBLinSum -> Integer

pbLinSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool

Non-linear Pseudo Boolean constraint

type PBTerm = (Integer, [Lit])

type PBSum = [PBTerm]

evalPBSum :: IModel m => m -> PBSum -> Integer

evalPBConstraint :: IModel m => m -> Constraint -> Bool

evalPBFormula :: IModel m => m -> Formula -> Maybe Integer

pbLowerBound :: PBSum -> Integer

pbUpperBound :: PBSum -> Integer

removeNegationFromPBSum :: PBSum -> PBSum

XOR Clause

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)

normalizeXORClause :: XORClause -> XORClause

Normalize XOR clause

instantiateXORClause :: forall m. Monad m => (Lit -> m LBool) -> XORClause -> m XORClause

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

Type classes for solvers

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

Minimal complete definition

newVar

Methods

newVar :: a -> m Var

Add a new variable

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

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

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

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

Instances

NewVar IO Solver

Defined in ToySolver.SAT.Solver.CDCL

Methods

newVar :: Solver -> IO Var

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

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

PrimMonad m => NewVar m (PBStore m)

Defined in ToySolver.SAT.Store.PB

Methods

newVar :: PBStore m -> m Var

newVars :: PBStore m -> Int -> m [Var]

newVars_ :: PBStore m -> Int -> m ()

Monad m => NewVar m (Encoder m)

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

newVar :: Encoder m -> m Var

newVars :: Encoder m -> Int -> m [Var]

newVars_ :: Encoder m -> Int -> m ()

Monad m => NewVar m (Encoder m)

Defined in ToySolver.SAT.Encoder.PBNLC

Methods

newVar :: Encoder m -> m Var

newVars :: Encoder m -> Int -> m [Var]

newVars_ :: Encoder m -> Int -> m ()

Monad m => NewVar m (Encoder m)

Defined in ToySolver.SAT.Encoder.PB

Methods

newVar :: Encoder m -> m Var

newVars :: Encoder m -> Int -> m [Var]

newVars_ :: Encoder m -> Int -> m ()

Monad m => NewVar m (Encoder m)

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

Methods

newVar :: Encoder m -> m Var

newVars :: Encoder m -> Int -> m [Var]

newVars_ :: Encoder m -> Int -> m ()

Monad m => NewVar m (Encoder m)

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

newVar :: Encoder m -> m Var

newVars :: Encoder m -> Int -> m [Var]

newVars_ :: Encoder m -> Int -> m ()

PrimMonad m => NewVar m (CNFStore m)

Defined in ToySolver.SAT.Store.CNF

Methods

newVar :: CNFStore m -> m Var

newVars :: CNFStore m -> Int -> m [Var]

newVars_ :: CNFStore m -> Int -> m ()

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

PrimMonad m => AddClause m (PBStore m)

Defined in ToySolver.SAT.Store.PB

Methods

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

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.Tseitin

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

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

Methods

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

PrimMonad m => AddClause m (CNFStore m)

Defined in ToySolver.SAT.Store.CNF

Methods

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

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

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

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

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

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

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

Minimal complete definition

addPBNLAtLeast

Methods

addPBNLAtLeast

Arguments

:: a

-> PBSum

List of terms [(c1,ls1),(c2,ls2),…]

-> Integer

n

-> m ()

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … ≥ n.

addPBNLAtMost

Arguments

:: a

-> PBSum

List of terms [(c1,ls1),(c2,ls2),…]

-> Integer

n

-> m ()

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … ≥ n.

addPBNLExactly

Arguments

:: a

-> PBSum

List of terms [(c1,ls1),(c2,ls2),…]

-> Integer

n

-> m ()

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … = n.

addPBNLAtLeastSoft

Arguments

:: a

-> Lit

Selector literal sel

-> PBSum

List of terms [(c1,ls1),(c2,ls2),…]

-> Integer

n

-> m ()

Add a soft non-linear pseudo boolean constraints sel ⇒ c1*ls1 + c2*ls2 + … ≥ n.

addPBNLAtMostSoft

Arguments

:: a

-> Lit

Selector literal sel

-> PBSum

List of terms [(c1,ls1),(c2,ls2),…]

-> Integer

n

-> m ()

Add a soft non-linear pseudo boolean constraints sel ⇒ c1*ls1 + c2*ls2 + … ≤ n.

addPBNLExactlySoft

Arguments

:: a

-> Lit

Selector literal sel

-> PBSum

List of terms [(c1,ls1),(c2,ls2),…]

-> Integer

n

-> m ()

Add a soft non-linear pseudo boolean constraints lit ⇒ c1*ls1 + c2*ls2 + … = n.

Instances

PrimMonad m => AddPBNL m (PBStore m)

Defined in ToySolver.SAT.Store.PB

Methods

addPBNLAtLeast :: PBStore m -> PBSum -> Integer -> m ()

addPBNLAtMost :: PBStore m -> PBSum -> Integer -> m ()

addPBNLExactly :: PBStore m -> PBSum -> Integer -> m ()

addPBNLAtLeastSoft :: PBStore m -> Lit -> PBSum -> Integer -> m ()

addPBNLAtMostSoft :: PBStore m -> Lit -> PBSum -> Integer -> m ()

addPBNLExactlySoft :: PBStore m -> Lit -> PBSum -> Integer -> m ()

PrimMonad m => AddPBNL m (Encoder m)

Defined in ToySolver.SAT.Encoder.PBNLC

Methods

addPBNLAtLeast :: Encoder m -> PBSum -> Integer -> m ()

addPBNLAtMost :: Encoder m -> PBSum -> Integer -> m ()

addPBNLExactly :: Encoder m -> PBSum -> Integer -> m ()

addPBNLAtLeastSoft :: Encoder m -> Lit -> PBSum -> Integer -> m ()

addPBNLAtMostSoft :: Encoder m -> Lit -> PBSum -> Integer -> m ()

addPBNLExactlySoft :: Encoder m -> Lit -> PBSum -> Integer -> m ()

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